Foundation Primitive Recognition Calculus Prcjcost Bridge To Existing Jcost Uniq

The bridge to uniqueness

The recognition calculus, a discrete record of events and their costs, builds its cost function on ratio orbits, the set of positive rational numbers. On that surface, the cost of a ratio q is written J(q) = ((q + q⁻¹) / 2) - 1. A theorem in the framework's machine-checked library of formal theorems proves this rational formula transports to the real numbers: for every positive rational q, the rational cost equals the existing real cost function Cost.Jcost. That is the bridge named in the declaration.

The declaration also carries the stronger result. It proves that any real-valued function satisfying five conditions, reciprocal symmetry, normalization, a composition law, calibration, and continuity on positive reals, must equal J(x) = ((x + x⁻¹) / 2) - 1 for every positive x. This is the continuous uniqueness theorem, already proved in the library. The bridge declaration simply restates it as a theorem about the rational cost surface, with the regularity commitment made explicit through the Aczél smoothness package.

What the bridge does not claim is a native uniqueness proof on the rational surface itself. The library names a target proposition, PRCNativeCostUniquenessTarget, which would classify every admissible cost on normalized ratio orbits directly. That target remains open. The bridge instead uses the continuous theorem as a premise, a deliberate and honest stopgap until the internal real completion exists.

The practical consequence is a certificate. The framework's library records that the rational cost surface is closed under the composition law and bridges honestly to the continuous uniqueness theorem. A reader can rely on the rational cost formula as the unique continuous cost, while knowing exactly where the proof chain pauses for a future pass.

/-- The PRC rational cost transports to the existing real `Cost.Jcost`
formula on the verifier display. -/
theorem onRatioOrbit_toReal_jcost (q : RatioOrbit) :
    ((onRatioOrbit q).toRat : ℝ) = Cost.Jcost ((q.toRat : ℚ) : ℝ) := by
  rw [onRatioOrbit_toRat]
  unfold Cost.Jcost
  rw [Rat.cast_sub, Rat.cast_div, Rat.cast_add, Rat.cast_inv]
  norm_num

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

/-- Exact missing native theorem for a later pass: classify every admissible
PRC cost on normalized ratio orbits, then transport to the continuous
positive-real theorem as a corollary rather than using the real theorem as
the premise. -/
def PRCNativeCostUniquenessTarget : Prop :=
  ∀ F : RatioOrbit → RatioOrbit,
    PRCNativeCostHypotheses F →
    ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)

What this page does not claim

The bridge does not prove a native uniqueness theorem on the rational surface. The bridge does not show the rational cost formula is the only cost satisfying the five conditions on rationals alone. The bridge does not derive the continuous uniqueness theorem from the rational surface; it uses the continuous theorem as a premise.

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: