Foundation Primitive Recognition Calculus Prcjcost

The rational cost object

The cost function J(q) = (q + 1/q)/2 - 1 measures the price of recognizing a ratio q. In the Recognition Science framework, a ledger (a discrete record of events) assigns this cost to every positive rational number. The module PRCJCost builds this object explicitly: it defines J on ratio orbits, which are fractions built from a primitive counting type, and proves the cost behaves correctly under arithmetic operations.

The central formula appears in the module as a definition: onRatioOrbit q equals (q + q⁻¹)/2 - 1. A theorem confirms this matches the real-number cost function Jcost used elsewhere in the framework. The module then proves three structural properties. First, reciprocal symmetry: J(q) = J(1/q), so recognizing a ratio costs the same as recognizing its inverse. Second, normalization invariance: reducing a fraction to lowest terms does not change its cost. Third, the composition law, a functional equation that ties costs of products and quotients to costs of the inputs. This last identity holds algebraically for all nonzero rational inputs.

These results are not the full uniqueness theorem. The continuous version, which classifies all smooth cost functions satisfying the same laws, already exists in the library. The new module bridges to it: given a real-valued function that is reciprocal, normalized, composition-law-satisfying, calibrated, and continuous on positive reals, the bridge theorem forces it to equal Jcost exactly. This is the proved theorem law_of_logic_forces_jcost, invoked with explicit regularity hypotheses.

The module also declares a target for future work: a native uniqueness theorem that classifies costs directly on the rational surface, without relying on the continuous theorem as a premise. That target remains open. For now, the certificate theorem PRCJCostCertificate packages all the rational surface results and the bridge into one statement, marking the pass complete.

/-- PRC's rational J-cost object on a ratio orbit:
`J(q) = ((q + q⁻¹) / 2) - 1`.

This is a ratio-orbit object. It is not the real analytic uniqueness theorem;
that theorem is bridged below. -/
def onRatioOrbit (q : RatioOrbit) : RatioOrbit :=
  RatioOrbit.sub (RatioOrbit.mul (RatioOrbit.add q (RatioOrbit.recip q)) half) RatioOrbit.one

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

/-- Reciprocal symmetry of the PRC rational cost. -/
theorem reciprocal_symmetric (q : RatioOrbit) :
    RatioOrbit.crossEq (onRatioOrbit q) (onRatioOrbit (RatioOrbit.recip q)) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq]
  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, RatioOrbit.recip_toRat]
  by_cases hq : q.toRat = 0
  · simp [hq]
  · field_simp [hq]
    ring

/-- Canonical PRC J-cost satisfies the RCL algebraically on nonzero ratio
orbits. This is the rational surface of the composition law, not the
continuous-real uniqueness theorem. -/
theorem canonical_rcl_surface {x y : RatioOrbit}
    (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
    RatioOrbit.crossEq (rclLHS x y) (rclRHS x y) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq]
  unfold rclLHS rclRHS
  rw [RatioOrbit.add_toRat, RatioOrbit.add_toRat, RatioOrbit.add_toRat,
    RatioOrbit.mul_toRat, RatioOrbit.mul_toRat, RatioOrbit.mul_toRat,
    RatioOrbit.mul_toRat,
    onRatioOrbit_toRat, onRatioOrbit_toRat, onRatioOrbit_toRat,
    onRatioOrbit_toRat, div_toRat]
  simp [two_toRat]
  rw [RatioOrbit.mul_toRat]
  have hxy : x.toRat * y.toRat ≠ 0 := mul_ne_zero hx hy
  field_simp [hx, hy, hxy]
  ring_nf

/-- 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 module does not prove a native uniqueness theorem for costs on the rational surface; that target is declared but open. The composition law alone does not force the Jcost formula; the continuous theorem requires calibration and continuity as additional hypotheses.

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: