unique_cost_on_pos
plain-language theorem explainer
Any function F on the positive reals satisfying the UniqueCostAxioms bundle equals the Jcost function. Researchers deriving physical constants from the Recognition Science functional equation cite this result to establish uniqueness of the cost measure. The proof is a direct term application of the complete T5 uniqueness theorem by extracting symmetry, unit normalization, convexity, calibration, continuity, and regularity fields from the axiom record.
Claim. Let $F:ℝ→ℝ$ satisfy the UniqueCostAxioms, which include symmetry $F(x)=F(x^{-1})$ for $x>0$, normalization $F(1)=0$, strict convexity on $(0,∞)$, the calibration condition that the second derivative of $F∘exp$ at 0 equals 1, continuity on $(0,∞)$, the cosh-addition identity, and the associated d'Alembert and ODE regularity hypotheses. Then $F(x)=Jcost(x)$ for all $x>0$.
background
The CostUniqueness module consolidates convexity, calibration, and functional-equation results into the main T5 uniqueness theorem. UniqueCostAxioms is the structure that packages the required hypotheses for uniqueness on ℝ₊: symmetry under inversion, unit normalization at 1, strict convexity on the open positive interval, calibration via the second derivative of the composed exponential at zero, continuity on that interval, the cosh-add identity, and several d'Alembert-to-ODE regularity conditions.
proof idea
The proof is a one-line term wrapper that applies T5_uniqueness_complete to F, supplying each required hypothesis by projecting the corresponding field from the UniqueCostAxioms structure hF, including symmetric, unit, convex, calibrated, continuousOn_pos, coshAdd, dAlembert_smooth, dAlembert_toODE, ode_cont, ode_diff, and ode_bootstrap.
why it matters
This declaration completes the central T5 uniqueness result for the Jcost function in the CostUniqueness module. It realizes the T5 J-uniqueness step in the forcing chain, which forces the self-similar fixed point phi and leads to the eight-tick octave and three spatial dimensions. The result underpins mass-ladder formulas and coupling-constant derivations within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.