IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost

   1/-
   2  PrimitiveRecognitionCalculus/PRCJCost.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6    δ/Logic_Functional_Equation.tex
   7
   8  Spec anchors:
   9    Build Order steps 5-7: ratio cost surface, RCL surface, and the strongest
  10    currently provable bridge to the existing J-cost uniqueness theorem.
  11
  12  Strength: δ-only for the rational cost object. The bridge to `Cost.Jcost`
  13  and `law_of_logic_forces_jcost` is a classical-extension transport surface
  14  because it lives on continuous positive real ratios.
  15-/
  16
  17import Mathlib
  18import IndisputableMonolith.Cost.FunctionalEquation
  19import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean
  20
  21namespace IndisputableMonolith
  22namespace Foundation
  23namespace PrimitiveRecognitionCalculus
  24
  25namespace PRCJCost
  26
  27/-! ## A rational PRC cost object -/
  28
  29/-- The two-step orbit position. -/
  30def twoOrbit : DistinctionNat :=
  31  DistinctionNat.succ DistinctionNat.one
  32
  33@[simp] theorem twoOrbit_toNat :
  34    twoOrbit.toNat = 2 := by
  35  rfl
  36
  37/-- The ratio orbit `2`. -/
  38def two : RatioOrbit where
  39  num := SignedOrbit.ofOrbit twoOrbit
  40  den := DistinctionNat.one
  41  den_ne_zero := DistinctionNat.one_ne_zero
  42
  43@[simp] theorem two_toRat :
  44    two.toRat = 2 := by
  45  unfold two RatioOrbit.toRat
  46  simp [twoOrbit_toNat, SignedOrbit.ofOrbit_toInt, DistinctionNat.one_toNat]
  47
  48/-- The ratio orbit `1/2`. -/
  49def half : RatioOrbit where
  50  num := SignedOrbit.ofOrbit DistinctionNat.one
  51  den := twoOrbit
  52  den_ne_zero := by
  53    intro h
  54    have hnat := congrArg DistinctionNat.toNat h
  55    rw [twoOrbit_toNat, DistinctionNat.toNat_zero] at hnat
  56    norm_num at hnat
  57
  58@[simp] theorem half_toRat :
  59    half.toRat = (1 / 2 : ℚ) := by
  60  unfold half RatioOrbit.toRat
  61  simp [twoOrbit_toNat, SignedOrbit.ofOrbit_toInt, DistinctionNat.one_toNat]
  62
  63/-- PRC's rational J-cost object on a ratio orbit:
  64`J(q) = ((q + q⁻¹) / 2) - 1`.
  65
  66This is a ratio-orbit object. It is not the real analytic uniqueness theorem;
  67that theorem is bridged below. -/
  68def onRatioOrbit (q : RatioOrbit) : RatioOrbit :=
  69  RatioOrbit.sub (RatioOrbit.mul (RatioOrbit.add q (RatioOrbit.recip q)) half) RatioOrbit.one
  70
  71theorem onRatioOrbit_toRat (q : RatioOrbit) :
  72    (onRatioOrbit q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1 := by
  73  unfold onRatioOrbit
  74  rw [RatioOrbit.sub_toRat, RatioOrbit.mul_toRat, RatioOrbit.add_toRat,
  75    RatioOrbit.recip_toRat, half_toRat, RatioOrbit.one_toRat]
  76  ring
  77
  78/-- The PRC rational cost transports to the existing real `Cost.Jcost`
  79formula on the verifier display. -/
  80theorem onRatioOrbit_toReal_jcost (q : RatioOrbit) :
  81    ((onRatioOrbit q).toRat : ℝ) = Cost.Jcost ((q.toRat : ℚ) : ℝ) := by
  82  rw [onRatioOrbit_toRat]
  83  unfold Cost.Jcost
  84  rw [Rat.cast_sub, Rat.cast_div, Rat.cast_add, Rat.cast_inv]
  85  norm_num
  86
  87/-- Reciprocal symmetry of the PRC rational cost. -/
  88theorem reciprocal_symmetric (q : RatioOrbit) :
  89    RatioOrbit.crossEq (onRatioOrbit q) (onRatioOrbit (RatioOrbit.recip q)) := by
  90  rw [RatioOrbit.crossEq_iff_toRat_eq]
  91  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, RatioOrbit.recip_toRat]
  92  by_cases hq : q.toRat = 0
  93  · simp [hq]
  94  · field_simp [hq]
  95    ring
  96
  97/-- Normalizing a ratio representative by native orbit GCD preserves the PRC
  98cost. -/
  99theorem normalized_invariant (q : RatioOrbit) :
 100    RatioOrbit.crossEq (onRatioOrbit q)
 101      (onRatioOrbit (DistinctionNat.normalizeRatio q)) := by
 102  rw [RatioOrbit.crossEq_iff_toRat_eq]
 103  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, DistinctionNat.normalizeRatio_toRat]
 104
 105/-- Division of ratio orbits, defined from multiplication and reciprocal. -/
 106def div (q r : RatioOrbit) : RatioOrbit :=
 107  RatioOrbit.mul q (RatioOrbit.recip r)
 108
 109theorem div_toRat (q r : RatioOrbit) :
 110    (div q r).toRat = q.toRat / r.toRat := by
 111  unfold div
 112  rw [RatioOrbit.mul_toRat, RatioOrbit.recip_toRat]
 113  rfl
 114
 115private def rclLHS (x y : RatioOrbit) : RatioOrbit :=
 116  RatioOrbit.add (onRatioOrbit (RatioOrbit.mul x y)) (onRatioOrbit (div x y))
 117
 118private def rclRHS (x y : RatioOrbit) : RatioOrbit :=
 119  RatioOrbit.add
 120    (RatioOrbit.add
 121      (RatioOrbit.mul two (RatioOrbit.mul (onRatioOrbit x) (onRatioOrbit y)))
 122      (RatioOrbit.mul two (onRatioOrbit x)))
 123    (RatioOrbit.mul two (onRatioOrbit y))
 124
 125/-- Canonical PRC J-cost satisfies the RCL algebraically on nonzero ratio
 126orbits. This is the rational surface of the composition law, not the
 127continuous-real uniqueness theorem. -/
 128theorem canonical_rcl_surface {x y : RatioOrbit}
 129    (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
 130    RatioOrbit.crossEq (rclLHS x y) (rclRHS x y) := by
 131  rw [RatioOrbit.crossEq_iff_toRat_eq]
 132  unfold rclLHS rclRHS
 133  rw [RatioOrbit.add_toRat, RatioOrbit.add_toRat, RatioOrbit.add_toRat,
 134    RatioOrbit.mul_toRat, RatioOrbit.mul_toRat, RatioOrbit.mul_toRat,
 135    RatioOrbit.mul_toRat,
 136    onRatioOrbit_toRat, onRatioOrbit_toRat, onRatioOrbit_toRat,
 137    onRatioOrbit_toRat, div_toRat]
 138  simp [two_toRat]
 139  rw [RatioOrbit.mul_toRat]
 140  have hxy : x.toRat * y.toRat ≠ 0 := mul_ne_zero hx hy
 141  field_simp [hx, hy, hxy]
 142  ring_nf
 143
 144/-! ## Bridge to the existing continuous positive-real uniqueness theorem -/
 145
 146/-- Hypotheses for the later PRC-native cost-classification theorem. The
 147`two_calibrated` field rules out the identically-zero cost on the discrete
 148rational surface, playing the role of the continuous theorem's unit
 149log-curvature calibration until the internal real completion exists. -/
 150structure PRCNativeCostHypotheses (F : RatioOrbit → RatioOrbit) : Prop where
 151  reciprocal :
 152    ∀ q, RatioOrbit.crossEq (F q) (F (RatioOrbit.recip q))
 153  normalized_invariant :
 154    ∀ q, RatioOrbit.crossEq (F q) (F (DistinctionNat.normalizeRatio q))
 155  canonical_rcl :
 156    ∀ {x y : RatioOrbit}, x.toRat ≠ 0 → y.toRat ≠ 0 →
 157      RatioOrbit.crossEq
 158        (RatioOrbit.add (F (RatioOrbit.mul x y)) (F (div x y)))
 159        (RatioOrbit.add
 160          (RatioOrbit.add
 161            (RatioOrbit.mul two (RatioOrbit.mul (F x) (F y)))
 162            (RatioOrbit.mul two (F x)))
 163          (RatioOrbit.mul two (F y)))
 164  unit_zero :
 165    F RatioOrbit.one = RatioOrbit.zero
 166  two_calibrated :
 167    RatioOrbit.crossEq (F two) (onRatioOrbit two)
 168
 169/-- Exact missing native theorem for a later pass: classify every admissible
 170PRC cost on normalized ratio orbits, then transport to the continuous
 171positive-real theorem as a corollary rather than using the real theorem as
 172the premise. -/
 173def PRCNativeCostUniquenessTarget : Prop :=
 174  ∀ F : RatioOrbit → RatioOrbit,
 175    PRCNativeCostHypotheses F →
 176    ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)
 177
 178/-- The real-domain uniqueness theorem currently used by PRC. The quantified
 179`AczelSmoothnessPackage` keeps the Aczél regularity commitment explicit. -/
 180theorem bridge_to_existing_jcost_uniqueness
 181    (F : ℝ → ℝ)
 182    (hAczel : Cost.FunctionalEquation.AczelSmoothnessPackage)
 183    (hRecip : Cost.FunctionalEquation.IsReciprocalCost F)
 184    (hNorm : Cost.FunctionalEquation.IsNormalized F)
 185    (hComp : Cost.FunctionalEquation.SatisfiesCompositionLaw F)
 186    (hCalib : Cost.FunctionalEquation.IsCalibrated F)
 187    (hCont : ContinuousOn F (Set.Ioi 0)) :
 188    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
 189  let _ : Cost.FunctionalEquation.AczelSmoothnessPackage := hAczel
 190  exact Cost.FunctionalEquation.law_of_logic_forces_jcost
 191    F hRecip hNorm hComp hCalib hCont
 192
 193/-- Certificate for the PRC cost pass. -/
 194structure PRCJCostCertificate : Prop where
 195  rational_formula :
 196    ∀ q : RatioOrbit,
 197      (onRatioOrbit q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1
 198  real_jcost_bridge :
 199    ∀ q : RatioOrbit,
 200      ((onRatioOrbit q).toRat : ℝ) = Cost.Jcost ((q.toRat : ℚ) : ℝ)
 201  reciprocal :
 202    ∀ q : RatioOrbit,
 203      RatioOrbit.crossEq (onRatioOrbit q) (onRatioOrbit (RatioOrbit.recip q))
 204  normalization :
 205    ∀ q : RatioOrbit,
 206      RatioOrbit.crossEq (onRatioOrbit q)
 207        (onRatioOrbit (DistinctionNat.normalizeRatio q))
 208  canonical_rcl :
 209    ∀ {x y : RatioOrbit}, x.toRat ≠ 0 → y.toRat ≠ 0 →
 210      RatioOrbit.crossEq (rclLHS x y) (rclRHS x y)
 211  existing_real_uniqueness :
 212    ∀ (F : ℝ → ℝ),
 213      Cost.FunctionalEquation.AczelSmoothnessPackage →
 214      Cost.FunctionalEquation.IsReciprocalCost F →
 215      Cost.FunctionalEquation.IsNormalized F →
 216      Cost.FunctionalEquation.SatisfiesCompositionLaw F →
 217      Cost.FunctionalEquation.IsCalibrated F →
 218      ContinuousOn F (Set.Ioi 0) →
 219      ∀ x : ℝ, 0 < x → F x = Cost.Jcost x
 220  native_uniqueness_target_named :
 221    PRCNativeCostUniquenessTarget = PRCNativeCostUniquenessTarget
 222
 223/-- The PRC rational cost surface is closed through canonical RCL and bridges
 224honestly to the existing continuous-real uniqueness theorem. -/
 225theorem prc_jcost_certificate : PRCJCostCertificate where
 226  rational_formula := onRatioOrbit_toRat
 227  real_jcost_bridge := onRatioOrbit_toReal_jcost
 228  reciprocal := reciprocal_symmetric
 229  normalization := normalized_invariant
 230  canonical_rcl := by
 231    intro x y hx hy
 232    exact canonical_rcl_surface hx hy
 233  existing_real_uniqueness := by
 234    intro F hA hR hN hC hCal hCont x hx
 235    exact bridge_to_existing_jcost_uniqueness F hA hR hN hC hCal hCont x hx
 236  native_uniqueness_target_named := rfl
 237
 238end PRCJCost
 239
 240end PrimitiveRecognitionCalculus
 241end Foundation
 242end IndisputableMonolith
 243