probMass_eq_inv_pow
plain-language theorem explainer
The forced recognition measure has closed form P(n) = φ^{-(n+2)} for every depth n. Anyone working the Shannon entropy of one recognition event cites this identity. The proof unfolds the geometric mass, substitutes the golden identities 1−ρ=φ^{-2} and ρ=φ^{-1}, and simplifies.
Claim. For every natural number $n$, the forced probability mass satisfies $P(n) = \varphi^{-(n+2)}$, where $\varphi$ is the golden ratio and $P(n)=(1-\rho)\rho^n$ with $\rho=\varphi^{-1}$.
background
Module RecognitionEventCapacity rebuilds the holographic access bound as the information content of one recognition event under the T9 forced measure, not as an orbit count. The deflation test killed the naive eight-states-per-site quotient; the physical bound is forced-measurement outcome quantization.
In Foundation.MeasureForcing, the per-step weight is $\rho=\varphi^{-1}$ and the normalized mass is $P(n)=(1-\rho)\rho^n$. The golden identity one_sub_rho states $1-\rho=\varphi^{-2}$ (normalization gap equals the inverse-square of the scale). Together these already imply a pure inverse power of $\varphi$; this theorem records that closed form.
The module's central numbers (forced entropy $(\varphi+2)\log\varphi$, effective outcomes $\varphi^{\varphi+2}$, bits per event) all rest on this mass law and its log-weight consequence.
proof idea
Term-mode algebraic reduction. Unfold $P(n)=(1-\rho)\rho^n$, rewrite $1-\rho$ by one_sub_rho to $\varphi^{-2}$, unfold $\rho=\varphi^{-1}$, then apply div_pow, one_pow, and pow_add to obtain $\varphi^{-2}\cdot\varphi^{-n}=\varphi^{-(n+2)}$. Non-vanishing of $\varphi$ (from positivity) lets field_simp finish.
why it matters
Feeds neglog_probMass immediately: $-\log P(n)=(n+2)\log\varphi$, the per-term log-weight law linear in recognition depth. That identity is the bridge from the geometric mass to Shannon entropy, and thence to forcedEntropy_eq, effectiveOutcomes_eq, and bitsPerEvent_eq.
In the Recognition framework this is the closed form of the T9 forced measure used as the physical alphabet of one recognition event. It replaces the spurious hard ceiling of 8 orbit states by a parameter-free geometric law whose perplexity is $\varphi^{\varphi+2}\approx 5.70$. The module is explicit that entropy is average channel capacity, not zero-error distinguishability; the Born bridge from this measure to recognition Hilbert space remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.