Jcost_is_normalized
plain-language theorem explainer
Jcost satisfies the normalization condition F(1) = 0 required by the Recognition Composition Law. Researchers deriving the unique cost functional from the forcing chain would cite this to confirm Jcost meets the unit calibration axiom. The proof is a direct one-line application of the evaluation lemma establishing Jcost(1) equals zero.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the cost functional on positive reals.
background
The Cost Uniqueness module consolidates results from Convexity, Calibration, and FunctionalEquation toward the main theorem T5: any cost functional F satisfying symmetry, unit normalization, strict convexity, and calibration must equal Jcost on positive reals. Jcost is defined by the explicit formula J(x) = (x-1)^2/(2x), which is equivalent to cosh(log x) - 1. IsNormalized is the predicate F(1) = 0. The upstream Composition axiom states that for all positive x, y, F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y), the multiplicative form of d'Alembert's equation.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0, which directly shows Jcost(1) = 0 by simplification of the explicit formula for Jcost.
why it matters
This result confirms that Jcost satisfies the normalization condition (F(1) = 0) from the Composition axiom and the IsNormalized predicate in DAlembert.Inevitability. It serves as a building block for the complete uniqueness theorem T5_uniqueness_complete in the same module, which establishes J as the unique cost functional meeting the axioms of Recognition Science. It aligns directly with T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.