Calibration
plain-language theorem explainer
The Calibration class encodes Axiom 3 for a cost functional F on positive reals: the second derivative at zero of F composed with the exponential equals one. Researchers deriving J-cost uniqueness or the phi-ladder cite it to fix the curvature scale at unity and rule out scaled families. The declaration is a direct class definition consisting of a single field that states the derivative condition.
Claim. A function $F : (0,∞) → ℝ$ satisfies calibration when $G''(0) = 1$, where $G(t) := F(e^t)$.
background
Module CostAxioms states the three primitive axioms that generate the Recognition Science framework. A1 is normalization: $F(1) = 0$. A2 is the Recognition Composition Law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$. A3 is the present calibration condition on the log-coordinate second derivative. The module doc notes that these axioms are more primitive than logic because low-cost configurations (J near zero) correspond to consistency while high-cost ones correspond to contradiction. Upstream, CostFromDistinction.Calibration supplies a distinguished inconsistent configuration α with positive cost δ that anchors the functional; the present class supplies the curvature normalization that makes the solution unique rather than a family.
proof idea
This is a direct class definition whose single field is the stated second-derivative equality; no lemmas or tactics are applied inside the declaration itself.
why it matters
Calibration supplies the missing scale that converts the composition law into the unique J-cost $J(x) = (x + x^{-1})/2 - 1$ (T5). It is invoked by washburn_uniqueness, IsCalibrated, composition_law_equiv_coshAdd, and downstream results such as Lambda_no_fine_tuning (Ω_Λ = 11/16 - α/π) and mass_ratio_bounds. The axiom therefore closes the axiomatic foundation for the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.