prc_cost_freedom_is_one_real
plain-language theorem explainer
Every continuous positive-curvature solution of the four recognition cost laws equals the scaled native cost for exactly one positive calibration constant. The residual gauge freedom is therefore a torsor under one positive real, with no redundancy. Anyone quantifying forced-versus-assumed structure in the PRC cost cites this. Existence comes from four-law completeness; uniqueness is a single-point match at ratio 2.
Claim. Assume the Aczél smoothness package. Let $F:(0,\infty)\to\mathbb{R}$ be reciprocal, normalized ($F(1)=0$), satisfy the recognition composition law, be continuous on the positive reals, and have positive curvature at the identity (i.e. the second derivative of $t\mapsto F(e^t)$ at $0$ is positive). Then there is a unique $c>0$ such that $F(x)$ equals the scaled native cost at calibration $c$, for every $x>0$.
background
In the Primitive Recognition Calculus the cost on positive ratios is constrained by four laws: reciprocity, normalization $F(1)=0$, the Recognition Composition Law (RCL), and continuity on $(0,\infty)$, plus a positive-curvature condition. The log reparametrization $G_F(t)=F(e^t)$ converts the RCL into a d'Alembert equation; the curvature hypothesis is $G_F''(0)>0$. The Aczél smoothness package supplies that continuous d'Alembert solutions are $C^\infty$, so the second derivative is well-defined.
The scaled native family $\mathrm{cost}\lambda(c,\cdot)$ is the one-parameter orbit of the canonical J-cost under multiplicative recalibration. Upstream, four-law completeness already produces some $c>0$ with $F=\mathrm{cost}\lambda(c,\cdot)$ on positives. The present result upgrades that existence to unique existence, packaging free action, transitive gauge action, and surjectivity into a single torsor statement.
proof idea
Existence is a direct appeal to four-law completeness under the same five hypotheses (reciprocity, normalization, composition, continuity, positive curvature), which yields some $c>0$ with $F=\mathrm{cost}_\lambda(c,\cdot)$ pointwise on positives.
For uniqueness, take any other $d>0$ that also reproduces $F$. Evaluating both calibrations at the fixed distinction ratio $x_0=2>1$ gives $\mathrm{cost}\lambda(d,2)=\mathrm{cost}\lambda(c,2)$. The single-point calibration lemma then forces $d=c$: two positive exponents that agree at one point strictly above 1 are identical. No further analysis is needed; the argument is pure packaging of free action, transitivity, and the prior existence theorem.
why it matters
This is the exact quantification of residual cost freedom in the PRC: the four laws plus positive curvature force the cost form, and exactly one positive-real unit remains free, uniquely pinned by $F$ itself. It sits on the T5 J-uniqueness landmark (the RCL forces the cosh-log shape) and makes the gauge orbit a torsor with no redundancy.
Downstream it feeds the full stratification certificate, which discharges the PRC strength layers field-by-field with no project-local axioms, and the successor-increment limit that shows the discrete $\delta$-act ladder sees exactly the calibration invariant $c^2$. Together those close the "what is forced versus assumed" ledger for native cost uniqueness on the continuous completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.