rho_pos
plain-language theorem explainer
The forced per-step recognition weight ρ = φ⁻¹ is strictly positive. Anyone building lattice or continuum weights, Gibbs forms, or α-residual closing loads cites this as the base positivity fact. The proof unfolds the definition and applies positivity of quotients from 1 > 0 and φ > 0.
Claim. Let $\rho := \varphi^{-1}$ be the forced per-step recognition weight. Then $0 < \rho$.
background
Module T9 (MeasureForcing) closes the missing weighting rule after the T0–T8 forcing chain: once J, φ, the eight-tick period, and D = 3 are fixed, one still needs which measure sits on recognition states. The lattice answer is geometric dilution by a single per-step factor ρ.
That factor is defined by rho := 1/φ, the reciprocal of the golden-ratio scale forced at T6. The module premises (factorization over independent composition, and the self-similar balance ρ = 1/(1+ρ)) pin ρ = φ⁻¹ uniquely; positivity of ρ is the first arithmetic fact needed before powers, logs, and continuum extensions.
Upstream, ρ is just the constant 1/φ. Downstream uniqueness theorems calibrate continuum weights by the step condition f(1) = ρ and rewrite ρ^t as the Gibbs form exp(−(ln φ)·t).
proof idea
One-line term proof after unfolding. Expand ρ to 1/φ, then apply the standard positivity lemma for quotients: numerator 1 is positive and denominator φ is positive (from the Constants/PhiSupport layer), so the quotient is positive.
why it matters
T9's entire measure story rests on ρ ∈ (0,1). This lemma supplies the lower bound. In-module parents include continuum_weight_forced (uniqueness of f(t) = ρ^t under factorization, antitonicity, and f(1) = ρ), contWeight_gibbs (the exp(−(ln φ)·t) form, which rewrites via rpow_def_of_pos rho_pos), contWeight_satisfies_premises, latticeWeight_pos, and f_zero.
Outside the module it feeds AlphaGenesis residual targets: log_rho_ne_zero uses rho_pos with rho_lt_one to get log ρ < 0; corrected_eq_codata_iff and corrected_at_closingLoad use the strict decrease of the dressed α⁻¹ load that follows from ρ < 1 and ρ > 0. Framework landmark: the geometric φ-measure of T9, the missing primitive behind Born weights, rung occupancy, and the α band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.