rho_lt_06212
plain-language theorem explainer
The forced per-step recognition weight ρ = φ⁻¹ is strictly less than 0.6212. Cosmologists and measure-forcing arguments cite this as a concrete decimal bound on the geometric φ-measure step. The proof unfolds ρ, clears the positive denominator, and finishes by nonlinear arithmetic from the library bound φ > 1.61.
Claim. Let $\rho := \varphi^{-1}$ be the forced per-step recognition weight. Then $\rho < 0.6212$.
background
Module T9 forces the weighting on recognition states after the T0–T8 chain has fixed the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$). Any admissible weight factorizes over independent composition and obeys the single-step self-similar balance $\rho = 1/(1+\rho)$, which pins $\rho = \varphi^{-1}$.
Here $\rho$ is defined exactly as $1/\varphi$. The constant $\varphi$ is the golden ratio forced by T6; the library already records the tight numerical lower bound $\varphi > 1.61$. Because $\rho$ is the reciprocal, that lower bound on $\varphi$ immediately yields an upper bound on $\rho$.
Sibling facts already give $\rho > 0$, $\rho < 1$, and the lattice weight $w(n) = \rho^n = \varphi^{-n}$. The present inequality is the decimal fuel for saturation and dark-energy deviation estimates that need a concrete number rather than the symbolic $\varphi^{-1}$.
proof idea
Unfold the definition $\rho = 1/\varphi$. Rewrite the goal via div_lt_iff₀ using positivity of $\varphi$, converting $\rho < 0.6212$ into $1 < 0.6212,\varphi$. Discharge the resulting linear inequality by nlinarith from the upstream lemma $\varphi > 1.61$ (since $1/1.61 < 0.6212$). No further structure is used.
why it matters
T9 identifies the geometric $\varphi$-measure as the unique admissible weighting of recognition states. Concrete decimal control on the step weight is required before one can bound occupancy tails and equilibrium deviations from $\Lambda$CDM.
Downstream, rho_pow_nine_lt lifts the bound by monotonicity of $x\mapsto x^9$ on $[0,\infty)$ to obtain $\rho^9 < 0.014$, so nine rungs already exhaust more than 98% of the measure. The same bound feeds deltaW0_gt_004: for every occupancy depth $N$, the equilibrium dark-energy deviation satisfies $\delta w_0(N) > 0.04$. A confirmed $|w_0+1| < 0.04$ would therefore falsify equilibrium T9 occupancy (not T9 itself).
In the forcing chain this sits after T5–T6 ($J$-uniqueness and $\varphi$ as the self-similar fixed point) and supplies the numerical hinge between the abstract weight rule and observational exclusion statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.