primitive_to_uniqueness_of_kernel
plain-language theorem explainer
Any function F satisfying the primitive cost hypotheses together with an Aczel regularity kernel on its shifted version HF must equal the canonical J-cost function for all positive reals. Recognition Science workers cite this as the public T5 uniqueness result that closes the forcing chain without JensenSketch. The term proof extracts normalization, continuity and d'Alembert properties from the input bundle, obtains smoothness from the kernel, and reduces directly to washburn_uniqueness.
Claim. Let $F : ℝ → ℝ$ satisfy the primitive cost hypotheses (reciprocal cost, normalized, satisfies the composition law, calibrated, and continuous on the positive reals). Suppose the shifted function $HF$ admits an Aczel regularity kernel. Then $F(x) = J_{cost}(x)$ for every $x > 0$.
background
The Aczel Classification module packages the d'Alembert segment of the forcing chain: continuous d'Alembert solutions are smooth and smoothness supplies the calibrated ODE kernel H'' = H. PrimitiveCostHypotheses bundles the five public assumptions: reciprocal cost, normalization, composition law, calibration, and continuity on the positive reals. AczelRegularityKernel packages the two regularity hypotheses (smoothness and ODE) extracted from the Aczel classification. Upstream, the shift H(x) := J(x) + 1 converts the recognition composition law into the standard d'Alembert equation.
proof idea
The term proof first obtains HF(0) = 1 via H_one_of_normalized, continuity of HF via H_continuous_of_positive_continuous, and the d'Alembert equation via H_dAlembert_of_composition. It then applies the smooth field of the supplied AczelRegularityKernel to deduce ContDiff smoothness of HF. Finally it invokes washburn_uniqueness on the five primitive fields together with the kernel's smooth and ode fields plus three ode_regularity lemmas derived from that smoothness.
why it matters
This supplies the official public T5 theorem with an explicit Aczel kernel seam and feeds directly into primitive_to_uniqueness_aczel and the public_cost_layer theorem. It completes the J-uniqueness step (T5) in the T0-T8 forcing chain of Recognition Science, where J(x) = (x + x^{-1})/2 - 1, ensuring the cost function is the unique solution under the listed hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.