Foundation Primitive Recognition Calculus Delta Real Calibration Calibration Dat

The one datum that fixes the unit

In the Recognition Science framework, a ledger (a discrete record of recognition events) is governed by a cost function that measures how expensive a recognition is. The framework's central theorem forces the shape of that cost, but it leaves one degree of freedom: a positive scaling unit, call it c, that stretches the cost's input. The declaration calibration_datum_necessary_and_sufficient is the formal statement that this residual freedom is closed by exactly one continuum-side datum: the curvature of the cost at its limit ratio.

Concretely, the framework defines the one-act curvature as the second derivative of the cost at the point where the recognition ratio is zero. For the cost family in question, this curvature equals c². The theorem then states that, for any positive c, the condition c = 1 is equivalent to the condition that this curvature equals 1. In plain terms: if you want the canonical unit, you must have the curvature equal to one, and if you have that curvature, you have the canonical unit. No more, no less.

The declaration is the exact closure of a calibration gap. A separate theorem, discrete_does_not_force_unit, proves that the discrete ledger alone cannot fix the unit: distinct units give distinct costs, and any positive unit can be rescaled into any other by a positive factor, so the freedom is a one-real torsor. The continuum datum, the one-act curvature, is what removes that freedom. The framework's library shows that a normalized interface, carrying just a positive unit and the assertion that its curvature is one, forces the unit to be 1, and that the canonical member itself provides such an interface.

What the declaration does not claim is as important as what it proves. It does not claim that the discrete ledger forces the unit; the companion theorem explicitly denies that. It does not claim that the curvature datum is derived from anything more primitive; it is taken as a named input, an honest conditional. It does not claim that the curvature value is measured or observed in the physical world; it is a mathematical normalization within the framework. The theorem is a precise statement about the structure of a cost family, not an empirical assertion about nature.

/-- For positive units, the one-act curvature datum is necessary and sufficient
for selecting the canonical member. This is the exact closure of the calibration
gap: one datum, no more and no less. -/
theorem calibration_datum_necessary_and_sufficient {c : ℝ} (hc : 0 < c) :
    c = 1 ↔ oneActCurvature c = 1 := by
  exact (unit_forced_by_one_act hc).symm

/-- **The discrete carrier does not force the unit.** The cost family is faithful
(distinct units give distinct costs) and transitively rescaled, so the residual
freedom is a one-real torsor. Without the one-act normalization datum the unit is
genuinely free. -/
theorem discrete_does_not_force_unit :
    (∀ c d : ℝ, 0 < c → 0 < d →
        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
          ∃ μ : ℝ, 0 < μ ∧
            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
  Calibration.cost_freedom_is_one_real_torsor

/-- Any normalized one-act interface forces the canonical cost unit. -/
theorem normalized_interface_forces_J (I : NormalizedOneActInterface) :
    I.unit = 1 :=
  (unit_forced_by_one_act I.positive).mp I.curvature_unit

What this page does not claim

The discrete ledger alone forces the unit; the theorem explicitly denies this. The curvature datum is derived from a more primitive principle; it is a named input. The curvature value is an empirical measurement; it is a mathematical normalization.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/DeltaRealCalibration.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: