rho_le_one
plain-language theorem explainer
The forced per-step recognition weight ρ = φ⁻¹ satisfies ρ ≤ 1. Anyone proving continuum weight premises or saturation monotonicity cites this non-strict bound. The proof is a one-line lift of the already-proved strict inequality ρ < 1.
Claim. Let $\rho = \varphi^{-1}$ be the forced per-step recognition weight. Then $\rho \leq 1$.
background
Module T9 (MeasureForcing) closes the missing weighting rule on recognition states after the T0–T8 shape chain. Lattice weights factorize over independent steps and obey the self-similar balance ρ = 1/(1+ρ), which forces ρ = φ⁻¹; continuum weights are the matching Gibbs form with that same rate.
Here ρ is defined as 1/φ. Upstream, rho_lt_one already shows ρ < 1 from φ > 1 and positivity of φ. The non-strict order on the reals is the usual ≤; the ArithmeticFromLogic and IntegerRational le edges are ambient order infrastructure, not the content of the claim.
proof idea
One-line wrapper: apply the standard strict-to-nonstrict coercion .le to rho_lt_one. No new arithmetic; the work sits in rho_lt_one (unfold ρ, rewrite by div_lt_one using φ > 0, then one_lt_phi).
why it matters
T9 needs ρ ≤ 1 as a premise ingredient, not just ρ < 1. Downstream, contWeight_satisfies_premises uses it to get antitonicity of the continuum weight on [0,∞) via Real.rpow_le_rpow_of_exponent_ge (with ρ > 0), discharging non-vacuity of the continuum uniqueness theorem. saturation_monotone uses it in pow_le_pow_of_le_one so higher lattice cutoffs shrink residual mass. Both sit on the geometric φ-measure path (weight φ⁻ⁿ per step, Gibbs rate ln φ) that answers Born weights, δw₀ saturation, and rung occupancy from one primitive. Landmark link: T6 uniqueness of φ as the self-similar scale pins ρ = φ⁻¹ < 1, hence ≤ 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.