primitive_to_uniqueness_of_kernel
plain-language theorem explainer
Any function F satisfying the primitive cost hypotheses (reciprocity, normalization, composition law, calibration, and continuity on positives) whose shifted version H F carries an Aczél regularity kernel must coincide with the canonical J-cost on positive reals. Researchers closing the T5 uniqueness step in Recognition Science cite this result to bridge the composition law to explicit form. The term proof extracts H F at zero, continuity, and the d'Alembert equation from the hypotheses, obtains smoothness via the kernel, and applies washburn_
Claim. Let $F : (0,∞) → ℝ$ satisfy reciprocity, normalization, the composition law, calibration, and continuity. Let the shifted function $H(F)$ admit an Aczél regularity kernel supplying smoothness and the ODE property. Then $F(x) = J(x)$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
PrimitiveCostHypotheses bundles the five assumptions (IsReciprocalCost, IsNormalized, SatisfiesCompositionLaw, IsCalibrated, ContinuousOn positives) that form the public T5 input surface. AczelRegularityKernel packages the two outputs of the Aczel classification: a smoothness implication for continuous d'Alembert solutions and the passage from that smoothness to the calibrated ODE H'' = H. The local module packages the d'Alembert forcing chain so that downstream exclusivity code depends only on the kernel rather than the raw Aczel axiom. Upstream, H is the shifted cost H(x) = J(x) + 1 under which the recognition composition law becomes the standard d'Alembert equation.
proof idea
The term proof first obtains H F 0 = 1 via H_one_of_normalized, continuity of H F via H_continuous_of_positive_continuous, and the d'Alembert functional equation via H_dAlembert_of_composition. It then feeds these into the kernel's smooth field to produce ContDiff ℝ ⊤ (H F). Finally it applies washburn_uniqueness to the five primitive hypotheses together with the kernel's smooth and ode fields and the three ode_regularity lemmas derived from smoothness.
why it matters
This is the official public T5 theorem with an explicit Aczél kernel seam, allowing the rest of the Recognition Science surface to cite uniqueness without touching JensenSketch or the raw Aczel axiom. It directly feeds primitive_to_uniqueness_aczel (the convenience form) and public_cost_layer in the dimensional constraints module. The declaration closes the T5 J-uniqueness step of the forcing chain (T0–T8) by using the Aczel package to convert continuous d'Alembert solutions into the explicit cosh(log x) – 1 form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.