Foundation Primitive Recognition Calculus Prcjcost Reciprocal Symmetric

The reciprocal symmetry theorem

The declaration reciprocal_symmetric establishes a symmetry property for a specific cost function defined on ratio orbits, the framework's discrete record of rational numbers. The cost function in question is J(q) = ((q + q⁻¹) / 2) - 1, which assigns a number to each ratio q. The theorem states that this cost is unchanged when q is replaced by its reciprocal 1/q: J(q) = J(1/q). For example, the cost of 2 equals the cost of 1/2. This is a formal, machine-checked proof that the symmetry holds for every nonzero rational ratio.

The proof works by direct algebraic manipulation. The declaration first defines the cost on ratio orbits, then proves that the rational value of the cost at q equals the rational value at 1/q. The argument handles the special case q = 0 separately, since the reciprocal is undefined there. The theorem is stated using the framework's own equality relation for ratio orbits, which identifies ratios that represent the same rational number. This is a narrow, precise result: it covers only the rational-number domain, not all real numbers.

In Recognition Science, this symmetry is one of the five plain conditions that, in the continuous real-number setting, force the cost function to be exactly J(x) = (x + 1/x)/2 - 1. The reciprocal symmetry is the condition that swapping a quantity for its inverse costs the same. The rational version proved here is a discrete surface of that condition. The declaration also includes a bridge theorem that transports this rational cost to the existing real-number formula, but that bridge relies on the separate continuous uniqueness theorem, not on this rational proof alone.

What reciprocal_symmetric does not claim is important. It does not prove the uniqueness theorem for the cost function on all positive real numbers. That theorem, which requires additional regularity conditions like continuity and a calibration condition, is a separate result in the library. The rational symmetry proof does not establish that J is the only cost function with this symmetry; other functions could share it on rational inputs. It also does not prove the symmetry for irrational ratios or for the full real-number domain. The declaration is a building block, not the final edifice.

For the reader, the practical consequence is that the framework's rational cost object has a verified algebraic symmetry, and that this symmetry is consistent with the larger continuous theory. The proof is a checkable fact about rational arithmetic, not a claim about the physical world. It is a piece of the framework's foundation, and its scope is deliberately limited to what the algebra supports.

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

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

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

This declaration does not prove the uniqueness of the cost function on all positive real numbers. It does not establish the symmetry for irrational ratios or for the full real-number domain. It does not claim that reciprocal symmetry alone forces the cost function form.

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: