meanRung_eq_phi
plain-language theorem explainer
The mean recognition depth under the forced geometric measure equals the golden ratio φ exactly. Anyone citing T9 measure forcing or the per-event entropy keystone needs this identity. The proof reduces the expectation of a geometric law with ratio ρ = φ⁻¹ to the closed form ρ/(1−ρ), which collapses to φ by self-similarity.
Claim. The expected recognition rung under the forced probability mass equals the golden ratio: $\langle n \rangle = \varphi$, where $\langle n \rangle = \sum_{n=0}^{\infty} n\,P(n)$ and $P$ is the geometric measure with per-step weight $\rho = \varphi^{-1}$ (so $P(n) = (1-\rho)\rho^n$).
background
Module T9 closes the missing weighting rule on recognition states after the T0–T8 shape chain (unique J-cost, φ-scale, eight-tick period, D = 3). Any admissible lattice weight must factorize over independent composition and obey the single-step self-similarity balance ρ = 1/(1+ρ), which forces ρ = φ⁻¹ and weights w(n) = φ⁻ⁿ.
The associated probability mass is the normalized geometric law P(n) = (1−ρ)ρⁿ. The mean rung is the expectation ∑ n P(n). Sibling facts pin the ingredients: ρ > 0, ρ < 1, and the identity 1−ρ in terms of φ (via one_sub_rho), so the series is absolutely convergent.
Upstream, φ ≠ 0 is the only Constants lemma needed for the final algebraic cleanup; the geometric-series API supplies the closed form ∑ n rⁿ = r/(1−r)² for ‖r‖ < 1.
proof idea
Unfold the mean as ∑ n·P(n). Pointwise, n·P(n) = (1−ρ)·(n ρⁿ), so factor (1−ρ) out of the tsum. Norm bound ‖ρ‖ < 1 follows from ρ > 0 and ρ < 1, unlocking the standard sum ∑ n ρⁿ = ρ/(1−ρ)². The product collapses to ρ/(1−ρ). Rewrite via the sibling identity for 1−ρ and the definition ρ = φ⁻¹, then field_simp with φ ≠ 0 yields φ. The inline comment records the arithmetic: (1−ρ)·ρ/(1−ρ)² = ρ/(1−ρ) = φ⁻¹·φ² = φ.
why it matters
This is one of the four numeric anchors inside the single T9 statement t9_measure_forced: lattice weights forced, continuum weights forced, partition function Z = φ², and mean rung = φ. The master certificate measureForcingCert packages the same facts.
Downstream holography uses it as a keystone. Per-event entropy equals (φ+2) log φ precisely because the Shannon sum splits into (mean rung)·log φ plus a normalization term; forcedEntropy_eq cites this identity together with ∑ P = 1. The per-term law −log P(n) = (n+2) log φ is the matching local ingredient.
In the broader RS chain, T6 already forced φ as the unique self-similar scale; T9 shows that the same φ is not only the step weight but also the mean depth of the forced measure. That closes the instance-selection gap (Born weights, rung occupancy, η_B prefactor) under one geometric rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.