Foundation Primitive Recognition Calculus Prccalibration Target Log Curvature

The residual gauge

In the Recognition Science framework, a ledger is a discrete record of recognition events, and each cost function assigns a price to a recognition event. The framework proves a unique cost function J(x) = (x + 1/x)/2 − 1 under five plain conditions, but before that uniqueness lands, a one-parameter family of candidate costs remains. The declaration logCurvature identifies the single number that distinguishes these candidates: the second derivative of the cost at the unit point, which equals c² for the member cosh(c·t) − 1.

This second derivative is called the log-curvature because it is read off in log coordinates, where the cost member takes the form cosh(c·t) − 1. The theorem states that for any real c, the second derivative at t = 0 is exactly c². A companion theorem, clog_inj, proves that distinct positive curvature parameters give distinct cost functions: if cosh(c·t) − 1 equals cosh(d·t) − 1 for all t, then c = d. Together these establish that the family is faithful, meaning the curvature parameter truly labels each member.

The framework then shows that setting this curvature to 1 selects exactly the J cost. The theorem curvature_one_iff_J states that the second derivative at the unit equals 1 if and only if c = 1. And costLambda_one_eq_J confirms the identification: cosh(ln x) − 1 equals (x + x⁻¹)/2 − 1 for positive x. So the calibration condition "curvature equals 1" is exactly the condition that picks out the unique J cost from the family.

The residual freedom is a torsor, meaning the family of costs forms a principal homogeneous space under the positive reals. The gauge action μ · F := F(μ·) is transitive: any member reaches any other through a positive rescaling of the log-coordinate. This is the sharpened statement cost_freedom_is_one_real_torsor. In plain language, the discrete ledger structure leaves exactly one real number free, the unit of scale, and that number is fixed only by the continuum-side calibration datum of curvature 1, which the discrete structure does not itself supply.

What logCurvature does not claim is equally precise. It does not assert that the unit c must be 1; that requires the external calibration choice. It does not prove that the discrete recognition structure alone determines the scale. And it does not claim that the cost family is the only possible one, only that within this family the curvature is the sole invariant. The declaration pins down the residual freedom exactly: one positive real, no more, no less.

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

/-- The cost family is faithful: distinct positive curvature parameters give
distinct cost functions. (Proved through the curvature, which is an invariant of
the function.) -/
theorem clog_inj {c d : ℝ} (hc : 0 < c) (hd : 0 < d)
    (h : (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1)) :
    c = d := by
  have e1 : deriv (deriv (fun t => Real.cosh (c * t) - 1)) 0 = c ^ 2 :=
    logCurvature c
  have e2 : deriv (deriv (fun t => Real.cosh (d * t) - 1)) 0 = d ^ 2 :=
    logCurvature d
  rw [h, e2] at e1
  have hsq : c ^ 2 = d ^ 2 := e1.symm
  have hfac : (c - d) * (c + d) = 0 := by nlinarith [hsq]
  rcases mul_eq_zero.mp hfac with h' | h'
  · linarith
  · linarith

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

The unit c is forced to be 1 by the discrete ledger structure alone. The curvature parameter is the only possible invariant of the cost family. The cost family considered here is the only family compatible with the framework's axioms.

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: