Foundation Primitive Recognition Calculus Prccalibration Independence

The calibration choice

A recognition cost is a number that measures the price of a recognition event, a discrete record of something being recognized. In Recognition Science, the central question is which cost function is forced by the laws of recognition. The answer, proved in the framework's machine-checked library, is the function J(x) = (x + 1/x)/2 − 1. But before that theorem can be trusted, one must ask: do the laws force J uniquely, or is there a hidden choice? The module PRCCalibrationIndependence answers this question directly.

The framework defines a family of cost functions, each labeled by a positive real number c. The function is costLambda c x = (x^c + x^(−c))/2 − 1. For c = 1, this is exactly J. For c = 2, it is a different function. Each member of the family satisfies the basic cost laws: it is symmetric, meaning costLambda c x = costLambda c (1/x), and it is normalized, meaning costLambda c 1 = 0. The family is also faithful: distinct values of c give genuinely distinct cost functions. So the family is a one-parameter set of legitimate costs, not a single point.

The module then proves a stronger statement. The full set of laws that the uniqueness theorem uses, including the reciprocal cost law (a composition identity that drives the classification) and continuity on the positive reals, is satisfied by every member of the family. The only hypothesis that distinguishes c = 1 from the rest is calibration, which requires the second derivative of the log-coordinate form at zero to equal 1. The theorem costLambda_isCalibrated_iff shows that this holds if and only if c = 1. Therefore, calibration is the single hypothesis that pins down J; all other laws are satisfied by the whole family.

The consequence is precise. The theorem calibration_is_the_only_hypothesis_pinning_J states that the four non-calibration hypotheses are satisfied by more than one function, so they cannot determine J. The unit of scale, which calibration fixes, is logically independent of the entire law set except for that one choice. In plain language: the laws of recognition force the shape of the cost, but they do not force its scale. The scale is an irreducible choice, and the module proves that this choice is exactly the calibration condition.

This result matters because it sharpens the meaning of the uniqueness theorem. The theorem law_of_logic_forces_jcost is not vacuous: it shows that J is the unique cost satisfying all five hypotheses. But the module shows that four of those hypotheses are shared by a whole family; the fifth, calibration, is what selects J. The framework does not hide this choice. It names it, proves it is the only choice, and thereby makes the derivation of J honest and complete.

/-- The δ-forced cost gauge family in multiplicative coordinates:
`costLambda c x = ½(x^c + x^{−c}) − 1`, with the real exponent taken via
`Real.rpow`. The `c = 1` member is `J`. -/
noncomputable def costLambda (c x : ℝ) : ℝ := (x ^ c + x ^ (-c)) / 2 - 1

/-- **Item 2, airtight: calibration is the ONLY hypothesis of the uniqueness theorem
that pins `J`.** Every gauge member satisfies the full non-calibration hypothesis set of
`law_of_logic_forces_jcost` (reciprocity, normalization, the RCL composition law, and
continuity on the positives); calibration holds iff `c = 1`; and the family contains
genuinely distinct members. Hence the four non-calibration hypotheses are satisfied by
more than one function and cannot determine `J`: the unit of scale is logically
independent of the entire law set except for the calibration choice. -/
theorem calibration_is_the_only_hypothesis_pinning_J :
    (∀ c : ℝ,
        Cost.FunctionalEquation.IsReciprocalCost (fun x => costLambda c x)
          ∧ Cost.FunctionalEquation.IsNormalized (fun x => costLambda c x)
          ∧ Cost.FunctionalEquation.SatisfiesCompositionLaw (fun x => costLambda c x)
          ∧ ContinuousOn (fun x => costLambda c x) (Set.Ioi 0))
      ∧ (∀ c : ℝ, 0 < c →
          (Cost.FunctionalEquation.IsCalibrated (fun x => costLambda c x) ↔ c = 1))
      ∧ (∃ c d : ℝ, 0 < c ∧ 0 < d ∧ c ≠ d
            ∧ (fun x => costLambda c x) ≠ (fun x => costLambda d x)) := by
  refine ⟨fun c => ⟨costLambda_isReciprocalCost c, costLambda_isNormalized c,
            costLambda_satisfiesCompositionLaw c, costLambda_continuousOn c⟩,
          fun c hc => costLambda_isCalibrated_iff hc, ?_⟩
  refine ⟨1, 2, one_pos, two_pos, by norm_num, ?_⟩
  intro h
  have h12 : (1 : ℝ) = 2 := costLambda_inj one_pos two_pos h
  norm_num at h12

/-- 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 module does not prove that J is the only cost function satisfying all five hypotheses; that is the upstream uniqueness theorem. The module does not claim that calibration is derived from more primitive laws; it proves calibration is an independent choice. The module does not address whether the calibration condition has a physical interpretation beyond its mathematical role.

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: