f_zero
plain-language theorem explainer
Any factorizing, antitone weight on nonnegative costs with single-step value φ⁻¹ must send cost 0 to 1. Continuum uniqueness (T9) and the natural-number power law cite this as the t=0 base case. The proof is a short algebraic fork: factorization gives f(0)=f(0)², antitonicity plus positivity of ρ force f(0)>0, so the only solution is f(0)=1.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ factorize over addition on the nonnegative reals ($f(a+b)=f(a)f(b)$ whenever $a,b\ge 0$), be antitone on $[0,\infty)$, and satisfy $f(1)=\varphi^{-1}$. Then $f(0)=1$.
background
Module T9 forces the weighting on recognition states after the T0–T8 chain has fixed the shape of the law (unique $J$, scale $\varphi$, eight-tick period, $D=3$). The missing primitive is which measure sits on allowed states. The continuum layer treats weight as a real function of additive cost.
Factorization means independent cost increments multiply weights: $f(a+b)=f(a)f(b)$ for $a,b\ge 0$. That is the multiplicative shadow of ledger cost additivity. The calibrated step is $\rho:=\varphi^{-1}$, forced by reciprocal self-similarity ($\rho=1/(1+\rho)$) and T6 uniqueness of $\varphi$; rho_pos records $\rho>0$.
Antitonicity on $[0,\infty)$ encodes that higher cost cannot raise weight. Together these premises pin the continuum Gibbs rule $f(t)=\varphi^{-t}$.
proof idea
Apply factorization at $(0,0)$ to obtain $f(0)=f(0)\cdot f(0)$. Antitonicity on $0\le 1$ with the step calibration $f(1)=\rho$ yields $f(0)\ge\rho$. Positivity of $\rho$ upgrades this to $f(0)>0$.
Rearrange the square identity to $f(0)(f(0)-1)=0$. The real zero-product property splits cases: $f(0)=0$ contradicts positivity, so $f(0)=1$. The argument is pure ordered-field arithmetic (nlinarith/linarith); no analysis beyond the three hypotheses.
why it matters
This is the $t=0$ anchor of T9 continuum uniqueness. Parent continuum_weight_forced states that any factorizing antitone $f$ with $f(1)=\varphi^{-1}$ equals $\varphi^{-t}$ for all $t\ge 0$; its zero-cost case is exactly $f(0)=1=\rho^0$. Sibling f_nmul reuses the same hypotheses to get $f(kx)=f(x)^k$ for natural $k$, the bridge from the step to the full exponential.
Framework-wise, T9 closes the weighting gap left by T5–T8: once $J$ and $\varphi$ are forced, the measure must be geometric with ratio $\varphi^{-1}$ (equivalently Gibbs with rate $\ln\varphi$). Downstream Born-rule routes and instance-selection problems (chirality, rung occupancy, $\eta_B$) inherit this normalization so probability mass at zero cost is one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.