bridge_to_existing_jcost_uniqueness
plain-language theorem explainer
Any continuous positive-real cost F that is reciprocal, normalized, calibrated, and obeys the Recognition Composition Law equals the classical J-cost J(x)=(x+x^{-1})/2-1, once Aczél smoothness is assumed. PRC cites this to hand off its rational cost surface to the existing continuous uniqueness theorem. The proof is a one-line term wrapper that installs the Aczél package and applies law_of_logic_forces_jcost.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be continuous on $(0,\infty)$, reciprocal ($F(x)=F(x^{-1})$), normalized ($F(1)=0$), calibrated ($G''(0)=1$ for $G(t)=F(e^t)$), and satisfy the Recognition Composition Law. Assume the Aczél smoothness package (continuous d'Alembert solutions are $C^\infty$). Then for every $x>0$, $F(x)=J(x)$ where $J(x)=(x+x^{-1})/2-1$.
background
In Recognition Science the cost of a positive ratio is the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The FunctionalEquation module packages the Recognition Composition Law (RCL) together with the standard side conditions: reciprocity, normalization $F(1)=0$, and calibration $G''(0)=1$ for $G(t)=F(e^t)$. Continuity on $(0,\infty)$ is the remaining analytic hypothesis.
The Aczél smoothness package records that every continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^\infty$; the classification is the constant $1$ and the family $\cosh(\lambda t)$. That regularity commitment is kept as an explicit quantified hypothesis rather than a silent axiom.
This module (Primitive Recognition Calculus / PRC J-cost) builds a rational cost surface on ratio orbits and needs a clean bridge from that discrete surface to the classical continuous uniqueness theorem already proved for $J$.
proof idea
Term-mode one-line wrapper. The proof first rebinds the incoming Aczél smoothness hypothesis as a local instance of AczelSmoothnessPackage, then applies Cost.FunctionalEquation.law_of_logic_forces_jcost to $F$ with the five remaining hypotheses (reciprocal, normalized, composition law, calibrated, continuous on positives). No extra algebraic work is done here; all force-to-$J$ content lives upstream in that lemma.
why it matters
This is the real-domain uniqueness theorem currently used by PRC. It closes the handoff from the rational PRC cost surface to the continuous $J$-uniqueness already in the Cost stack (the T5 landmark: $J$ is the unique calibrated reciprocal RCL cost). Downstream, prc_jcost_certificate packages the rational formula, real bridge, reciprocity, normalization, and canonical RCL into a single certificate, quoting this theorem as the real bridge. Separately, PRCRecognizerLawOfLogicBridgeTarget_proved is literally an intro-and-apply of this result, discharging the recognizer-side Law-of-Logic bridge target. Without the explicit Aczél package in the signature, the PRC certificate would hide a regularity commitment; keeping it quantified makes the bridge honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.