Foundation Primitive Recognition Calculus Delta Real Calibration Unit Forced By

The one-act calibration

The declaration unit_forced_by_one_act answers a calibration question: given a family of cost functions that differ only by a positive scaling unit c, how many observations are needed to pin down c exactly? The theorem states that one continuum-interface datum, the value of the function's second derivative at its origin (its one-act curvature), is both necessary and sufficient. If that curvature is set to 1, then c must equal 1, and conversely. The proof is a direct calculation: for the cost family cosh(c·t) − 1, the second derivative at t = 0 is exactly c², so the normalization forces c = 1.

What the declaration does not claim is just as important. The discrete carrier, the world of individual recognition events, cannot force the unit on its own. The theorem discrete_does_not_force_unit proves that distinct units give distinct cost functions, and that any positive unit can be rescaled into any other by a positive factor; the residual freedom is a one-real torsor. Without the one-act curvature datum, the unit is genuinely free. The calibration is therefore an honest conditional: it is not discrete-forced, and the single continuum datum that closes the gap is named explicitly rather than hidden.

In Recognition Science, this result closes the calibration gap for the canonical cost function J. The framework's library proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 − 1. The unit_forced_by_one_act theorem supplies the missing normalization: the minimal continuum-side interface, a positive unit and the assertion that the primitive one-act chart has unit log-curvature, forces the canonical member. The structure NormalizedOneActInterface packages exactly those two data, and the theorem normalized_interface_forces_J shows that any such interface has unit equal to 1.

The practical consequence is that the framework's unit is not a free parameter. It is derived from a single, explicitly named continuum-interface datum, and the derivation is machine-checked. The cost-unit issue is fully classified: it is not discrete-forced, and it is closed exactly by the minimal second-order recognition interface. The reader can now see that the framework's calibration claim rests on a precise, minimal input, and that the input is not smuggled in from the discrete side.

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

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

What this page does not claim

The declaration does not claim that the discrete recognition events alone determine the cost unit. It does not claim that the one-act curvature datum is derived from within the framework; it is supplied as an external normalization. It does not claim that the canonical cost function J is the only function satisfying the five conditions; that is a separate theorem.

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: