Foundation Primitive Recognition Calculus Prccalibration Target Cost Lambda One

The unit cost

The declaration costLambda_one_eq_J is a proved identity in the framework's machine-checked library of formal theorems. It states that for any positive real number x, the expression cosh(ln x) − 1 equals (x + x⁻¹)/2 − 1. In plain words, the hyperbolic cosine of the natural logarithm of a positive number is exactly the average of that number and its reciprocal, minus one. This is a fact about real analysis, and the proof in the library is a direct algebraic rewrite using the definition of hyperbolic cosine and the inverse property of logarithms.

The identity matters because it connects two different ways of writing the same cost function. The left side, cosh(ln x) − 1, is the form that arises from a one-parameter family of candidate cost functions, each indexed by a positive real number c. The right side, (x + x⁻¹)/2 − 1, is the canonical form called J, which the framework's forcing chain derives from five plain conditions on any cost function. The declaration shows that when the parameter c equals 1, the family member is exactly J. This is not a new physical assumption; it is a calculation that identifies two expressions.

In Recognition Science, a ledger is a discrete record of recognition events, and the cost of a recognition is a number that measures how expensive that event is. The framework models this cost with a function of a positive real variable. The family cosh(c·t) − 1, written in log-coordinates, leaves one free positive real parameter c, called the unit of scale. The theorem logCurvature shows that the second derivative of this family at t = 0 is c², so the parameter is readable as a curvature. The theorem curvature_one_iff_J then proves that setting this curvature to 1 is equivalent to c = 1, which by costLambda_one_eq_J is exactly the canonical cost J.

The framework's library also proves that this residual freedom is a torsor: the positive reals act freely and transitively on the family, meaning any member can be rescaled into any other by exactly one positive factor. The unit c is therefore not fixed by the discrete ledger structure itself; it is a gauge that must be set by one calibration datum. The declaration costLambda_one_eq_J does not claim that this calibration datum is derived from the discrete structure, nor that the value c = 1 is forced by the five conditions on cost. It only establishes the algebraic identity that selects J once the gauge is fixed. The physical origin of the calibration remains an open target within the framework.

/-- The `c = 1` member is exactly J: in multiplicative coordinates,
`cosh(ln x) − 1 = ½(x + x⁻¹) − 1`. -/
theorem costLambda_one_eq_J (x : ℝ) (hx : 0 < x) :
    Real.cosh (Real.log x) - 1 = (x + x⁻¹) / 2 - 1 := by
  rw [Real.cosh_eq, Real.exp_neg, Real.exp_log hx]

/-- The log-curvature of the cost member `cosh(c·t) − 1` at the unit (t = 0) is
`c²`. This is the residual gauge parameter read off as a second derivative. -/
theorem logCurvature (c : ℝ) :
    deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = c ^ 2 := by
  have hderiv1 : deriv (fun t => Real.cosh (c * t) - 1)
      = fun t => c * Real.sinh (c * t) := by
    funext t
    have hinner : HasDerivAt (fun s => c * s) (c * 1) t :=
      (hasDerivAt_id t).const_mul c
    have h : HasDerivAt (fun t => Real.cosh (c * t) - 1)
        (Real.sinh (c * t) * (c * 1)) t :=
      ((Real.hasDerivAt_cosh (c * t)).comp t hinner).sub_const 1
    rw [h.deriv]; ring
  rw [hderiv1]
  have hinner0 : HasDerivAt (fun s => c * s) (c * 1) (0 : ℝ) :=
    (hasDerivAt_id (0 : ℝ)).const_mul c
  have h2 : HasDerivAt (fun t => c * Real.sinh (c * t))
      (c * (Real.cosh (c * 0) * (c * 1))) (0 : ℝ) :=
    ((Real.hasDerivAt_sinh (c * 0)).comp (0 : ℝ) hinner0).const_mul c
  rw [h2.deriv]
  simp only [mul_zero, Real.cosh_zero, one_mul, mul_one]
  ring

/-- Curvature normalized to 1 picks out exactly the `c = 1` member, i.e. J. -/
theorem curvature_one_iff_J {c : ℝ} (hc : 0 < c) :
    deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = 1 ↔ c = 1 := by
  rw [logCurvature c]
  constructor
  · intro h
    have hfac : (c - 1) * (c + 1) = 0 := by nlinarith [h]
    rcases mul_eq_zero.mp hfac with h' | h'
    · linarith
    · linarith
  · intro h; rw [h]; norm_num

/-- **Item 2, sharpened: the residual freedom is a torsor, exactly one real.** The
gauge action of the positive reals on the cost family is free (`clog_inj`) and
transitive (`gauge_action_transitive`). A free transitive action exhibits the
family as a principal homogeneous space under `(ℝ_{>0}, ·)`, so the residual
freedom in the cost is exactly one positive real, the unit of scale. It is fixed
by one calibration datum (curvature 1), and that datum is not supplied by the
discrete δ structure. -/
theorem cost_freedom_is_one_real_torsor :
    (∀ 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)) :=
  ⟨fun _ _ hc hd h => clog_inj hc hd h, fun _ _ hc hd => gauge_action_transitive hc hd⟩

What this page does not claim

This declaration does not claim that the value c = 1 is derived from the discrete ledger structure. This declaration does not claim that the calibration datum is forced by the five conditions on cost. This declaration does not claim that the physical origin of the unit of scale is established.

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/PRCCalibrationTarget.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: