primitive_to_uniqueness_aczel
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness without the Aczél smoothness assumption.
- Does not apply to non-positive arguments.
- Does not derive the smoothness property itself.
- Does not address functions that violate normalization or the composition law.
formal statement (Lean)
116theorem primitive_to_uniqueness_aczel [AczelSmoothnessPackage] (F : ℝ → ℝ)
117 (hF : PrimitiveCostHypotheses F) :
118 ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
proof body
Term-mode proof.
119 primitive_to_uniqueness_of_kernel F hF (aczelRegularityKernel (H F))
120
121end FunctionalEquation
122end Cost
123end IndisputableMonolith