feat(formal): mechanize the four Wave-0 siblings (P-2, P-3, F-3, F-4) (#626)

## What

Turns the four **stated** Wave-0 siblings in `Siblings_Stated.v` into
**mechanized proofs**. Each new file builds a concrete model, proves the
property, and ends in a `*_discharged : Siblings_Stated.<name> … :=
<proof>` line that type-checks the concrete proof *against the stated
obligation*. All Coq/Rocq 8.18, **axiom-free** (`Print Assumptions` →
*"Closed under the global context"*), no `Admitted`.

| File | Obligation | Proven |
|---|---|---|
| `P2_Progress.v` | **P-2** | progress + preservation for a simply-typed
first-order calculus (nat/bool/`add`/`if`), small-step CBV, with
canonical forms |
| `P3_BorrowSound.v` | **P-3** | a one-resource borrow checker is sound
**and rejects the #554 witness** `[OBorrow; OMove; OUseRef]` |
| `F3_PragmaDecidable.v` | **F-3** | the alias table is a function;
detection factors through the scanned region (independent of bytes past
the pragma) |
| `F4_ErrorFaithful.v` | **F-4** | the face renderer preserves an
error's **class + referent**, changing only vocabulary |

`P3_BorrowSound.v` matches `lib/borrow.ml`'s **post-#554-fix** behaviour
(per the new `SOUNDNESS.adoc`): the sound checker is exactly the one
that now rejects use-after-move through a callee-returned borrow.

## Scope (honest)
These are small fragments — enough to **discharge the obligation and pin
its meaning**, not the full language. Growing them is Wave 1:
functions/binders/QTT for P-2, the real borrow graph + Polonius (#553)
for P-3.

## Wiring & docs
- `justfile check` + `_CoqProject` compile **all eight** files in
dependency order and assert no axioms — **11 closure reports**.
- `.hypatia-ignore` extends the Coq-`.v`-isn't-V-lang carve-out to the
four new files.
- `PROOF-NEEDS.adoc`: P-2/P-3/F-3/F-4 → `partial` (mechanized model);
Wave-0 row marked **done**. `README.adoc` + the `Siblings_Stated` header
point at the discharge files.

## Check
```sh
just -f formal/justfile check
```
Verified locally: 8 files, 11 closure reports, **zero axioms**.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

---
_Generated by [Claude
Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_

Co-authored-by: hyperpolymath <paraordinate@yahoo.co.uk>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: 3 people

.hypatia-ignore

@@ -51,3 +51,11 @@ cicd_rules/vlang_detected:formal/F1_TransformerPreservation.v
 cicd_rules/banned_language_file:formal/F1_TransformerPreservation.v
 cicd_rules/vlang_detected:formal/Siblings_Stated.v
 cicd_rules/banned_language_file:formal/Siblings_Stated.v
+cicd_rules/vlang_detected:formal/F3_PragmaDecidable.v
+cicd_rules/banned_language_file:formal/F3_PragmaDecidable.v
+cicd_rules/vlang_detected:formal/F4_ErrorFaithful.v
+cicd_rules/banned_language_file:formal/F4_ErrorFaithful.v
+cicd_rules/vlang_detected:formal/P3_BorrowSound.v
+cicd_rules/banned_language_file:formal/P3_BorrowSound.v
+cicd_rules/vlang_detected:formal/P2_Progress.v
+cicd_rules/banned_language_file:formal/P2_Progress.v

docs/PROOF-NEEDS.adoc

@@ -71,8 +71,9 @@ than the prose corpus suggests:
   **exists** (Coq/Rocq 8.18), axiom-free throughout: `K1_CodegenPreservation.v`
   (K-1, minimal fragment) + `K1Let_CodegenPreservation.v` (K-1 grown with
   variables/`let`/environment) + `F1_TransformerPreservation.v` (F-1, composing
-  on K-1) are mechanized; `Siblings_Stated.v` states P-2/P-3/F-3/F-4 as
-  parametric propositions (see <<outstanding>>, <<faces>>).
+  on K-1) are mechanized; `Siblings_Stated.v` states P-2/P-3/F-3/F-4, now
+  **discharged for concrete models** in `P2_Progress.v` / `P3_BorrowSound.v` /
+  `F3_PragmaDecidable.v` / `F4_ErrorFaithful.v` (see <<outstanding>>, <<faces>>).
 * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/`
   (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`,
   `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue,
@@ -122,14 +123,18 @@ obligations. They are the "we might have missed" half of the brief.
 | **Solo progress + preservation.** Discharge the two holes in `Soundness.idr`:
   give `Step` its constructors and prove
   `progress`/`preservation`/`affinePreservation`.
-| XL | `stated`
-| #513 must-have 1; solo-core Track F1 wks 3–12
+| XL | `partial`
+| #513 must-have 1; solo-core (Idris2) `stated`; **small-step progress +
+  preservation mechanized** for a first-order nat/bool/`add`/`if` fragment in
+  `formal/P2_Progress.v`
 
 | P-3
 | **Borrow-graph soundness.** A well-typed program never observes a moved/aliased
   value. Must *exclude* the #554 counterexample (callee-returned borrow).
-| XL | `prose`
-| #513 must-have 2; counterexample #554; #553
+| XL | `partial`
+| #513 must-have 2; **mechanized** for a one-resource model in
+  `formal/P3_BorrowSound.v` (sound checker rejects the #554 witness); #554 fixed
+  (SOUNDNESS.adoc), Polonius #553
 
 | P-4
 | **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly
@@ -252,8 +257,9 @@ cover them.
   jaffa→Js, pseudo→Pseudocode, lucid→Lucid, cafe→Cafe, +brand names) is a
   *function* (no name maps to two faces); and dispatch `--face` > pragma >
   extension is confluent (same source ⇒ same face). Face analogue of P-7.
-| M | `stated`
-| Coq statement: `formal/Siblings_Stated.v` (F3); `lib/face_pragma.ml`
+| M | `partial`
+| **mechanized** for a model: `formal/F3_PragmaDecidable.v` (discharges the
+  Siblings_Stated F3 statements); `lib/face_pragma.ml`
 
 | F-4
 | **Error-vocabulary faithfulness (simulation).** Each `Face.format_*_for_face`
@@ -262,8 +268,9 @@ cover them.
   is a total simulation of the canonical error algebra (exhaustiveness is
   OCaml-checked; *semantic* faithfulness is not), so a face can never make error
   *X* read as a different error *Y*.
-| M | `stated`
-| Coq statement: `formal/Siblings_Stated.v` (F4); `lib/face.ml`
+| M | `partial`
+| **mechanized** for a model: `formal/F4_ErrorFaithful.v` (discharges the
+  Siblings_Stated F4 statement); `lib/face.ml`
 
 | F-5
 | **`render_ty` faithfulness / non-collision.** The per-face type renaming
@@ -327,10 +334,13 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | Wave | Items | Gates
 
 | 0
-| *Substantially done.* `formal/` stood up (Coq); **K-1 mechanized** + **grown**
-  (variables/`let`); **F-1 mechanized** (composes on K-1); **P-2/P-3/F-3/F-4
-  stated** as Coq signatures. All axiom-free. NEXT: grow K-1 with `if`;
-  discharge a stated sibling; cross-link `CAPABILITY-MATRIX.adoc` rows (K-4).
+| **Done.** `formal/` stood up (Coq); **K-1 mechanized** + **grown**
+  (variables/`let`); **F-1 mechanized** (composes on K-1); and **P-2/P-3/F-3/F-4
+  mechanized** for concrete models (small-step progress+preservation; borrow
+  soundness rejecting #554; pragma locality + alias functionality; error
+  faithfulness). 11 closure reports, all axiom-free. NEXT (Wave 1): grow each
+  model toward the real language — `if`/functions/QTT in P-2, the real borrow
+  graph in P-3 — and cross-link `CAPABILITY-MATRIX.adoc` rows (K-4).
 | —
 
 | 1

formal/F3_PragmaDecidable.v

@@ -0,0 +1,76 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   F3_PragmaDecidable.v
+   ════════════════════
+   Mechanizes obligation **F-3** (face pragma detection) for a concrete model,
+   discharging both statements from Siblings_Stated.v — axiom-free, no Admitted.
+
+   Models `lib/face_pragma.ml`: the alias table `parse_face_name` and the fact
+   that `detect_in_source` reads only a bounded leading *region* and stops at
+   the first code token, so its result is independent of bytes past the pragma.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import ASFormal.Siblings_Stated.
+
+(* The six established faces. *)
+Inductive face := FCanonical | FPython | FJs | FPseudo | FLucid | FCafe.
+
+(* ── F3_alias_functional: the alias table is a function ─────────────────── *)
+
+(* Recognised pragma tokens (a representative slice of parse_face_name's
+   accepted names + brand aliases). *)
+Inductive pname :=
+  | NCanonical | NPython | NRattle | NJs | NJaffa
+  | NPseudo | NLucid | NCafe | NUnknown.
+
+Definition resolve_name (n : pname) : option face :=
+  match n with
+  | NCanonical        => Some FCanonical
+  | NPython | NRattle => Some FPython        (* python / rattle / rattlescript *)
+  | NJs | NJaffa      => Some FJs            (* js / javascript / jaffa(script) *)
+  | NPseudo           => Some FPseudo
+  | NLucid            => Some FLucid
+  | NCafe             => Some FCafe
+  | NUnknown          => None
+  end.
+
+Theorem alias_functional :
+  forall n f1 f2, resolve_name n = Some f1 -> resolve_name n = Some f2 -> f1 = f2.
+Proof. intros n f1 f2 H1 H2; rewrite H1 in H2; injection H2; auto. Qed.
+
+(* ── F3_pragma_local: detection ignores bytes past the scanned region ───── *)
+
+(* A source = the pragma in its scanned leading window + arbitrary trailing
+   bytes. `pragma_region` keeps the window and discards the trailing bytes;
+   `detect` consults only the window. So detection cannot depend on anything
+   past the pragma — the precise content of F-3. *)
+Record src := mkSrc { window : option pname; trailing : nat }.
+
+Definition pragma_region (s : src) : src := mkSrc (window s) 0.
+
+Definition detect (s : src) : option face :=
+  match window (pragma_region s) with
+  | Some n => resolve_name n
+  | None   => None
+  end.
+
+Theorem pragma_local :
+  forall s1 s2, pragma_region s1 = pragma_region s2 -> detect s1 = detect s2.
+Proof. intros s1 s2 H; unfold detect; rewrite H; reflexivity. Qed.
+
+(* ── discharge the stated obligations ──────────────────────────────────── *)
+
+Definition F3_alias_discharged
+  : F3_alias_functional face pname resolve_name
+  := alias_functional.
+
+Definition F3_local_discharged
+  : F3_pragma_local src face detect pragma_region
+  := pragma_local.
+
+Print Assumptions F3_alias_discharged.
+Print Assumptions F3_local_discharged.

formal/F4_ErrorFaithful.v

@@ -0,0 +1,63 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   F4_ErrorFaithful.v
+   ══════════════════
+   Mechanizes obligation **F-4** (error-vocabulary faithfulness) for a concrete
+   model, discharging the statement from Siblings_Stated.v — axiom-free.
+
+   Models `lib/face.ml`'s `format_*_for_face`: a face changes only the *words*
+   of an error message; it must preserve the canonical error's *class* (which
+   error) and *referent* (the offending identifier/site). The model makes
+   `render` carry class + referent through unchanged while choosing
+   face-specific vocabulary, and proves the rendering preserves both — so a
+   face can never make error X read as a different error Y.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import ASFormal.Siblings_Stated.
+
+Inductive face := FCanonical | FPython | FJs | FPseudo | FLucid | FCafe.
+
+(* A canonical error: which error (class) and what it is about (referent). *)
+Record canon_error := mkErr { ce_class : nat; ce_referent : nat }.
+
+(* A rendered message: the preserved class + referent, plus face-chosen words. *)
+Record rendered := mkRendered { r_class : nat; r_referent : nat; r_vocab : nat }.
+
+(* Face-specific vocabulary for a given error class (the part that legitimately
+   varies between faces — e.g. "single-use" vs "linear" vs "one-shot"). *)
+Definition face_vocab (f : face) (cls : nat) : nat :=
+  match f with
+  | FCanonical => cls
+  | FPython    => cls + 1
+  | FJs        => cls + 2
+  | FPseudo    => cls + 3
+  | FLucid     => cls + 4
+  | FCafe      => cls + 5
+  end.
+
+(* The face renderer: vocabulary may change; class and referent are carried
+   through verbatim. *)
+Definition render (f : face) (e : canon_error) : rendered :=
+  mkRendered (ce_class e) (ce_referent e) (face_vocab f (ce_class e)).
+
+Definition rendered_class    (r : rendered) : nat := r_class r.
+Definition rendered_referent (r : rendered) : nat := r_referent r.
+
+Theorem error_faithful :
+  forall f e,
+    rendered_class    (render f e) = ce_class e /\
+    rendered_referent (render f e) = ce_referent e.
+Proof. intros f e; split; reflexivity. Qed.
+
+(* ── discharge the stated obligation ───────────────────────────────────── *)
+
+Definition F4_faithful_discharged
+  : F4_error_faithful canon_error face rendered render
+      ce_class ce_referent rendered_class rendered_referent
+  := error_faithful.
+
+Print Assumptions F4_faithful_discharged.

formal/P2_Progress.v

@@ -0,0 +1,109 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   P2_Progress.v
+   ═════════════
+   Mechanizes obligation **P-2** (progress + preservation) for a minimal typed
+   calculus, discharging both statements from Siblings_Stated.v — axiom-free,
+   no Admitted.
+
+   Calculus: types Nat | Bool; terms numbers, booleans, `add`, and `if` (a real
+   elimination form, so progress is non-trivial — a `tif` on a non-boolean is
+   ruled out only by typing). Small-step, call-by-value. This is the classic
+   "arith + bool" type-soundness core.
+
+   Scope (honest): this is the *simply-typed, first-order* core of the Solo
+   fragment. Functions/`let`/binders (substitution or environments), products,
+   sums, and the QTT/affine quantities are the next increments — solo-core's
+   Duet/Ensemble direction. (Codegen preservation WITH `let`/variables is
+   already mechanized in K1Let_CodegenPreservation.v.)
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import ASFormal.Siblings_Stated.
+
+Inductive ty := TNat | TBool.
+
+Inductive tm :=
+| tnum  (n : nat)
+| tbool (b : bool)
+| tadd  (a b : tm)
+| tif   (c t e : tm).
+
+Inductive value : tm -> Prop :=
+| v_num  : forall n, value (tnum n)
+| v_bool : forall b, value (tbool b).
+
+Inductive has_type : tm -> ty -> Prop :=
+| T_Num  : forall n, has_type (tnum n) TNat
+| T_Bool : forall b, has_type (tbool b) TBool
+| T_Add  : forall a b, has_type a TNat -> has_type b TNat -> has_type (tadd a b) TNat
+| T_If   : forall c t e T,
+    has_type c TBool -> has_type t T -> has_type e T -> has_type (tif c t e) T.
+
+Inductive step : tm -> tm -> Prop :=
+| S_Add1 : forall a a' b, step a a' -> step (tadd a b) (tadd a' b)
+| S_Add2 : forall a b b', value a -> step b b' -> step (tadd a b) (tadd a b')
+| S_AddNum : forall m n, step (tadd (tnum m) (tnum n)) (tnum (m + n))
+| S_If : forall c c' t e, step c c' -> step (tif c t e) (tif c' t e)
+| S_IfTrue  : forall t e, step (tif (tbool true) t e) t
+| S_IfFalse : forall t e, step (tif (tbool false) t e) e.
+
+(* ── canonical forms ───────────────────────────────────────────────────── *)
+
+Lemma canon_nat : forall v, value v -> has_type v TNat -> exists n, v = tnum n.
+Proof. intros v Hv HT; inversion Hv; subst; inversion HT; subst; eauto. Qed.
+
+Lemma canon_bool : forall v, value v -> has_type v TBool -> exists b, v = tbool b.
+Proof. intros v Hv HT; inversion Hv; subst; inversion HT; subst; eauto. Qed.
+
+(* ── progress ──────────────────────────────────────────────────────────── *)
+
+Theorem progress : forall t T, has_type t T -> value t \/ (exists t', step t t').
+Proof.
+  intros t T HT; induction HT.
+  - left; constructor.
+  - left; constructor.
+  - (* tadd a b *)
+    right; destruct IHHT1 as [Hva | [a' Ha]].
+    + destruct (canon_nat a Hva HT1) as [m ->].
+      destruct IHHT2 as [Hvb | [b' Hb]].
+      * destruct (canon_nat b Hvb HT2) as [n ->]; eauto using S_AddNum.
+      * eauto using S_Add2, v_num.
+    + eauto using S_Add1.
+  - (* tif c t e *)
+    right; destruct IHHT1 as [Hvc | [c' Hc]].
+    + destruct (canon_bool c Hvc HT1) as [[] ->]; eauto using S_IfTrue, S_IfFalse.
+    + eauto using S_If.
+Qed.
+
+(* ── preservation ──────────────────────────────────────────────────────── *)
+
+Theorem preservation : forall t t' T, has_type t T -> step t t' -> has_type t' T.
+Proof.
+  intros t t' T HT Hstep; revert T HT.
+  induction Hstep; intros T HT; inversion HT; subst.
+  - apply T_Add; auto.
+  - apply T_Add; auto.
+  - constructor.
+  - apply T_If; auto.
+  - assumption.
+  - assumption.
+Qed.
+
+(* ── discharge the stated obligations (ctx instantiated to unit) ────────── *)
+
+Definition P2_progress_discharged
+  : P2_progress tm ty unit tt (fun (_ : unit) (t : tm) (T : ty) => has_type t T)
+                value step
+  := progress.
+
+Definition P2_preservation_discharged
+  : P2_preservation tm ty unit (fun (_ : unit) (t : tm) (T : ty) => has_type t T)
+                    step
+  := fun (_ : unit) t t' T HT Hs => preservation t t' T HT Hs.
+
+Print Assumptions P2_progress_discharged.
+Print Assumptions P2_preservation_discharged.