rho_nonneg

Module T9 (MeasureForcing) closes the weighting gap left by the T0–T8 forcing chain. That chain fixes the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$) but not how much of reality sits in each allowed recognition state. The module derives that any admissible weight factorizes over independent composition and obeys the single-step self-similar balance $\rho=1/(1+\rho)$, which forces $\rho=\varphi^{-1}$.

Here $\rho$ is defined as the real $1/\varphi$. Strict positivity $\rho>0$ is already available from positivity of $\varphi$ and of the unit. The present statement only weakens that to the closed inequality $0\le\rho$, the form demanded by Mathlib geometric-series and power lemmas.

One-line wrapper: apply the real-order lemma that turns a strict inequality $0<\rho$ into the weak inequality $0\le\rho$. No unfolding of $\rho$ or of $\varphi$ is required; the work sits entirely in rho_pos.

This inequality is the nonnegativity gate for the forced geometric measure. Downstream it is fed directly into the geometric sum that proves the partition function equals $\varphi^2$ exactly, into normalization $\sum P(n)=1$, into monotonicity and limit-one of cumulative saturation, into the numerical bound $\rho^9<0.014$, and into the rational uniqueness argument for continuum weights $f(p/q)=\rho^{p/q}$. It also appears in the holography identity for forced entropy. In framework terms it is a T9 primitive supporting the claim that the Gibbs rate is pinned by the self-similar ledger rather than chosen.