probMass_zero
plain-language theorem explainer
The normalized probability of the zero-step recognition state equals φ⁻². Anyone deriving Born weights, rung occupancy, or the forced geometric measure on recognition states cites this as the vacuum share. The proof unfolds the geometric mass formula P(n)=(1−ρ)ρⁿ and rewrites via the golden identity 1−ρ=φ⁻².
Claim. The normalized probability mass at zero recognition steps is $P(0)=\varphi^{-2}$. Explicitly, with $P(n)=(1-\rho)\rho^{n}$ and $\rho=\varphi^{-1}$, one has $P(0)=(1-\rho)\rho^{0}=1-\rho=\varphi^{-2}$.
background
Module T9 forces the weighting on recognition states after T0–T8 have fixed the law’s shape (unique J-cost, φ-scale, eight-tick period, D=3). Any admissible lattice weight must factorize over independent composition and obey per-step self-similar balance ρ=1/(1+ρ), which pins ρ=φ⁻¹ and yields w(n)=φ⁻ⁿ.
The normalized probability mass is the geometric law P(n)=(1−ρ)ρⁿ. The companion identity one_sub_rho states that the normalization gap equals the inverse-square of the scale: 1−ρ=φ⁻². That gap is exactly the ground-state share once the n=0 power is evaluated.
Upstream, ρ is the forced single-step attenuation from BIT-kernel self-similarity; φ is the unique self-similar fixed point (T6). The continuum layer later rewrites the same rule as a Gibbs weight with rate ln φ.
proof idea
Term-mode rewrite after unfolding the definition. Expand P(0)=(1−ρ)ρ⁰; apply pow_zero to get ρ⁰=1, then mul_one to drop the unit factor, leaving 1−ρ. Finish by rewriting with the golden identity one_sub_rho : 1−ρ=1/φ². No case splits or induction.
why it matters
Closes the n=0 case of the forced geometric measure: the vacuum (ground-state) share on the recognition ladder is φ⁻², not a free parameter. Downstream it is consumed by measureForcingCert, the master certificate that packages lattice forcing, uniqueness, continuum Gibbs form, and nonvacuity for T9.
In the broader chain this is the discrete normalization step that turns the self-similar attenuation ρ=φ⁻¹ into a probability. Every later instance-selection problem listed in the module (Born weights, chirality, δw₀ saturation, η_B prefactor, rung occupancy) projects off this same geometric measure; fixing P(0) anchors the whole series Σ P(n)=1 with the φ-native gap.
Landmark contact: T6 uniqueness of φ, the reciprocal self-similarity fixed point, and the lattice half of T9’s forced measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.