pith. machine review for the scientific record. sign in
class definition def or abbrev high

Calibration

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  78class Calibration (F : ℝ → ℝ) : Prop where
  79  second_deriv_at_zero : deriv (deriv (fun t => F (exp t))) 0 = 1
  80
  81/-- The complete axiom bundle for a cost functional. -/

used by (37)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 7 more

depends on (8)

Lean names referenced from this declaration's body.