proof(L1): choreographic experiment 2 — non-collapsed trace model closes the congruence fork in-model (#332)

## What this is

The next step on the **choreographic re-derivation** route for the
eliminator fork — the single invariant the two open L1 admits
(`step_pop_disjoint_from_type_l1`, `preservation_l1`) share.

Experiment 1 (`formal/L1ChoreoExperiment.v`) returned **"relocates"**
and its own *honest-gaps* §2 prescribed the next move: build a
**non-collapsed** apparatus and aim it at the **congruence** cases
(`S_Let_Step` / `S_App_Step2` / `S_Pair_Step2` / `S_Case_Step` — *inner
pop erased from the outer result type*), **not** the clean `ERegion`
exit (already `Qed`). `formal/L1ChoreoExperiment2.v` does exactly that.

## The model & the decisive result

One region's lifecycle is a `Trace` of `Open`/`Close`/`Use` events
**relative to the subterm structure**, run from `k = cnt rv R`. The
trace keeps the same balance the scalar `cnt rv R` keeps **but also
keeps the order** — which separates two configs the snapshot *conflates*
at the `e1`/`e2` boundary:

- **internal scope** (stepping sibling rv-net-neutral) ⇒ surviving
sibling coherent at the original `k` —
`congruence_internal_scope_carries`;
- **escaping close** (stepping sibling closes an outer `rv` the
surviving sibling still uses) ⇒ **impossible** in a coherent trace: the
post-step balance is forced `>= 1` — `sibling_use_keeps_region_live`.

`sibling_use_keeps_region_live` is **precisely the obligation
`step_pop_disjoint_from_type_l1` relocates to** (`In rv (free_regions T)
-> In rv R -> In rv R'`), proved here as a pure structural fact,
**non-circularly** (no appeal to preservation). The snapshot can't state
it because it carries only the final balance, not the witness that the
`Use` is *ordered after* the stepping sibling.

## Verdict

Congruence verdict upgraded from **"relocates"** to **"closes in the
trace model, reduced to ONE wiring lemma"** (`wiring_obligation`: typing
⇒ `valid` trace at `k = cnt rv R`). Experiment 1's re-entry failure mode
**provably does not recur** (`valid` is defined to permit re-entry). The
wiring lemma is plausibly a *structural induction* on the typing
derivation — that is the precise next target.

## Honest status

**Closes no admit; adds no axiom.** The 3 outer `Admitted.` markers
(legacy `Semantics.v` + `step_pop` + `preservation_l1`) are unchanged.
This is the consolidation/sharpening step that names the next target —
not the closure. Stays fully inside the owner fences (no patching of the
fenced admits, no new `Axiom`, no cross-layer side-conditions).

## Verification (coqc 8.18.0)

- Full `formal/` rebuild green (exit 0).
- `Print Assumptions` on every new lemma → **"Closed under the global
context"** (axiom-free, admit-free).
- Outer `Admitted.` markers unchanged: `Semantics.v:1` +
`Semantics_L1.v:2` = **3** (matches `PROOF-NEEDS.md §4` status-gate
marker).

## Also (doc hygiene)

- `formal/L1-ELIMINATOR-FORK.md`: new **§9** recording experiment 2.
- `formal/L1ChoreoExperiment.v`: forward-reference from honest-gaps §2.
- `PROOF-NEEDS.md §5.4`: route step **2b** added; §1 row corrected.
- `TEST-NEEDS.md` / `PROOF-NEEDS.md §1`: stale admit counts (`4`/`5`)
corrected to verified ground truth (**3** total, **2** in
`Semantics_L1.v` at lines 3315/3336).

🤖 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

@@ -57,7 +57,7 @@ For the architectural background see
 | L1 judgment indexed by modality `m : Modality` | `formal/TypingL1.v` | landed via PRs #176 + #177 |
 | L2 modality core (`Modality.v`, `linear_to_affine`) | `formal/Modality.v` | 1 Qed, zero axioms |
 | L3 calculus (echo / residue fiber + degrade + no-section proof) | `formal/Echo.v` | 12 Qed, 0 admits |
-| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 37 Qed; 3 outer `Admitted.` markers cover 5 internal `admit.` cases at current lines 576/646/1994/2014/3132. Phase 3b Stage 1a (#252, MERGED 2026-05-30: `tfuneff_lambda_free` + `Counterexample_L2_nested.v`) and Stage 1b (#253, MERGED 2026-05-31: closed-value substitution + `preservation_l2_app_eff_beta` β-case for TFunEff). Slice 4 L3 wiring delivered `preservation_l3_region_active_echo` / `preservation_l3_drop_echo` / `preservation_l3` umbrella. |
+| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 37 Qed; **2** outer `Admitted.` markers (`step_pop_disjoint_from_type_l1` / `preservation_l1`) cover **2** internal `admit.` cases at current lines 3315/3336 (rebuilt `coqc 8.18.0` ground truth 2026-06-27; the earlier 5-internal / lines-576/646/1994/2014/3132 figure is pre-dissolution, superseded by the §4 marker = 3 total). Phase 3b Stage 1a (#252, MERGED 2026-05-30: `tfuneff_lambda_free` + `Counterexample_L2_nested.v`) and Stage 1b (#253, MERGED 2026-05-31: closed-value substitution + `preservation_l2_app_eff_beta` β-case for TFunEff). Slice 4 L3 wiring delivered `preservation_l3_region_active_echo` / `preservation_l3_drop_echo` / `preservation_l3` umbrella. |
 | L2 β-case lemmas (Stage 1b) | `formal/TypingL2.v` | 10 Qed total: `weaken_modality` family (5), `preservation_l2_via_l1` (conditional on `preservation_l1`), `linear_value_retype_l1_m`, and 3 `preservation_l2_app_eff_beta_*` variants (Linear / ground_nonlinear / tfuneff conditional on Stage 1b side conditions P1+P2+P3). Stage 2/3/4 (#240/#241/#242) drop the conditions. |
 | L4 labelling scaffold (Phase A, 2026-05-28) | `formal/L4.v` | `ProgramMode` enum (`PModeLinear` / `PModeAffine` / `PModeBoundaryMix`) + `program_mode_to_modality` round-trip. Definitions only — no theorems, zero axioms. |
 | Counterexample_L2 regression witnesses (Phase 4c + 3b) | `formal/Counterexample_L2.v`, `formal/Counterexample_L2_nested.v` | 5 + 5 Qed pinning the Phase 4c (fresh-region scope crossing) and Phase 3b (nested TFunEff) soundness-gap classes |
@@ -425,11 +425,29 @@ Real Idris Qed proofs verified clean (no `believe_me`/`assert_total`/holes):
    `EDrop (EVar j : TString rv)` choreography over two segments — does subject
    reduction carry liveness through `S_Region_Exit rv` coherently, or relocate
    it into a projection-coherence side-condition? (`L1-ELIMINATOR-FORK.md §6`.)
+   **DONE** (`formal/L1ChoreoExperiment.v`): verdict **relocates** — and it
+   sharpened *why* (the naive model collapses projection onto the scalar
+   predicate, which is false at re-entry; the real fork lives in the
+   **congruence** cases, not the clean `ERegion` exit).
+2b. **Congruence experiment (non-collapsed model):** **DONE**
+   (`formal/L1ChoreoExperiment2.v`, `L1-ELIMINATOR-FORK.md §9`). A trace model
+   that keeps subterm-relative **order** (not just the scalar balance)
+   **closes — in the model** — the obligation `step_pop` relocates to:
+   `sibling_use_keeps_region_live` is `Qed`, axiom-free, non-circular, and
+   unprovable from the snapshot alone. The congruence verdict is upgraded from
+   "relocates" to "closes in the trace model, reduced to **one wiring lemma**"
+   (`wiring_obligation`: typing ⇒ `valid` trace at `k = cnt rv R`). Experiment
+   1's re-entry failure mode provably does not recur. **Closes no admit yet**
+   (honest count still 3); it is the consolidation step that names the precise
+   next target.
 3. **If green → choreographic-foundational re-derivation:** region liveness as
    a tropically-graded choreography across time segments (regions = session-
    typed resources, scopes = segments, preservation = subject reduction).
    Closes #3 → **2 → 0**, and likely gives **L4** its dyadic (2-party
-   choreography) structure for free — one foundation, all four layers.
+   choreography) structure for free — one foundation, all four layers. **Next
+   concrete step:** discharge `wiring_obligation` (plausibly a structural
+   induction on the typing derivation — each trace `Close`/`Use` `>= 1` premise
+   mirrors a local `In r R` premise in `T_Region_Active_L1` / `T_Loc_L1`).
 
 ### 5.5 Foundation trust audit (2026-06-16) — GO
 

TEST-NEEDS.md

@@ -36,9 +36,11 @@
 ### Point-to-Point (P2P)
 **Source counts:** 49 Rust (19 crates) + 98 .eph files + 17 Idris2 + 3 V
 
-**Coq admitted proofs remaining: 4** (1 outer `Admitted.` in
-`formal/Semantics.v` + 3 outer `Admitted.` markers in
-`formal/Semantics_L1.v` covering 5 internal `admit.` cases). Single-
+**Coq admitted proofs remaining: 3** (1 outer `Admitted.` in
+`formal/Semantics.v` + 2 outer `Admitted.` markers in
+`formal/Semantics_L1.v` — `step_pop_disjoint_from_type_l1` /
+`preservation_l1` — covering 2 internal `admit.` cases at lines
+3315/3336; rebuilt `coqc 8.18.0` ground truth 2026-06-27). Single-
 source breakdown lives in `PROOF-NEEDS.md §4`; `scripts/status-gate.sh`
 reads from there.
 
@@ -52,7 +54,7 @@ reads from there.
 - Example programs not verified in CI
 
 #### Known issues:
-- 4 Admitted markers in Coq (1 in `Semantics.v` — provably-false legacy preservation, sacrosanct; 3 in `Semantics_L1.v` covering 5 inner `admit.` cases — pre-existing L1 structural debt + parallel mirrors per PROOF-NEEDS.md §4)
+- 3 Admitted markers in Coq (1 in `Semantics.v` — provably-false legacy preservation, sacrosanct; 2 in `Semantics_L1.v` — `step_pop_disjoint_from_type_l1` + `preservation_l1`, the eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.md §4)
 - 5 remaining tasks (#15-#19) from type checker audit
 - interp env-leak fix was made 2026-03-28
 

formal/L1-ELIMINATOR-FORK.md

@@ -191,3 +191,61 @@ 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.
+
+## 9. Result of experiment 2 (2026 — `formal/L1ChoreoExperiment2.v`)
+
+Experiment 1 (§5/§6, `L1ChoreoExperiment.v`) returned **"relocates"**, but its
+own "honest gaps" §2 recorded *why* and prescribed the next move: it had
+**collapsed** the projection onto the scalar predicate
+`expr_no_exit_of_region` (discarding subterm-relative order) and had targeted
+the **clean** `ERegion rv` exit (already `Qed`) rather than the genuinely-open
+**congruence** cases (`S_Let_Step` / `S_App_Step2` / `S_Pair_Step2` /
+`S_Case_Step` — *inner pop erased from the outer result type*). Experiment 2
+builds the minimal **non-collapsed** apparatus that gap asked for and aims it at
+the congruence boundary.
+
+**The model.** One region `rv`'s lifecycle is a `Trace` of events
+(`Open`/`Close`/`Use`) *relative to the subterm structure*, run from an initial
+balance `k = cnt rv R`. The trace keeps the same open/close balance the scalar
+`cnt rv R` keeps — but, unlike a snapshot, it keeps the **order**. `valid k t`
+is the local well-nesting condition (a `Close` or `Use` requires balance `>= 1`
+at that point).
+
+**The decisive result (all `Qed`, axiom-free — `Print Assumptions` clean).**
+The order is exactly enough to separate two configurations the snapshot
+*conflates* at the `e1`/`e2` boundary:
+
+- **Internal scope** — the stepping sibling is `rv`-net-neutral
+  (`final_balance k t1 = k`): the surviving sibling is coherent at the original
+  `k`, independent of `t1`'s internal region activity
+  (`congruence_internal_scope_carries`).
+- **Escaping close** — the stepping sibling closes an outer `rv` while the
+  surviving sibling still uses it: **impossible in a coherent trace**. If the
+  surviving sibling's dependence is a `Use` ordered after `t1`, the post-`t1`
+  balance is forced `>= 1` (`sibling_use_keeps_region_live`). This is precisely
+  the obligation `step_pop_disjoint_from_type_l1` *relocates to*
+  (`In rv (free_regions T) -> In rv R -> In rv R'`), and it is proved here as a
+  pure structural fact — **non-circularly**, with no appeal to preservation.
+  The snapshot cannot state it because it carries only the final balance, not
+  the witness that the `Use` is *ordered after* the stepping sibling.
+
+**Verdict.** For the congruence cases — where experiment 1 located the
+genuinely-open fork — the non-collapsed trace model **closes** the relocated
+obligation *in the model*, and reduces the open question to **one wiring
+lemma**: that `has_type_l1` of a congruence redex induces a `valid` trace at
+`k = cnt rv R` with the surviving sibling's `rv`-dependence as a trailing
+`Use` (`wiring_obligation`, stated honestly, never faked — mirroring
+experiment 1's `close_derives_coherence`). Crucially, experiment 1's specific
+failure mode (the relocated predicate is *false* at re-entry) **provably does
+not recur**: the trace's `valid` is *defined* to permit re-entry (nested
+`Open`/`Close`, balance `> 1`). So the verdict for the congruence boundary is
+upgraded from **"relocates"** to **"closes in the trace model, reduced to one
+wiring lemma"**, and the wiring lemma is named as the precise next target.
+
+This experiment closes **no** admit and adds **no** axiom (honest count
+unchanged); it is the consolidation+sharpening step, not the closure. The
+remaining gate to an actual ADMIT-3 closure is `wiring_obligation` — extract a
+`valid` trace from a typing derivation — which, unlike experiment 1's dead end,
+is plausibly a *structural induction* on the typing derivation (each `Close` /
+`Use` event's `>= 1` premise mirrors a local `In r R` premise in
+`T_Region_Active_L1` / `T_Loc_L1`), not a preservation-strength obligation.

formal/L1ChoreoExperiment.v

@@ -187,6 +187,10 @@ Qed.
        ([S_Let_Step] / [S_App_Step2] / [S_Pair_Step2] / [S_Case_Step],
        [Semantics_L1.v:3271-3284], inner pop erased from outer type) —
        NOT the clean [ERegion rv] exit, which is already Qed.
+       STARTED in [L1ChoreoExperiment2.v]: the non-collapsed trace model
+       aimed at the congruence boundary CLOSES the relocated obligation
+       in-model ([sibling_use_keeps_region_live], Qed, axiom-free) and
+       reduces the fork to one wiring lemma. See [L1-ELIMINATOR-FORK.md] §9.
 
     3. The tropical/Lean side has the monotonicity backbone
        ([matStar_mono], [id_le_star], [parametric_resource_transport]) but