partitionZ_eq_phi_sq
plain-language theorem explainer
The partition function of the forced geometric measure on recognition steps equals φ² exactly. Anyone citing T9 measure forcing, normalized lattice weights, or mean-rung identities needs this closed form. The proof is a short rewrite: geometric-series summation under ρ<1, then the golden identity 1−ρ=φ⁻².
Claim. The partition function $Z=\sum_{n=0}^{\infty}\rho^n$ equals $\varphi^2$, where $\rho=\varphi^{-1}$ is the forced per-step recognition weight (so $0\le\rho<1$).
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain: once J, φ, the eight-tick period, and D=3 are fixed, which measure sits on allowed recognition states remains open. The lattice answer is geometric: weight ρ per independent recognition step, with ρ forced to φ⁻¹ by reciprocal self-similarity (the same fixed point that pins the BIT kernel rung dilution).
Here partitionZ is the raw sum $Z=\sum_{n\ge0}\rho^n$. Upstream, rho_nonneg and rho_lt_one give the geometric-series hypotheses, and one_sub_rho records the golden identity $1-\rho=\varphi^{-2}$ ("the normalization gap of the forced measure is the inverse-square of the scale"). The continuum side later reads the same object as a Gibbs weight with rate $\ln\varphi$.
proof idea
Unfold partitionZ to the tsum $\sum_n\rho^n$. Apply Mathlib's tsum_geometric_of_lt_one with rho_nonneg and rho_lt_one to obtain $1/(1-\rho)$. Rewrite via one_sub_rho so the denominator is $\varphi^{-2}$, then one_div and inv_inv yield $\varphi^2$. Pure algebraic closed form; no induction or analysis beyond the geometric series.
why it matters
T9's one-statement theorem t9_measure_forced lists four concrete identities; this is the partition-function clause ($Z=\varphi^2$), paired with mean rung $\varphi$. The master certificate measureForcingCert packages lattice uniqueness, continuum forcing, and Gibbs form; normalized probabilities $P(n)=(1-\rho)\rho^n$ sit on this $Z$.
Framework-wise it ties the forced scale from T6 (φ as self-similar fixed point) to the measure layer: the same φ that gates the ledger also normalizes occupancy. The doc-comment flags a BRIDGE observation that this φ² matches the emergent voice-density gate, while the equality proved here is internal and unconditional. Closes the normalization half of the open instance-selection problems named in the module (Born weights, rung occupancy, η_B prefactor).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.