Foundation Primitive Recognition Calculus Prcjcost Normalized Invariant

The normalization guarantee

The declaration normalized_invariant is a machine-checked theorem inside the Recognition Science framework's library of formal theorems. It concerns the framework's cost function, a formula that assigns a number to any ratio of two positive quantities. The formula is J(x) = ((x + 1/x) / 2) - 1, and it measures, in a sense made precise by the framework, the price of recognizing one quantity in terms of another. The theorem states that this cost does not depend on how the ratio is represented: if a ratio is simplified by dividing numerator and denominator by their greatest common divisor, the cost is unchanged.

In the framework's own notation, a ratio is stored as a pair of natural numbers called a ratio orbit. The declaration normalized_invariant proves that applying the cost function to a ratio orbit and applying it to the normalized version of that orbit always yields the same result. The proof is short and purely algebraic: it expands both sides using the definition of the cost and the fact that normalization preserves the rational value of the ratio. This is a theorem about the rational cost object, not about the real-number uniqueness theorem that the framework also contains.

The practical consequence is that the cost formula is well-defined on equivalence classes of ratios, not just on individual representations. This matters because the framework's later results, including the composition law and the bridge to the continuous uniqueness theorem, rely on being able to treat ratios as abstract objects. Without normalization invariance, those results would be hostage to a choice of representation. The theorem removes that ambiguity at the foundational level, before any real analysis enters.

What the declaration does not claim is equally important. It does not prove that the cost function is the only possible one satisfying certain axioms; that is the job of the separate continuous uniqueness theorem, which requires smoothness and calibration assumptions. It does not assert anything about irrational or real ratios, only about the rational ones representable as pairs of natural numbers. And it does not establish that normalization itself is computable or that the cost is finite; those are separate facts about the underlying definitions.

In Recognition Science, this theorem is a small but load-bearing brick. It lets later proofs assume that the cost function respects the ledger's native notion of equality between ratios. A reader who wants to verify the claim can check the Lean declaration directly: it is a theorem with no axioms beyond the standard three, and its proof is a few lines of rewriting and ring arithmetic.

/-- Normalizing a ratio representative by native orbit GCD preserves the PRC
cost. -/
theorem normalized_invariant (q : RatioOrbit) :
    RatioOrbit.crossEq (onRatioOrbit q)
      (onRatioOrbit (DistinctionNat.normalizeRatio q)) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq]
  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, DistinctionNat.normalizeRatio_toRat]

/-- Normalizing a ratio representative by native orbit GCD preserves the PRC
cost. -/
theorem normalized_invariant (q : RatioOrbit) :
    RatioOrbit.crossEq (onRatioOrbit q)
      (onRatioOrbit (DistinctionNat.normalizeRatio q)) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq]
  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, DistinctionNat.normalizeRatio_toRat]

/-- The real-domain uniqueness theorem currently used by PRC. The quantified
`AczelSmoothnessPackage` keeps the Aczél regularity commitment explicit. -/
theorem bridge_to_existing_jcost_uniqueness
    (F : ℝ → ℝ)
    (hAczel : Cost.FunctionalEquation.AczelSmoothnessPackage)
    (hRecip : Cost.FunctionalEquation.IsReciprocalCost F)
    (hNorm : Cost.FunctionalEquation.IsNormalized F)
    (hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw F)
    (hCalib : Cost.FunctionalEquation.IsCalibrated F)
    (hCont : ContinuousOn F (Set.Ioi 0)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  let _ : Cost.FunctionalEquation.AczelSmoothnessPackage := hAczel
  exact Cost.FunctionalEquation.law_of_logic_forces_jcost
    F hRecip hNorm hComp hCalib hCont

What this page does not claim

The declaration does not prove any uniqueness property for the cost function. It does not apply to irrational ratios or to the real-number domain. It does not establish that normalization is computable or that the cost is finite.

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