meanRung
plain-language theorem explainer
Defines the mean occupied rung ⟨n⟩ as the expectation Σ n·P(n) under the forced geometric measure on recognition depths. Anyone citing T9 measure forcing, partition-function identities, or the per-event entropy keystone uses this scalar. It is a one-line tsum definition, not a proved identity; equality to φ is the next theorem.
Claim. The mean occupied rung is $\langle n\rangle := \sum_{n=0}^{\infty} n\, P(n)$, where $P(n)=(1-\rho)\rho^n$ is the normalized geometric probability mass at lattice depth $n$ and $\rho=\varphi^{-1}$.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain has fixed cost shape $J$, scale $\varphi$, eight-tick period, and $D=3$. Admissible lattice weights factorize over independent steps and obey per-step self-similar balance $\rho=1/(1+\rho)$, which forces $\rho=\varphi^{-1}$ and $w(n)=\varphi^{-n}$.
The normalized masses are the geometric law $P(n)=(1-\rho)\rho^n$ (probMass). The mean rung is the first moment of that discrete law: ordinary expectation of depth under the forced measure. Continuum cousins use the same rate as a Gibbs weight $\exp(-(ln\varphi)\cdot t)$ on additive cost.
Upstream, probMass supplies the summands; the geometric parameter $\rho$ is the unique self-similar attenuation already forced by BIT-kernel shape arguments and T6 uniqueness of $\varphi$.
proof idea
Definitional, not a proof. The body is the single tsum $\sum' n\cdot\mathrm{probMass}(n)$ over $\mathbb{N}$. Downstream proofs unfold this name, rewrite $n\cdot P(n)=(1-\rho),n\rho^n$, pull out the constant factor, and evaluate the arithmetico-geometric series to obtain $\langle n\rangle=\varphi$.
why it matters
T9 needs not only the weight rule but its first moments. The master certificate and the one-line T9 statement both list $\mathrm{meanRung}=\varphi$ beside partition function $Z=\varphi^2$, lattice forcing $w(n)=\varphi^{-n}$, and continuum Gibbs form. The equality theorem meanRung_eq_phi is the immediate consumer.
Holography uses the same moment: forced per-event entropy equals $(\varphi+2)\log\varphi$, obtained by rewriting Shannon entropy through mean depth $\varphi$ and normalization of $P$. That pins a concrete information capacity per recognition event once the measure is forced.
In the broader chain this is the weighting half of the ledger: T5–T8 fix $J$, $\varphi$, octave, and dimension; T9 fixes how much mass sits on each rung, with mean depth exactly the golden ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.