f_nonneg_of_nonneg
plain-language theorem explainer
If a real map factorizes over addition on the nonnegative reals, it is nonnegative there. Continuum-layer measure forcing cites this before matching values on rationals to the geometric φ-weight. The proof rewrites f(x) as a square via equal-half factorization.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy $f(a+b)=f(a)f(b)$ whenever $a,b\ge 0$. Then $f(x)\ge 0$ for every $x\ge 0$.
background
Module T9 (MeasureForcing) closes the weighting gap left by T0–T8: those steps force J-cost uniqueness, φ as scale, the eight-tick period, and D=3, but not which measure sits on recognition states. The continuum layer treats weight as a real function of additive cost.
The named hypothesis is factorization on the nonnegative domain: $f(a+b)=f(a)f(b)$ for $a,b\ge 0$. Module text calls this the multiplicative shadow of ledger cost additivity—independent composite steps multiply weights, else a correlation appears with no posting that pays for it.
Sibling continuum premises (antitonicity, $f(1)=\rho$ with $\rho=\varphi^{-1}$) are not used here; they enter only when identifying the explicit form of $f$.
proof idea
Apply factorization at the equal split $a=b=x/2$ (both nonnegative when $x\ge 0$). The sum identity $x/2+x/2=x$ rewrites the left side as $f(x)$, so $f(x)=f(x/2)\cdot f(x/2)$. A product of a real with itself is nonnegative by the standard square lemma. Purely algebraic; no analysis or uniqueness lemmas.
why it matters
Parent use is f_rat: with factorization, antitonicity, and $f(1)=\rho$, one gets $f(p/q)=\rho^{p/q}$ by uniqueness of positive $q$-th roots. That rational identification is the bridge from the discrete lattice rule $w(n)=\varphi^{-n}$ (forced by factorization plus step self-similarity $\rho=1/(1+\rho)$) to the continuum Gibbs form $\propto\exp(-(\ln\varphi)\cdot\mathrm{cost})$.
In the T9 program this is a small but load-bearing positivity gate: without nonnegativity the root-uniqueness step that pins the rational values fails. Downstream it supports the claim that every admissible weighting is the geometric φ-measure (weight $\varphi^{-1}$ per recognition step), closing instance-selection gaps (Born weights, rung occupancy, etc.) under the same machinery that forced J and the BIT kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.