measureForcingCert
plain-language theorem explainer
Master certificate packing T9: every admissible weighting of recognition states is the geometric φ-measure (φ⁻ⁿ on the lattice, exp(−(ln φ)·cost) in the continuum). Anyone citing the forced Born/occupancy rule, partition Z=φ², mean rung φ, chirality blindness, or the δw₀ equilibrium band uses this bundle. The body is a pure structure inhabitant wiring already-proved field lemmas.
Claim. There exists a completed T9 certificate: every lattice weight rule equals $w(n)=\varphi^{-n}$ and any two agree; every factorizing antitone continuum weight with step value $\varphi^{-1}$ equals $\varphi^{-t}$ for $t\ge 0$; the continuum weight is non-vacuous and equals $\exp(-(ln\varphi)\,t)$; the partition function is $\varphi^2$ with mean rung $\varphi$; the weight is cost-blind to chirality labels; and the BIT $\delta w_0$ window and equilibrium band $w_0\in(-0.896,-0.88)$ for $N\ge 8$ hold.
background
Module T9 closes the gap left by the T0–T8 forcing chain. That chain fixes the shape of the law (unique J-cost, φ as self-similar scale, eight-tick period, D=3) but not the weighting: given allowed recognition states, how much of reality sits in each? Born weights, chirality selection, δw₀ saturation, and rung occupancy are projections of that missing primitive.
On the lattice (fundamental, discrete layer), a weight rule must factorize over independent composition and obey per-step self-similar balance ρ=1/(1+ρ). The latter forces ρ=φ⁻¹ by the same reciprocal fixed-point uniqueness that pins T6, yielding w(n)=φ⁻ⁿ. Continuum weights of a real additive cost are forced by factorization, antitonicity, and calibration f(1)=φ⁻¹ to f(t)=φ⁻ᵗ, equivalently the Gibbs form exp(−(ln φ)·t).
MeasureForcingCert is the structure that packages lattice forcing and uniqueness, continuum forcing, non-vacuity, Gibbs form, partition and mean-rung identities, sub-Gaussian and chirality no-go facts, concrete lattice-weight instances (θ, ℏ, rung-44, BIT kernel), and the δw₀ window/equilibrium band into one certificate.
proof idea
Pure structure construction: each field of MeasureForcingCert is filled by an existing lemma. Lattice forcing and uniqueness delegate to RecognitionWeightRule.weight_forced and weight_unique. Continuum forcing is a direct apply of continuum_weight_forced (multiplicative Cauchy plus monotone uniqueness). Non-vacuity and Gibbs form are contWeight_satisfies_premises and contWeight_gibbs. Partition, ground share, mean rung, sub-Gaussian tail, and chirality blindness wire partitionZ_eq_phi_sq, probMass_zero, meanRung_eq_phi, sub_gaussian_in_J, and weight_blind_to_label. Instance fields point at the concrete lattice-weight witnesses (θ, ℏ, rung 44, kernel dilution). The δw₀ fields package the strict window bounds and the equilibrium band for N≥8. No new mathematics is proved here; the def only assembles the certificate.
why it matters
This is the single inhabited T9 master certificate: one unique weighting rule for recognition states, forced rather than fitted. It sits at the end of the same machinery that forced J (T5), φ (T6), the eight-tick octave (T7), and D=3 (T8), and answers the open instance-selection problems listed in the module doc (Born weights, chirality, δw₀, η_B prefactor, rung occupancy).
Downstream the certificate is the citation point for any claim that reality uses the geometric φ-measure, that the continuum form is Gibbs with rate ln φ, that Z=φ² and mean rung equals φ, or that BIT amplitude reduces to one integer inside the equilibrium band w₀∈(−0.896,−0.88) for N≥8. No used_by edges are recorded yet; the declaration is the terminal packaging of the measure-forcing development rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.