feat(formal): P-4 dynamic half — β-reduction preserves the QTT usage profile

.hypatia-ignore

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

docs/PROOF-NEEDS.adoc

@@ -70,7 +70,7 @@ 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), axiom-free throughout — **13 files, 22 `Print
+  **exists** (Coq/Rocq 8.18), axiom-free throughout — **14 files, 23 `Print
   Assumptions` closure reports**, all "Closed under the global context". Codegen
   keystone: `K1_CodegenPreservation.v` (K-1 minimal) +
   `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment).
@@ -81,7 +81,8 @@ than the prose corpus suggests:
   `P3_BorrowGraph.v` (multi-resource loan graph) / `F3_PragmaDecidable.v` /
   `F4_ErrorFaithful.v`. Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) +
   `AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative
-  typing, `usage x t = Γ x` sound). See <<outstanding>>, <<faces>>.
+  typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half:
+  β-reduction preserves the usage profile). 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,
@@ -151,12 +152,15 @@ 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; **mechanized** across three files: `formal/QttSemiring.v`
+| #513 must-have 3; **mechanized** across four 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
+  affine, `λx. x x` not), `formal/QttTyping.v` — a quantitative type system whose
+  usage context Γ is proven to track usage exactly (`usage x t = Γ x`) — and
+  `formal/QttDynamic.v`, the *dynamic* half: β-reduction **preserves the usage
+  profile** (`t → t' ⇒ ∀z, usage z t' = usage z t`), with the QTT scaling law
+  (`qof_mult`) and `qtt_context_preserved` composing it with `usage_soundness`.
+  The full operational development on the *real* AST (substitution lemma past the
+  binder-free / closed-value fragment) is the remaining lift; prose
   `quantitative-types.md`
 
 | P-5
@@ -368,11 +372,13 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | Wave 0
 
 | 2
-| **Done (static).** The affine/QTT layer — **`QttSemiring.v`** (`{0,1,ω}` laws +
+| **Done.** The affine/QTT layer — **`QttSemiring.v`** (`{0,1,ω}` laws +
   occurrence homomorphism), **`AffineUsage.v`** (`λx.x` affine, `λx. x x` not),
-  **`QttTyping.v`** (quantitative typing, `usage x t = Γ x` sound). *Leftover:*
-  the *dynamic* half — a quantitative substitution lemma over `P2_Stlc.v` that
-  carries the quantity accounting through reduction.
+  **`QttTyping.v`** (static quantitative typing, `usage x t = Γ x` sound), and
+  **`QttDynamic.v`** — the *dynamic* half: β-reduction preserves the usage
+  profile (`step_preserves_usage`), the QTT scaling law, and `qtt_context_preserved`
+  tying it back to `usage_soundness`. *Leftover:* generalise the dynamic
+  development past the binder-free / closed-value fragment onto the real AST.
 | Wave 1
 
 | 3

formal/QttDynamic.v

@@ -0,0 +1,197 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   QttDynamic.v
+   ════════════
+   Wave 3, the DYNAMIC half of P-4. QttTyping.v proved the *static* quantity
+   discipline sound — the typing context records exactly the usage
+   (`usage x t = Γ x`). This file proves that discipline is preserved **under
+   reduction**: a small-step β-reduction relation on the QTT term language
+   (`AffineUsage.tm`) carries the whole usage profile forward unchanged.
+
+   Headline — `step_preserves_usage`:
+
+       t → t'  →  ∀ z, usage z t' = usage z t
+
+   so the quantity accounting is a dynamic invariant. Composed with QttTyping's
+   `usage_soundness` it yields the capstone-completing corollary
+   `qtt_context_preserved`:
+
+       qtt Γ t A → t → t' → ∀ x, usage x t' = Γ x
+
+   — a well-typed term's QTT context stays valid across a reduction step.
+
+   Two further results expose the QTT *scaling* law that makes substructurality
+   bite. Substituting v for a variable used at multiplicity q scales v's usage by
+   q (`usage_subst_scaling`, via the new ×-homomorphism `qof_mult`); and an
+   affine redex never increases any variable's usage (`affine_no_increase`) — the
+   dynamic face of the affine bound. β here substitutes a *closed* value (the
+   call-by-value, closed-program convention P2_Stlc.v also uses), so capture
+   cannot arise and the development stays axiom-free — no Admitted, no axioms.
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+*)
+
+Require Import PeanoNat.
+Require Import Lia.
+Require Import ASFormal.QttSemiring.
+Require Import ASFormal.AffineUsage.
+Require Import ASFormal.QttTyping.
+
+(* ── qof is also a homomorphism for multiplication ──────────────────────────
+   QttSemiring gives qof_plus (occurrences add); the scaling law below needs the
+   × analogue (occurrences multiply through a binder of a given multiplicity). *)
+Lemma qof_mult : forall m n, qof (m * n) = qmult (qof m) (qof n).
+Proof.
+  intros m n; destruct m as [|[|m]]; destruct n as [|[|n]];
+    try reflexivity; rewrite Nat.mul_0_r; reflexivity.
+Qed.
+
+(* ── capture-permitting substitution (only ever applied to closed values) ─── *)
+Fixpoint subst (x : id) (s t : tm) : tm :=
+  match t with
+  | var y   => if Nat.eqb x y then s else var y
+  | app f a => app (subst x s f) (subst x s a)
+  | lam y b => if Nat.eqb x y then lam y b else lam y (subst x s b)
+  end.
+
+Definition closed (t : tm) : Prop := forall z, count z t = 0.
+
+(* ── small-step β-reduction (call-by-value, closed argument) ──────────────── *)
+Inductive value : tm -> Prop :=
+| v_lam : forall x b, value (lam x b).
+
+Inductive step : tm -> tm -> Prop :=
+| ST_AppAbs : forall x b v,
+    value v -> closed v -> step (app (lam x b) v) (subst x v b)
+| ST_App1 : forall f f' a, step f f' -> step (app f a) (app f' a)
+| ST_App2 : forall f a a', value f -> step a a' -> step (app f a) (app f a').
+
+(* ── substituting a closed value: counts untouched off x, zeroed at x ─────── *)
+
+Lemma count_subst_closed_diff : forall x v b z,
+  closed v -> z <> x -> count z (subst x v b) = count z b.
+Proof.
+  intros x v b z Hc Hzx.
+  induction b as [ y | f IHf a IHa | y b IHb ].
+  - (* var y *) cbn [subst]. destruct (Nat.eqb x y) eqn:E.
+    + rewrite (Hc z). apply Nat.eqb_eq in E; subst y.
+      cbn. apply Nat.eqb_neq in Hzx. rewrite Hzx. reflexivity.
+    + reflexivity.
+  - (* app *) simpl. rewrite IHf, IHa. reflexivity.
+  - (* lam y b *) cbn [subst]. destruct (Nat.eqb x y) eqn:E.
+    + reflexivity.
+    + simpl. destruct (Nat.eqb z y); [ reflexivity | exact IHb ].
+Qed.
+
+Lemma count_subst_closed_same : forall x v b,
+  closed v -> count x (subst x v b) = 0.
+Proof.
+  intros x v b Hc.
+  induction b as [ y | f IHf a IHa | y b IHb ].
+  - cbn [subst]. destruct (Nat.eqb x y) eqn:E.
+    + apply (Hc x).
+    + cbn. rewrite E. reflexivity.
+  - simpl. rewrite IHf, IHa. reflexivity.
+  - cbn [subst]. destruct (Nat.eqb x y) eqn:E.
+    + cbn. rewrite E. reflexivity.
+    + cbn. rewrite E. exact IHb.
+Qed.
+
+(* ── headline: reduction preserves the full usage profile ─────────────────── *)
+
+Theorem step_preserves_usage : forall t t',
+  step t t' -> forall z, usage z t' = usage z t.
+Proof.
+  intros t t' Hs; induction Hs as
+    [ x b v Hval Hcl | f f' a Hs IH | f a a' Hval Hs IH ]; intro z.
+  - (* ST_AppAbs *)
+    rewrite usage_app.
+    assert (Hzv : usage z v = Zero) by (unfold usage; rewrite Hcl; reflexivity).
+    rewrite Hzv, qplus_0_r.
+    destruct (Nat.eqb z x) eqn:E.
+    + apply Nat.eqb_eq in E; subst z.
+      rewrite usage_lam_bound.
+      unfold usage; rewrite (count_subst_closed_same x v b Hcl); reflexivity.
+    + assert (Hzx : z <> x) by (apply Nat.eqb_neq; exact E).
+      unfold usage. rewrite (count_subst_closed_diff x v b z Hcl Hzx).
+      simpl. rewrite E. reflexivity.
+  - (* ST_App1 *) rewrite !usage_app, (IH z). reflexivity.
+  - (* ST_App2 *) rewrite !usage_app, (IH z). reflexivity.
+Qed.
+
+(* ── the QTT scaling law (binder-free fragment, open v) ────────────────────
+   Substituting v for x scales v's usage by x's multiplicity:
+       usage z (subst x v b) = usage z b  +  (usage x b · usage z v).
+   Stated on the lam-free fragment so capture cannot arise even for open v —
+   enough to exhibit the qmult scaling that the closed-value headline hides. *)
+
+Fixpoint lam_free (t : tm) : Prop :=
+  match t with
+  | var _   => True
+  | app f a => lam_free f /\ lam_free a
+  | lam _ _ => False
+  end.
+
+Lemma usage_subst_scaling : forall x v b z,
+  z <> x -> lam_free b ->
+  usage z (subst x v b) = qplus (usage z b) (qmult (usage x b) (usage z v)).
+Proof.
+  intros x v b; induction b as [ y | f IHf a IHa | y b IHb ];
+    intros z Hzx Hlf.
+  - (* var y *) cbn [subst]. destruct (Nat.eqb x y) eqn:E.
+    + apply Nat.eqb_eq in E; subst y.
+      rewrite (usage_var_diff z x Hzx), (usage_var_same x), qmult_1_l, qplus_0_l.
+      reflexivity.
+    + assert (Hxy : x <> y) by (apply Nat.eqb_neq; exact E).
+      rewrite (usage_var_diff x y Hxy), qmult_0_l, qplus_0_r. reflexivity.
+  - (* app f a *) destruct Hlf as [Hlf Hla].
+    cbn [subst].
+    rewrite (usage_app z (subst x v f) (subst x v a)).
+    rewrite (IHf z Hzx Hlf), (IHa z Hzx Hla).
+    rewrite (usage_app z f a), (usage_app x f a).
+    destruct (usage z f), (usage x f), (usage z a), (usage x a), (usage z v);
+      reflexivity.
+  - (* lam *) cbn in Hlf; destruct Hlf.
+Qed.
+
+(* An affine redex (bound variable used ≤ 1×) never increases any variable's
+   usage: the dynamic counterpart of the static affine bound. *)
+Corollary affine_no_increase : forall x v b z,
+  z <> x -> lam_free b -> qle (usage x b) One ->
+  qle (usage z (subst x v b)) (qplus (usage z b) (usage z v)).
+Proof.
+  intros x v b z Hzx Hlf Haff.
+  rewrite usage_subst_scaling by assumption.
+  revert Haff; unfold qle.
+  destruct (usage x b), (usage z b), (usage z v); simpl; lia.
+Qed.
+
+(* A *linear* redex (bound variable used exactly once) preserves usage exactly,
+   matching the closed-value headline but now for open v. *)
+Corollary linear_exact : forall x v b z,
+  z <> x -> lam_free b -> usage x b = One ->
+  usage z (subst x v b) = qplus (usage z b) (usage z v).
+Proof.
+  intros x v b z Hzx Hlf Hlin.
+  rewrite usage_subst_scaling by assumption.
+  rewrite Hlin, qmult_1_l. reflexivity.
+Qed.
+
+(* ── tie back to the Wave-3 static capstone ───────────────────────────────── *)
+
+(* A well-typed term's QTT context stays valid across a reduction step:
+   static usage_soundness (qtt Γ t A → usage x t = Γ x) composed with the
+   dynamic invariant. Static + dynamic ⇒ the quantity discipline is sound. *)
+Corollary qtt_context_preserved : forall G t A t',
+  qtt G t A -> step t t' -> forall x, usage x t' = G x.
+Proof.
+  intros G t A t' HT Hs x.
+  rewrite (step_preserves_usage t t' Hs x).
+  exact (usage_soundness G t A HT x).
+Qed.
+
+Print Assumptions step_preserves_usage.
+Print Assumptions usage_subst_scaling.
+Print Assumptions qtt_context_preserved.

formal/README.adoc

@@ -84,6 +84,11 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires.
 | **P-4** (Wave 3) — quantitative typing fusing all three: the typing context
   tracks usage, proven sound (`usage x t = Γ x`)
 | **mechanized**, axiom-free
+
+| `QttDynamic.v`
+| **P-4** (Wave 3) — the *dynamic* half: β-reduction preserves the usage profile;
+  QTT scaling law; ties back to `usage_soundness`
+| **mechanized**, axiom-free
 |===
 
 All mechanized theorems report *Closed under the global context* under `Print
@@ -152,9 +157,20 @@ The quantities `{0,1,ω}` and their algebra are what make AffineScript *affine*:
   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`).
+* **`QttDynamic.v`** (Wave 3) — the *dynamic* half. A small-step β-reduction on
+  the QTT terms with the headline `step_preserves_usage`: `t → t'` implies
+  `usage z t' = usage z t` for every `z`, so the quantity accounting is a
+  *dynamic invariant*. Adds the QTT *scaling* law
+  `usage z (subst x v b) = usage z b + usage x b · usage z v` (via the new
+  `qof_mult` ×-homomorphism), an affine-no-increase corollary, and
+  `qtt_context_preserved`, which composes the dynamic invariant with
+  `usage_soundness` so a well-typed term's QTT context stays valid across a
+  step. β substitutes a closed value (the closed-program convention `P2_Stlc.v`
+  also uses), so it is capture-/axiom-free.
+
+The remaining step is the full operational development on the *real* AST: the
+quantity-preserving substitution lemma generalised past the binder-free fragment
+and the closed-value convention.
 
 == K-1 and its growth
 

formal/_CoqProject

@@ -12,3 +12,4 @@ P2_Stlc.v
 QttSemiring.v
 AffineUsage.v
 QttTyping.v
+QttDynamic.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 QttTyping; do
+             QttSemiring AffineUsage QttTyping QttDynamic; do
       echo "== coqc $f.v =="
       o="$(coqc -Q . ASFormal "$f.v")"
       printf '%s\n' "$o"