proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit (#178)

## Summary

Replaces the opaque `Axiom region_liveness_at_split_l1` with a
structurally-proved `Lemma … Admitted.` that closes **24 of 26 inductive
cases concretely**, leaving exactly 1 admit at the documented
counterexample sub-case (T_Region_Active_L1 with binder = rv).

The lemma's STATEMENT is unchanged — still universal `forall e`, still
false in the residual sub-case. **This PR is about transparency of proof
debt, not soundness.** The remaining admit accepts the same false
sub-case the Axiom did. But future closure work now has a clearly
identified target rather than an opaque hide-all.

## Closure pattern (24/26 cases proved concretely)

| Case class | Count | Discharge |
|---|---|---|
| R-unchanged base (T_Unit, T_Bool, T_I32, T_Var_*, T_Loc, T_StringNew,
T_Lam, T_Borrow, T_Borrow_Val) | 10 | `try assumption` (IH-free;
hypothesis [In rv R] = goal) |
| Compound (T_StringConcat, T_StringLen, T_Let, T_LetLin, T_App, T_Pair,
T_Fst, T_Snd, T_Inl, T_Inr, T_Drop, T_Copy) | 12 | IH chain |
| Branch-converging (T_Case, T_If) | 2 | IH through R1 to R_final |
| T_Region_L1 (fresh binder, ~In r R) | 1 |
`remove_first_L1_count_other` (r ≠ rv from ~In r R ∧ In rv R) |
| T_Region_Active_L1 r ≠ rv | 1 (sub-case) | same as T_Region_L1 |
| **T_Region_Active_L1 r = rv** | **1 (sub-case)** | **`admit.` —
GENUINELY FALSE** |

The remaining admit is at `formal/Semantics_L1.v:1055`. Documented
source-level counterexample:

```
ERegion rv (EI32 5) : TBase TI32 -| []  at  R = [rv]
```

The rule pops the only `rv` from `R_body`, so `In rv R = True` but `In
rv R' = False`.

## Closure paths forward (in-file + proof-debt.adoc)

- **(i)** Restate with a `no_region_active_pop_of rv e` side condition
and discharge at the 9 call sites in `subst_typing_gen_l1` (smallest
step, consistent with §4.8 closure approach (b)).
- **(ii)** Multi-set `region_env` (substantial L1 redesign).
- **(iii)** Weaker contextual signature.

(i) is the smallest step and the recommended next slice.

## Side update: `docs/proof-debt.adoc`

- Refreshed line numbers post-#170 + post-this-PR (entries now point to
actual current positions in `Semantics_L1.v`).
- Replaced the Axiom L903 entry with the Lemma L998 + admit L1055 +
Admitted L1068 trio.
- Echo.v K entry updated to note PR #173's K-freedom closure (no more
current escape hatch in Echo.v).

## Branch base

Stacked off `proof/l1-region-threading-design` (head `f03d7e7`,
post-#173).

## Test plan

- [x] `coqc 8.18.0` builds `Semantics_L1.v` cleanly
- [x] Clean full-project rebuild passes — 9 .v files including Echo.v,
Modality.v, TypingL2.v
- [x] `Counterexample.v` still Qed (regression test for the L1 design
counterexample)
- [x] 0 Axiom declarations in `Semantics_L1.v` (down from 1)
- [x] `Print Assumptions subst_preserves_typing_l1` still mentions
`region_liveness_at_split_l1` (now as an opaque Admitted-Lemma, not
Axiom — same logical state)
- [x] `proof-debt.adoc` line numbers cover all 9 current escape-hatch
positions (8 admits/Admitted + 1 Lemma-name marker)
- [ ] CI green on the next #153 cycle

## Caveats

- This is **not a soundness improvement**. The lemma's statement is
universal, the residual sub-case is genuinely false, and the `Admitted.`
makes Coq accept it the same way `Axiom` did.
- The improvement is **proof-debt visibility**: 24 cases now have
concrete witnesses, the residual obstacle has a clear narrow definition,
and closure work can attack just one specific structural sub-case.

Refs PR #153, PR #169, PR #170, PR #173, PRESERVATION-DESIGN.md §4.8 +
§4.8.1 + §5.1.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

docs/proof-debt.adoc

@@ -141,31 +141,46 @@ sequenced under the four-layer redesign plan.
   a documentation comment, not a Coq `Admitted.` declaration.
   Listed here for the scanner's substring match; no escape hatch
   at this position.
-* **`formal/Semantics_L1.v:466`** — `admit.` inside
+* **`formal/Semantics_L1.v:471`** (formerly L466) — `admit.` inside
   `region_shrink_preserves_typing_l1_gen` (T_Region_Active_L1
-  shadowed case). Blocked on a list-vs-multiset structural
-  mismatch with three documented closure approaches (lemma's
-  design note, lines 458-465).
-* **`formal/Semantics_L1.v:488`** — `Admitted.` capping the
-  `region_shrink_preserves_typing_l1_gen` lemma. Closes when its
-  one residual internal admit (above) closes.
-* **`formal/Semantics_L1.v:903`** — `Axiom region_liveness_at_split_l1`.
-  Documented in-file (lines 882-902) as understated: the universal
-  `forall e` form is not true, requires either statement
-  strengthening + 9-call-site propagation OR a global invariant via
-  approach (a) (strengthen `T_Var_Lin_L1`). Investigation 2026-05-27
-  concluded approach (c) is L2-gated via effect-typed `TFun`.
-* **`formal/Semantics_L1.v:1258`** — `admit.` for `S_StringConcat_Step2`
-  in `preservation_l1`. Needs a `step_pop_disjoint_from_type_l1`
-  lemma — tractable, deferred to L1.G slice.
-* **`formal/Semantics_L1.v:1344`** — `admit.` for `S_App_Step2` in
-  `preservation_l1`. Lambda-rigidity gap per
-  `PRESERVATION-DESIGN.md` §4.8 — explicitly L2/L3-gated.
-* **`formal/Semantics_L1.v:1385`** — `admit.` for `S_Pair_Step2` in
-  `preservation_l1`. Same lambda-rigidity gap as `S_App_Step2`.
-* **`formal/Semantics_L1.v:1515`** — `Admitted.` capping
-  `preservation_l1`. Closes when its three internal admits
-  (1258 / 1344 / 1385) close — L2-gated.
+  shadowed case). Blocked on a list-vs-multiset structural mismatch
+  with three documented closure approaches (lemma's design note).
+* **`formal/Semantics_L1.v:493`** (formerly L488) — `Admitted.`
+  capping the `region_shrink_preserves_typing_l1_gen` lemma. Closes
+  when its one residual internal admit (above) closes.
+* **`formal/Semantics_L1.v:998`** (formerly `Axiom` at L903 / L977) —
+  `Lemma region_liveness_at_split_l1`. Now a structurally-proved
+  lemma rather than an opaque axiom: 24 of 26 inductive cases close
+  with concrete proof bodies (8 R-unchanged cases auto-discharge;
+  10 compound cases route through IH chains; 1 region case closes
+  via [remove_first_L1_count_other]; 1 sub-case admitted — see
+  L1055). Statement still universal and still false in the L1055
+  sub-case; closure requires either (i) statement strengthening with
+  a `no_region_active_pop_of rv e` side-condition, (ii) a multi-set
+  region environment, or (iii) a weaker contextual signature. All
+  three are L1 follow-up; (i) is the smallest step.
+* **`formal/Semantics_L1.v:1055`** — `admit.` inside
+  `region_liveness_at_split_l1`'s `T_Region_Active_L1` `r = rv`
+  sub-case. GENUINELY FALSE: counterexample at the source level is
+  `ERegion rv (EI32 5)` typed at `R = [rv]` — the rule pops the only
+  `rv` from `R_body`, so `In rv R` holds but `In rv R'` does not.
+* **`formal/Semantics_L1.v:1068`** — `Admitted.` capping
+  `region_liveness_at_split_l1`. Closes when the L1055 sub-case
+  closes via any of (i)/(ii)/(iii).
+* **`formal/Semantics_L1.v:1428`** (formerly L1258) — `admit.` for
+  `S_StringConcat_Step2` in `preservation_l1`. Needs a
+  `step_pop_disjoint_from_type_l1` lemma — tractable, deferred to
+  L1.G slice.
+* **`formal/Semantics_L1.v:1514`** (formerly L1344) — `admit.` for
+  `S_App_Step2` in `preservation_l1`. Lambda-rigidity gap per
+  `PRESERVATION-DESIGN.md` §4.8 + §5.1 — explicitly L2-gated via
+  effect-typed `TFun`.
+* **`formal/Semantics_L1.v:1555`** (formerly L1385) — `admit.` for
+  `S_Pair_Step2` in `preservation_l1`. Same lambda-rigidity gap as
+  `S_App_Step2`.
+* **`formal/Semantics_L1.v:1685`** (formerly L1515) — `Admitted.`
+  capping `preservation_l1`. Closes when its three internal admits
+  (1428 / 1514 / 1555) close — L2-gated.
 
 All eight sites are tracked in the L1 closure plan (PRs
 https://github.com/hyperpolymath/ephapax/pull/155[#155]–https://github.com/hyperpolymath/ephapax/pull/163[#163]).
@@ -174,18 +189,15 @@ explicitly NOT scheduled before
 https://github.com/hyperpolymath/ephapax/pull/153[#153] lands on
 `main`.
 
-=== `formal/Echo.v` — L3 layer's documented K dependency
-
-* **`formal/Echo.v` `mode_le_trans` + `degrade_mode_comp`** — pull
-  in Coq's standard `Eqdep.Eq_rect_eq.eq_rect_eq` (K / UIP) axiom
-  via `dependent destruction`. The Agda upstream
-  (`echo-types/proofs/agda/EchoLinear.agda`) is `--safe --without-K`;
-  the rest of the Ephapax Coq codebase is K-free. Tracked closure:
-  rewrite both with raw dependent pattern matching using motive
-  tricks (see `formal/Modality.v`'s `modality_le_trans` for the
-  K-free template). All other 10+ lemmas in `Echo.v` (including
-  the headline `no_section_collapse_to_residue`) are closed under
-  the global context — zero axioms.
+=== `formal/Echo.v` — L3 layer K dependency CLOSED 2026-05-27
+
+* The previously-documented K dependency in `mode_le_trans` +
+  `degrade_mode_comp` (via `dependent destruction`) was discharged
+  in PR #173 using the K-free motive-trick template from
+  `formal/Modality.v`. **All 16+ lemmas in `Echo.v` 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`.
 
 === `idris2/src/Main.idr:21` — `%default partial`
 

formal/Semantics_L1.v

@@ -973,12 +973,99 @@ Proof. intros. apply T_Loc_L1. assumption. Qed.
     and consistent with the side-conditioning the design doc lists as
     closure approach (b). The strengthening landed in this PR is
     independently valuable (closes the §4.8 soundness gap) and is a
-    prerequisite for (i) discharging cleanly at call sites. *)
-Axiom region_liveness_at_split_l1 :
+    prerequisite for (i) discharging cleanly at call sites.
+
+    === 2026-05-27 partial discharge: Axiom → Lemma with 1 narrow admit ===
+
+    [Axiom] is replaced with [Lemma .. Admitted.] below. The proof
+    body now structurally encodes the case-by-case analysis the
+    header describes:
+
+    - 23 base + compound cases close mechanically (R unchanged or
+      threaded through sub-derivations via IH).
+    - T_Region_L1 (fresh binder) closes via [remove_first_L1_count_other]:
+      [~ In r R ∧ In rv R] gives [r ≠ rv], so the pop preserves rv.
+    - T_Region_Active_L1 (re-entry binder):
+      * Sub-case [r ≠ rv]: same [remove_first_L1_count_other] argument.
+      * Sub-case [r = rv]: the GENUINELY-FALSE case. One [admit] sits
+        here, with a comment quoting the counterexample at the source
+        level (ERegion rv (EI32 5)).
+
+    This converts an opaque universal Axiom into a Lemma with one
+    explicitly-narrow admit. The remaining admit is a structural
+    obligation tied to a documented counterexample, addressable by
+    any of the three closure paths (i)/(ii)/(iii) above. *)
+Lemma region_liveness_at_split_l1 :
   forall R G e T R' G' rv,
     R; G |=L1 e : T -| R'; G' ->
     In rv R ->
     In rv R'.
+Proof.
+  intros R G e T R' G' rv Ht.
+  induction Ht; intros Hin; try assumption.
+  (* Compound cases — thread rv through sub-derivations via IH. *)
+  - (* T_StringConcat_L1: R -> R1 -> R2 *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_StringLen_L1: R -> R' *)
+    apply IHHt. assumption.
+  - (* T_Let_L1: R -> R1 -> R2 *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_LetLin_L1: R -> R1 -> R2 *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_App_L1: R -> R1 -> R2 *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_Pair_L1: R -> R1 -> R2 *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_Fst_L1: R -> R' *)
+    apply IHHt. assumption.
+  - (* T_Snd_L1: R -> R' *)
+    apply IHHt. assumption.
+  - (* T_Inl_L1: R -> R' *)
+    apply IHHt. assumption.
+  - (* T_Inr_L1: R -> R' *)
+    apply IHHt. assumption.
+  - (* T_Case_L1: R -> R1 -> R_final (both branches converge) *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_If_L1: R -> R1 -> R2 (both branches converge) *)
+    apply IHHt2. apply IHHt1. assumption.
+  - (* T_Region_L1 (fresh): premise ~ In r R, body input r::R, output
+       remove_first_L1 r R_body. Since ~In r R but In rv R, r ≠ rv;
+       remove_first_L1 preserves rv. *)
+    assert (Hne : r <> rv).
+    { intro Heq. subst rv. apply H. exact Hin. }
+    (* Body's input is r :: R; In rv R lifts to In rv (r :: R) on the right *)
+    assert (Hin_body_in : In rv (r :: R)) by (right; exact Hin).
+    pose proof (IHHt Hin_body_in) as HinRbody.
+    (* Goal: In rv (remove_first_L1 r R_body) *)
+    apply (count_occ_In string_dec).
+    pose proof (remove_first_L1_count_other r rv R_body Hne) as Heq.
+    unfold cnt in Heq. rewrite Heq.
+    apply (count_occ_In string_dec). exact HinRbody.
+  - (* T_Region_Active_L1 (re-entry): premise In r R, body input R,
+       output remove_first_L1 r R_body. Two sub-cases: *)
+    destruct (string_dec r rv) as [Heq|Hne].
+    + (* r = rv: GENUINELY FALSE. Counterexample at the source level:
+         ERegion rv (EI32 5) types at R = [rv] via T_Region_Active_L1
+         (T = TBase TI32, ~In rv (free_regions T) holds vacuously,
+         body R_body = [rv]); the rule pops the only rv, R' = [] —
+         so In rv R = True but In rv R' = False.
+
+         This is the residual structural obstacle described in the
+         header. Closing it requires one of (i)/(ii)/(iii). *)
+      admit.
+    + (* r ≠ rv: same shape as T_Region_L1. *)
+      pose proof (IHHt Hin) as HinRbody.
+      apply (count_occ_In string_dec).
+      pose proof (remove_first_L1_count_other r rv R_body Hne) as Heq.
+      unfold cnt in Heq. rewrite Heq.
+      apply (count_occ_In string_dec). exact HinRbody.
+  (* T_Borrow_L1, T_Borrow_Val_L1: both have R unchanged — auto-
+     discharged by [try assumption] above. *)
+  - (* T_Drop_L1: R -> R' *)
+    apply IHHt. assumption.
+  - (* T_Copy_L1: R -> R' *)
+    apply IHHt. assumption.
+Admitted.
 
 (** Generalized substitution: at depth [k] for a linear value [v].
     Mirrors legacy [subst_typing_gen]. The only L1-specific gap is the