weight_forced
plain-language theorem explainer
Any admissible recognition weight rule assigns weight φ^{-n} after n recognition steps on the discrete lattice. This is the lattice half of T9 (forced measure), cited by uniqueness of the measure, the master measure-forcing certificate, and the one-statement T9 theorem. The proof is a one-line transport: convert the weight rule to a rung-dilution object and apply the forced occupancy law.
Claim. Let $R$ be a recognition weight rule: a strictly positive map $w:\mathbb{N}\to\mathbb{R}$ that factorizes under independent composition ($w(m+n)=w(m)w(n)$) and whose single-step weight satisfies the reciprocal self-similar balance. Then for every $n\in\mathbb{N}$, $w(n)=\varphi^{-n}$.
background
Module T9 closes the weighting gap left by the T0–T8 forcing chain. That chain fixes 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 open instance-selection problem in the library (Born weights, chirality, $\delta w_0$, $\eta_B$, rung occupancy) is a projection of that missing primitive.
A recognition weight rule is a positive weight $w(n)$ after $n$ recognition steps, required to factorize over independent composition (multiplicative shadow of ledger cost additivity) and to obey per-step reciprocal self-similar balance. The lattice weight is the geometric target $w(n)=\varphi^{-n}$. The conversion map exhibits any such rule as field-for-field identical to a rung-dilution object from BIT kernel shape forcing.
Upstream, the rung dilution law is already forced: occupancy after $n$ rungs equals $\varphi^{-n}$, by induction from the zero-rung normalization and the one-rung self-similarity fixed point (which pins the single-step factor to $\varphi^{-1}$ by T6 uniqueness of scale).
proof idea
One-line term proof. Transport the weight rule across the structure map that reinterprets its fields as a rung-dilution record (occupancy := weight, positivity and composition and one-rung self-similarity copied verbatim). Apply the already-proved occupancy forcing theorem on that record at $n$, which yields $w(n)=\varphi^{-n}$. No separate induction is written here; the induction lives in the BIT kernel result.
why it matters
This is the lattice-layer forcing step of T9: the weight rule is forced to $\varphi^{-n}$. It feeds three parents in the same module. Uniqueness of the measure is the two-line rewrite that both rules equal the lattice weight, hence equal each other. The master certificate packages lattice forcing (this theorem), lattice uniqueness, continuum forcing, nonvacuousness, and Gibbs form. The one-statement T9 theorem conjoins lattice forcing with continuum $\rho^t$ forcing, partition function $\varphi^2$, mean rung $\varphi$, cost-blindness, and the BIT equilibrium band.
Framework role: after T5–T8 fix $J$, $\varphi$, the eight-tick octave, and $D=3$, T9 supplies the unique measure on recognition states. The same self-similar balance that forced $\varphi$ as scale now forces the geometric weight per step, equivalently the Gibbs rule with rate $\ln\varphi$ in the continuum layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.