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

Continues the choreographic re-derivation route for the eliminator fork
(the single invariant the two open L1 admits share). Experiment 1
(formal/L1ChoreoExperiment.v) returned "relocates" and its own honest-gaps
section 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. It models one region's
lifecycle as 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
configurations 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 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 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), with experiment 1's re-entry failure mode
provably absent (valid is defined to permit re-entry). The wiring lemma is
plausibly a structural induction on the typing derivation, not a
preservation-strength obligation — that is the precise next target.

Honest status: this closes NO admit and adds NO axiom. The 3 outer
Admitted markers (Semantics.v legacy + step_pop + preservation_l1) are
unchanged; it is the consolidation/sharpening step that names the next
target.

## Verification
- coqc 8.18.0 builds all of formal/ clean (exit 0); full project rebuild green.
- Print Assumptions on every new lemma (congruence_internal_scope_carries,
  sibling_use_keeps_region_live, congruence_dichotomy,
  step_pop_obligation_holds_in_trace_model, wiring_discharges_step_pop_holds):
  "Closed under the global context" — axiom-free and admit-free.
- Outer Admitted markers unchanged: Semantics.v:1 + Semantics_L1.v:2 = 3
  (matches PROOF-NEEDS.md §4 status-gate marker).

## Docs
- formal/L1-ELIMINATOR-FORK.md: new §9 recording experiment 2's result.
- formal/L1ChoreoExperiment.v: forward-reference from honest-gaps §2.
- PROOF-NEEDS.md §5.4: route step 2b added; §1 row corrected to ground truth.
- 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).

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

Author: claude

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