prc_four_law_completeness_target
plain-language theorem explainer
Every positive-log-curvature solution of the four algebraic cost laws is gauge-equivalent to a calibrated (unit log-curvature) solution. Completeness arguments cite this to discharge the analytic blocker T1′. The proof lifts the composition law to a continuous d'Alembert equation for H = G+1, applies Aczél smoothness for C^∞, then rescales by the square root of the log-curvature at the origin.
Claim. Assume continuous d'Alembert solutions with $H(0)=1$ are $C^\infty$. If $F:\mathbb{R}\to\mathbb{R}$ is reciprocal and normalized, satisfies the composition law, is continuous on $(0,\infty)$, and has positive log-curvature $\frac{d^2}{dt^2}(F\circ\exp)(0)>0$, then there exists $c>0$ such that $x\mapsto F(x^{1/c})$ is calibrated (unit second log-derivative at the origin).
background
In the Primitive Recognition Calculus cost layer, a cost $F$ on positive reals is reciprocal ($F(x)=F(x^{-1})$), normalized ($F(1)=0$), and obeys the Recognition Composition Law. The log-chart transforms are $G F = F\circ\exp$ and $H F = G F + 1$. Under $H$, the composition law becomes the classical d'Alembert equation $H(t+u)+H(t-u)=2 H(t)H(u)$, with $H(0)=1$.
The module isolates four-law completeness: the positive-curvature solution set should be exactly the gauge orbit of calibrated costs. The Prop PRCFourLawCompletenessTarget is the remaining analytic step: every non-trivial four-law solution is gauge-equivalent to a calibrated one (unit log-curvature).
Upstream, composition_law_equiv_coshAdd converts the multiplicative law into a cosh-addition identity on $G$, and aczel_dAlembert_smooth (from AczelSmoothnessPackage) upgrades continuous d'Alembert solutions to $C^\infty$. That package encodes Aczél's classification: continuous solutions are constant or $\cosh(\lambda t)$.
proof idea
Introduce $G_F=F\circ\exp$ and $H_F=G_F+1$. Normalization plus the definitions give $H_F(0)=1$. Continuity of $F$ on $(0,\infty)$ yields continuity of $G_F$ and hence of $H_F$. The composition law is rewritten as a cosh-addition identity, then as a direct identity for $G_F$; a short ring calculation upgrades that to the d'Alembert equation for $H_F$.
Apply aczel_dAlembert_smooth to obtain $H_F\in C^\infty$, so $G_F$ is $C^\infty$ and twice differentiable. Set $c=\sqrt{G_F''(0)}>0$ from the curvature hypothesis. The gauge map $x\mapsto x^{1/c}$ sends $G_F$ to $t\mapsto G_F(t/c)$. The chain rule lemma deriv2_comp_mul_left_at_zero gives second derivative $c^{-2}\cdot\kappa=1$ at the origin, so the rescaled cost is calibrated.
why it matters
This declaration discharges T1′: the isolated analytic blocker for four-law completeness is now a theorem, not a hypothesis. Downstream, prc_four_law_completeness uses it to prove unconditionally that every positive-log-curvature four-law solution equals costLambda c for some $c>0$. Together with the reverse inclusion (the scale family sits inside the solution set), the positive-curvature solution set is exactly the gauge orbit.
In the Recognition forcing chain this pins the residual freedom of the native cost to a single positive calibration constant. That is the analytic half of J-uniqueness (T5): once calibration is fixed, the composition law forces the cosh form $J(x)=\frac{x+x^{-1}}{2}-1$. Nothing outside the gauge orbit satisfies the four laws under the stated regularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.