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

Runs the L1-ELIMINATOR-FORK.md §6 deciding experiment in Coq. Driving
step_pop_disjoint_from_type_l1 by step_R_change_shape (Semantics.v, Qed —
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 region. The 255-line
induction with 11 admits becomes ~15 lines with 1.

The single residual obligation is exactly:
  step exits r0  /\  r0 in free_regions(T)  ==>  cnt r0 R >= 2.
Its direct-exit sub-case is vacuous (a head ERegion r0 v is typed by
T_Region_Active_L1, whose ~In r0 (free_regions T) contradicts the premise);
the residue is the congruence-exit case (r0 from a sibling's type, a
distinct occurrence). Establishing that distinctness is the temporal/segment
coherence the snapshot env + result type cannot express; every route
collapses to connecting the dynamic exit to the static output = preservation
itself. Verdict: RELOCATES (the §2 wall), now to ONE minimal obligation.

Diagnosis corrected in-source: the obstruction is NOT §4.8 lambda-rigidity
(the witness EDrop (EVar j : TString rv) has no lambda) but region-count
coherence at a region exit.

Verified: coqc 8.18.0 builds clean; Print Assumptions unchanged
(preservation_l3 still axiom-free; step_pop + preservation_l1 surface
themselves). Outer Admitted count UNCHANGED (3); this is clarity + isolation,
not an axiom-count reduction. L1-ELIMINATOR-FORK.md §8 + PROOF-NEEDS.md §5.2
updated with the verdict.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

Author: claude

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.