Factorizes
plain-language theorem explainer
Defines the factorization premise for continuum weights: a real function f multiplies under addition of nonnegative costs. Anyone proving uniqueness of the geometric φ-measure (T9 continuum layer) cites this as the multiplicative Cauchy hypothesis. It is a pure Prop abbreviation, not a theorem.
Claim. A function $f:\mathbb{R}\to\mathbb{R}$ factorizes over cost addition when, for all $a,b\ge 0$, one has $f(a+b)=f(a)\,f(b)$.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain has fixed J, φ, the eight-tick period, and D=3. The continuum layer treats weight as a real function of additive cost. Two structural premises plus a calibrated step force the unique solution $f(t)=\varphi^{-t}$.
Factorization is the first continuum premise: independent cost increments multiply in weight. It is the continuous shadow of ledger cost additivity; a non-factorizing weight would encode correlation with no posting that pays for it. The companion premises are antitonicity on $[0,\infty)$ and the self-similar step $f(1)=\rho=\varphi^{-1}$.
The same multiplicative structure appears on the lattice as the discrete recognition-weight rule and, downstream, as the survival-fraction axiom in self-similar dressing for α-calibration.
proof idea
Pure definition: the body is the universal quantification stating $f(a+b)=f(a)f(b)$ for nonnegative reals. No proof obligations.
why it matters
This Prop is the first hypothesis of the continuum uniqueness theorem continuum_weight_forced: any factorizing, antitone $f$ with $f(1)=\varphi^{-1}$ equals $\varphi^{-t}$ for all $t\ge 0$. It is also discharged by the forced weight itself in contWeight_satisfies_premises, and is reused to obtain integer multiples (f_nmul), nonnegativity (f_nonneg_of_nonneg), and the rational case (f_rat).
Outside the module it appears as the factorization field of SelfSimilarDressing in α-genesis calibration forcing, tying gap-load survival to the same ledger premises. Within the Recognition framework it is the continuum half of T9: the geometric φ-measure (Gibbs form with rate fixed by self-similarity) rather than an externally chosen Born or Boltzmann weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.