feat(formal): Wave 3 capstone — quantitative typing tracks usage soundly

.hypatia-ignore

@@ -67,3 +67,5 @@ 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
+cicd_rules/vlang_detected:formal/QttTyping.v
+cicd_rules/banned_language_file:formal/QttTyping.v

docs/PROOF-NEEDS.adoc

@@ -143,11 +143,13 @@ obligations. They are the "we might have missed" half of the brief.
 | **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly
   once, `0`-vars erased, semiring laws hold.
 | 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`
+| #513 must-have 3; **mechanized** across three files: `formal/QttSemiring.v`
+  (`{0,1,ω}` laws + occurrence homomorphism), `formal/AffineUsage.v` (`λx.x`
+  affine, `λx. x x` not), and `formal/QttTyping.v` — a quantitative type system
+  whose usage context Γ is proven to track usage exactly
+  (`usage x t = Γ x`). The *dynamic* half (operational progress+preservation
+  preserving the quantity accounting under reduction) remains; prose
+  `quantitative-types.md`
 
 | P-5
 | **HM inference soundness + principality.** Inferred types are well-typed and

formal/QttTyping.v

@@ -0,0 +1,92 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   QttTyping.v
+   ═══════════
+   Wave 3 (capstone): a **quantitative type system** that fuses the three Wave-1/2
+   pieces — the term structure + typing discipline of P2_Stlc, the multiplicity
+   semiring of QttSemiring, and the occurrence-count usage of AffineUsage — into
+   one judgment whose context *tracks quantities*.
+
+   `qtt Γ t A` : Γ : uctx (a usage context, var ↦ quantity) records how much each
+   variable is used in t. Q_Var consumes one variable once; Q_App ADDS the two
+   subcontexts (`Γ₁ + Γ₂`, the QTT context-splitting read backwards); Q_Lam binds
+   a variable at the multiplicity it is used.
+
+   The capstone theorem **usage_soundness**: the typing context records EXACTLY
+   the QTT usage of every variable —
+
+       qtt Γ t A  →  ∀ x, usage x t = Γ x
+
+   — so the type system's quantity bookkeeping is sound w.r.t. actual occurrence
+   counts. Corollary **linear_uses_once**: a term typed in a singleton context
+   uses exactly that one variable, exactly once. Axiom-free, no Admitted.
+
+   Scope: the *static* quantity discipline is now unified and proven sound
+   against usage. Operational progress+preservation that PRESERVES the quantity
+   accounting under reduction (the dynamic half) is the remaining step.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import PeanoNat.
+Require Import ASFormal.QttSemiring.
+Require Import ASFormal.AffineUsage.
+
+(* Multiplicity-annotated types: a function records how often it uses its arg. *)
+Inductive qty := QBase | QArr (q : quant) (A B : qty).
+
+(* Usage contexts. *)
+Definition uctx := id -> quant.
+Definition uadd    (G1 G2 : uctx) : uctx := fun x => qplus (G1 x) (G2 x).
+Definition usingle (x : id)       : uctx := fun y => if Nat.eqb x y then One else Zero.
+Definition uext    (G : uctx) (x : id) (q : quant) : uctx :=
+  fun y => if Nat.eqb x y then q else G y.
+
+(* Quantitative typing: the context records each variable's usage. *)
+Inductive qtt : uctx -> tm -> qty -> Prop :=
+| Q_Var : forall x A, qtt (usingle x) (var x) A
+| Q_App : forall G1 G2 f a q A B,
+    qtt G1 f (QArr q A B) -> qtt G2 a A -> qtt (uadd G1 G2) (app f a) B
+| Q_Lam : forall G x q A B b,
+    G x = Zero -> qtt (uext G x q) b B -> qtt G (lam x b) (QArr q A B).
+
+(* ── capstone: the typing context records exactly the usage ─────────────── *)
+
+Theorem usage_soundness : forall G t A,
+  qtt G t A -> forall x, usage x t = G x.
+Proof.
+  intros G t A H.
+  induction H as [ x A
+                 | G1 G2 f a q A B Hf IHf Ha IHa
+                 | G x q A B b Hz Hb IHb ]; intro z.
+  - (* Q_Var *)
+    unfold usage, usingle; simpl. rewrite (Nat.eqb_sym x z).
+    destruct (Nat.eqb z x); reflexivity.
+  - (* Q_App *)
+    rewrite usage_app, (IHf z), (IHa z); unfold uadd; reflexivity.
+  - (* Q_Lam *)
+    destruct (Nat.eqb z x) eqn:E.
+    + apply Nat.eqb_eq in E; subst z.
+      rewrite usage_lam_bound; symmetry; exact Hz.
+    + assert (usage z (lam x b) = usage z b) as Hlz
+        by (unfold usage; simpl; rewrite E; reflexivity).
+      rewrite Hlz, (IHb z); unfold uext; rewrite (Nat.eqb_sym x z), E; reflexivity.
+Qed.
+
+(* A term typed in a singleton context uses exactly that one variable, once —
+   the essence of linearity, now read off the typing. *)
+Corollary linear_uses_once : forall x t A,
+  qtt (usingle x) t A ->
+  usage x t = One /\ (forall y, y <> x -> usage y t = Zero).
+Proof.
+  intros x t A H; split.
+  - rewrite (usage_soundness _ _ _ H x); unfold usingle; rewrite Nat.eqb_refl; reflexivity.
+  - intros y Hy. rewrite (usage_soundness _ _ _ H y); unfold usingle.
+    assert (x <> y) as Hxy by (intro Hc; apply Hy; symmetry; exact Hc).
+    apply Nat.eqb_neq in Hxy; rewrite Hxy; reflexivity.
+Qed.
+
+Print Assumptions usage_soundness.
+Print Assumptions linear_uses_once.

formal/README.adoc

@@ -79,6 +79,11 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **P-4** (Wave 2) — affine usage over the semiring: `λx.x` affine, `λx. x x`
   not (variable totals `ω`)
 | **mechanized**, axiom-free
+
+| `QttTyping.v`
+| **P-4** (Wave 3) — quantitative typing fusing all three: the typing context
+  tracks usage, proven sound (`usage x t = Γ x`)
+| **mechanized**, axiom-free
 |===
 
 All mechanized theorems report *Closed under the global context* under `Print
@@ -139,10 +144,17 @@ The quantities `{0,1,ω}` and their algebra are what make AffineScript *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.
+* **`QttTyping.v`** (Wave 3 capstone) — a **quantitative type system** fusing all
+  three: `qtt Γ t A` where the usage context Γ tracks quantities (`Q_App` adds
+  `Γ₁ + Γ₂`, `Q_Lam` binds at the used multiplicity). The capstone theorem
+  `usage_soundness : qtt Γ t A → ∀x, usage x t = Γ x` proves the typing context
+  records *exactly* the QTT usage — the static quantity discipline is sound
+  against occurrence counts. Corollary: a term typed in a singleton context uses
+  that variable exactly once.
+
+The remaining step is the *dynamic* half: operational progress + preservation
+that PRESERVES the quantity accounting under reduction (a quantitative
+substitution lemma over `P2_Stlc.v`).
 
 == K-1 and its growth
 

formal/_CoqProject

@@ -11,3 +11,4 @@ P2_Progress.v
 P2_Stlc.v
 QttSemiring.v
 AffineUsage.v
+QttTyping.v

formal/justfile

@@ -12,7 +12,7 @@ check:
     for f in K1_CodegenPreservation K1Let_CodegenPreservation Siblings_Stated \
              F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \
              P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \
-             QttSemiring AffineUsage; do
+             QttSemiring AffineUsage QttTyping; do
       echo "== coqc $f.v =="
       o="$(coqc -Q . ASFormal "$f.v")"
       printf '%s\n' "$o"