diff --git a/.hypatia-ignore b/.hypatia-ignore
index 7547adef..8c05bc2e 100644
--- a/.hypatia-ignore
+++ b/.hypatia-ignore
@@ -45,3 +45,9 @@ cicd_rules/banned_language_file:tools/res-to-affine/test/fixtures/phase3c.res
 # an inert no-op under the scanner's `grep -qxF` whole-line match.
 cicd_rules/vlang_detected:formal/K1_CodegenPreservation.v
 cicd_rules/banned_language_file:formal/K1_CodegenPreservation.v
+cicd_rules/vlang_detected:formal/K1Let_CodegenPreservation.v
+cicd_rules/banned_language_file:formal/K1Let_CodegenPreservation.v
+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
diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc
index 3682bed4..d68816d6 100644
--- a/docs/PROOF-NEEDS.adoc
+++ b/docs/PROOF-NEEDS.adoc
@@ -68,9 +68,11 @@ than the prose corpus suggests:
   `TypeSafety.v` is example lemmas about list length, not AffineScript. Not
   core-metatheory.
 * **`formal/`** — the directory #513 names as the mechanized-proof target now
-  **exists** (Coq/Rocq 8.18). It holds the Wave-0 **K-1 seed**
-  (`formal/K1_CodegenPreservation.v`) — a complete, axiom-free
-  codegen-preservation proof for a minimal nat/bool fragment (see <<outstanding>>).
+  **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>>).
 * **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,
@@ -222,8 +224,8 @@ cover them.
   well-typed face-`F` programs `p`. This is the *front-end* analogue of the
   backend keystone K-1; together they give end-to-end "same cube". Needs the
   AffineScript AST + wasm semantics formalised.
-| XL | `absent`
-| new
+| XL | `partial`
+| mechanized fragment: `formal/F1_TransformerPreservation.v` (composes on K-1)
 
 | F-2
 | **Same-cube cross-face agreement (observational).** Any two faces compiling
@@ -242,8 +244,8 @@ 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 | `absent`
-| new; `lib/face_pragma.ml`
+| M | `stated`
+| Coq statement: `formal/Siblings_Stated.v` (F3); `lib/face_pragma.ml`
 
 | F-4
 | **Error-vocabulary faithfulness (simulation).** Each `Face.format_*_for_face`
@@ -252,8 +254,8 @@ 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 | `absent`
-| new; `lib/face.ml`
+| M | `stated`
+| Coq statement: `formal/Siblings_Stated.v` (F4); `lib/face.ml`
 
 | F-5
 | **`render_ty` faithfulness / non-collision.** The per-face type renaming
@@ -317,10 +319,10 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | Wave | Items | Gates
 
 | 0
-| *In progress.* DONE: `formal/` stood up (Coq/Rocq); **K-1 seed mechanized**
-  (`K1_CodegenPreservation.v`, axiom-free). NEXT: *state* P-2, P-3 (rejecting
-  #554), F-1, F-3, F-4 as signatures, mirroring solo-core; cross-link
-  `CAPABILITY-MATRIX.adoc` rows (K-4).
+| *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).
 | —
 
 | 1
diff --git a/formal/F1_TransformerPreservation.v b/formal/F1_TransformerPreservation.v
new file mode 100644
index 00000000..d235542b
--- /dev/null
+++ b/formal/F1_TransformerPreservation.v
@@ -0,0 +1,129 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   F1_TransformerPreservation.v
+   ════════════════════════════
+   Wave-0 seed of obligation **F-1** from docs/PROOF-NEEDS.adoc: the *real*
+   same-cube theorem — each face's surface→canonical transform `T_F` preserves
+   the typed-WASM denotation. F-1 is the front-end twin of K-1; this file
+   *composes on top of* K-1 (it `Require`s it) exactly as the inventory says.
+
+   A "face" is an alternate surface syntax (rattle/jaffa/pseudo/lucid/cafe/…)
+   whose parser yields a surface AST `fexp`; `elaborate : fexp -> sexp` is the
+   transform `T_F` into the canonical AST that K-1's `compile` consumes. We give
+   the face its OWN big-step semantics `feval` (what a reader of that surface
+   expects) and prove the transform preserves it — then chain K-1 to get
+   end-to-end codegen preservation, and state the cross-face "same cube".
+
+   Like K-1, everything here is complete and axiom-free (no `Admitted`).
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+
+   Check:  coqc -Q . ASFormal F1_TransformerPreservation.v   (after K-1)
+*)
+
+Require Import List.
+Import ListNotations.
+Require Import ASFormal.K1_CodegenPreservation.
+
+(* ═══════════ A face surface: canonical forms + parser sugar ═══════════════ *)
+
+(* `FSum3`/`FAll3` are surface sugar a face parser may emit (n-ary fold spelt
+   as one node) — they stand in for any derived surface form that elaborates
+   to a tree of canonical operations. *)
+Inductive fexp : Type :=
+| FNat  (n : nat)
+| FBool (b : bool)
+| FAdd  (a b : fexp)
+| FAnd  (a b : fexp)
+| FSum3 (a b c : fexp)    (* sugar for  a + (b + c)  *)
+| FAll3 (a b c : fexp).   (* sugar for  a && (b && c) *)
+
+(* The transform T_F : surface AST -> canonical AST (`sexp` from K-1). *)
+Fixpoint elaborate (f : fexp) : sexp :=
+  match f with
+  | FNat n     => SNat n
+  | FBool b    => SBool b
+  | FAdd a b   => SAdd (elaborate a) (elaborate b)
+  | FAnd a b   => SAnd (elaborate a) (elaborate b)
+  | FSum3 a b c => SAdd (elaborate a) (SAdd (elaborate b) (elaborate c))
+  | FAll3 a b c => SAnd (elaborate a) (SAnd (elaborate b) (elaborate c))
+  end.
+
+(* The face's own big-step semantics — what a reader of this surface expects,
+   defined directly (not via elaboration), so that agreement is a theorem. *)
+Fixpoint feval (f : fexp) : option sval :=
+  match f with
+  | FNat n  => Some (VNat n)
+  | FBool b => Some (VBool b)
+  | FAdd a b =>
+      match feval a, feval b with
+      | Some (VNat x), Some (VNat y) => Some (VNat (x + y))
+      | _, _ => None
+      end
+  | FAnd a b =>
+      match feval a, feval b with
+      | Some (VBool x), Some (VBool y) => Some (VBool (andb x y))
+      | _, _ => None
+      end
+  | FSum3 a b c =>
+      match feval a, feval b, feval c with
+      | Some (VNat x), Some (VNat y), Some (VNat z) => Some (VNat (x + (y + z)))
+      | _, _, _ => None
+      end
+  | FAll3 a b c =>
+      match feval a, feval b, feval c with
+      | Some (VBool x), Some (VBool y), Some (VBool z) => Some (VBool (andb x (andb y z)))
+      | _, _, _ => None
+      end
+  end.
+
+(* ════════════ F-1: the transform preserves meaning ═══════════════════════ *)
+
+(* Transform semantics-preservation: the face's own semantics agrees, on the
+   nose, with elaborating-then-evaluating canonically. *)
+Theorem f1_transform_preserves_eval : forall f, feval f = seval (elaborate f).
+Proof.
+  induction f as [ n | b | a IHa b IHb | a IHa b IHb
+                 | a IHa b IHb c IHc | a IHa b IHb c IHc ]; simpl.
+  - reflexivity.
+  - reflexivity.
+  - rewrite IHa, IHb; reflexivity.
+  - rewrite IHa, IHb; reflexivity.
+  - (* FSum3: flat 3-way match vs nested — destruct to align *)
+    rewrite IHa, IHb, IHc;
+    destruct (seval (elaborate a)) as [[x | ] | ];
+    destruct (seval (elaborate b)) as [[y | ] | ];
+    destruct (seval (elaborate c)) as [[z | ] | ]; reflexivity.
+  - rewrite IHa, IHb, IHc;
+    destruct (seval (elaborate a)) as [[ | x] | ];
+    destruct (seval (elaborate b)) as [[ | y] | ];
+    destruct (seval (elaborate c)) as [[ | z] | ]; reflexivity.
+Qed.
+
+(* End-to-end (the F-1 "same cube" at the value level): compiling the
+   elaborated face program agrees with the face's own semantics — obtained by
+   chaining the transform lemma with K-1's backend theorem. *)
+Theorem f1_codegen_preservation : forall f v,
+  feval f = Some v ->
+  wexec (compile (elaborate f)) [] = Some [obs v].
+Proof.
+  intros f v Hf.
+  apply k1_preservation_holds.
+  rewrite <- f1_transform_preserves_eval.
+  exact Hf.
+Qed.
+
+(* Cross-face same-cube: two faces whose transforms land on the same canonical
+   AST emit byte-identical code (hence the same wasm). The observational
+   version for the trailing-statement/tail split is mechanized separately in
+   invariant-path/proofs/SameCube.agda (F-2). *)
+Corollary f1_same_cube : forall f1 f2,
+  elaborate f1 = elaborate f2 ->
+  compile (elaborate f1) = compile (elaborate f2).
+Proof.
+  intros f1 f2 H; rewrite H; reflexivity.
+Qed.
+
+Print Assumptions f1_transform_preserves_eval.
+Print Assumptions f1_codegen_preservation.
diff --git a/formal/K1Let_CodegenPreservation.v b/formal/K1Let_CodegenPreservation.v
new file mode 100644
index 00000000..34849dd2
--- /dev/null
+++ b/formal/K1Let_CodegenPreservation.v
@@ -0,0 +1,179 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   K1Let_CodegenPreservation.v
+   ═══════════════════════════
+   K-1, GROWN. Extends the minimal K1_CodegenPreservation fragment with the
+   first real binder: de Bruijn **variables** and **`let`**, evaluated under an
+   environment. The target machine gains a **locals** register alongside the
+   operand stack; compilation balances `IBind`/`IUnbind` so locals scope
+   correctly. The codegen-preservation theorem is re-proven for this richer
+   fragment — still complete and axiom-free (no `Admitted`).
+
+   This is a step of the K-1 obligation toward the real AST (binders →
+   environments). `if`/control-flow is the next increment (it needs structured
+   target control + a termination measure, deliberately out of this step).
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+   Check:  coqc -Q . ASFormal K1Let_CodegenPreservation.v
+*)
+
+Require Import List.
+Import ListNotations.
+
+(* ════════════════════════ Source (env-based, with let) ═══════════════════ *)
+
+Inductive sval : Type := VNat (n : nat) | VBool (b : bool).
+
+Inductive sexp : Type :=
+| SNat (n : nat)
+| SBool (b : bool)
+| SVar (i : nat)             (* de Bruijn index into the environment *)
+| SAdd (a b : sexp)
+| SAnd (a b : sexp)
+| SLet (e1 e2 : sexp).       (* let x = e1 in e2 ; x is index 0 in e2 *)
+
+Definition senv := list sval.
+
+Fixpoint seval (env : senv) (e : sexp) : option sval :=
+  match e with
+  | SNat n  => Some (VNat n)
+  | SBool b => Some (VBool b)
+  | SVar i  => nth_error env i
+  | SAdd a b =>
+      match seval env a, seval env b with
+      | Some (VNat x), Some (VNat y) => Some (VNat (x + y))
+      | _, _ => None
+      end
+  | SAnd a b =>
+      match seval env a, seval env b with
+      | Some (VBool x), Some (VBool y) => Some (VBool (andb x y))
+      | _, _ => None
+      end
+  | SLet e1 e2 =>
+      match seval env e1 with
+      | Some v => seval (v :: env) e2
+      | None   => None
+      end
+  end.
+
+(* ═══════════════ Target: stack machine + a locals register ════════════════ *)
+
+Inductive wval : Type := WNat (n : nat) | WBool (b : bool).
+
+Definition obs (v : sval) : wval :=
+  match v with VNat n => WNat n | VBool b => WBool b end.
+
+Inductive instr : Type :=
+| IPushN (n : nat)
+| IPushB (b : bool)
+| IGet   (i : nat)   (* push locals[i] onto the stack *)
+| IAdd
+| IAnd
+| IBind              (* pop stack top, push it onto locals (new index 0) *)
+| IUnbind.           (* drop locals[0]; operand stack unchanged *)
+
+Definition code   := list instr.
+Definition locals := list wval.
+Definition stack  := list wval.
+
+Definition wstep (i : instr) (l : locals) (s : stack) : option (locals * stack) :=
+  match i, l, s with
+  | IPushN n, l, s                   => Some (l, WNat n :: s)
+  | IPushB b, l, s                   => Some (l, WBool b :: s)
+  | IGet k, l, s                     =>
+      match nth_error l k with
+      | Some w => Some (l, w :: s)
+      | None   => None
+      end
+  | IAdd, l, WNat b :: WNat a :: s'  => Some (l, WNat (a + b) :: s')
+  | IAnd, l, WBool b :: WBool a :: s' => Some (l, WBool (andb a b) :: s')
+  | IBind, l, w :: s'                => Some (w :: l, s')
+  | IUnbind, _ :: l', s              => Some (l', s)
+  | _, _, _                          => None
+  end.
+
+Fixpoint wexec (c : code) (l : locals) (s : stack) : option (locals * stack) :=
+  match c with
+  | []        => Some (l, s)
+  | i :: rest =>
+      match wstep i l s with
+      | Some (l', s') => wexec rest l' s'
+      | None          => None
+      end
+  end.
+
+Fixpoint compile (e : sexp) : code :=
+  match e with
+  | SNat n     => [IPushN n]
+  | SBool b    => [IPushB b]
+  | SVar i     => [IGet i]
+  | SAdd a b   => compile a ++ compile b ++ [IAdd]
+  | SAnd a b   => compile a ++ compile b ++ [IAnd]
+  | SLet e1 e2 => compile e1 ++ [IBind] ++ compile e2 ++ [IUnbind]
+  end.
+
+(* ═════════════════════════ preservation (no Admitted) ════════════════════ *)
+
+(* Execution distributes over code concatenation — the workhorse that lets the
+   `let` case step its `IBind`/`IUnbind` cleanly without continuation juggling. *)
+Lemma wexec_app : forall c1 c2 l s,
+  wexec (c1 ++ c2) l s =
+  match wexec c1 l s with
+  | Some (l', s') => wexec c2 l' s'
+  | None          => None
+  end.
+Proof.
+  induction c1 as [| i c1 IH]; intros c2 l s; simpl.
+  - reflexivity.
+  - destruct (wstep i l s) as [[l' s'] |]; [apply IH | reflexivity].
+Qed.
+
+(* Codegen preservation, generalized over the operand stack `s` and carrying
+   the environment/locals correspondence `l = map obs env`. `IUnbind` restores
+   locals, so the machine returns to the same `l` it started with. *)
+Lemma compile_correct : forall e env v l s,
+  seval env e = Some v ->
+  l = map obs env ->
+  wexec (compile e) l s = Some (l, obs v :: s).
+Proof.
+  induction e as [n | b | i | a IHa b IHb | a IHa b IHb | e1 IH1 e2 IH2];
+    intros env v l s Hev Hl; simpl in Hev; subst l.
+  - (* SNat *)  inversion Hev; subst; reflexivity.
+  - (* SBool *) inversion Hev; subst; reflexivity.
+  - (* SVar *)
+    apply (map_nth_error obs) in Hev; simpl; rewrite Hev; reflexivity.
+  - (* SAdd *)
+    destruct (seval env a) as [[x | xb] |] eqn:Ha; try discriminate;
+    destruct (seval env b) as [[y | yb] |] eqn:Hb; try discriminate;
+    inversion Hev; subst; clear Hev; simpl compile;
+    rewrite wexec_app, (IHa env (VNat x) (map obs env) s Ha eq_refl); simpl;
+    rewrite wexec_app, (IHb env (VNat y) (map obs env) (WNat x :: s) Hb eq_refl); simpl;
+    reflexivity.
+  - (* SAnd *)
+    destruct (seval env a) as [[xn | x] |] eqn:Ha; try discriminate;
+    destruct (seval env b) as [[yn | y] |] eqn:Hb; try discriminate;
+    inversion Hev; subst; clear Hev; simpl compile;
+    rewrite wexec_app, (IHa env (VBool x) (map obs env) s Ha eq_refl); simpl;
+    rewrite wexec_app, (IHb env (VBool y) (map obs env) (WBool x :: s) Hb eq_refl); simpl;
+    reflexivity.
+  - (* SLet *)
+    destruct (seval env e1) as [v1 |] eqn:H1; try discriminate; simpl in Hev;
+    simpl compile;
+    rewrite wexec_app, (IH1 env v1 (map obs env) s H1 eq_refl); simpl;
+    rewrite wexec_app, (IH2 (v1 :: env) v (obs v1 :: map obs env) s Hev eq_refl); simpl;
+    reflexivity.
+Qed.
+
+(* For a closed program (empty env) the locals balance back to empty and the
+   result is the single wasm value on the operand stack. *)
+Theorem k1let_preservation_holds : forall e v,
+  seval [] e = Some v ->
+  wexec (compile e) [] [] = Some ([], [obs v]).
+Proof.
+  intros e v H.
+  exact (compile_correct e [] v [] [] H eq_refl).
+Qed.
+
+Print Assumptions k1let_preservation_holds.
diff --git a/formal/README.adoc b/formal/README.adoc
index a04c2736..7f46ab07 100644
--- a/formal/README.adoc
+++ b/formal/README.adoc
@@ -8,8 +8,8 @@ Jonathan D.A. Jewell
 This directory is the machine-checked home for the proof obligations
 catalogued in `docs/PROOF-NEEDS.adoc`, and is the `formal/` target directory
 issue #513 names for mechanized proofs. Prover: **Coq/Rocq 8.18** — chosen for
-K-1 because the typed-WASM target semantics interoperate with `typed-wasm` and
-ephapax, both of which use Coq (`Semantics.v`).
+the codegen/K-1 track because the typed-WASM target semantics interoperate with
+`typed-wasm` and ephapax, both of which use Coq (`Semantics.v`).
 
 [IMPORTANT]
 .`.v` here is Coq, not V-lang
@@ -29,54 +29,79 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | File | Obligation | Status
 
 | `K1_CodegenPreservation.v`
-| **K-1** — codegen → typed-WASM semantic-preservation
-| **mechanized** for a minimal fragment (no `Admitted`, no axioms). The full
-  obligation remains open — see <<scope>>.
+| **K-1** — codegen → typed-WASM preservation (minimal fragment)
+| **mechanized**, axiom-free
+
+| `K1Let_CodegenPreservation.v`
+| **K-1, grown** — adds variables, `let`, and an environment
+| **mechanized**, axiom-free
+
+| `F1_TransformerPreservation.v`
+| **F-1** — face transformer semantics-preservation (composes on K-1)
+| **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)
 |===
 
-== What `K1_CodegenPreservation.v` proves
+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.
+
+== K-1 and its growth
 
-A complete, axiom-free compiler-correctness theorem for a minimal two-type
-AffineScript fragment (nat + bool, with `add` and `and`) compiled to a small
-stack machine that stands in for typed-WASM:
+`K1_CodegenPreservation.v` proves, for a minimal two-type fragment (nat + bool,
+`add` + `and`) compiled to a small stack machine:
 
 [source,coq]
 ----
 Definition K1_preservation : Prop :=
   forall e v, seval e = Some v -> wexec (compile e) [] = Some [obs v].
-
-Theorem k1_preservation_holds : K1_preservation.   (* proven *)
+Theorem k1_preservation_holds : K1_preservation.        (* proven *)
 ----
 
-i.e. whenever the source big-step evaluates to a value `v`, the compiled code
-run on the empty operand stack yields exactly the corresponding wasm value
-`[obs v]`. `Print Assumptions k1_preservation_holds` reports *Closed under the
-global context* — the proof rests on no axioms, honouring the estate rule that
-load-bearing proofs be constructive and complete (no `Admitted`, no
-`postulate`). This mirrors how `invariant-path/proofs/SameCube.agda` grounds
-F-2 with a real `--safe` proof rather than a stated hole.
+`K1Let_CodegenPreservation.v` re-proves the same shape for a **grown** fragment
+with de Bruijn **variables** and **`let`**, evaluated under an environment; the
+target machine gains a *locals* register and compilation balances
+`IBind`/`IUnbind`. `if`/structured control is the next increment (it needs a
+target control construct + a termination measure, deliberately out of scope
+here).
 
-[#scope]
-== Scope (honest)
+== F-1 composes on K-1
 
-This is the **Wave-0 seed** of K-1, not the discharged obligation. The fragment
-is deliberately tiny: no functions, binders, effects, ownership, traits, or
-the real instruction set. The full theorem needs the real AffineScript AST and
-the real typed-WASM operational semantics; expanding this core is the analogue
-of solo-core's Duet/Ensemble tracks expanding the Solo fragment. Tracked in
-`docs/PROOF-NEEDS.adoc` (K-1) and #513 (must-have 7).
+`F1_TransformerPreservation.v` models a face surface `fexp` with parser sugar,
+a transform `elaborate : fexp -> sexp` (the `T_F` of ADR-010), and the face's
+own semantics `feval`. It proves the transform preserves meaning
+(`feval f = seval (elaborate f)`) and then *chains K-1* to get end-to-end
+codegen preservation, plus the cross-face same-cube corollary (faces landing on
+the same canonical AST emit identical code). The observational version for the
+trailing-statement/tail split is mechanized separately in
+`invariant-path/proofs/SameCube.agda` (F-2).
+
+== Scope (honest)
 
-The faces twin **F-1** (transformer semantics-preservation) composes *on top
-of* K-1: prove the backend preserves meaning once here, and each
-`lib/<face>_face.ml` front-end transform need only preserve the canonical AST
-denotation for the same-cube result to follow end-to-end.
+These are Wave-0 seeds, not the discharged obligations. The fragments are
+deliberately small; the full theorems need the real AffineScript AST and the
+real typed-WASM operational semantics, expanded the way solo-core's
+Duet/Ensemble tracks expand Solo. Tracked in `docs/PROOF-NEEDS.adoc` and #513.
 
 == Checking
 
 [source,sh]
 ----
-just -f formal/justfile check        # or:  cd formal && coqc K1_CodegenPreservation.v
+just -f formal/justfile check
+# or, by hand (F-1 Requires K-1, so compile K-1 first):
+cd formal
+for f in K1_CodegenPreservation K1Let_CodegenPreservation \
+         F1_TransformerPreservation Siblings_Stated; do
+  coqc -Q . ASFormal "$f.v"
+done
 ----
 
 Requires Coq 8.18+ (`apt install coq`, or opam `coq`). The `check` recipe fails
-if the proof ever starts depending on an axiom or `Admitted`.
+if any proof depends on an axiom or `Admitted`.
diff --git a/formal/Siblings_Stated.v b/formal/Siblings_Stated.v
new file mode 100644
index 00000000..1968087a
--- /dev/null
+++ b/formal/Siblings_Stated.v
@@ -0,0 +1,108 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   Siblings_Stated.v
+   ═════════════════
+   Wave-0 *statements* (NOT proofs) of the remaining Wave-0 obligations from
+   docs/PROOF-NEEDS.adoc — P-2, P-3, F-3, F-4 — as parametric Coq propositions.
+
+   Each obligation abstracts the not-yet-modelled syntax/judgments via a
+   `Section` with `Variable`s and records the property as `Definition
+   ..._statement : Prop`. At `End`, the Variables are discharged into ordinary
+   universally-quantified propositions, so:
+     * the file is complete and **axiom-free** (no `Admitted`, no `Axiom`,
+       no `Parameter`); and
+     * 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).
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+(* ═══════════════════ P-2 — Solo progress + preservation ══════════════════ *)
+Section P2_Solo.
+  Variable term : Type.
+  Variable ty   : Type.
+  Variable ctx  : Type.
+  Variable empty    : ctx.
+  Variable has_type : ctx -> term -> ty -> Prop.
+  Variable value    : term -> Prop.
+  Variable step     : term -> term -> Prop.
+
+  (* A well-typed closed term is a value or can step. *)
+  Definition P2_progress : Prop :=
+    forall t a, has_type empty t a -> value t \/ (exists t', step t t').
+
+  (* Typing is preserved by a step (subject reduction). *)
+  Definition P2_preservation : Prop :=
+    forall g t t' a, has_type g t a -> step t t' -> has_type g t' a.
+End P2_Solo.
+
+(* ═══════════ P-3 — borrow-graph soundness (must reject #554) ══════════════ *)
+Section P3_Borrow.
+  Variable term : Type.
+  Variable borrow_ok       : term -> Prop.   (* the borrow checker accepts t *)
+  Variable uses_after_move : term -> Prop.   (* t observes a moved value at runtime *)
+  Variable example_554     : term.           (* let r = pick(a); consume(a); *r *)
+
+  (* Soundness: an accepted program never uses-after-move. *)
+  Definition P3_borrow_soundness : Prop :=
+    forall t, borrow_ok t -> ~ uses_after_move t.
+
+  (* The #554 obligation made explicit: the witness program DOES use-after-move,
+     so a sound checker must REJECT it. (Today's checker accepts it — that gap
+     is exactly #554 / the Polonius residual #553.) This is a direct corollary
+     of P3_borrow_soundness applied to example_554. *)
+  Definition P3_rejects_554 : Prop :=
+    uses_after_move example_554 -> ~ borrow_ok example_554.
+End P3_Borrow.
+
+(* ═════════ F-3 — face pragma detection: deterministic + functional ═══════ *)
+Section F3_Pragma.
+  Variable source : Type.
+  Variable face   : Type.
+  Variable detect        : source -> option face.   (* Face_pragma.detect_in_source *)
+  Variable pragma_region : source -> source.        (* the leading lines actually scanned *)
+
+  (* Totality and determinism are automatic for a Coq function `detect`; the
+     real content is *locality* — the result depends only on the scanned
+     region, never on bytes past the first code token. *)
+  Definition F3_pragma_local : Prop :=
+    forall s1 s2, pragma_region s1 = pragma_region s2 -> detect s1 = detect s2.
+
+  (* The alias table (rattle→Python, jaffa→Js, …) is a function: a name resolves
+     to at most one face. *)
+  Variable name         : Type.
+  Variable resolve_name : name -> option face.
+  Definition F3_alias_functional : Prop :=
+    forall n f1 f2, resolve_name n = Some f1 -> resolve_name n = Some f2 -> f1 = f2.
+End F3_Pragma.
+
+(* ═══════════ F-4 — error-vocabulary faithfulness (a simulation) ══════════ *)
+Section F4_ErrorVocab.
+  Variable canon_error : Type.   (* canonical compiler error term *)
+  Variable face        : Type.
+  Variable rendered    : Type.   (* face-specific rendered message *)
+  Variable render : face -> canon_error -> rendered.
+
+  (* Observables recoverable from a canonical error and from a rendering. *)
+  Variable err_class          : canon_error -> nat.   (* the error's kind *)
+  Variable err_referent       : canon_error -> nat.   (* the offending identifier/site *)
+  Variable rendered_class     : rendered -> nat.
+  Variable rendered_referent  : rendered -> nat.
+
+  (* Faithfulness: a face rendering preserves the canonical error's class and
+     referent — a face can never make error X read as a different error Y.
+     (OCaml's exhaustiveness checks `render` is total; this is the *semantic*
+     obligation it does not check.) *)
+  Definition F4_error_faithful : Prop :=
+    forall f e,
+      rendered_class    (render f e) = err_class e /\
+      rendered_referent (render f e) = err_referent e.
+End F4_ErrorVocab.
diff --git a/formal/_CoqProject b/formal/_CoqProject
index 2acbf5d1..b4c5ba62 100644
--- a/formal/_CoqProject
+++ b/formal/_CoqProject
@@ -1,2 +1,5 @@
 -Q . ASFormal
 K1_CodegenPreservation.v
+K1Let_CodegenPreservation.v
+F1_TransformerPreservation.v
+Siblings_Stated.v
diff --git a/formal/justfile b/formal/justfile
index 0e4e43bb..e20c1776 100644
--- a/formal/justfile
+++ b/formal/justfile
@@ -2,15 +2,23 @@
 # Coq/Rocq proof checks for the AffineScript `formal/` track.
 # (Mustfile/justfile per estate policy — no Makefiles.)
 
-# Type-check every proof and assert it closes under no axioms.
+# Type-check every proof in dependency order (F-1 Requires K-1) and assert
+# none depends on an axiom or Admitted.
 check:
     #!/usr/bin/env bash
     set -euo pipefail
-    out="$(coqc K1_CodegenPreservation.v)"
-    printf '%s\n' "$out"
-    grep -q "Closed under the global context" <<<"$out" \
-      || { echo "::error:: K-1 proof depends on an axiom / Admitted"; exit 1; }
-    echo "OK: K-1 fragment mechanized, no axioms."
+    all=""
+    for f in K1_CodegenPreservation K1Let_CodegenPreservation \
+             F1_TransformerPreservation Siblings_Stated; do
+      echo "== coqc $f.v =="
+      o="$(coqc -Q . ASFormal "$f.v")"
+      printf '%s\n' "$o"
+      all+="$o"$'\n'
+    done
+    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."
 
 # Remove Coq build artifacts.
 clean: