proof(L1): reduce step_pop's 11 eliminator admits to 1 via step_R_change_shape (§6 experiment)

[hyperpolymath]

Summary

Runs the formal/L1-ELIMINATOR-FORK.md §6 deciding experiment in Coq, and lands its concrete by-product: step_pop_disjoint_from_type_l1 goes from 11 internal admits to 1.

Driving the proof by step_R_change_shape (Semantics.v, Qed — every step leaves R unchanged, prepends a fresh region, or removes exactly one) makes all ten eliminator/erasing congruences trivial: a region free in the result type survives unless the step exits that exact region. 255 lines + 11 admits → ~15 lines + 1 admit.

The single residual obligation

step exits r0 ∧ r0 ∈ free_regions(T) ⟹ cnt r0 R ≥ 2 (In r0 (remove_first r0 R))

• Direct-exit sub-case is vacuous: a head redex ERegion r0 v is typed by T_Region_Active_L1, whose ~In r0 (free_regions T) premise contradicts r0 ∈ free_regions(T).
• Residue = congruence-exit: the exiting ERegion r0 is under an eliminator and r0 comes from a sibling's type — a distinct occurrence.

Verdict: relocates (§6 "no"), but cleanly

Proving that distinctness is region-count coherence at a region exit — the temporal/segment structure the snapshot env + result type cannot express. Every closure route (free_regions ⊆ R_out, count_occ_le_l1_m, linking the dynamic exit to the static output) collapses to connecting the dynamic step to the static typing output, which is preservation. The §2 "same wall," mechanically reconfirmed.

Diagnosis corrected: the obstruction is not the §4.8 lambda-rigidity gap (the minimal witness EDrop (EVar j : TString rv) has no lambda) — it's region-count coherence at a region exit. The cleanest possible target for the §3/§5.1 tropically-graded choreography, which stays the recommended closure route.

What this is / isn't

• Is: a clarity + isolation improvement (−224 net lines; one minimal, precisely-stated obligation instead of eleven scattered §4.8 admits) + the §6 verdict recorded in L1-ELIMINATOR-FORK.md §8 and PROOF-NEEDS.md.
• Isn't: an axiom-count change. Outer Admitted count unchanged (still 3); step_pop and preservation_l1 honestly remain Admitted.

Verification

• coqc 8.18.0 builds formal/ clean (exit 0).
• Print Assumptions: preservation_l3 still Closed (unconditionally axiom-free); region_liveness_no_exit_l1_gen axiom-free; step_pop/preservation_l1 surface themselves (honest Admitted).

🤖 Generated with Claude Code

https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

---

Generated by Claude Code