composition_law_monotone_forces_costLambda
plain-language theorem explainer
Any reciprocal, normalized cost obeying the Recognition Composition Law whose log-transform is monotone on the nonnegative reals equals a single member of the scale family costLambda on the positive reals. Completeness is never used. Downstream uniqueness and the order-only forcing of J cite this as the monotone half of the continuum classification. The proof reduces to the cosh-family form and rewrites through the shifted cost H.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be reciprocal ($F(x)=F(x^{-1})$ for $x>0$), normalized ($F(1)=0$), and satisfy the composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$. Write $H_F(t)=F(e^{t})+1$. If $H_F$ is monotone on $[0,\infty)$, then there exists $c\in\mathbb{R}$ such that $F(x)=\cosh(c\log x)-1$ for all $x>0$.
background
In the Primitive Recognition Calculus cost layer, admissible costs are real functions on the positive reals obeying three algebraic axioms: reciprocal symmetry, normalization at the identity, and the Recognition Composition Law (RCL). The shifted transform $H_F(t)=F(e^t)+1$ converts RCL into d'Alembert's functional equation $H(xy)+H(x/y)=2H(x)H(y)$. Under the CostAlgebra convention, $H(x)=J(x)+1=\tfrac12(x+x^{-1})$ for the canonical recognition cost $J$.
The scale family is $F_c(x)=\cosh(c\log x)-1$, written costLambda c in the development. Continuity of $F$ on $(0,\infty)$ already forces membership in this family; the present result replaces continuity by monotonicity of $H_F$ on $[0,\infty)$, so the argument is completeness-free. The immediate upstream lemma is the cosh-family form: the same hypotheses yield $H_F(t)=\cosh(c,t)$ for some $c$.
proof idea
One-step reduction to the cosh-family theorem. Apply composition_law_monotone_forces_cosh_family to obtain $c$ with $H_F(t)=\cosh(c,t)$ for all real $t$. For fixed $x>0$, write $x=e^{\log x}$. Unfolding $H_F(\log x)=F(x)+1$ and the identity $G(\mathrm{costLambda},c)(\log x)=\cosh(c\log x)$ (via G_costLambda) gives $F(x)+1=\cosh(c\log x)$. Subtracting 1 recovers $F(x)=\mathrm{costLambda},c,x$. The arithmetic is pure rewriting and linarith; no analytic estimates appear.
why it matters
This is the §9 family-form payoff of the monotone uniqueness track: every order-regular RCL cost is some costLambda c, with residual freedom exactly one real scale parameter. Combined with injectivity of the positive-exponent map (the next capstone in the module), the monotone class is faithfully parameterized by a single positive real, irreducible by any order-only datum.
Downstream, continuum_monotone_class_is_the_scale_family packages both inclusions of the continuum comparison; Jcost_forced_by_monotonicity and law_of_logic_forces_jcost_monotone specialize to the recognition cost $J$ (with calibration $c=1$ recovering $J$ exactly); costLambda_successor_increment_tendsto reads the calibration invariant $c^2$ off the discrete $\delta$-act ladder for the whole family. In the forcing chain this sits under T5 J-uniqueness: monotonicity alone, without completeness, already pins costs to the cosh-log family whose unit-calibrated member is $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.