f_ratCast
plain-language theorem explainer
Any factorizing, antitone weight on the nonnegative reals with unit step equal to φ⁻¹ agrees with the geometric measure φ⁻ᵗ at every nonnegative rational. Continuum uniqueness (T9) cites this to pass from the natural-number lattice case to dense rationals before closing by monotonicity. The proof rewrites the rational cast as a numerator/denominator quotient and applies the already-proved p/q case.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ factorize over addition on $[0,\infty)$ (i.e. $f(a+b)=f(a)f(b)$ for $a,b\ge 0$), be antitone on $[0,\infty)$, and satisfy $f(1)=\rho$ with $\rho=\varphi^{-1}$. Then for every rational $q\ge 0$, $f(q)=\rho^{q}$.
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 claim is that any admissible weight is the geometric $\varphi$-measure.
On the continuum layer the weight is a real function of additive cost. Factorization means $f(a+b)=f(a)f(b)$ for nonnegative $a,b$: the multiplicative shadow of ledger cost additivity. The calibrated step is $\rho:=\varphi^{-1}$, forced by reciprocal self-similarity. Antitonicity on $[0,\infty)$ supplies the regularity that pins the multiplicative Cauchy equation.
The sibling theorem for natural numerators and denominators already gives $f(p/q)=\rho^{p/q}$. The present result lifts that statement to an arbitrary nonnegative rational via the standard $\mathbb{Q}\to\mathbb{R}$ cast.
proof idea
Cast nonnegativity of the real image of $q$ back to $q\ge 0$ in $\mathbb{Q}$, hence $q.\mathrm{num}\ge 0$. Rewrite the real cast as $$(q:\mathbb{R})=(q.\mathrm{num}.\mathrm{toNat}:\mathbb{R})/(q.\mathrm{den}:\mathbb{R})$$ using $\mathrm{Rat.cast_def}$ and $\mathrm{Int.toNat_of_nonneg}$. Apply the sibling rational theorem $f_\mathrm{rat}$ to the pair $(q.\mathrm{num}.\mathrm{toNat},,q.\mathrm{den})$ with the nonzero-denominator hypothesis. The three structural hypotheses (factorization, antitonicity, unit step) are threaded through unchanged.
why it matters
This is the dense-rational bridge inside T9 continuum uniqueness. The parent theorem continuum_weight_forced states that any factorizing antitone weight with $f(1)=\varphi^{-1}$ equals $\varphi^{-t}$ for every real $t\ge 0$, with no a-priori power-law restriction: pure multiplicative Cauchy plus monotonicity. That proof splits $t=0$ from $t>0$ and needs the rational case on a dense set before antitonicity closes the gap.
In the broader framework this finishes the continuum half of the forced measure: lattice weights $w(n)=\varphi^{-n}$ already match BIT-kernel rung dilution; the continuum form is the Gibbs rule with rate $\ln\varphi$ pinned by T6 self-similarity, not chosen. Downstream instance-selection problems (Born weights, chirality, $\delta w_0$, $\eta_B$, rung occupancy) all project onto this single primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.