Encyclopedia Foundation Foundation Primitive Recognition Calculus Prccalibration Target Calibration Unit

ARTICLE 4 claims 4 theorems

Foundation Primitive Recognition Calculus Prccalibration Target Calibration Unit

In the Recognition Science framework, the cost function's unit of scale is not fixed by the discrete structure itself; it remains a free positive real, a gauge, until one calibration datum selects it.

Verify this page

The calibration unit

The declaration calibration_unit_is_a_gauge concerns the family of cost functions of the form cosh(c·t) − 1, where t is a log-coordinate and c is a positive real parameter. It establishes three facts about this family. First, the log-curvature of any member at the unit (t = 0) is exactly c². Second, the family is faithful: distinct positive curvature parameters give distinct cost functions, so the parameter c is not redundant. Third, normalizing the curvature to 1 selects precisely the c = 1 member, which in multiplicative coordinates is J(x) = (x + 1/x)/2 − 1, the framework's canonical cost function.

The theorem's name states its interpretive content: the unit c is a gauge. The discrete δ structure that forces the general cost form does not fix this continuum-side second-derivative property. The residual freedom is exactly one positive real, the unit of scale. The framework proves this freedom is a torsor: the positive reals act freely and transitively on the cost family by rescaling the log-coordinate, so any member reaches any other through a positive rescaling. One calibration datum, curvature equal to 1, fixes the unit and selects J.

The declaration does not claim that the calibration datum is derived from within the framework. It does not assert that c = 1 is forced by the discrete structure; the theorem explicitly leaves c as a free positive real. It also does not claim that the gauge freedom is eliminated or that the unit of scale is unique across all possible frameworks. The theorem establishes the structure of the freedom, not its resolution.

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 · costLambda_one_eq_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
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 equal to 1 is derived from the discrete δ structure. The unit c = 1 is forced uniquely by the framework's axioms. The gauge freedom is eliminated or physically resolved within the framework.

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