weight_unique
plain-language theorem explainer
Any two admissible recognition weight rules assign identical weight at every step count n; the lattice-layer measure is unique. Anyone citing T9 uniqueness (Born weights, rung occupancy, chirality selection) uses this. The proof is a one-line double rewrite through the forced form w(n)=φ^{-n}.
Claim. Let $R$ and $S$ be recognition weight rules: positive maps $w:\mathbb{N}\to\mathbb{R}$ that factorize under independent composition and whose single-step weight satisfies the reciprocal self-similar balance. Then for every $n\in\mathbb{N}$, the two weight functions agree: $w_R(n)=w_S(n)$.
background
Module T9 closes the missing weighting primitive left open by the T0–T8 forcing chain. That chain fixed the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$) but not how much of reality sits in each allowed recognition state. Every recurring instance-selection problem in the library (Born weights, chirality, $\delta w_0$, $\eta_B$, rung occupancy) is a projection of that gap.
A recognition weight rule is a positive $w:\mathbb{N}\to\mathbb{R}$ with two premises: factorization $w(m+n)=w(m)w(n)$ (multiplicative shadow of ledger cost additivity), and per-step self-similar balance forcing the single-step weight $\rho=\varphi^{-1}$. Upstream, weight_forced already shows every such rule equals the lattice weight $\varphi^{-n}$. The geometric series $\sum_{n\ge 0}\varphi^{-n}$ is the partition function of the forced measure.
proof idea
One-line tactic proof. Rewrite both sides by the lattice forcing theorem: each rule's weight at $n$ equals the canonical lattice weight $\varphi^{-n}$. The two sides become identical terms, so equality is immediate. No case split, induction, or extra hypotheses beyond the structure fields already used to force the form.
why it matters
This is the uniqueness half of the T9 lattice layer. Downstream, the master certificate measureForcingCert wires it in as lattice_unique, pairing it with lattice_forced (the existence/form half). Together they discharge: any admissible weighting of recognition states is the geometric $\varphi$-measure, equivalently the Gibbs rule with rate pinned by the self-similar ledger.
Framework landmark: T9 sits after T5–T8 (unique $J$, $\varphi$, eight-tick octave, $D=3$) and supplies the missing measure that those steps did not force. It underwrites uniqueness claims for Born-type weights and rung occupancy without importing a second scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.