Encyclopedia Foundation Foundation Primitive Recognition Calculus Prccalibration Target

ARTICLE 5 claims 5 theorems

Foundation Primitive Recognition Calculus Prccalibration Target

A single family of cost functions survives the framework's forcing, and one number, a curvature, picks out the unique member the framework needs.

Verify this page

The calibration target

The recognition framework, a discrete record of events and their costs, forces a family of cost functions of the form cosh(c·t) − 1, where t is a log-coordinate and c is a positive real number. This one-parameter family is the entire residual freedom left after the framework's discrete structure is imposed. The calibration target is the statement of what that freedom is and how it is removed.

The key fact is that the parameter c is not fixed by the discrete recognition structure. It is a gauge, a free choice of scale. The second derivative of the cost at the unit point equals c², so c is read off as a curvature. Distinct positive c values give distinct cost functions, so the family is faithful. The action of rescaling the log-coordinate moves any member to any other, so the family is a torsor: exactly one positive real number of freedom remains.

That one number is fixed by a single calibration datum: setting the curvature to 1. The theorem curvature_one_iff_J proves that curvature 1 holds exactly when c = 1. The c = 1 member is J(x) = (x + 1/x)/2 − 1 in multiplicative coordinates, the unique cost function that the framework's main theorem selects. The calibration target is thus the statement that the residual freedom is one real number, and that the datum curvature = 1 is the selection condition.

In Recognition Science, this establishes that the framework's discrete forcing does not overdetermine the cost. One free scale remains, and it must be set by an external calibration. This is a precise, machine-checked statement of what the framework does and does not fix.

THEOREM logCurvature · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean
logCurvature · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean:74 
/-- 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
THEOREM clog_inj · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean
clog_inj · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean:97 
/-- 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
THEOREM curvature_one_iff_J · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean
curvature_one_iff_J · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean:114 
/-- 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
THEOREM costLambda_one_eq_J · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean
costLambda_one_eq_J · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean:126 
/-- 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]
THEOREM cost_freedom_is_one_real_torsor · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean
cost_freedom_is_one_real_torsor · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCalibrationTarget.lean:156 
/-- **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 calibration datum curvature equals 1 is derived from within the framework. The cost family includes functions outside the cosh(c·t) − 1 form. The module proves the uniqueness of J without the calibration condition.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND