continuum_monotone_class_is_the_scale_family
plain-language theorem explainer
The monotone class of reciprocal, normalized, composition-law costs equals the one-parameter scale family. Continuum uniqueness arguments for the Recognition Composition Law cite this: every positive scale is admissible and continuous, and any monotone solution is some scale member. Proof is a term pair applying the full-scale-family admission lemma and the monotone-forces-scale lemma.
Claim. For every $l>0$, the scale-family cost $F_l$ is reciprocal ($F_l(x)=F_l(x^{-1})$), normalized ($F_l(1)=0$), obeys the Recognition Composition Law, and is continuous on $(0,\infty)$. Conversely, if $F:(0,\infty)\to\mathbb{R}$ is reciprocal, normalized, obeys the composition law, and the shifted cost $H_F$ is monotone on $[0,\infty)$, then there exists $c\in\mathbb{R}$ such that $F(x)=F_c(x)$ for all $x>0$.
background
The Recognition Composition Law (RCL) reads $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for $x,y>0$. Reciprocity is $F(x)=F(x^{-1})$ on positives; normalization is $F(1)=0$. The shifted cost $H_F(t)=G_F(t)+1$ with $G_F(t)=F(e^t)$ turns RCL into the d'Alembert identity $H(xy)+H(x/y)=2H(x)H(y)$. Classically $H(x)=\tfrac12(x+x^{-1})$ recovers $J(x)=H(x)-1$.
The scale family is the continuum of costs obtained by varying a real exponent parameter on the classical $J$-shape. T5 forces $J$ itself among continuous solutions; here the comparison is deliberately monotone against monotone, with no continuity or completeness on the converse side.
This module is the structural ledger for the primitive recognition calculus native cost: which algebraic and regularity hypotheses admit a continuum of solutions, and which pin the native cost.
proof idea
Term-mode pair constructor, no tactics. Left conjunct is a direct application of the lemma that the composition law admits the full positive scale family: every $l>0$ yields a reciprocal, normalized, RCL-satisfying cost continuous on $(0,\infty)$. Right conjunct applies the lemma that reciprocity, normalization, RCL, and monotonicity of $H_F$ on $[0,\infty)$ force $F$ to equal some single scale-family member. Continuity is used only on the forward inclusion.
why it matters
Feeds the structural stratification certificate, which packages uniqueness, slim contraction, positivity, and gauge inhabitation for the native-cost ledger. The doc-comment states the design choice explicitly: the honest continuum comparison is monotone against monotone, not monotone against continuous. That sits next to T5 $J$-uniqueness in the forcing chain and uses the RCL (and its $H$-form d'Alembert equation) as the algebraic engine. Without this double inclusion, the ledger could not separate the continuum scale family from discrete or non-monotone competitors when certifying the native cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.