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

[hyperpolymath]

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-proof(L1.G): strengthen T_Var_*_L1 with region well-formedness (§4.8 path 3) #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 proof(L3.K): rewrite Echo.v K-free — eliminate eq_rect_eq dependency #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

• coqc 8.18.0 builds Semantics_L1.v cleanly
• Clean full-project rebuild passes — 9 .v files including Echo.v, Modality.v, TypingL2.v
• Counterexample.v still Qed (regression test for the L1 design counterexample)
• 0 Axiom declarations in Semantics_L1.v (down from 1)
• Print Assumptions subst_preserves_typing_l1 still mentions region_liveness_at_split_l1 (now as an opaque Admitted-Lemma, not Axiom — same logical state)
• proof-debt.adoc line numbers cover all 9 current escape-hatch positions (8 admits/Admitted + 1 Lemma-name marker)
• CI green on the next proof+design: verified counterexample + four-layer preservation redesign #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