PRCFourLawCompletenessTarget
plain-language theorem explainer
Isolates the single analytic gap for four-law cost completeness: every continuous reciprocal normalized composition-law cost with positive log-curvature is gauge-equivalent to a unit-calibrated cost. Completeness theorems cite this Prop as the calibratability hypothesis. It is a pure statement of existence of a positive rescaling exponent, not a proved theorem.
Claim. For every $F:\mathbb{R}\to\mathbb{R}$ that is a reciprocal cost, normalized, satisfies the recognition composition law, is continuous on $(0,\infty)$, and has positive second log-derivative at the origin ($G_F''(0)>0$ where $G_F(t)=F(e^t)$), there exists $c>0$ such that $x\mapsto F(x^{1/c})$ is calibrated: its log-curvature equals $1$.
background
In the Primitive Recognition Calculus cost track, admissible costs obey four algebraic laws: reciprocity $F(x)=F(x^{-1})$, normalization $F(1)=0$, the Recognition Composition Law, and continuity on the positive reals. The log reparametrization is $G_F(t)=F(e^t)$; calibration means $G_F''(0)=1$ (unit log-curvature at the identity).
The existing FunctionalEquation pipeline classifies calibrated continuous solutions as the J-cost (equivalently $\cosh-1$ after the log change of variables), baking $c=1$ into d'Alembert from the start. Uniqueness up to gauge therefore needs one extra fact: every positive-curvature four-law solution can be rescaled onto the calibrated slice.
This definition packages exactly that missing analytic claim as a named Prop, so completeness can be stated conditionally without smuggling an unproved classification.
proof idea
No proof: this is a definition of a proposition. The body is the universal quantification over four-law continuous $F$ with $G_F''(0)>0$, asserting existence of $c>0$ making $x\mapsto F(x^{1/c})$ calibrated. Downstream, prc_four_law_completeness_target discharges it via the free-frequency d'Alembert analysis and positivity; cost_laws_complete_of_calibratable consumes it as a hypothesis.
why it matters
Closes the honest terminal form of four-law completeness in the PRC native-cost uniqueness module. Parent theorem cost_laws_complete_of_calibratable turns this Prop into the inclusion ${\text{four-law solutions}}\subseteq{\mathrm{costLambda},c:c>0}$; with the reverse inclusion from the full-scale family, the solution set is exactly the gauge orbit of $J$. That pins residual freedom to the calibration unit alone, feeding T5 J-uniqueness and the RCL forcing chain.
The companion prc_four_law_completeness_target later proves the Prop under the Aczel smoothness package, converting the conditional completeness into an unconditional theorem. Isolating the blocker here keeps the analytic gap explicit rather than hidden inside a sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.