cost_laws_complete_of_calibratable
plain-language theorem explainer
Every continuous positive-log-curvature solution of the four algebraic cost laws equals a member of the gauge family cost_λ(c,·), once calibratability is assumed. Recognition theorists cite this to pin residual freedom of the native cost to a single positive scale. The proof rescales to unit curvature via the target hypothesis, applies calibrated J-uniqueness, and unwinds the identity cost_λ(c,x)=J(x^c).
Claim. Assume the Aczél smoothness package and the calibratability fact: every reciprocal, normalized, composition-satisfying, continuous-on-$(0,\infty)$ cost $F$ with positive second derivative of its log-coordinate transform at $0$ is gauge-equivalent to a calibrated cost. Then for any such $F$ there is $c>0$ with $F(x)=\mathrm{cost}_\lambda(c,x)$ for all $x>0$.
background
The Recognition Composition Law and its companions (reciprocity $F(x)=F(x^{-1})$, normalization $F(1)=0$, and continuity on $(0,\infty)$) constrain admissible cost functionals on positive reals. The canonical solution is the J-cost $J(x)=(x+x^{-1})/2-1$, forced under unit log-curvature by the calibrated uniqueness theorem (law_of_logic_forces_jcost). The gauge family is $\mathrm{cost}_\lambda(c,x)=J(x^c)$ for $c>0$.
Log-curvature is read from the second derivative at the origin of the log-coordinate transform $G F$. Positive curvature excludes the zero solution. The isolated analytic blocker PRCFourLawCompletenessTarget asserts that every such four-law solution is gauge-equivalent to a calibrated one: some $c>0$ makes $x\mapsto F(x^{1/c})$ have unit curvature.
This module sits in Primitive Recognition Calculus and isolates that blocker so the algebraic remainder of four-law completeness can be discharged independently of the analytic input.
proof idea
Apply the calibratability hypothesis to $F$ to obtain $c>0$ such that $\tilde F(y):=F(y^{1/c})$ is calibrated. Gauge invariance of the four laws under positive power rescaling (cost_laws_gauge_invariant at exponent $c^{-1}$) yields that $\tilde F$ is reciprocal, normalized, composition-satisfying, and continuous on $(0,\infty)$. Calibrated uniqueness (law_of_logic_forces_jcost) then gives $\tilde F=J$ on $(0,\infty)$.
For $x>0$, rewrite $F(x)=F((x^c)^{1/c})=J(x^c)$ by the power identity $(x^c)^{1/c}=x$, and finish with the gauge-orbit identity $\mathrm{cost}_\lambda(c,x)=J(x^c)$.
why it matters
This is the exact conditional half of four-law completeness: solutions ⊆ gauge orbit, given only the calibratability blocker. Downstream, prc_four_law_completeness removes the hypothesis and states the unconditional biconditional (with the converse family-inclusion already known): the positive-curvature four-law solution set is exactly ${\mathrm{cost}_\lambda(c):c>0}$.
In the forcing chain this locks T5-style J-uniqueness up to residual gauge: the calibration unit is the only free parameter left by the algebraic laws. Nothing outside the orbit can satisfy reciprocity, normalization, composition, continuity, and positive log-curvature. The sibling calculus lemma on second derivatives under left scaling supports transporting curvature across the same gauge substitution used here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.