Foundation Primitive Recognition Calculus Prccalibration Target Clog Inj

The gauge parameter

The cost function, the price a system pays for recognizing an event, is not unique. The framework's core theorem forces a general shape, but leaves one real number free: a scale parameter, written c. The family of allowed costs is the set of functions cosh(c·t) − 1, where t is a log-coordinate and c is any positive real. The theorem clog_inj states that different positive values of c give different functions. If c and d are both positive and the two functions cosh(c·t) − 1 and cosh(d·t) − 1 are equal for every t, then c = d. This is the injectivity property: the map from the positive reals to the cost family loses no information.

The proof runs through the second derivative at t = 0. For the function cosh(c·t) − 1, that second derivative is c², a quantity the framework calls the log-curvature. Two functions with the same curvature at the unit point are the same function, because the curvature determines c up to sign, and positivity fixes the sign. The theorem is proved in the framework's machine-checked library of formal theorems, and it is a theorem in the strict sense: it is derived, not assumed.

This injectivity has a precise consequence. The family of costs is not just a set; it carries an action of the positive reals by rescaling the log-coordinate. The theorem that distinct parameters give distinct functions says that action is free. A companion theorem shows the action is also transitive: any member of the family can be rescaled into any other. A free and transitive action makes the family a principal homogeneous space, a torsor, under the positive reals. The residual freedom in the cost is exactly one positive real number, nothing more and nothing less.

That one number is a gauge, a unit of scale that the discrete structure of recognition events does not fix. The framework proves that setting the curvature to 1 selects the specific member c = 1, which is the cost function J(x) = (x + 1/x)/2 − 1. But the discrete δ carrier does not supply the curvature datum; it must come from outside, from a calibration choice. The theorem clog_inj is what makes that choice meaningful: because the parameter is faithful, choosing a calibration is choosing a cost, and no two different choices collapse into the same function.

What clog_inj does not claim is just as important. It does not say which value of c is correct, or that c = 1 is forced by the discrete structure. It does not claim that the cost family is the only possible family, only that within this family the parameter is honest. It does not assert that the log-curvature is the only invariant, though the framework's theorems show it is the invariant that matters for calibration. The theorem is a statement about the family's internal structure, not about which member the world uses.

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

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

/-- The gauge action `μ • F := F(μ · )` is transitive on the cost family: any
member reaches any other through a positive rescaling of the log-coordinate. -/
theorem gauge_action_transitive {c d : ℝ} (hc : 0 < c) (hd : 0 < d) :
    ∃ μ : ℝ, 0 < μ ∧
      (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1) := by
  refine ⟨d / c, div_pos hd hc, ?_⟩
  funext t
  have hcne : c ≠ 0 := ne_of_gt hc
  have hkey : c * (d / c * t) = d * t := by field_simp
  rw [hkey]

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

What this page does not claim

clog_inj does not determine which positive value of c is physically realized. The theorem does not assert that the cosh family is the only possible cost family. Nothing in clog_inj says the discrete recognition structure itself fixes the curvature.

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: