diff --git a/.hypatia-ignore b/.hypatia-ignore
index 8c05bc2e..5ce529ee 100644
--- a/.hypatia-ignore
+++ b/.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
diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc
index d3e7abc0..91697f12 100644
--- a/docs/PROOF-NEEDS.adoc
+++ b/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
diff --git a/formal/F3_PragmaDecidable.v b/formal/F3_PragmaDecidable.v
new file mode 100644
index 00000000..0c53e37b
--- /dev/null
+++ b/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.
diff --git a/formal/F4_ErrorFaithful.v b/formal/F4_ErrorFaithful.v
new file mode 100644
index 00000000..6638d8c1
--- /dev/null
+++ b/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.
diff --git a/formal/P2_Progress.v b/formal/P2_Progress.v
new file mode 100644
index 00000000..1ee1c0e1
--- /dev/null
+++ b/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.
diff --git a/formal/P3_BorrowSound.v b/formal/P3_BorrowSound.v
new file mode 100644
index 00000000..cc2e60ab
--- /dev/null
+++ b/formal/P3_BorrowSound.v
@@ -0,0 +1,75 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   P3_BorrowSound.v
+   ════════════════
+   Mechanizes obligation **P-3** (borrow-graph soundness, and the explicit
+   "reject #554" obligation) for a concrete model, discharging the statements
+   from Siblings_Stated.v — axiom-free, no Admitted.
+
+   A minimal single-resource borrow calculus: a program is a sequence of ops on
+   one owned value `a` and one reference `r` borrowed from it. The #554 shape
+   `let r = pick(a); consume(a); *r` is `[OBorrow; OMove; OUseRef]`. The dynamic
+   semantics tracks whether `r` still aliases a LIVE value; the modelled checker
+   is the precise validity analysis (what `lib/borrow.ml` does post-#554-fix —
+   the model abstracts the borrow graph as a single validity bit). We prove the
+   checker is sound and that it REJECTS the #554 witness.
+
+   Scope: this models the *intended* sound checker on a one-resource fragment;
+   the full obligation needs `lib/borrow.ml`'s actual graph + Polonius (#553).
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import List.
+Import ListNotations.
+Require Import ASFormal.Siblings_Stated.
+
+Inductive op := OBorrow | OMove | OUseRef.
+Definition prog := list op.
+
+(* Dynamic semantics: `rvalid` = r currently aliases a live value. OBorrow makes
+   r valid; OMove consumes a and invalidates r; OUseRef on an invalid r is a
+   use-after-move. Returns true iff some OUseRef observes a moved value. *)
+Fixpoint runs_uam (rvalid : bool) (p : prog) : bool :=
+  match p with
+  | []            => false
+  | OBorrow :: p' => runs_uam true p'
+  | OMove   :: p' => runs_uam false p'   (* moving a invalidates the borrow r *)
+  | OUseRef :: p' => if rvalid then runs_uam rvalid p' else true
+  end.
+
+Definition uses_after_move (p : prog) : Prop := runs_uam false p = true.
+
+(* The intended sound checker: accept iff the program never uses a moved value. *)
+Definition borrow_ok (p : prog) : Prop := runs_uam false p = false.
+
+Definition example_554 : prog := [OBorrow; OMove; OUseRef].
+
+(* Soundness: an accepted program never uses-after-move. *)
+Theorem borrow_soundness : forall p, borrow_ok p -> ~ uses_after_move p.
+Proof.
+  unfold borrow_ok, uses_after_move; intros p H Hc; rewrite H in Hc; discriminate.
+Qed.
+
+(* The #554 witness genuinely uses-after-move ... *)
+Theorem example_554_is_uam : uses_after_move example_554.
+Proof. reflexivity. Qed.
+
+(* ... so the sound checker rejects it (the obligation the fixed checker meets). *)
+Theorem rejects_554 : ~ borrow_ok example_554.
+Proof. unfold borrow_ok, example_554; simpl; discriminate. Qed.
+
+(* ── discharge the stated obligations ──────────────────────────────────── *)
+
+Definition P3_soundness_discharged
+  : P3_borrow_soundness prog borrow_ok uses_after_move
+  := borrow_soundness.
+
+Definition P3_rejects_discharged
+  : P3_rejects_554 prog borrow_ok uses_after_move example_554
+  := fun _ => rejects_554.
+
+Print Assumptions P3_soundness_discharged.
+Print Assumptions P3_rejects_discharged.
diff --git a/formal/README.adoc b/formal/README.adoc
index 7f46ab07..473483ce 100644
--- a/formal/README.adoc
+++ b/formal/README.adoc
@@ -41,17 +41,55 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **mechanized**, axiom-free
 
 | `Siblings_Stated.v`
-| **P-2, P-3, F-3, F-4** — progress/preservation, borrow soundness (rejecting
-  #554), pragma determinism, error-vocabulary faithfulness
-| **stated** (parametric propositions; not yet proven)
+| **P-2, P-3, F-3, F-4** — the obligation *statements* (parametric propositions)
+| **stated** — and now discharged for concrete models below
+
+| `P2_Progress.v`
+| **P-2** — progress + preservation (nat/bool/`add`/`if`, small-step)
+| **mechanized**, axiom-free
+
+| `P3_BorrowSound.v`
+| **P-3** — borrow soundness + the #554 witness rejected
+| **mechanized**, axiom-free
+
+| `F3_PragmaDecidable.v`
+| **F-3** — pragma locality + alias-table functionality
+| **mechanized**, axiom-free
+
+| `F4_ErrorFaithful.v`
+| **F-4** — error rendering preserves class + referent
+| **mechanized**, axiom-free
 |===
 
 All mechanized theorems report *Closed under the global context* under `Print
 Assumptions` — no `Admitted`, no axioms — honouring the estate rule that
-load-bearing proofs be constructive and complete. `Siblings_Stated.v` proves
-nothing: it records the obligation shapes as `Definition ... : Prop` over
-section `Variable`s (discharged at `End` into closed, universally-quantified
-props), the Coq analogue of solo-core's statement-only Idris2 skeleton.
+load-bearing proofs be constructive and complete. `Siblings_Stated.v` records
+the obligation shapes as `Definition ... : Prop` over section `Variable`s
+(discharged at `End` into closed, universally-quantified props); the
+`P2_/P3_/F3_/F4_` files give concrete models and prove those propositions hold,
+each ending in a `*_discharged : Siblings_Stated.<name> … := <proof>` line that
+type-checks the concrete proof against the stated obligation.
+
+== Mechanized siblings (P-2, P-3, F-3, F-4)
+
+Each is proven for a deliberately small concrete model — enough to discharge
+the stated obligation and pin its meaning, not the full language:
+
+* **P-2** (`P2_Progress.v`) — a simply-typed first-order calculus
+  (nat/bool/`add`/`if`), small-step, call-by-value, with the standard
+  canonical-forms / progress / preservation development. Functions, binders,
+  products/sums and the QTT quantities are the next increments (codegen
+  preservation *with* `let`/variables is already in `K1Let_…`).
+* **P-3** (`P3_BorrowSound.v`) — a one-resource borrow calculus; proves the
+  precise validity checker is sound and **rejects the #554 witness**
+  (`[OBorrow; OMove; OUseRef]`), matching `lib/borrow.ml`'s post-#554-fix
+  behaviour. Full P-3 needs the real borrow graph + Polonius (#553).
+* **F-3** (`F3_PragmaDecidable.v`) — the alias table is a function, and
+  detection factors through the scanned region, so it cannot depend on bytes
+  past the pragma.
+* **F-4** (`F4_ErrorFaithful.v`) — the face renderer preserves an error's
+  *class* and *referent*, changing only vocabulary, so no face can make error
+  X read as a different error Y.
 
 == K-1 and its growth
 
diff --git a/formal/Siblings_Stated.v b/formal/Siblings_Stated.v
index 1968087a..a1be4d29 100644
--- a/formal/Siblings_Stated.v
+++ b/formal/Siblings_Stated.v
@@ -16,11 +16,13 @@
      * NOTHING is claimed proven — these are signatures, the Coq analogue of
        solo-core's statement-only Idris2 skeleton.
 
-   Each becomes a real theorem once its abstracted pieces are given concrete
-   models: the Solo calculus (P-2), `lib/borrow.ml`'s graph (P-3),
-   `lib/face_pragma.ml` (F-3), `lib/face.ml` (F-4). F-1 is already discharged
-   in F1_TransformerPreservation.v; K-1 in K1_CodegenPreservation.v (and the
-   grown K1Let_CodegenPreservation.v).
+   Each is now DISCHARGED for a concrete model (small fragments, not the full
+   language): P-2 in P2_Progress.v, P-3 in P3_BorrowSound.v, F-3 in
+   F3_PragmaDecidable.v, F-4 in F4_ErrorFaithful.v — each ending in a
+   `*_discharged : <this statement> ... := <proof>` line. F-1 is discharged in
+   F1_TransformerPreservation.v; K-1 in K1_CodegenPreservation.v (and the grown
+   K1Let_CodegenPreservation.v). Growing these models toward the real language
+   (functions/QTT for P-2, the real borrow graph for P-3) is Wave 1.
 
    `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
 *)
diff --git a/formal/_CoqProject b/formal/_CoqProject
index b4c5ba62..0831f7e9 100644
--- a/formal/_CoqProject
+++ b/formal/_CoqProject
@@ -1,5 +1,9 @@
 -Q . ASFormal
 K1_CodegenPreservation.v
 K1Let_CodegenPreservation.v
-F1_TransformerPreservation.v
 Siblings_Stated.v
+F1_TransformerPreservation.v
+F3_PragmaDecidable.v
+F4_ErrorFaithful.v
+P3_BorrowSound.v
+P2_Progress.v
diff --git a/formal/justfile b/formal/justfile
index e20c1776..2112ea26 100644
--- a/formal/justfile
+++ b/formal/justfile
@@ -2,14 +2,16 @@
 # Coq/Rocq proof checks for the AffineScript `formal/` track.
 # (Mustfile/justfile per estate policy — no Makefiles.)
 
-# Type-check every proof in dependency order (F-1 Requires K-1) and assert
-# none depends on an axiom or Admitted.
+# Type-check every proof in dependency order (F-1 Requires K-1; the F-/P-
+# discharge proofs Require Siblings_Stated) and assert none depends on an
+# axiom or Admitted.
 check:
     #!/usr/bin/env bash
     set -euo pipefail
     all=""
-    for f in K1_CodegenPreservation K1Let_CodegenPreservation \
-             F1_TransformerPreservation Siblings_Stated; do
+    for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \
+             F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \
+             P3_BorrowSound P2_Progress; do
       echo "== coqc $f.v =="
       o="$(coqc -Q . ASFormal "$f.v")"
       printf '%s\n' "$o"
@@ -18,7 +20,7 @@ check:
     if printf '%s' "$all" | grep -q "Axioms:"; then
       echo "::error:: a proof depends on an axiom / Admitted"; exit 1
     fi
-    echo "OK: K-1, K1Let, F-1 mechanized (no axioms); P-2/P-3/F-3/F-4 stated."
+    echo "OK: K-1/K1Let/F-1 + P-2/P-3/F-3/F-4 mechanized; no axioms."
 
 # Remove Coq build artifacts.
 clean: