feat(proofs): S3c.3-choice — head-coupled select/branch n-party subject reduction (axiom-free)

The CHOICE analogue of S3c.3-msg: nstep_sr_choice_head (+ coupled corollary
nstep_gstep_sr_choice_head), the new functional gbranch label-lookup gbget,
the GStep_Bra global choice step, and helpers proj_br_selected /
proj_uninv_selected. Same 3-way located role split as the message head;
the label l drives both GStep_Bra and NStep_Sel onto the same selected
branch Gl = gbget l bs. The uninvolved-role arm — the genuinely-new part
vs the message head — is discharged via merge_forces_eq (plain merge =
identity-meet, so every branch projects an uninvolved r to the SAME type,
hence so does Gl). Non-vacuity: choice3_head_fires_end_to_end on g_choice3.

Strictly ADDITIVE (bytes 1-2868 SHA-identical to baseline; sole prior-region
edit = gbget + the GStep_Bra constructor on the gstep Inductive). Dedicated
proofs.yml S3c.3-choice Print-Assumptions gate. STATUS/AXIS/ALIGNMENT updated.
Design-panel-validated + independently adversary-verified (fresh recompile,
negative control, run-ahead + disagreeing-branch break attempts).

Also adds a STATUS.md "Implementation <-> spec coupling" fence recording the
spec<->impl gaps as absent/deferred-to-P-later (the verified Coq `check` has
no Rust counterpart; the interpreter has no adequacy proof; EchoMode/Ty::Echo
are inert; no session runtime; me elaboration is abstract-only) so the
proved/implemented boundary is not mistaken for closed.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/proofs.yml

@@ -316,6 +316,32 @@ jobs:
               || { echo "::error::SessionPi.${thm} is NOT axiom-free"; exit 1; }
           done
 
+      - name: Assert S3c.3-choice head-coupled select/branch subject reduction is axiom-free
+        working-directory: proofs/verification/coq/solo-core
+        run: |
+          # S3c.3-choice (axis-2 STRUCTURE): the CHOICE analogue of
+          # S3c.3-msg. The HEAD select/branch sanctioned by a head
+          # GBra p q {l_i:G_i} carries wf from G to its SELECTED branch
+          # continuation Gl = gbget l bs (nstep_sr_choice_head, 3-way
+          # located role split: selector p / offerer q / uninvolved r).
+          # The label l drives BOTH the global step (GStep_Bra) and the
+          # located step (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) and
+          # is discharged by proj_uninv_selected via merge_forces_eq
+          # (plain merge = identity-meet, so every branch projects an
+          # uninvolved r to the SAME type, hence so does the selected one).
+          # PLAIN proj only (label-UNION merge = S3); HEAD choice only
+          # (run-ahead = S3c.3-perm); PRESERVATION only (NO progress = S3c.4).
+          for thm in proj_br_selected proj_uninv_selected \
+                     nstep_sr_choice_head nstep_gstep_sr_choice_head \
+                     wf_ra_choice3 choice3_head_fires_end_to_end; do
+            echo "Require Import SoloCore.SessionPi. Print Assumptions ${thm}." \
+              | coqtop -R . SoloCore 2>/dev/null | tee "/tmp/assum_s3c3choice_${thm}.txt"
+            grep -q "Closed under the global context" "/tmp/assum_s3c3choice_${thm}.txt" \
+              || { echo "::error::SessionPi.${thm} is NOT axiom-free"; exit 1; }
+          done
+
   idris:
     name: Idris2 solo-core
     runs-on: ubuntu-latest

proofs/ALIGNMENT-PLAN.md

@@ -210,6 +210,19 @@ canonical track; Idris2 is a definitions + `progress` cross-check only.)*
   rule + soundness); full-union merge + n-party SR/progress/coherence (**S3c** — where "duet" stops
   and "ensemble" begins). Echo-types: NOT-RELEVANT (axis-2 STRUCTURE vs axis-3 MODALITY).
 
+  **S3c done through S3c.3-choice (2026-06-14/15):** the n-party operational frontier, all axiom-free
+  (per-rung detail in STATUS.md). S3c.0 full label-union merge (`umerge`/`umerge_idem`); S3c.1
+  union-projection (`proj_u`/`projection_total_u`, `merge_forces_eq`); S3c.2 n-ary located opsem
+  (`nstep`/`gstep`, ring run, with the honesty witness `nstep_breaks_wf_at_fixed_G` proving SR must be
+  stated against a *stepping* G); S3c.3-msg the first EARNED n-party safety half — head-coupled MESSAGE
+  subject reduction (`nstep_sr_msg_head`); and **S3c.3-choice** the head-coupled SELECT/BRANCH SR
+  (`nstep_sr_choice_head`), whose uninvolved-role arm is the genuinely-new part (rides `proj_uninv`,
+  discharged by the new `proj_uninv_selected` via `merge_forces_eq` = plain-merge-is-identity-meet).
+  Both SR rungs are design-panel-validated + independently adversary-verified. **Remaining:** S3c.3-perm
+  (run-ahead / asynchronous-permutation SR — a bigger swap theory); S3c.4 n-party progress /
+  deadlock-freedom (**research-hard** — the MPST liveness frontier where "ensemble" earns its keep); and
+  μ typing/SR up-to-unfolding (**S1.3b-meta**, still deferred).
+
 ### Phase F2 — Effects metatheory (mechanised)
 Closes part of **G2/G4**. Lift `proofs/shared/effect-system/` to a
 mechanised effect-row calculus with an effect-soundness statement, then

proofs/AXIS-ARCHITECTURE.md

@@ -147,8 +147,11 @@ my-lang is parametric over **both**, and identifies **neither**.
       (nstep/gstep, ring run, adequacy-only);
       S3c.3-msg ✓ head-coupled message subject
       reduction (nstep_sr_msg_head, first EARNED
-      n-party safety half); all axiom-free.
-      S3c.3-choice/perm + S3c.4 progress = open)
+      n-party safety half); S3c.3-choice ✓
+      head-coupled select/branch SR
+      (nstep_sr_choice_head, uninvolved arm via
+      proj_uninv_selected/merge_forces_eq); all
+      axiom-free. S3c.3-perm + S3c.4 progress = open)
 ```
 
 Dependency spine: `R0 → R1 → R2 → {R3, R4} ; R3 → R5` ; `R2 + echo-core → E4` ; `S1 → S2`.
@@ -454,6 +457,27 @@ Dependency spine: `R0 → R1 → R2 → {R3, R4} ; R3 → R5` ; `R2 + echo-core
   (select/branch SR, reusing `pty_sel_inv`/`pty_bra_inv`/`pget`); S3c.3-perm (run-ahead, needs a
   gstep-with-swap relation); S3c.4 n-party progress (research-hard — fence). **Echo-types audit:
   NOT-RELEVANT** (axis-2 STRUCTURE).
+- **S3c.3-choice DONE — head-coupled select/branch subject reduction, axiom-free 2026-06-15.** The fifth S3c
+  sub-rung — the CHOICE analogue of S3c.3-msg. Design-panel-validated (3 lenses) + **independently
+  adversary-verified** (a SEPARATE adversary recompiled all 11 modules clean, re-instantiated at a fresh
+  4-role label-1 choreography exercising the recursive arms of `gbget`/`proj_br_selected`/`proj_uninv_selected`,
+  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 to its SELECTED branch continuation
+  `Gl = gbget l bs`: **`nstep_sr_choice_head`** (same 3-way located role split as the message head — selector
+  `p` via `pty_sel_inv`, offerer `q` via `pty_bra_inv` + the per-label coverage, 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:** the uninvolved arm is no longer DEFINITIONAL (as in the message head)
+  — it rides `proj_uninv` (the plain-merge fold) and is discharged by the new **`proj_uninv_selected`** via
+  **`merge_forces_eq`** (plain merge = identity-meet ⇒ every branch projects an uninvolved `r` to the SAME type,
+  so the selected branch does too; the ≥2-branch case needs an explicit one-level unfold to avoid `cbn` over-
+  unfolding). Coupled corollary `nstep_gstep_sr_choice_head`; non-vacuity `choice3_head_fires_end_to_end` on the
+  agreeing 3-party `g_choice3`. Strictly ADDITIVE (bytes 1-2868 SHA-identical to baseline; sole prior-region
+  edit = `gbget` + the `GStep_Bra` constructor). **Fences:** HEAD choice only (run-ahead = S3c.3-perm); PLAIN
+  `proj` (label-UNION merge = S3, with a **regression pin** — widening `merge` breaks `proj_uninv_selected` and
+  the theorem becomes false-as-stated); coupled corollary is a head wrapper, NOT general SR; PRESERVATION only
+  (NO progress = S3c.4). Naming `_choice_head`, not `n_party_safety`. **Remaining S3c (solo):** S3c.3-perm
+  (run-ahead), S3c.4 n-party progress (research-hard — fence). **Echo-types audit: NOT-RELEVANT** (axis-2 STRUCTURE).
 - **S1.3 DONE — choice / congruence / μ type-layer, axiom-free 2026-06-14.** The last/hardest S1
   sub-rungs, design-panel-validated. **S1.3a (choice):** n-ary LABELLED select/branch (`⊕/&{lᵢ:Sᵢ}`)
   in the fused form; `sty`/`party` gain `SSelect`/`SBranch`/`QSel`/`QBra` over dedicated mutual