MeasureForcingCert
plain-language theorem explainer
T9 master certificate for the forced geometric measure on recognition states: every admissible lattice weight is φ^{-n}, continuum factorizing antitone weights are φ^{-t}, with uniqueness, Gibbs form, Z=φ², and θ, ℏ, rung-44, kernel dilution as instances. Cite for Born/occupancy weights, chirality no-go, or δw₀ bounds. Pure structure of named fields; inhabitance is separate.
Claim. A certificate that: every recognition weight rule satisfies $w(n)=\rho^n$ with $\rho=\varphi^{-1}$; any two rules agree; every factorizing antitone $f$ on $[0,\infty)$ with $f(1)=\rho$ equals $\rho^t$; the continuum weight is non-vacuous and equals $\exp(-(\ln\varphi)\,t)$; partition $Z=\varphi^2$, ground share $\varphi^{-2}$, mean rung $\varphi$; sub-Gaussian Born bound via $J$; cost-sufficient weights are chirality-blind; $\theta=\varphi^{-4}$, $\hbar=\varphi^{-5}$, $\varphi^{-44}$, and rung dilution are lattice instances; $\delta w_0$ lies in $(0.04,J(\varphi))$ and near-ceiling for $N\ge 8$.
background
After T0–T8 force the shape of the law (unique $J$-cost, $\varphi$ scale, eight-tick period, $D=3$), the open gap is weighting: which rule assigns mass to each recognition state. This module derives that any admissible weighting is the geometric $\varphi$-measure (weight $\varphi^{-1}$ per step, equivalently Gibbs with rate fixed by the self-similar ledger).
A recognition weight rule is a positive $w:\mathbb{N}\to\mathbb{R}$ that factorizes under addition (multiplicative shadow of ledger cost additivity) and whose single-step weight obeys reciprocal self-similar balance $\rho=1/(1+\rho)$, forcing $\rho=\varphi^{-1}$. Continuum factorization is $f(a+b)=f(a)f(b)$ on nonnegative reals. A cost-sufficient weight factors through cost alone, so equal-cost mirror labels get equal weight.
Upstream, rung dilution is the identical structure for cosmic aging attenuation; native $\hbar$ is defined as $\varphi^{-5}$; $J(x)=(x+x^{-1})/2-1$.
proof idea
This declaration is a structure (interface contract), not a proved theorem. It enumerates the fifteen fields that constitute the T9 master certificate. Inhabitation is discharged by the downstream definition measureForcingCert, which wires each field to a prior lemma: lattice forcing and uniqueness from weight_forced / weight_unique on recognition weight rules; continuum forcing from continuum_weight_forced; non-vacuity and Gibbs form from the continuum weight premises and contWeight_gibbs; partition, ground share, mean rung, sub-Gaussian, chirality no-go, constant instances ($\theta$, $\hbar$, rung-44, kernel), and $\delta w_0$ window/band from the corresponding proved equalities and inequalities. No new proof body lives here.
why it matters
This is the T9 master certificate (dated 2026-06-09). It unifies every recurring instance-selection problem in the library (Born weights, chirality selection, $\delta w_0$ saturation, $\eta_B$ prefactor, rung occupancy) as projections of one forced measure. Downstream, measureForcingCert inhabits the structure and is the single citation point for the whole package.
Framework landmarks: T6 $\varphi$ uniqueness pins the step weight via reciprocal self-similarity; the same factorization that forced BIT kernel rung dilution forces lattice weights (via the conversion exhibiting the two objects as identical); constants $\theta=\varphi^{-4}$ and $\hbar=\varphi^{-5}$ become lattice weights at rungs 4 and 5; rung-44 matches the baryogenesis scale. Closes the open weighting primitive left after the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.