Foundation Primitive Recognition Calculus Delta Real Calibration

Calibration by one act

The cost function J(x) = (x + 1/x)/2 - 1 is the unique function satisfying five plain conditions, a theorem checked by machine. But uniqueness up to scaling leaves a gap: the unit of cost is free. The discrete rules that force J's shape do not fix the scale, and this work closes that gap with exactly one continuum datum.

We define a family of cost functions parameterized by a positive real c, written as cosh(c·t) - 1 in a log coordinate. Distinct c values give distinct costs, and any one can be rescaled into any other, so the freedom is a one-real torsor: a line of equally valid choices. No discrete rule breaks the tie.

The tie is broken at the continuum interface. We define one-act curvature as the second derivative of the cost at the limit ratio t = 0. For the family above, this curvature equals c². The single normalization "one-act curvature equals 1" then forces c = 1, selecting the canonical J. The theorem calibration_datum_necessary_and_sufficient proves this datum is both necessary and sufficient: for positive units, c = 1 if and only if the one-act curvature is 1.

The minimal interface that closes the gap is a structure holding a positive unit and the assertion that its one-act curvature is 1. Any such interface forces the unit to be 1, and the canonical member itself provides an example. The calibration gap is fully classified: not discrete-forced, closed exactly by one second-order recognition act.

In plain terms: the discrete ledger of recognition events cannot choose its own scale, but a single continuum measurement, the curvature at the identity, can. This is the honest conditional we state: the unit is not derived from discrete rules alone, and the one continuum datum is named rather than hidden.

/-- The one-act curvature is `c²`: the residual gauge parameter read as a
second derivative. -/
theorem oneActCurvature_eq (c : ℝ) : oneActCurvature c = c ^ 2 :=
  Calibration.logCurvature c

/-- **One continuum datum fixes the unit.** At the continuum interface, the single
normalization "one-act curvature equals 1" forces `c = 1`, i.e. selects the
canonical J. -/
theorem unit_forced_by_one_act {c : ℝ} (hc : 0 < c) :
    oneActCurvature c = 1 ↔ c = 1 := by
  unfold oneActCurvature
  exact Calibration.curvature_one_iff_J hc

/-- **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

/-- Existence of a normalized interface: the canonical member itself carries one. -/
def canonicalInterface : NormalizedOneActInterface where
  unit := 1
  positive := by norm_num
  curvature_unit := by
    rw [oneActCurvature_eq]
    norm_num

/-- 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

What this page does not claim

The discrete rules alone force the unit of cost. The one-act curvature is derived from the discrete carrier. The work proves the cost function J is unique without the five conditions.

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: