Foundation Primitive Recognition Calculus Prccalibration Target Cost Freedom Is

The residual freedom

The hyperbolic cosine function cosh(t) describes a family of curves when scaled: cosh(c·t) for any positive number c. These curves appear in the Recognition Science framework as candidate cost functions, where a cost is the price the framework assigns to a recognition event, a discrete record of something being identified. The framework's central forcing theorem pins the cost to the form cosh(c·t) − 1, but the parameter c itself is not forced by that theorem. The declaration cost_freedom_is_one_real_torsor states what that leftover freedom is: exactly one positive real number, the scale c, and nothing else.

To see why, consider two members of the family, cosh(c·t) − 1 and cosh(d·t) − 1. The first theorem component says that if these two functions are identical, then c must equal d. No two different scales give the same curve. The second component says the opposite direction: given any two positive scales c and d, there is a positive number μ such that cosh(c·(μ·t)) − 1 equals cosh(d·t) − 1. A simple rescaling of the input t by μ moves any member to any other. Together, these two properties, distinctness and reachability, make the family a torsor: a space where the positive reals act freely and transitively. The residual freedom in the cost is therefore exactly one positive real, the unit of scale.

That single parameter is not a defect. It is the framework's calibration target. The second derivative of cosh(c·t) − 1 at t = 0 equals c², a quantity the framework calls log-curvature. Setting that curvature to 1 selects the member with c = 1, which in multiplicative coordinates is exactly J(x) = (x + 1/x)/2 − 1, the framework's unique forced cost. The theorem curvature_one_iff_J proves this equivalence: curvature 1 holds if and only if c = 1. The discrete recognition structure that forces the cost family does not, by itself, fix this curvature; the framework states plainly that the unit c is a gauge, a free parameter that only a calibration datum, such as curvature 1, can pin down.

What the declaration does not claim is just as important. It does not claim that the calibration datum curvature 1 is derived from the discrete structure; the theorem explicitly leaves that datum as a free choice. It does not claim that the family contains any member beyond the cosh form. It does not claim that the parameter c has a physical interpretation or a measured value; it is a mathematical degree of freedom. The declaration's content is narrow and precise: the residual freedom in the cost family is exactly one positive real number, and that number is a scale to be set, not a hidden variable to be discovered.

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

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

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

What this page does not claim

The calibration datum curvature 1 is derived from the discrete recognition structure. The parameter c has a physical interpretation or a measured value. The cost family contains any member beyond the cosh form.

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: