prc_four_law_completeness
plain-language theorem explainer
Every continuous positive-log-curvature cost on (0,∞) that is reciprocal, normalized, and obeys the recognition composition law equals costLambda c for some c>0. Recognition theorists cite this as four-law completeness (T1′ closed): the solution set is exactly the gauge orbit. The proof is a one-line application of the calibratable completeness lemma to a fixed target package.
Claim. Assume the Aczél smoothness package. Let $F:(0,\infty)\to\mathbb{R}$ be continuous, reciprocal ($F(x)=F(1/x)$), normalized, and satisfy the recognition composition law. If the second derivative of its log-coordinate transform $G_F$ is strictly positive at $0$, then there exists $c>0$ such that $F(x)=\mathrm{cost}_\lambda(c,x)$ for all $x>0$.
background
In the Primitive Recognition Calculus, a native cost is a real function on positive ratios obeying four algebraic/analytic laws: reciprocity under $x\mapsto 1/x$, a normalization convention at the identity ratio, the Recognition Composition Law (the d'Alembert-type identity that forces the J-shape), and continuity on $(0,\infty)$. The log-coordinate transform $G_F$ converts multiplicative structure on ratios into an additive functional equation on $\mathbb{R}$.
Positive log-curvature means $G_F''(0)>0$: the cost bends away from the flat (trivial) solution. Under the Aczél smoothness package, every continuous d'Alembert solution with $H(0)=1$ is $C^\infty$, so the curvature hypothesis is well-defined and the classical classification (constants and cosh branches) applies.
The one-parameter family $\mathrm{cost}_\lambda(c,\cdot)$ is the gauge orbit of the canonical J-cost under multiplicative reparameterization of the ratio coordinate. Upstream completeness for calibratable targets already classifies solutions once a calibration hook is supplied; this theorem specializes that machinery to the four-law native-cost package.
proof idea
Term-mode one-liner. Apply cost_laws_complete_of_calibratable to the fixed target prc_four_law_completeness_target, feeding the five hypotheses (reciprocity, normalization, composition law, continuity on $(0,\infty)$, and positive second derivative of $G_F$ at $0$). No local case split or fresh analysis: the target packages the calibration data that the general completeness lemma needs, and the conclusion is exactly existence of $c>0$ with $F=\mathrm{cost}_\lambda(c,\cdot)$ pointwise on positives.
why it matters
Closes T1′ in the PRC native-cost uniqueness arc: every positive-curvature four-law solution lies in the gauge orbit ${\mathrm{cost}_\lambda(c):c>0}$. Paired with the converse inclusion (the scale family satisfies the laws), the solution set is exactly that orbit, so the only residual freedom is the calibration unit.
Immediate parent is prc_cost_freedom_is_one_real, which upgrades this existential statement to unique existence ($\exists!$), packaging free action, transitive gauge action, and surjectivity into the torsor claim that residual cost freedom is exactly one positive real. That is the program's forced-versus-assumed split for the cost: form forced by the four laws plus curvature; one positive real unit assumed.
Framework landmark: this is the PRC-side counterpart of T5 J-uniqueness and the RCL, stating that the composition law plus mild regularity pins the cost to the cosh/J family up to gauge. It does not yet fix the physical unit (that is a later calibration step).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.