probMass_pos
plain-language theorem explainer
The geometric probability mass at every finite recognition step count n is strictly positive. Anyone building the forced φ-measure (Born weights, rung occupancy, continuum Gibbs form) needs this positivity lemma. The proof unfolds P(n)=(1−ρ)ρⁿ and multiplies the two strict inequalities 1−ρ>0 and ρⁿ>0.
Claim. Let $\rho=\varphi^{-1}$. For every natural number $n$, the normalized probability mass $P(n)=(1-\rho)\rho^{n}$ satisfies $P(n)>0$.
background
Module T9 closes the missing weighting rule on recognition states after the T0–T8 forcing chain has fixed J, φ, the eight-tick period, and D=3. Admissible weights factorize over independent composition and obey per-step self-similar balance, which forces the single-step factor ρ=φ⁻¹ and the lattice weights w(n)=ρⁿ.
The normalized probability mass is the geometric law P(n)=(1−ρ)ρⁿ. Here ρ:=1/φ is already known to be positive and strictly less than one (from φ>1). The factor (1−ρ) is the normalizing constant of the infinite geometric series Σ ρⁿ, so positivity of each mass is the elementary gate before proving Σ_n P(n)=1 and before any continuum Gibbs identification.
proof idea
Unfold the definition P(n)=(1−ρ)ρⁿ. From ρ<1 obtain 1−ρ>0 by linear arithmetic. From ρ>0 obtain ρⁿ>0 by the standard power-positivity lemma. Conclude with the product of two positive reals.
why it matters
Positivity of every lattice mass is the first arithmetic fact in the forced geometric measure: without it the φ-measure cannot serve as a probability on recognition states, and the module’s claim that every admissible weighting is this geometric law would be empty at the measure level.
It sits immediately upstream of the normalization identity Σ P(n)=1 (the next declaration in the file) and of the continuum layer that identifies the same rule with the Gibbs weight exp(−(ln φ)·cost). Framework-wise it is the measure-side counterpart of T6 (φ uniqueness) and of the BIT-kernel rung dilution: the same ρ=φ⁻¹ that balances the ledger now appears as a strictly positive geometric step weight. No downstream dependents are recorded yet; the lemma is infrastructure for the T9 normalization and continuum bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.