contWeight_satisfies_premises
plain-language theorem explainer
The continuum weight w(t)=ρ^t with ρ=φ^{-1} satisfies the three continuum premises of measure forcing: it factorizes over nonnegative cost addition, is antitone on [0,∞), and hits ρ at unit cost. Anyone citing continuum uniqueness or the non-vacuity half of MeasureForcingCert needs this witness. The proof is a three-field term packing standard real-power identities.
Claim. Let $\rho=\varphi^{-1}$ and $w(t)=\rho^t$. Then $w$ factorizes on nonnegative arguments ($w(a+b)=w(a)w(b)$ for $a,b\ge 0$), is antitone on $[0,\infty)$, and $w(1)=\rho$.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain has fixed the shape of the law (unique J-cost, φ-scale, eight-tick period, D=3). Lattice weights are forced to $w(n)=\varphi^{-n}$; the continuum layer asks the same question for a real-valued additive cost.
The continuum premises are: factorization over cost addition on the nonnegative domain (Factorizes), antitonicity on $[0,\infty)$, and the unit-step normalization $w(1)=\rho$ with $\rho=\varphi^{-1}$ the forced per-step weight. The candidate continuum weight is the pure power $w(t)=\rho^t=\varphi^{-t}$.
These three conditions are exactly the hypotheses of the continuum uniqueness theorem in the same module; inhabiting them shows the uniqueness statement is non-vacuous.
proof idea
Term-mode triple constructor. Factorization is Real.rpow_add at base $\rho>0$ (from rho_pos). Antitonicity on $[0,\infty)$ is Real.rpow_le_rpow_of_exponent_ge using $\rho>0$ and $\rho\le 1$ (from rho_le_one). The unit evaluation is Real.rpow_one. No custom lemmas beyond the positivity/bound facts already proved for $\rho$.
why it matters
This is the non-vacuity witness for continuum measure forcing. Downstream, measureForcingCert records it as nonvacuous, and CalibrationForcing.canonical builds a SelfSimilarDressing whose factorizes and antitone fields are the first two conjuncts of this theorem.
In the Recognition framework it anchors T9: after T5–T8 force J, φ, the eight-tick octave and D=3, the weighting of recognition states is forced to the geometric φ-measure (Gibbs form $\propto\exp(-(\ln\varphi)\cdot\mathrm{cost})$). Without a concrete function meeting the continuum premises, uniqueness would be empty. The Born-regime section that follows uses the same weight as the L² seed of the still-open Born bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.