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

## 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 `admit`s → ~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.com/claude-code)

https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

---
_Generated by [Claude
Code](https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -385,7 +385,7 @@ future drift is flagged. (A′ shifts the line numbers but not the count.)
 |---|---|---|---|---|---|
 | 1 | `region_shrink_preserves_typing_l1_gen_m` | `Semantics_L1.v:441` | `:572`, `:642` | **live structural** (list-vs-multiset tear) | **Dissolves** — carrier refactor `region_env : list` → count-map. `L1-REGION-REFOUNDATION-PLAN.md` |
 | 2 | `region_liveness_at_split_l1_gen` | `Semantics_L1.v:1904` | `:1956`, `:1976` | **provably FALSE** as written (witness `ERegion rv (EI32 5)` at `R=[rv]`) | **Repaired** — restate as graded `live R rv ∧ no-exit-of-rv ⇒ live R' rv`; prove from `count_occ_le_l1_m` monotonicity + ~13-site call audit. `L1-REGION-REFOUNDATION-PLAN.md §5` |
-| 3 | `step_pop_disjoint_from_type_l1` | `Semantics_L1.v:3106` | **~9–11** across every eliminator/erasing context (`S_App_Step2`, `S_Pair_Step2`, `S_Inl/Inr_Step`, `S_Case_Step`, `S_Let_Step`, `S_Region_Step`) — all blocked on the §4.8 lambda-rigidity gap | **the eliminator fork** | **Open research** — choreographic typing across time segments, used foundationally. `L1-ELIMINATOR-FORK.md` |
+| 3 | `step_pop_disjoint_from_type_l1` | `Semantics_L1.v` | **1** (reduced from ~9–11 in 2026 via the `step_R_change_shape` rewrite — see `L1-ELIMINATOR-FORK.md` §8). The single residual obligation is `step exits r0 ∧ r0 ∈ free_regions(T) ⟹ cnt r0 R ≥ 2`; its direct-exit sub-case is vacuous, the residue is congruence-exit count-coherence. Diagnosis corrected: **not** §4.8 lambda-rigidity (the witness has no lambda) but region-count coherence at a region exit. | **the eliminator fork** | **Open research** — the tropically-graded choreography over time segments. `L1-ELIMINATOR-FORK.md` §3–§8 |
 | 4 | `preservation_l1` (capstone) | `Semantics_L1.v:3367` | `:3379` | **gated** on 1–3 | follows once 1–3 land |
 
 `preservation_l3` (`Semantics_L1.v`, **Qed**) is real and depends on **only**

formal/L1-ELIMINATOR-FORK.md

@@ -153,3 +153,41 @@ relocate the difficulty into projection coherence, and the sequential-language
 foundation is non-standard. The §5/§6 experiment is the inexpensive way to
 learn which — and it is the recommended next step on the eliminator fork, run in
 parallel with (not blocking) the clean-win carrier refactor.
+
+## 8. Result of the §6 experiment (2026 — run in Coq)
+
+The §6 deciding experiment was run against the live judgment. Outcome: the
+verdict is the predicted **"no" — it relocates** — but the experiment also
+produced a concrete simplification worth keeping.
+
+**(a) `step_pop_disjoint_from_type_l1` reduces from 11 admits to 1.** Driving
+the proof by `step_R_change_shape` (every step leaves `R` fixed, 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. The 255-line induction with eleven `admit`s
+becomes ~15 lines with one. (Landed; `coqc 8.18.0` + `Print Assumptions`
+verified; outer `Admitted` count unchanged.)
+
+**(b) The single residual obligation, exactly:** the step exits `r0` while
+`r0 ∈ free_regions(T)` ⟹ `cnt r0 R ≥ 2` (i.e. `In r0 (remove_first r0 R)`).
+Its **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)`. The residue is the **congruence-exit**
+case (`ERegion r0` under an eliminator; `r0` from a sibling's type — a
+distinct occurrence).
+
+**(c) Why it relocates (the §2 wall, mechanically reconfirmed).** Discharging
+the congruence case needs the sibling's `r0` proved a *distinct* occurrence
+from the exiting one — exactly the temporal/segment coherence the snapshot
+env + result type cannot express. Every closure route tried
+(`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. Circular.
+
+**(d) The §4.8 framing was wrong** and is corrected in the source: the
+obstruction is not lambda-rigidity (the witness has no lambda) but
+region-count coherence at a region exit. **Net: ADMIT 3 stays open at the
+honest count (still 2 outer `Admitted`), but is now ONE minimal, precisely
+characterised obligation** — the cleanest possible target for the §3 / §5.1
+tropically-graded choreography. That choreographic closure is the
+unchanged recommended next step.