diff --git a/.hypatia-ignore b/.hypatia-ignore
index d6607c23..48c0049b 100644
--- a/.hypatia-ignore
+++ b/.hypatia-ignore
@@ -63,3 +63,7 @@ cicd_rules/vlang_detected:formal/P3_BorrowGraph.v
 cicd_rules/banned_language_file:formal/P3_BorrowGraph.v
 cicd_rules/vlang_detected:formal/P2_Stlc.v
 cicd_rules/banned_language_file:formal/P2_Stlc.v
+cicd_rules/vlang_detected:formal/QttSemiring.v
+cicd_rules/banned_language_file:formal/QttSemiring.v
+cicd_rules/vlang_detected:formal/AffineUsage.v
+cicd_rules/banned_language_file:formal/AffineUsage.v
diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc
index 564388a5..1fdb76f8 100644
--- a/docs/PROOF-NEEDS.adoc
+++ b/docs/PROOF-NEEDS.adoc
@@ -142,8 +142,12 @@ obligations. They are the "we might have missed" half of the brief.
 | P-4
 | **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly
   once, `0`-vars erased, semiring laws hold.
-| L | `prose`
-| #513 must-have 3; prose `quantitative-types.md`
+| L | `partial`
+| #513 must-have 3; **semiring + affine-usage mechanized** in
+  `formal/QttSemiring.v` (`{0,1,ω}` laws + occurrence homomorphism) and
+  `formal/AffineUsage.v` (`λx.x` affine, `λx. x x` not). The full *typed* QTT
+  calculus (context splitting, progress+preservation tracking quantities)
+  remains; prose `quantitative-types.md`
 
 | P-5
 | **HM inference soundness + principality.** Inferred types are well-typed and
diff --git a/formal/AffineUsage.v b/formal/AffineUsage.v
new file mode 100644
index 00000000..950c2d03
--- /dev/null
+++ b/formal/AffineUsage.v
@@ -0,0 +1,97 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   AffineUsage.v
+   ═════════════
+   Wave 2: the affine-usage layer over the QTT semiring (QttSemiring.v).
+
+   Reads the multiplicity of a variable in a term as the QTT abstraction of its
+   free-occurrence count: `usage x t := qof (count x t)`. Proves that usage is
+   compositional under the semiring — through an application the usages ADD:
+
+       usage x (app f a) = qplus (usage x f) (usage x a)         (from qof_plus)
+
+   — and defines **affine well-formedness** (every binder consumes its variable
+   at most once, `usage x b ≤ 1`). The payoff theorems: the identity `λx.x` is
+   affine, while self-application `λx. x x` is NOT — its variable totals `ω`,
+   which exceeds the affine bound. That is the mechanized statement of "a
+   linear/affine value may not be duplicated".
+
+   Advances **P-4** (docs/PROOF-NEEDS.adoc). Axiom-free, no `Admitted`. The full
+   *typed* QTT calculus (context splitting Γ = Γ₁ + Γ₂, progress+preservation
+   tracking quantities) is the next increment, on top of this + P2_Stlc.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import PeanoNat.
+Require Import Lia.
+Require Import ASFormal.QttSemiring.
+
+Definition id := nat.
+
+Inductive tm :=
+| var (x : id)
+| app (f a : tm)
+| lam (x : id) (b : tm).
+
+(* Free-occurrence count of x in t. *)
+Fixpoint count (x : id) (t : tm) : nat :=
+  match t with
+  | var y   => if Nat.eqb x y then 1 else 0
+  | app f a => count x f + count x a
+  | lam y b => if Nat.eqb x y then 0 else count x b
+  end.
+
+(* The multiplicity at which x is used in t, as a QTT quantity. *)
+Definition usage (x : id) (t : tm) : quant := qof (count x t).
+
+(* ── usage is compositional under the semiring ─────────────────────────── *)
+
+(* Through an application, usages ADD (qplus) — the crux of the affine reading:
+   a variable used once in `f` and once in `a` is used ω in `f a`. *)
+Theorem usage_app : forall x f a,
+  usage x (app f a) = qplus (usage x f) (usage x a).
+Proof. intros x f a; unfold usage; simpl; apply qof_plus. Qed.
+
+Lemma usage_var_same : forall x, usage x (var x) = One.
+Proof. intro x; unfold usage; simpl; rewrite Nat.eqb_refl; reflexivity. Qed.
+
+Lemma usage_var_diff : forall x y, x <> y -> usage x (var y) = Zero.
+Proof.
+  intros x y H; unfold usage; simpl.
+  apply Nat.eqb_neq in H; rewrite H; reflexivity.
+Qed.
+
+Lemma usage_lam_bound : forall x b, usage x (lam x b) = Zero.
+Proof. intros x b; unfold usage; simpl; rewrite Nat.eqb_refl; reflexivity. Qed.
+
+(* ── affine well-formedness ────────────────────────────────────────────── *)
+
+Fixpoint affine (t : tm) : Prop :=
+  match t with
+  | var _   => True
+  | app f a => affine f /\ affine a
+  | lam x b => qle (usage x b) One /\ affine b
+  end.
+
+(* The identity is affine: its bound variable is used exactly once. *)
+Example affine_id : forall x, affine (lam x (var x)).
+Proof.
+  intro x; simpl; split.
+  - rewrite usage_var_same; apply qle_refl.
+  - exact I.
+Qed.
+
+(* Self-application λx. x x is NOT affine: x is used twice, totalling ω, which
+   exceeds the affine bound `≤ 1`. *)
+Example not_affine_selfapp : forall x, ~ affine (lam x (app (var x) (var x))).
+Proof.
+  intro x; simpl; intros [Hle _].
+  unfold usage, qle in Hle; simpl in Hle.
+  rewrite !Nat.eqb_refl in Hle; simpl in Hle; lia.
+Qed.
+
+Print Assumptions usage_app.
+Print Assumptions not_affine_selfapp.
diff --git a/formal/QttSemiring.v b/formal/QttSemiring.v
new file mode 100644
index 00000000..1723fa1c
--- /dev/null
+++ b/formal/QttSemiring.v
@@ -0,0 +1,109 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   QttSemiring.v
+   ═════════════
+   Wave 2: the **QTT quantity semiring {0, 1, ω}** — the algebraic core of
+   AffineScript's affine / quantitative type system (the `Quantity` module of
+   the Solo calculus). Mechanizes the multiplicity semiring with its `+`
+   (context addition) and `·` (scaling) operations, the usage order
+   `0 ≤ 1 ≤ ω`, and the bridge to occurrence counts:
+
+       qof (m + n) = qplus (qof m) (qof n)
+
+   i.e. *occurrences add under QTT addition*. So using a **linear** (`1`)
+   variable in BOTH the function and the argument of an application totals `ω`
+   (`qplus One One = Omega`), exceeding the affine bound — the algebraic reason
+   a linear value cannot be used twice.
+
+   Advances **P-4** (docs/PROOF-NEEDS.adoc) from prose to a mechanized core.
+   All laws hold by exhaustive case analysis — axiom-free, no `Admitted`.
+   A usage-counted linear *calculus* (the "1-var used exactly once" typing
+   theorem) builds on this in AffineUsage.v.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import PeanoNat.
+Require Import Lia.
+
+Inductive quant := Zero | One | Omega.
+
+(* Context addition: how usages combine when a variable is used in two places.
+   1 + 1 = ω is the crux — two linear uses exceed the affine bound. *)
+Definition qplus (p q : quant) : quant :=
+  match p with
+  | Zero  => q
+  | One   => match q with Zero => One | _ => Omega end
+  | Omega => Omega
+  end.
+
+(* Scaling: how a usage is multiplied when passing through a binder of a given
+   multiplicity. *)
+Definition qmult (p q : quant) : quant :=
+  match p with
+  | Zero  => Zero
+  | One   => q
+  | Omega => match q with Zero => Zero | _ => Omega end
+  end.
+
+(* ── semiring laws (exhaustive case analysis) ──────────────────────────── *)
+
+Lemma qplus_0_l : forall q, qplus Zero q = q.       Proof. reflexivity. Qed.
+Lemma qplus_0_r : forall q, qplus q Zero = q.       Proof. destruct q; reflexivity. Qed.
+Lemma qplus_comm : forall p q, qplus p q = qplus q p.
+Proof. destruct p, q; reflexivity. Qed.
+Lemma qplus_assoc : forall p q r, qplus p (qplus q r) = qplus (qplus p q) r.
+Proof. destruct p, q, r; reflexivity. Qed.
+
+Lemma qmult_0_l : forall q, qmult Zero q = Zero.    Proof. reflexivity. Qed.
+Lemma qmult_0_r : forall q, qmult q Zero = Zero.    Proof. destruct q; reflexivity. Qed.
+Lemma qmult_1_l : forall q, qmult One q = q.        Proof. reflexivity. Qed.
+Lemma qmult_1_r : forall q, qmult q One = q.        Proof. destruct q; reflexivity. Qed.
+Lemma qmult_comm : forall p q, qmult p q = qmult q p.
+Proof. destruct p, q; reflexivity. Qed.
+Lemma qmult_assoc : forall p q r, qmult p (qmult q r) = qmult (qmult p q) r.
+Proof. destruct p, q, r; reflexivity. Qed.
+
+Lemma qdistrib_l : forall p q r, qmult p (qplus q r) = qplus (qmult p q) (qmult p r).
+Proof. destruct p, q, r; reflexivity. Qed.
+Lemma qdistrib_r : forall p q r, qmult (qplus p q) r = qplus (qmult p r) (qmult q r).
+Proof. destruct p, q, r; reflexivity. Qed.
+
+(* ── the usage order  0 ≤ 1 ≤ ω  ───────────────────────────────────────── *)
+
+Definition rank (q : quant) : nat :=
+  match q with Zero => 0 | One => 1 | Omega => 2 end.
+Definition qle (p q : quant) : Prop := rank p <= rank q.
+
+Lemma qle_refl  : forall q, qle q q.                  Proof. intro; apply Nat.le_refl. Qed.
+Lemma qle_trans : forall p q r, qle p q -> qle q r -> qle p r.
+Proof. unfold qle; intros p q r H1 H2; eapply Nat.le_trans; eauto. Qed.
+Lemma qle_zero_min : forall q, qle Zero q.            Proof. intro q; unfold qle; apply Nat.le_0_l. Qed.
+Lemma qle_omega_max : forall q, qle q Omega.          Proof. destruct q; unfold qle; simpl; lia. Qed.
+
+(* ── the affine facts ──────────────────────────────────────────────────── *)
+
+(* Using a linear (1) value twice overflows to ω — i.e. exceeds the affine
+   bound `≤ 1`. This is the algebraic heart of "a linear value is used once". *)
+Lemma linear_used_twice : qplus One One = Omega.      Proof. reflexivity. Qed.
+Lemma affine_bound_exceeded : ~ qle (qplus One One) One.
+Proof. unfold qle; rewrite linear_used_twice; simpl; lia. Qed.
+
+(* Erased (0) variables contribute nothing and absorb under scaling. *)
+Lemma erased_scales_away : forall q, qmult Zero q = Zero.   Proof. reflexivity. Qed.
+
+(* ── bridge: occurrence counts abstract to quantities ──────────────────── *)
+
+Definition qof (n : nat) : quant :=
+  match n with 0 => Zero | 1 => One | _ => Omega end.
+
+(* `qof` is a semiring homomorphism on addition: occurrences add under qplus.
+   So a variable used m times in `f` and n times in `a` is used (m+n) times in
+   `f a`, abstracting to qplus — and if both are 1, the total is ω. *)
+Theorem qof_plus : forall m n, qof (m + n) = qplus (qof m) (qof n).
+Proof. intros m n; destruct m as [| [| m]]; destruct n as [| [| n]]; reflexivity. Qed.
+
+Corollary qof_linear_twice : qof 1 = One /\ qof (1 + 1) = Omega.
+Proof. split; reflexivity. Qed.
diff --git a/formal/README.adoc b/formal/README.adoc
index a31f8a99..91f255ed 100644
--- a/formal/README.adoc
+++ b/formal/README.adoc
@@ -69,6 +69,16 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | `F4_ErrorFaithful.v`
 | **F-4** — error rendering preserves class + referent
 | **mechanized**, axiom-free
+
+| `QttSemiring.v`
+| **P-4** (Wave 2) — the QTT quantity semiring `{0,1,ω}`: operations, semiring
+  + order laws, occurrence-count homomorphism
+| **mechanized**, axiom-free
+
+| `AffineUsage.v`
+| **P-4** (Wave 2) — affine usage over the semiring: `λx.x` affine, `λx. x x`
+  not (variable totals `ω`)
+| **mechanized**, axiom-free
 |===
 
 All mechanized theorems report *Closed under the global context* under `Print
@@ -114,6 +124,26 @@ the stated obligation and pin its meaning, not the full language:
   *class* and *referent*, changing only vocabulary, so no face can make error
   X read as a different error Y.
 
+== Wave 2: the affine/QTT layer (P-4)
+
+The quantities `{0,1,ω}` and their algebra are what make AffineScript *affine*:
+
+* **`QttSemiring.v`** — the multiplicity semiring: `qplus` (context addition,
+  with `1 + 1 = ω`) and `qmult` (scaling), all semiring + order laws by
+  exhaustive case analysis, and the homomorphism
+  `qof (m + n) = qplus (qof m) (qof n)` (occurrence counts add under QTT
+  addition).
+* **`AffineUsage.v`** — reads a variable's multiplicity as `qof (count x t)`,
+  proves usage composes under the semiring through application
+  (`usage x (app f a) = qplus (usage x f) (usage x a)`), and defines affine
+  well-formedness. Payoff: `λx.x` is affine; `λx. x x` is **not** — its variable
+  totals `ω`, exceeding the affine bound. The mechanized statement of "a linear
+  value may not be duplicated".
+
+The full *typed* QTT calculus — context splitting `Γ = Γ₁ + Γ₂`, progress +
+preservation tracking quantities, on top of `P2_Stlc.v` — is the next
+increment.
+
 == K-1 and its growth
 
 `K1_CodegenPreservation.v` proves, for a minimal two-type fragment (nat + bool,
diff --git a/formal/_CoqProject b/formal/_CoqProject
index 4aee801e..2f8e878b 100644
--- a/formal/_CoqProject
+++ b/formal/_CoqProject
@@ -9,3 +9,5 @@ P3_BorrowSound.v
 P3_BorrowGraph.v
 P2_Progress.v
 P2_Stlc.v
+QttSemiring.v
+AffineUsage.v
diff --git a/formal/justfile b/formal/justfile
index be481dd8..f589dc16 100644
--- a/formal/justfile
+++ b/formal/justfile
@@ -11,7 +11,8 @@ check:
     all=""
     for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \
              F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \
-             P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc; do
+             P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \
+             QttSemiring AffineUsage; do
       echo "== coqc $f.v =="
       o="$(coqc -Q . ASFormal "$f.v")"
       printf '%s\n' "$o"