docs: port §4.8.1 + §5.1 + L1 admit enumeration to main

hyperpolymath · hyperpolymath · commit f32b6871eaed · 2026-05-27T12:53:25.000+01:00
Brings three doc-only improvements from the design branch onto main: 1. PRESERVATION-DESIGN.md §4.8.1 (from design-branch PR #170 — T_Var strengthening landed via the m-indexed has_type_l1 in #176). Docs what §4.8 path (3) closes and what it does not. 2. PRESERVATION-DESIGN.md §5.1 (from design-branch PR #172) — L1's lambda-rigidity gap (S_App_Step2 / S_Pair_Step2 admits in preservation_l1) closes at L2 Phase 2 via effect-typed TFun. Documents the §5 table's "✓ (L1 fix)" cell as conditional, and explains why effect-typing is L2's job not L1's. 3. docs/proof-debt.adoc — adds the L1 admit enumeration that the design branch carried via PR #169. Eight current escape-hatch sites in Semantics_L1.v listed by file:line per the trusted-base policy substring-match convention. Plus the Echo.v K-closure note (from PR #173's main re-port). No source/proof changes — pure documentation. Allows the trusted-base reduction policy check to substring-match all escape-hatch sites in Semantics_L1.v. Refs design-branch PRs #169 / #170 / #172 / #173, PR #176 (L2 hybrid).
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
@@ -149,21 +149,70 @@ for refutation budgets (`docs/proof-debt.adoc` §(b) in that repo).
   close — namely the affine side, which needs L2 + the weakening
   lemma).
 
+=== `formal/Semantics_L1.v` — in-flight L1 admits (post-#176 L2 hybrid)
+
+After the L2 hybrid landing (#176), main's `Semantics_L1.v` carries
+the following escape-hatch sites. All are tracked, structurally
+diagnosed, and sequenced under the four-layer redesign plan.
+
+NOTE: line numbers are point-in-time and may shift with subsequent
+edits. The substring match is `file:line`; entries below cover the
+current positions on main.
+
+* **`formal/Semantics_L1.v:343`** — `Admitted.` capping one of the
+  region-shrink helpers (T_Region_Active_L1 shadowed case at the
+  list-vs-multiset boundary). Three documented closure approaches
+  in-file.
+* **`formal/Semantics_L1.v:400`** — `Admitted.` (related
+  region-shrink admit; same structural class as L343).
+* **`formal/Semantics_L1.v:412`** — `Admitted.` (related).
+* **`formal/Semantics_L1.v:520`** — `Admitted.` (related).
+* **`formal/Semantics_L1.v:608`** — `Axiom region_liveness_at_split_l1`.
+  Documented in-file as universally false; the residual obstacle is
+  T_Region_Active_L1 with binder=rv. Three closure paths documented:
+  (i) restate with `no_region_active_pop_of rv e` side condition,
+  (ii) multi-set `region_env`, (iii) weaker contextual signature.
+  L1.G follow-up converts this to a Lemma + 1 narrow admit (per
+  PR #178 / its main re-port).
+* **`formal/Semantics_L1.v:632`** — `Admitted.` capping
+  `preservation_l1` (related to L1.G's gap above; L2-gated per
+  §5.1 — closes once L2 Phase 2's effect-typed `TFun` lands).
+* **`formal/Semantics_L1.v:703`** — `admit.` inside `preservation_l1`
+  for one of the lambda-rigidity admits (S_App_Step2 / S_Pair_Step2
+  per §4.8 + §5.1).
+* **`formal/Semantics_L1.v:704`** — `Admitted.` capping
+  `preservation_l1` (same lambda-rigidity gap).
+
+All are tracked in the L1 closure plan and sequenced under the
+four-layer redesign. None are soundness-relevant in the legacy
+`Semantics.v`; they live entirely on the L1 redesign side.
+
+=== `formal/Echo.v` — L3 layer K dependency CLOSED 2026-05-27
+
+PR #173 (design branch) / its main re-port discharged the
+`Eqdep.Eq_rect_eq` (K / UIP) dependency in `mode_le_trans` +
+`degrade_mode_comp` via the motive-trick K-free template from
+`formal/Modality.v`. **All Echo.v lemmas are now closed under the
+global context** — zero K, zero UIP, zero axioms. Entry kept here
+for historical visibility; no current escape hatch in `Echo.v`.
+
 == What this repo does *not* establish today
 
 Per `formal/PRESERVATION-DESIGN.md` §12.15.4, even after the in-flight
 L1 work lands, the following remain open and are tracked here so
 downstream consumers do not overclaim:
 
-* The `ephapax-affine` sublanguage is not separately mechanised.
-  Rust `LinearChecker` and `AffineChecker` are independent
-  (behavioural tests only); the Coq judgment covers a single
-  judgment resembling linear discipline. The Linear ⇒ Affine lemma
-  is L2 work, not L1.
-* No mechanised correspondence between the Rust checkers and the Coq
-  judgment.
-* L3 `formal/Echo.v` does not exist; the theory lives upstream at
-  `hyperpolymath/echo-types`.
+* The `ephapax-affine` sublanguage's mechanisation in `formal/`
+  exists (post-#176: `has_type_l1` carries the modality parameter,
+  `linear_to_affine : has_type_l1 Linear ... → has_type_l1 Affine ...`
+  is Qed, mode-specific T_Lam_L1_*, T_Case_L1_*, T_If_L1_* land).
+  The Rust `AffineChecker` is independent (behavioural tests only);
+  no mechanised correspondence between the Rust checkers and the
+  Coq judgment.
+* L3 `formal/Echo.v` mechanises the residue type former layer per
+  PRESERVATION-DESIGN.md §6 (Mode, LEcho, weaken, EchoR + headline
+  `no_section_collapse_to_residue`). Type-former integration into
+  Syntax.v / Typing.v / Semantics.v is forward-looking.
 * L4 mode-elaboration soundness is a research track, not scheduled.
 
 Per the policy schema, these are *plan items* rather than (d) DEBT
diff --git a/formal/PRESERVATION-DESIGN.md b/formal/PRESERVATION-DESIGN.md
@@ -317,6 +317,35 @@ proof-engineering gap but a calculus-design gap.
 The L1.E PR documents this in-source. None of (1)/(2)/(3) is in scope
 for the L1 minimal-fix; each is a follow-up. See ROADMAP for sequencing.
 
+### 4.8.1 Resolution path (3) landed 2026-05-27 — and what it does not close
+
+`T_Var_Lin_L1` and `T_Var_Unr_L1` were strengthened with the premise
+`forall r, In r (free_regions T) -> In r R` (originally as PR #170
+on the design branch, subsumed into the m-indexed main via #176).
+The strengthening:
+
+- **Closes the source-level soundness gap**: programs like
+
+      let_lin x = (ELoc 0 "r") in (ELet (ERegion "r" (EI32 5)) (EDrop (EVar 1)))
+
+  no longer type, because the `EDrop (EVar 1)` site fails the
+  variable rule's new well-formedness premise at R = `[]`.
+
+What the strengthening does **not** close: the
+`region_liveness_at_split_l1` lemma's residual admit (formerly the
+opaque `Axiom`, converted to an Admitted Lemma with 28-of-29 cases
+proved concretely in the L1.G follow-up). An empirical closure
+attempt closes most cases trivially via the IH chain, but the
+T_Region_Active_L1 case with `binder = rv` exhibits a real
+counterexample even under the strengthened judgment:
+
+    ERegion rv (EI32 5) : TBase TI32 — In rv R, In rv R' = False
+                                        (because remove_first_L1 pops the only rv)
+
+Three follow-up paths (side-conditioned lemma, multi-set R,
+contextual weaker signature) remain L1 follow-up work, independent
+of and additional to this §4.8 resolution.
+
 ---
 
 ## 5. Layer 2 in detail — Linear vs Affine modality
@@ -376,7 +405,7 @@ recipe (echo-types' `degradeMode-comp`, `EchoLinear.agda:93-101`).
 
 | Property | Ephapax-Linear | Ephapax-Affine |
 |---|---|---|
-| Preservation | ✓ (L1 fix) | ✓ (same fix; Affine derivations are L1-safe by weakening) |
+| Preservation | ✓ (L1 fix, *conditional on §5.1*) | ✓ (same fix; Affine derivations are L1-safe by weakening) |
 | Progress | ✓ | ✓ |
 | **No-leak** (every introduced linear value is consumed) | proved | does **not** hold; replaced by "no-duplicate" |
 | **No-duplicate** | trivially (Linear ⇒ no-duplicate) | proved as a structural property |
@@ -387,6 +416,69 @@ Cross-mode: the Linear ⇒ Affine weakening lemma is a single induction.
 Combined with monomode preservation, this gives Affine preservation
 for free.
 
+### 5.1 Cross-layer dependency: L1's lambda-rigidity gap closes at L2
+
+The "Preservation ✓ (L1 fix)" cell above is **not realised by L1 alone**.
+`formal/Semantics_L1.v`'s `preservation_l1` is currently `Admitted`
+because of three internal admits in its proof body:
+
+- `S_StringConcat_Step2` — tractable; needs a
+  `step_pop_disjoint_from_type_l1` lemma.
+- `S_App_Step2` and `S_Pair_Step2` — the **lambda-rigidity gap** per
+  §4.8: `T_Lam_L1_*` fixes the body's region environment at lambda-
+  creation time; the rules give no way to re-derive the lambda's
+  typing at a shifted `R'` after the inner step.
+
+§4.8.1 records that path (3) — strengthening `T_Var_*_L1` — landed
+2026-05-27 via PR #170 (and subsumed via #176). It closes the
+source-level *variable* soundness gap but leaves the lambda-body
+case open because the body's typing is fixed at `T_Lam_L1_*`-
+introduction, not at variable-use. Path (3) is necessary but **not
+sufficient**.
+
+**Path (1) — effect-typed lambdas — is L2 Phase 2's mechanism.** The
+mode-specific `T_Lam_L1_Linear` / `T_Lam_L1_Affine` constructors
+should carry an annotation of the body's region effect (how `R`
+shifts through the body). Concretely, the lambda type would extend
+from
+
+```
+TFun T1 T2
+```
+
+to
+
+```
+TFun T1 T2 (R_in : region_env) (R_out : region_env)
+```
+
+(or an equivalent abstract `Effect` parameter). At application time,
+`T_App_L1` would consume `R_in` and produce `R_out`, threading the
+region change properly. This lets `S_App_Step2`'s preservation
+close: the lambda's typing at the post-step `R'` is derived from the
+recorded effect, not blocked by rigid `T_Lam` introduction.
+
+**Sequencing.** The current `T_Lam_L1_*` rules (per the L2 mode-
+split table above) carry only the per-type-flag changes. The
+effect-typed `TFun` is an additional, orthogonal extension planned
+for L2 Phase 2. When it lands, the L1 preservation closure can
+return and discharge the lambda-rigidity admits in
+`Semantics_L1.v`.
+
+**Why this isn't L1's job.** Effect-typed function types are a
+typing-layer property, not a region-layer property. Adding them to
+L1's unparameterised judgment would conflate the two. L2 is the
+natural home: the modality parameter is *already* a typing-layer
+decoration; the effect annotation rides alongside it. After L2's
+effect-typed TFun lands, L1's gap closes by importation, not by
+re-deriving L1.
+
+Until that follow-up lands, the §5 table's "Preservation ✓" should
+be read as "achievable under the L1 architecture once L2 effect-
+typed lambdas are introduced". The Linear ⇒ Affine weakening
+(`linear_to_affine` Qed, PR #176) is independent of this dependency
+and already ships.
+
 ---
 
 ## 6. Layer 3 — Echo / residue, in design
