hyperpolymath
diff --git a/‎proofs/STATUS.md‎
Lines changed: 3 additions & 3 deletions b/‎proofs/STATUS.md‎
Lines changed: 3 additions & 3 deletions
@@ -59,11 +59,11 @@ Last verified: 2026-06-14.
 | Session-π **head-coupled select/branch subject reduction** (`nstep_sr_choice_head`, `nstep_gstep_sr_choice_head`, `gbget`/`GStep_Bra`, `proj_br_selected`, `proj_uninv_selected`) | Coq `solo-core/SessionPi.v` | **machine-checked (Coq)** | **S3c.3-choice (axis-2 STRUCTURE, 2026-06-15).** The FIFTH S3c sub-rung — the CHOICE analogue of S3c.3-msg, all real `Qed`, **axiom-free** (`Print Assumptions` closed, dedicated `proofs.yml` S3c.3-choice gate). **Design-panel-validated + independently adversary-verified** (3 design lenses → coq-mechanic clean from-scratch rebuild on Coq 8.18 → a SEPARATE adversary that recompiled all 11 modules, re-instantiated at a fresh 4-role label-1 choreography exercising the recursive arms, and ran run-ahead + disagreeing-branch break attempts; verdict **sound-and-honest, land as-is**). The **head** select/branch sanctioned by a head `GBra p q {lᵢ:Gᵢ}` carries wf from `G` to its **selected** branch continuation `Gl = gbget l bs`: **`nstep_sr_choice_head : p≠q → gbget l bs = Some Gl → wf_assignment_f (GBra p q bs) ra → ra_get ra p = Some (QSel l P) → ra_get ra q = Some (QBra bsP) → pget l bsP = Some Q → wf_assignment_f Gl (ra_set (ra_set ra p P) q Q)`**. Proved by the SAME **3-way located role case-split** as the message head (selector `p` via `ra_set_get_eq` + `pty_sel_inv`; offerer `q` via `pty_bra_inv` + the per-label coverage `Hcov`; uninvolved `r`). The label `l` drives BOTH the new global step (**`GStep_Bra`** on the new functional gbranch lookup **`gbget`** — no such lookup pre-existed; only `proj_br`/`proj_uninv` consumed `gbranch`) and the located **`NStep_Sel`** onto the **SAME** `Gl`. **The genuinely-new part vs the message head:** the uninvolved arm is no longer **definitional** — it rides `proj_uninv` (the plain-merge fold over all branches) and is discharged by the new **`proj_uninv_selected`** via **`merge_forces_eq`** (plain merge is the IDENTITY-MEET, so every branch projects an uninvolved `r` to the SAME type, hence so does the selected `Gl`; the ≥2-branch case uses an explicit one-level unfold to avoid `cbn [proj_uninv]` over-unfolding). The coupled corollary **`nstep_gstep_sr_choice_head`** packages `gstep`+`nstep`+`wf'` for the head step. **Non-vacuity:** `choice3_head_fires_end_to_end` fires the rung end-to-end on the agreeing 3-party choice `g_choice3` (+ `wf_ra_choice3`). **Honest fences:** (1) **HEAD choice only** — run-ahead/non-head selection = S3c.3-perm (a non-head has no matching head `GStep_Bra`); (2) **PLAIN `proj`** (not `proj_u`) — the uninvolved arm leans on `merge_forces_eq`=identity-meet; the label-UNION merge is S3 (**regression pin**: widening `merge` breaks `proj_uninv_selected` and this theorem becomes false-as-stated — that IS the S3 fence); (3) coupled corollary is a head **wrapper** for ONE step, NOT general SR/bisimulation; (4) `p≠q`-as-hypothesis + **functional** `wf_assignment_f` inherited; (5) **PRESERVATION only** — NO progress (S3c.4). Naming avoids the overclaim trap (`_choice_head`, not `n_party_safety`). Strictly **ADDITIVE** (bytes 1-2868 SHA-identical to baseline; sole prior-region edit = the `gbget` fixpoint + the `GStep_Bra` constructor on the `gstep` Inductive). **Remaining S3c (solo):** S3c.3-perm (run-ahead), S3c.4 n-party progress (research-hard — fence). Echo-types audit: **NOT-RELEVANT** (axis-2 STRUCTURE). |
 | Solo syntax / contexts / typing | Idris2 + Coq `solo-core/` | **definitions-only** | de Bruijn terms, QTT context split/scale/zero, context-splitting typing judgement. |
 | `progress` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem progress : Progress.` real `Qed`, axiom-free. Phase F1.3. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed. |
-| `progress` | Idris2 `solo-core/Soundness` | **locally-checked** | Hole-free total function (no `?todo_progress`); accepted by `idris2`, package built in CI (`proofs.yml`). Phase F1.3. |
+| `progress` | Idris2 `solo-core/Soundness` | **locally-checked** | Hole-free total function (no `?todo_progress`); accepted by `idris2`, package built in CI (`proofs.yml`). Phase F1.3. **Re-proven over the SEPARATED context (`Tctx`/`Uvec`) + both products (`TWith`/`TTensor`, `LetPair`) in the 2026-06-15 F1.4 design migration** — closed-term inversions now massage only the usage vector (`uaddEmpty`/`uscaleEmpty`), since the shared type context stays `TEmpty` automatically; `:total progress` confirms totality. |
 | `preservation` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem preservation : Preservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed (and likewise `affine_pres`). |
-| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`. Proof = Phase F1.4 (Idris track). |
+| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. |
 | Small-step `step` | Coq `solo-core/SoloCore` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. |
-| Small-step `Step` | Idris2 `solo-core/Soundness` | **statement-only** | Idris twin (unverified on this track). |
+| Small-step `Step` | Idris2 `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, both products: additive `SFst`/`SSnd` fire on `With` values, multiplicative `SLetPair` fires on a `Tensor` value via `subst2`; plus the echo residue rules (`SWeaken`). Consumed by the verified `progress`. Migrated 2026-06-15. |
 | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. |
 | Echo **residue-measure SEAM** (`RESIDUE_MEASURE`, `EchoTraceTropical`, `echo_measure_not_injective`) | Coq `solo-core/ResourceAlgebra.v` + `EchoMeasure.v` | **machine-checked (Coq)** | **E4 SEAM — Coq mirror (axis-3 ECHO, 2026-06-14).** The my-lang half of the joint seam capstone ("interaction, not identification, is a theorem"), all real `Qed`, **axiom-free** (`Print Assumptions` closed, dedicated `proofs.yml` E4 gate). The former PENDING prose sketch in `ResourceAlgebra.v` is now the real **`Module Type RESIDUE_MEASURE (S : SEMIRING)`** — `measure : Residue → S.Q` with `measure_empty`/`measure_combine` (a monoid homomorphism `(Residue,combine,empty) → (S.Q,qmul,one)`, needing only the DONE R2 SEMIRING) — a faithful mirror of the upstream `tropical-resource-typing` `Resource/EchoBridge.lean` `structure ResidueMeasure`. `EchoMeasure.v` **inhabits** it at the DONE R4 Tropical cost carrier (`EchoTraceTropical`: a residue is an echo reindexing trace, `measure` = accumulated `Affine`-collapse cost = tropical `Fin`), and witnesses measure-**independence** on the Coq side via **`echo_measure_not_injective`** (`[Affine]` and `[Linear;Affine]` both cost `Fin 1` → the measure cannot reconstruct the residue). **Echo-types audit: RELEVANT (axis-3 ECHO)** — the audit confirmed the seam is already mechanised upstream on both foundations (echo-types `Echo/Measure/Interface.agda` `ResidueMeasure` + `Separation/NotResourceInstance.agda` `equal-measure-does-not-imply-equal-echo`, `--safe --without-K`); per the audit directive the Coq side **reuses** rather than re-derives. **Honest fences:** (1) the Coq mirror carries the measure HOMOMORPHISM + residue-level non-injectivity; the full measure-independence over the degrade-compose modality (the `ECHO_MODALITY` `act` transport, sketch (b)) is upstream-**CITED**, not re-derived — hence the ladder marks E4 `◑` (Coq mirror ✓, full seam upstream); (2) **hard IS-NOT invariant kept** — Echo is NOT a resource/SEMIRING instance, `measure` is a one-directional `E→R` lossy decoration, and `EchoMode.v`/`EchoResidue.v` stay `Quantity`-independent; (3) the trace carrier is the **free** residue monoid (the minimal composition skeleton), not a claim to BE the full echo residue object. |