Foundation Primitive Recognition Calculus Prcjcost Prc Jcost Certificate

The rational cost certificate

The declaration prc_jcost_certificate is a machine-checked certificate in the Recognition Science framework's library of formal theorems. It establishes that a specific rational cost function, defined on ratio orbits (a discrete representation of positive rational numbers), satisfies the algebraic requirements of the framework's cost calculus. The cost function is J(q) = ((q + q⁻¹) / 2) - 1, and the certificate proves it is reciprocal-symmetric, invariant under normalization, and obeys the canonical composition law on nonzero rational inputs. These are the rational-surface properties that the continuous real-domain cost theorem later generalizes.

The certificate also bridges this rational construction to the existing continuous uniqueness theorem. It shows that the rational cost formula, when transported to real numbers, equals the framework's real cost function J(x) = (x + 1/x)/2 - 1. The bridge theorem explicitly assumes an Aczél smoothness package, reciprocal symmetry, normalization, the composition law, calibration, and continuity on positive reals, then concludes the unique form. This is the same theorem that forces the golden ratio and the eight-tick cycle in the broader framework, so the certificate connects the discrete rational surface to that larger forcing chain.

What the certificate does not claim is equally important. It does not prove the uniqueness of the cost function on the rational surface itself. The certificate names a target proposition, PRCNativeCostUniquenessTarget, which would classify all admissible rational costs, but that theorem is not proved in this pass. The certificate instead relies on the continuous real-domain theorem for uniqueness, using the rational construction as a supporting surface. It also does not claim the rational cost is identical to the real cost as a function; it proves only that the rational formula transports correctly to the real formula under the bridge.

/-- The PRC rational cost surface is closed through canonical RCL and bridges
honestly to the existing continuous-real uniqueness theorem. -/
theorem prc_jcost_certificate : PRCJCostCertificate where
  rational_formula := onRatioOrbit_toRat
  real_jcost_bridge := onRatioOrbit_toReal_jcost
  reciprocal := reciprocal_symmetric
  normalization := normalized_invariant
  canonical_rcl := by
    intro x y hx hy
    exact canonical_rcl_surface hx hy
  existing_real_uniqueness := by
    intro F hA hR hN hC hCal hCont x hx
    exact bridge_to_existing_jcost_uniqueness F hA hR hN hC hCal hCont x hx
  native_uniqueness_target_named := rfl

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

What this page does not claim

The certificate does not prove uniqueness of the cost function on the rational surface itself; that target remains open. The certificate does not claim the rational cost and real cost are identical as functions, only that the rational formula transports correctly to the real formula. The certificate does not derive the golden ratio or any downstream constants; it only establishes the rational cost surface and its bridge.

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: