primitive_to_uniqueness_aczel
plain-language theorem explainer
Any function F satisfying the primitive cost hypotheses (reciprocity, normalization, composition law, calibration, and continuity on positives) equals the J-cost function on positive reals. Recognition Science researchers cite this at the T5 uniqueness step when they invoke the Aczél smoothness package to close the regularity seam automatically. The proof is a one-line wrapper that builds the AczelRegularityKernel from the shifted cost H and delegates to the kernel-based uniqueness theorem.
Claim. Let $F:ℝ→ℝ$ satisfy reciprocity, normalization, the composition law, calibration, and continuity on $(0,∞)$. Then $F(x)=J(x)$ for all $x>0$, where $J(x)=½(x+x^{-1})-1$.
background
The Aczel Classification module packages the d'Alembert forcing chain: continuous solutions of the shifted-cost equation are smooth, after which the calibrated ODE kernel follows. PrimitiveCostHypotheses bundles the canonical T5 inputs as a single Prop: reciprocal-cost, normalized, composition law, calibrated, and continuous on the positive reals. The upstream AczelSmoothnessPackage states that any continuous solution of H(t+u)+H(t-u)=2 H(t) H(u) with H(0)=1 is C^∞; the H function is the shifted cost H(x)=J(x)+1.
proof idea
The proof is a one-line wrapper that applies primitive_to_uniqueness_of_kernel to F and its hypotheses after constructing the regularity kernel via aczelRegularityKernel (H F).
why it matters
This supplies the public interface to T5 J-uniqueness in the forcing chain, where J(x)=(x+x^{-1})/2-1. It feeds the kernel-based uniqueness theorem and lets later steps (T6 phi fixed point, T7 eight-tick octave) proceed without separate regularity arguments. The Aczél smoothness package closes the seam so downstream exclusivity code depends only on the calibrated kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.