continuum_weight_forced
plain-language theorem explainer
Any real weight that multiplies under cost addition, decreases on [0,∞), and hits ρ=φ⁻¹ at unit cost must equal ρᵗ everywhere on the nonnegative reals. Continuum T9 uniqueness: the multiplicative Cauchy equation plus monotonicity pins the geometric measure with no extra regularity. Cited by the T9 master certificate and by alpha-genesis dressing/response forcing. Proof squeezes f(t) between rational powers via density and log trichotomy.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ factorize under nonnegative cost addition ($f(a+b)=f(a)f(b)$ for $a,b\ge 0$), be antitone on $[0,\infty)$, and satisfy the calibrated step $f(1)=\rho$ with $\rho=\varphi^{-1}$. Then for every $t\ge 0$, $f(t)=\rho^{t}=\varphi^{-t}$.
background
Module T9 closes the missing weighting rule after the T0–T8 shape chain (unique J-cost, φ-scale, eight-tick period, D=3). Lattice weights already force $w(n)=\varphi^{-n}$ from factorization plus the self-similar step $\rho=1/(1+\rho)$, which BIT kernel forcing identifies with $\rho=\varphi^{-1}$. The continuum layer treats weight as a function of a real additive cost.
Factorizes f is the multiplicative Cauchy law on the nonnegative cone: independent cost increments multiply weights. Antitonicity on $[0,\infty)$ is the only regularity used; the step calibration $f(1)=\rho$ pins the geometric base. Sibling facts supply $\rho\in(0,1)$ and the rational evaluation lemma that any such $f$ equals $\rho^{q}$ at every rational $q\ge 0$.
The continuum claim is the full uniqueness statement of T9's continuous layer: no a-priori power-law ansatz, only factorization, monotonicity, and the forced step.
proof idea
Case split on $t=0$ versus $t>0$. At zero, rewrite and apply the zero-evaluation lemma for factorizing antitone step-calibrated weights.
For $t>0$, set $L:=f(t)$. Antitonicity plus the rational-cast lemma give two sandwich families: if $t\le q$ then $\rho^{q}\le L$; if $0\le q\le t$ then $L\le\rho^{q}$. Positivity of $L$ follows from a rational above $t$.
Trichotomy on $L$ versus $\rho^{t}$. Equality is the goal. If $L<\rho^{t}$, take logs (using $\log\rho<0$), produce a rational $q>t$ with $\rho^{q}>L$, contradicting the upper sandwich. If $L>\rho^{t}$, produce a rational $0\le q<t$ with $\rho^{q}<L$, contradicting the lower sandwich. Density of rationals and the exp/log dictionary close both contradictions.
why it matters
This is the continuum half of T9: reality weights recognition states by the unique geometric φ-measure, equivalently the Gibbs rule $\propto\exp(-(ln\varphi)\cdot\mathrm{cost})$ with rate fixed by the self-similar ledger rather than chosen. It feeds t9_measure_forced (the one-statement T9 package) and the master certificate measureForcingCert, which records continuum uniqueness as continuum_forced.
Downstream alpha-genesis uses it directly: response_forced identifies every self-similar dressing response with the forced continuum weight, and dressedCoupling_forced then yields the form-(E) dressed coupling with no free calibration. That path is how the continuum measure enters the fine-structure constant band.
Framework landmark: after T5–T8 force J, φ, the eight-tick octave, and D=3, T9 forces the measure. Closing continuum uniqueness removes the last free weighting ansatz behind Born weights, rung occupancy, and related instance-selection problems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.