f_rat
plain-language theorem explainer
Any nonnegative real map that multiplies under cost addition, is antitone on [0,∞), and sends 1 to ρ=φ⁻¹ must send every rational p/q to ρ^{p/q}. Continuum measure-forcing cites this to pin the geometric weight on nonnegative rationals before density extends it. The argument reduces to uniqueness of positive q-th roots after the integer scaling identity.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy $f(a+b)=f(a)f(b)$ for all $a,b\ge 0$, be antitone on $[0,\infty)$, and obey $f(1)=\rho$ with $\rho=\varphi^{-1}$. Then for all $p,q\in\mathbb{N}$ with $q\ne 0$, $f(p/q)=\rho^{p/q}$.
background
Module T9 (MeasureForcing) supplies the missing weighting rule left open by the T0–T8 chain. Lattice recognition already forces per-step weight ρ=φ⁻¹; the continuum layer asks which real functions of additive cost are admissible weights. The three premises are: factorization over cost addition on the nonnegative domain, antitonicity on [0,∞), and the single-step normalization f(1)=ρ.
Factorization means f(a+b)=f(a)f(b) whenever a,b≥0: the multiplicative shadow of ledger cost additivity. Here ρ is defined as 1/φ. Upstream, the integer scaling law already gives f(k·x)=f(x)^k for natural k, and nonnegativity of f on the nonnegative ray is established so that real roots are well-defined.
proof idea
Set x=p/q≥0. Integer scaling yields f(q·x)=f(x)^q. The argument simplifies to p, and scaling at the unit step gives f(p)=ρ^p, hence f(x)^q=ρ^p. The geometric candidate satisfies the same power identity: (ρ^x)^q=ρ^p. Both sides are nonnegative, and q≠0, so left-injectivity of the map t↦t^q on [0,∞) forces f(x)=ρ^x.
why it matters
T9 closes the single open primitive after T0–T8: once J, φ, the eight-tick octave, and D=3 are forced, which measure sits on recognition states? This rational identity is the bridge from lattice weights w(n)=φ^{-n} to the continuum geometric law f(x)=ρ^x. Downstream, the ℚ-cast form lifts the statement to rational casts, the natural interface for density arguments that finish continuum forcing. It is the continuum counterpart of the forced lattice weight rule and the BIT-kernel rung dilution, with the rate pinned by T6 uniqueness of φ rather than chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.