partitionZ
plain-language theorem explainer
Defines the lattice partition function as the geometric series Z = Σ_{n≥0} ρ^n with ρ = φ⁻¹. Anyone citing the T9 forced measure or the identity Z = φ² needs this normalization constant. The body is a one-line tsum definition, not a proof.
Claim. The partition function is the real number $Z := \sum_{n=0}^{\infty} \rho^n$, where $\rho = \varphi^{-1}$ is the forced per-step weight.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain: J-cost uniqueness, φ as self-similar scale, eight-tick period, and D = 3. Shape is forced; the measure on recognition states is not, until this module.
The lattice layer takes two premises only: factorization over independent composition, and per-step self-similar balance ρ = 1/(1+ρ). The latter pins ρ = φ⁻¹ (via BIT kernel self-similar attenuation), so admissible weights are w(n) = φ⁻ⁿ.
rho is that forced per-step weight 1/φ. The partition function sums the unnormalized geometric weights over all rung counts n ∈ ℕ, giving the total mass before normalization to a probability measure P(n) = (1−ρ)ρⁿ.
proof idea
Pure definition: partitionZ is the topological sum ∑' n : ℕ, rho ^ n. No tactics, no lemmas. Convergence and closed form are deferred to partitionZ_eq_phi_sq, which rewrites the geometric tsum under rho_nonneg and rho_lt_one, then simplifies via one_sub_rho to φ².
why it matters
Supplies the normalization constant named in the T9 master certificate and in t9_measure_forced: reality weights states by φ⁻¹ per step (lattice) or exp(−(ln φ)·cost) (continuum), with partition function exactly φ² and mean rung φ.
Downstream, partitionZ_eq_phi_sq proves Z = φ² exactly (theorem, not bridge). That identity is listed as clause 3 of the one-statement T9 theorem and as item in MeasureForcingCert. Numerically φ² also gates emergent voice density elsewhere; the doc flags that link as bridge observation while keeping Z = φ² as theorem here.
Closes the open instance-selection primitive (Born weights, chirality, δw₀, η_B, rung occupancy) by fixing the total mass of the forced geometric measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.