probMass
plain-language theorem explainer
Normalized geometric probability mass on discrete recognition rungs: P(n)=(1−ρ)ρⁿ with ρ=φ⁻¹. Anyone citing the T9 forced-measure lattice law, mean rung depth, or Born-style occupancy uses this as the base distribution. It is a one-line definitional expansion of the forced per-step weight.
Claim. For each natural number $n$, the normalized probability mass at rung $n$ is $P(n)=(1-\rho)\,\rho^{n}$, where $\rho=\varphi^{-1}$ is the forced per-step recognition weight.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain. Those steps fix the shape of the law (unique J-cost, φ as scale, eight-tick period, D=3) but not how much of reality sits in each allowed recognition state. The lattice layer answers that with two premises: factorization over independent composition, and per-step self-similar balance ρ=1/(1+ρ).
The upstream constant ρ is defined as φ⁻¹. Self-similar attenuation forces that value: any other ratio would import a second scale and contradict T6 uniqueness. Unnormalized lattice weights are then w(n)=ρⁿ=φ⁻ⁿ. The continuum side recovers the same object as a Gibbs weight exp(−(ln φ)·cost).
probMass is the normalized geometric law built from that ρ: the factor (1−ρ) makes the masses sum to one over ℕ.
proof idea
Pure definition: expand as (1−ρ)·ρⁿ. No tactics or lemmas. Downstream positivity, normalization, and mean-rung proofs unfold this equation and apply geometric-series identities together with the elementary bounds 0<ρ<1.
why it matters
This is the concrete occupancy measure of T9. It feeds meanRung (⟨n⟩=Σ n·P(n)) and the exact identity meanRung_eq_phi, which states that mean recognition depth equals φ itself. Normalization (Σ P(n)=1), positivity, the ground-state share P(0)=φ⁻², and the saturation lemmas all quote it directly.
The master certificate MeasureForcingCert packages lattice forcing (every admissible weight rule is φ⁻ⁿ), uniqueness, continuum forcing, and the Gibbs form. Those clauses rest on this normalized mass as the probability-facing presentation of the forced geometric weight. In the broader framework it is the single primitive behind recurring instance-selection problems (Born weights, chirality, δw₀ saturation, η_B, rung occupancy).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.