f_nmul
plain-language theorem explainer
Under additive factorization on the nonnegative reals, antitonicity on [0,∞), and unit step f(1)=ρ=φ⁻¹, natural scaling is pure powering: f(kx)=f(x)^k for every natural k and every x≥0. Continuum-measure derivations that lift the lattice geometric weight cite this. Proof is induction on k, using the zero lemma f(0)=1 and factorization at the successor step.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ factorize over addition on the nonnegative reals ($f(a+b)=f(a)f(b)$ for $a,b\geq 0$), be antitone on $[0,\infty)$, and satisfy $f(1)=\rho$ with $\rho=\varphi^{-1}$. Then for every $x\geq 0$ and every $k\in\mathbb{N}$, $f(kx)=f(x)^k$.
background
Module T9 (MeasureForcing) closes the weighting gap left by T0–T8. Those steps force the shape of the law (unique J-cost, φ-scale, eight-tick period, D=3) but not how much of reality sits in each allowed recognition state. The module derives that any admissible weight is the geometric φ-measure: weight φ⁻¹ per step, or Gibbs with rate fixed by the self-similar ledger.
On the continuum layer, a candidate weight f of real additive cost must factorize over cost addition on the nonnegative domain, be antitone there, and match the forced per-step weight at unit cost. Factorization means f(a+b)=f(a)f(b) whenever a,b≥0: the multiplicative shadow of ledger cost additivity. The constant ρ is defined as 1/φ, forced by the reciprocal self-similarity fixed point ρ=1/(1+ρ).
The upstream zero lemma already gives f(0)=1 under the same three hypotheses, by specializing factorization at (0,0) and using antitonicity to discard the zero root.
proof idea
Fix x≥0 and induct on the natural multiplier k. The base k=0 is the upstream zero lemma under the same factorization, antitonicity, and unit-step hypotheses, yielding f(0)=1. For the successor, rewrite (k+1)x = kx + x by push_cast and ring, record kx≥0 by positivity, apply factorization to obtain f(kx+x)=f(kx)·f(x), substitute the inductive hypothesis, and close with the power-successor identity. Antitonicity and the unit-step value are not used in the inductive step; they travel only to discharge the zero case.
why it matters
Integer scaling is the bridge from continuum factorization axioms to the geometric law f(t)=ρ^t. The immediate parent is the rational-case theorem, which obtains f(p/q)=ρ^(p/q) by uniqueness of positive q-th roots and applies this powering identity on numerator and denominator scales. Together they feed the continuum forcing that any admissible weight equals the geometric φ-measure, closing T9.
That weighting is the common primitive behind Born weights, chirality selection, δw₀ saturation, the η_B prefactor, and rung occupancy. The lattice side already forces w(n)=φ^{-n} by the same factorization-plus-self-similar-balance argument used for BIT kernel rung dilution; this lemma is the matching continuum step for natural multiples of a real cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.