You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Field data for `docs/echo-types/composition.md`. Today's ephapax sessions surfaced a concrete failure mode of trying to close a thin-poset-decoration gap by patching inside one layer rather than respecting the cross-layer obligation. Echo-types' `degradeMode-comp` lemma (`proofs/agda/EchoLinear.agda:93–101`) is the upstream theorem; the ephapax failure is a downstream test of what goes wrong when the discipline is violated.
Not asking you to take ephapax code into echo-types. Asking whether you want this captured as a methodological note in `composition.md`.
The failure mode (concise)
Ephapax has a four-layer redesign matching echo-types' fiber + thin-poset template:
L1 — region-capability tracking (R-threaded judgment in `formal/TypingL1.v`).
L3 — echo / residue (`formal/Echo.v`, ported from `EchoLinear.agda` and `EchoResidue.agda`).
L4 — dyadic mode (not started).
An axiom (`Axiom region_liveness_at_split_l1` in `formal/Semantics_L1.v`) was stated within L1 to discharge a residual obligation in the substitution lemma for the R-threaded judgment. An empirical closure attempt today (hyperpolymath/ephapax PR #170) tried to close the axiom by strengthening T_Var_*_L1 within L1 alone — adding the well-formedness premise `forall r, In r (free_regions T) -> In r R`.
The PR landed. It did not close the axiom. The residual case (`T_Region_Active_L1` with binder = the tracked region) remains false even under the strengthened judgment — a minimal counterexample at the typing level is `ERegion rv (EI32 5) : TBase TI32` at `R = [rv]`, which still types and still pops the only `rv` on exit.
The honest closure path is cross-layer: the obligation lives at the L1→L2 boundary — specifically, effect-typed `TFun` in mode-distinguished `T_Lam_Linear_L2` carries the region-effect that L1's R-threading lacks. The L1-internal patching attempt was structurally the wrong shape.
In echo-types vocabulary
This is the same shape as trying to close an obligation that lives at the degrade map (`LEcho Linear → LEcho Affine`) by patching inside one of the endpoints. The endpoint patch can absorb a visible discrepancy (and PR #170 did absorb the source-level soundness gap from §4.8) but cannot eliminate the cross-decoration obligation. The decoration discipline says: obligations between decorations must close at the decoration map, not within either endpoint.
Suggested content for composition.md
A short subsection — "anti-pattern: closing a degrade-map obligation within an endpoint" — with three concrete pieces:
The shape: when a decoration `D_1 ≤ D_2` connects two indexed instances of a fiber, obligations that mention both endpoints close at the degrade map, not within either endpoint.
Detection heuristic: if a proof attempt requires strengthening a typing rule with a premise referring to another decoration's invariant (e.g., region presence in a modality-indexed rule), the discipline is being violated.
What this is
Field data for `docs/echo-types/composition.md`. Today's ephapax sessions surfaced a concrete failure mode of trying to close a thin-poset-decoration gap by patching inside one layer rather than respecting the cross-layer obligation. Echo-types' `degradeMode-comp` lemma (`proofs/agda/EchoLinear.agda:93–101`) is the upstream theorem; the ephapax failure is a downstream test of what goes wrong when the discipline is violated.
Not asking you to take ephapax code into echo-types. Asking whether you want this captured as a methodological note in `composition.md`.
The failure mode (concise)
Ephapax has a four-layer redesign matching echo-types' fiber + thin-poset template:
An axiom (`Axiom region_liveness_at_split_l1` in `formal/Semantics_L1.v`) was stated within L1 to discharge a residual obligation in the substitution lemma for the R-threaded judgment. An empirical closure attempt today (hyperpolymath/ephapax PR #170) tried to close the axiom by strengthening T_Var_*_L1 within L1 alone — adding the well-formedness premise `forall r, In r (free_regions T) -> In r R`.
The PR landed. It did not close the axiom. The residual case (`T_Region_Active_L1` with binder = the tracked region) remains false even under the strengthened judgment — a minimal counterexample at the typing level is `ERegion rv (EI32 5) : TBase TI32` at `R = [rv]`, which still types and still pops the only `rv` on exit.
The honest closure path is cross-layer: the obligation lives at the L1→L2 boundary — specifically, effect-typed `TFun` in mode-distinguished `T_Lam_Linear_L2` carries the region-effect that L1's R-threading lacks. The L1-internal patching attempt was structurally the wrong shape.
In echo-types vocabulary
This is the same shape as trying to close an obligation that lives at the degrade map (`LEcho Linear → LEcho Affine`) by patching inside one of the endpoints. The endpoint patch can absorb a visible discrepancy (and PR #170 did absorb the source-level soundness gap from §4.8) but cannot eliminate the cross-decoration obligation. The decoration discipline says: obligations between decorations must close at the decoration map, not within either endpoint.
Suggested content for composition.md
A short subsection — "anti-pattern: closing a degrade-map obligation within an endpoint" — with three concrete pieces:
_<ᵇᵘ_via rank-embedding transport #170 + issue docs: stale-claim sweep after Slice 3+4 Route A 6-PR arc (#165-#170) #171 comment, which document the failure and the cross-layer closure path.I'm happy to draft the actual prose if useful. Filed without doing so to avoid presuming the framing you want.
What I am NOT proposing
This is purely about whether the ephapax failure data point is worth capturing in echo-types' methodological doc.
References
_<ᵇᵘ_via rank-embedding transport #170 (the patching attempt, with honest in-source documentation of why it failed): proof(L1.G): strengthen T_Var_*_L1 with region well-formedness (§4.8 path 3) ephapax#170🤖 Generated with Claude Code