UniqueCostAxioms
plain-language theorem explainer
UniqueCostAxioms collects the symmetry under inversion, unit normalization, strict convexity on positives, calibration via second derivative, continuity, cosh-add identity and d'Alembert regularity conditions that force a cost function on positive reals to match Jcost. Researchers deriving the T5 uniqueness step in Recognition Science cite this bundle when applying the main theorem. The declaration is a structure definition that packages these properties into one hypothesis without performing derivations.
Claim. A function $F : ℝ → ℝ$ satisfies the axioms when $F(x) = F(x^{-1})$ for all $x > 0$, $F(1) = 0$, $F$ is strictly convex on $(0,∞)$, the second derivative of $F ∘ exp$ at 0 equals 1, $F$ is continuous on $(0,∞)$, $F$ obeys the cosh-add identity, and the shifted $H_F$ meets the continuous d'Alembert smoothness, ODE derivation, and regularity bootstrap conditions.
background
The CostUniqueness module consolidates results showing that the J-cost is the unique functional on positive reals obeying symmetry, normalization, convexity and calibration. The shifted cost is defined as $H(x) = J(x) + 1 = ½(x + x^{-1})$, under which the recognition composition law becomes the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. Upstream, the CoshAddIdentity encodes the cosh-type relation for the reparametrized function. Aczél's theorem states that continuous solutions to the d'Alembert equation are analytic and of the form cosh(λx). The ODE hypotheses derive that such functions satisfy $H'' = H$ with calibration $H''(0) = 1$, plus regularity bootstraps for smoothness.
proof idea
The declaration defines a structure that directly assembles the ten listed field properties into one Prop. No lemmas are applied; it functions as a hypothesis interface for the uniqueness theorems that follow.
why it matters
This bundle supplies the hypotheses for the main uniqueness statement on positives, which concludes that any such F equals Jcost on (0,∞), and for the axiom-free uniqueness theorem on the paper's RCL surface. It completes the T5 J-uniqueness step in the forcing chain by consolidating convexity, calibration and functional equation results. The construction leaves open whether the regularity hypotheses can be derived from the composition law alone without separate assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.