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

hyperpolymath · hyperpolymath · commit 2aebf633fbf5 · 2026-05-27T12:56:26.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
diff --git a/formal/PROOF-STATUS.a2ml b/formal/PROOF-STATUS.a2ml
@@ -3,18 +3,20 @@
 #
 # PROOF-STATUS.a2ml — machine-readable Coq proof state
 #
-# Snapshot of formal/*.v as of 2026-05-27 (post-L1.A through L1.F).
+# Snapshot of formal/*.v as of 2026-05-27 (post-L1.A through L1.F,
+# post-#176 L2 hybrid, post-#180 K-free Echo.v, post-#181 Axiom→Lemma).
 # Consumed by automated proof-debt trackers, status dashboards, and
 # CI gates that need to know "what counts as proven here".
 #
-# Human-readable companion: formal/PRESERVATION-DESIGN.md §4.7 and §4.8.
+# Human-readable companion: formal/PRESERVATION-DESIGN.md §4.7, §4.8,
+# §4.8.1, §5.1.
 
 [metadata]
-version = "1.0.0"
+version = "1.1.0"
 snapshot-date = "2026-05-27"
-design-branch = "proof/l1-region-threading-design"
 spec-doc = "formal/PRESERVATION-DESIGN.md"
 counterexample = "formal/Counterexample.v"
+note = "Design-branch is superseded by main's L2 hybrid (#176/#177). All L1+L2+L3 work now lives on main."
 
 # ============================================================================
 # FILES — what's in formal/ and its proof-status posture
@@ -61,12 +63,36 @@ note = "Legacy preservation has 1 residual admit (S_Region_Step + T_Region_Activ
 
 [[files]]
 path = "formal/Semantics_L1.v"
-purpose = "L1 preservation theorem + helpers"
+purpose = "L1 preservation theorem + helpers (now m-indexed per #176)"
 status = "active"
-admit-count = 4
-axiom-count = 1
-admitted-lemma-count = 2
-landed-in = ["PR-157", "PR-158", "PR-159", "PR-160", "PR-161", "PR-162", "PR-163"]
+admit-count = 4  # post-#181: 1 in region_liveness_at_split_l1_gen + 3 lambda-rigidity in preservation_l1
+axiom-count = 0  # post-#181: Axiom region_liveness_at_split_l1 → Lemma + 1 admit
+admitted-lemma-count = 3  # region_shrink_..._gen + region_liveness_at_split_l1_gen + preservation_l1
+landed-in = ["PR-157", "PR-158", "PR-159", "PR-160", "PR-161", "PR-162", "PR-163", "PR-176", "PR-181"]
+
+[[files]]
+path = "formal/Modality.v"
+purpose = "L2 modality datatype + thin-poset (Linear ≤ Affine)"
+status = "stable"
+qed-only = true
+landed-in = ["PR-168", "PR-176"]
+note = "K-free throughout. All Qed lemmas (refl/trans/prop) closed under the global context."
+
+[[files]]
+path = "formal/TypingL2.v"
+purpose = "L2 has_type_l2 modality-indexed judgment skeleton"
+status = "stable"
+qed-only = true
+landed-in = "PR-168"
+note = "Single L2_lift_l1 constructor + weaken_modality Qed (zero axioms). Mode-specific T_Lam_*, T_Case_*, T_If_* now live directly on m-indexed has_type_l1 per #176; this file's role is to be the cross-layer entry point for callers wanting the L2 framing explicitly."
+
+[[files]]
+path = "formal/Echo.v"
+purpose = "L3 residue/echo type former — forward-looking scaffold"
+status = "stable"
+qed-only = true
+landed-in = ["PR-166", "PR-167", "PR-180"]
+note = "K-free throughout (post-#180/#173). Headlines: Echo fiber, LEcho mode-polymorphic carrier, weaken Linear→Affine, EchoR + collapse_to_residue + no_section_collapse_to_residue (the irreversibility theorem; closed under the global context, zero axioms)."
 
 # ============================================================================
 # L1 PROOF CHAIN — Qed lemmas
@@ -181,11 +207,12 @@ follow-up = "see PRESERVATION-DESIGN.md §4.8"
 [[proof-debt]]
 id = "L1.C-region-liveness"
 file = "Semantics_L1.v"
-line-anchor = "region_liveness_at_split_l1 (Axiom)"
-class = "carry-invariant-through-induction"
+line-anchor = "region_liveness_at_split_l1_gen T_Region_Active_L1 r=rv (post-#181)"
+class = "structurally-false-as-universal"
 tractable = true
-diagnosis = "subst_typing_gen_l1 needs to know that In rv R_inner at each compound-rule split point. The outer call provides In rv R; the inductive descent doesn't propagate it because T_Var_Lin_L1 doesn't enforce In rv R."
-closes-when = "one of (1) strengthen T_Var_Lin_L1 to require In rv R, (2) add a side condition to subst_typing_gen_l1 stating In rv R at every R_inner reached, (3) prove a region-liveness corollary of L1.B's count monotonicity"
+diagnosis = "ERegion rv (EI32 5) at R = [rv] gives In rv R but In rv R' = False (the rule pops the only rv from R_body). The Lemma's universal statement is false in this sub-case; 28/29 cases proved concretely via PR #181."
+closes-when = "one of (i) restate with a no_region_active_pop_of rv e side condition + discharge at the 9 call sites in subst_typing_gen_l1, (ii) multi-set region_env, (iii) weaker contextual signature"
+status-history = "Axiom (pre-#181) → Lemma with 1 narrow admit (post-#181). Transparency improvement, not soundness."
 
 # ============================================================================
 # DOCUMENTATION POINTERS
