PrimitiveCostHypotheses
plain-language theorem explainer
A bundle of five hypotheses on a cost function F enables the uniqueness identification with the J-cost in the Recognition Science T5 step. Researchers on the forcing chain cite this bundle when stating the public uniqueness theorem. The definition records reciprocity, normalization, the composition law, calibration, and continuity explicitly as a structure.
Claim. A function $F : (0,∞) → ℝ$ satisfies the primitive cost hypotheses if $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for all $x,y > 0$, $lim_{t→0} 2F(e^t)/t^2 = 1$, and $F$ is continuous on $(0,∞)$.
background
The Aczel Classification module packages the d'Alembert forcing chain supplied by the Aczel classification theorem: continuous d'Alembert solutions are smooth and the calibrated ODE kernel follows. Upstream definitions include reciprocal cost as $F(x) = F(1/x)$ for $x > 0$, normalized as $F(1) = 0$, the composition law as the Recognition Composition Law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for $x,y > 0$, calibrated as the limit condition equivalent to $G''(0) = 1$ for $G(t) = F(e^t)$, and continuity on the positive reals. This bundle replaces the earlier JensenSketch layer with explicit assumptions for the primitive-to-uniqueness route.
proof idea
The declaration is a structure definition that directly conjoins the five properties: reciprocity, normalization, satisfaction of the composition law, calibration, and continuity on $(0,∞)$. It serves as a packaging definition for downstream uniqueness theorems with no separate proof steps.
why it matters
This supplies the canonical input hypotheses for the T5 J-uniqueness theorem, feeding into the theorems that prove any such F equals the J-cost. It fills the primitive-to-uniqueness route in the Aczel package of the d'Alembert chain, corresponding to T5 in the T0-T8 forcing chain where J-uniqueness is forced. It supports the public cost layer in dimensional constraints and makes the seam with the Aczel regularity kernel explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.