Foundation Primitive Recognition Calculus Prccalibration Independence Calibratio

Calibration as a free choice

A recognition cost is a function that assigns a nonnegative penalty to the discrepancy between two observations; the framework's central theorem states that under five conditions the cost must be J(x) = (x + 1/x)/2 − 1. But one of those conditions, calibration, is not forced by the others. The machine-checked theorem calibration_unit_not_forced_by_cost_laws proves that the first four conditions, reciprocity, normalization, the composition law, and continuity, are satisfied by a whole family of functions, not just by J.

The family is parameterized by a positive real number c, with each member given by costLambda(c, x) = (x^c + x^(−c))/2 − 1. For every positive c, this function is symmetric, vanishes at x = 1, and satisfies the same composition identity that drives the uniqueness theorem. The c = 1 member is exactly J. But the family is faithful: distinct c values give distinct functions, so the laws leave a full one-dimensional freedom. Calibration, which fixes the second derivative at the unit scale, holds if and only if c = 1. Thus calibration is the single hypothesis that selects J; without it, the unit of scale remains a free gauge choice.

In Recognition Science, this result is the precise statement of what the framework does and does not determine. The cost laws force the shape of the cost function up to a scale, but they do not force the scale itself. The unit of scale is an irreducible choice, fixed only by an extra calibration assumption. This is not a gap in the framework; it is the one place where a convention enters, and the framework names it exactly.

/-- **Item 2, the negative direction.** The recognition cost laws
(`Cost.CostRequirements`) do not force the unit of scale.

The conjunction records: every member of the gauge family is a bona fide cost
(symmetric + unit law); the family is faithful (so the residual freedom is exactly
one real); the `c = 1` member is `J`; and there exist two genuinely distinct
members (`costLambda 1 = J` and `costLambda 2`) both satisfying the cost laws.
The last clause is the independence: the laws are satisfied by more than one
function, hence cannot single out `J`. The unit is fixed only by the extra
calibration hypothesis of the upstream uniqueness theorem, and is therefore the
one irreducible gauge choice. -/
theorem calibration_unit_not_forced_by_cost_laws :
    (∀ c : ℝ, Cost.CostRequirements (fun x => costLambda c x))
      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
          (fun x => costLambda c x) = (fun x => costLambda d x) → c = d)
      ∧ (∀ x : ℝ, 0 < x → costLambda 1 x = Cost.Jcost x)
      ∧ (∃ c d : ℝ, 0 < c ∧ 0 < d ∧ c ≠ d
            ∧ Cost.CostRequirements (fun x => costLambda c x)
            ∧ Cost.CostRequirements (fun x => costLambda d x)
            ∧ (fun x => costLambda c x) ≠ (fun x => costLambda d x)) := by
  refine ⟨fun c => costLambda_isCostRequirements c,
          fun c d hc hd h => costLambda_inj hc hd h,
          fun x hx => costLambda_one_eq_Jcost hx,
          ⟨1, 2, one_pos, two_pos, by norm_num,
           costLambda_isCostRequirements 1, costLambda_isCostRequirements 2, ?_⟩⟩
  intro h
  have h12 : (1 : ℝ) = 2 := costLambda_inj one_pos two_pos h
  norm_num at h12

/-- **Every gauge member is a bona fide recognition cost.** For every positive
`c`, `costLambda c` satisfies `Cost.CostRequirements` (the same structure
`PRCCompletenessIndependence.jcost_isCostRequirements` verifies for `J`). -/
theorem costLambda_isCostRequirements (c : ℝ) :
    Cost.CostRequirements (fun x => costLambda c x) where
  symmetric := fun {_} hx => costLambda_symm c hx
  unit0 := costLambda_unit0 c

theorem costLambda_satisfiesCompositionLaw (c : ℝ) :
    Cost.FunctionalEquation.SatisfiesCompositionLaw (fun x => costLambda c x) :=
  (Cost.FunctionalEquation.composition_law_equiv_coshAdd _).mpr (costLambda_coshAddIdentity c)

/-- The remaining hypothesis, calibration (`G''(0) = 1`), holds iff `c = 1`, because
`G(costLambda c)'' (0) = c²`. -/
theorem costLambda_isCalibrated_iff {c : ℝ} (hc : 0 < c) :
    Cost.FunctionalEquation.IsCalibrated (fun x => costLambda c x) ↔ c = 1 := by
  have hG : Cost.FunctionalEquation.G (fun x => costLambda c x)
      = fun t => Real.cosh (c * t) - 1 := by
    funext t; exact G_costLambda c t
  unfold Cost.FunctionalEquation.IsCalibrated
  rw [hG]
  exact curvature_one_iff_J hc

What this page does not claim

The theorem does not claim that calibration is arbitrary in a physical sense; it claims only logical independence from the other cost laws. The theorem does not claim that the cost laws are insufficient to determine J; it claims that calibration is the specific hypothesis that does the pinning. The theorem does not claim that the gauge family contains pathological or discontinuous functions; every member is continuous on the positive reals.

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/PRCCalibrationIndependence.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: