t9_measure_forced
plain-language theorem explainer
T9 packages the unique admissible weighting of recognition states: lattice weight φ⁻ⁿ per step, continuum weight φ⁻ᵗ under factorization and antitonicity, partition function φ², mean rung φ, cost-blind chirality, and the BIT equilibrium band w₀ ∈ (−0.896, −0.88) for N ≥ 8. Cite it as the single measure-forcing statement after the T0–T8 shape chain. The proof is a six-conjunct term that assembles already-proved layer lemmas.
Claim. The following hold simultaneously: (i) every recognition weight rule (positive, factorizing over independent steps, with single-step reciprocal self-similar balance) satisfies $w(n)=\rho^n$ with $\rho=\varphi^{-1}$; (ii) every $f:\mathbb{R}\to\mathbb{R}$ that factorizes over nonnegative cost addition, is antitone on $[0,\infty)$, and has $f(1)=\rho$ equals $\rho^t$ for all $t\ge 0$; (iii) the partition function is $\varphi^2$ and the mean rung is $\varphi$; (iv) any cost-sufficient weight on labeled states is blind to the chirality label; (v) for occupancy $N\ge 8$, $-1+\delta w_0(N)\in(-0.896,-0.88)$.
background
Module T9 closes the 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 the weighting of allowed recognition states. 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 map $w:\mathbb{N}\to\mathbb{R}$ that factorizes under independent composition and whose single-step weight obeys the reciprocal self-similar balance $\rho=1/(1+\rho)$. That balance, via the BIT kernel self-similar attenuation result, forces $\rho=\varphi^{-1}$. On the continuum, factorization means $f(a+b)=f(a)f(b)$ for $a,b\ge 0$; with antitonicity and the calibrated step $f(1)=\rho$, the multiplicative Cauchy equation yields $f(t)=\rho^t$.
Cost-sufficiency says the weight depends only on cost, not on labels. The equilibrium amplitude is $\delta w_0(N)=J(\varphi)\cdot\mathrm{saturation}(N)$, reducing a free real to one integer occupancy depth.
proof idea
Pure term-mode packaging: a six-tuple of already-proved facts, no new tactics.
- Lattice uniqueness: apply
RecognitionWeightRule.weight_forcedpointwise. - Continuum uniqueness: apply
continuum_weight_forced(factorizing + antitone + $f(1)=\rho$ implies $f(t)=\rho^t$). - Partition function:
partitionZ_eq_phi_sq. - Mean rung:
meanRung_eq_phi. - Chirality no-go:
weight_blind_to_label(cost-sufficient weights equalize mirror labels). - Equilibrium band:
equilibrium_w0_bandfor $N\ge 8$, giving $-1+\delta w_0(N)\in(-0.896,-0.88)$.
Each conjunct is discharged by naming the corresponding upstream lemma; the theorem is the single conjunction that states T9 in one place.
why it matters
This is the canonical T9 statement: after T0–T8 force the shape of the law, T9 forces the measure. The module doc frames it as the unique geometric $\varphi$-measure (weight $\varphi^{-1}$ per recognition step, equivalently Gibbs with rate $\ln\varphi$ pinned by the self-similar ledger). Landmarks engaged: T6 ($\varphi$ uniqueness via the reciprocal fixed point), the BIT kernel shape-forcing that pins $\rho=\varphi^{-1}$, and the eight-tick floor $N\ge 8$ in the equilibrium band.
No downstream consumers are wired yet (used_by empty); the declaration is the export surface for the whole MeasureForcing module. The equilibrium band is jointly conditional on the H-theorem reading of $\delta w_0$ and is observationally falsifiable by DESI Y3+/Roman/Euclid outside $(-0.896,-0.88)$. Chirality blindness closes the cost-sufficiency no-go: no weight that factors through cost can select a preferred mirror label.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.