rho_ne_one

Module T9 forces the weighting on recognition states after the T0–T8 chain has fixed the shape of the law (unique cost J, scale φ, eight-tick period, D = 3). The missing primitive is which measure sits on the allowed states. The lattice layer answers with a factorizing, self-similar weight rule, which pins the single-step factor to ρ = φ⁻¹.

Here ρ is defined as 1/φ. Upstream, rho_lt_one already shows ρ < 1 from φ > 1 and positivity of φ. The golden-ratio fixed point φ = 1 + 1/φ is the unique positive solution of the reciprocal self-similarity balance that BIT-kernel forcing supplies; any other ratio would import a second scale and contradict T6.

Geometric-sum identities for cumulative mass need the common ratio unequal to 1. That is the only role of the present lemma: convert the strict bound into a disequality usable by the field and sum APIs.

One-line term proof. Apply the standard lemma that a < b implies a ≠ b, instantiated at the already-proved fact ρ < 1. No unfolding of ρ or φ is required at this step; those reductions live inside rho_lt_one.

Feeds the closed-form saturation identity in the same module: saturation N = 1 − ρ^(N+1). That proof rewrites the finite geometric sum and must discharge ρ ≠ 1 (and the companion ρ − 1 ≠ 0) before field simplification. Without the disequality the geometric-sum API does not fire.

In the broader T9 story this is bookkeeping, not a new physical claim: the measure is already forced to be the geometric φ-weight w(n) = φ⁻ⁿ. The lemma simply keeps the algebraic pipeline honest so that probability-mass and saturation formulas close without sorry. It sits downstream of the self-similar attenuation that forces ρ = φ⁻¹ and upstream of every identity that treats the lattice weight as a proper geometric series.