IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField

   1/-
   2  PrimitiveRecognitionCalculus/RationalField.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 4: package the PRC rational quotient as the reusable
   9    field-like substrate needed by PRC real completion and cost.
  10
  11  Strength: δ-only for the object operations and positivity predicate.
  12  Verifier `ℚ` appears only in display theorems and law proofs.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCost
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22namespace RatioOrbit
  23
  24/-- PRC-native positivity for a ratio orbit: positive signed numerator over a
  25nonzero orbit denominator. The denominator is an orbit position, so nonzero
  26means positive in the verifier display but is not part of the object definition. -/
  27def positive (q : RatioOrbit) : Prop :=
  28  SignedOrbit.nonneg q.num ∧ ¬ SignedOrbit.balanced q.num SignedOrbit.zero
  29
  30theorem positive_iff_toRat_pos (q : RatioOrbit) :
  31    positive q ↔ 0 < q.toRat := by
  32  unfold positive RatioOrbit.toRat
  33  have hdenNat : 0 < q.den.toNat := Nat.pos_of_ne_zero q.den_toNat_ne_zero
  34  have hdenQ : 0 < (q.den.toNat : ℚ) := by exact_mod_cast hdenNat
  35  constructor
  36  · intro h
  37    have hnum_nonneg : 0 ≤ q.num.toInt :=
  38      (SignedOrbit.nonneg_iff_toInt_nonneg q.num).mp h.1
  39    have hnum_ne : q.num.toInt ≠ 0 := by
  40      intro hz
  41      exact h.2 ((SignedOrbit.balanced_iff_toInt_eq q.num SignedOrbit.zero).mpr (by
  42        rw [hz, SignedOrbit.zero_toInt]))
  43    have hnum_pos : 0 < q.num.toInt := by omega
  44    have hnumQ : 0 < (q.num.toInt : ℚ) := by exact_mod_cast hnum_pos
  45    positivity
  46  · intro h
  47    have hnum_pos : 0 < q.num.toInt := by
  48      have hden_ne : (q.den.toNat : ℚ) ≠ 0 := q.den_cast_ne_zero
  49      have hmul : 0 < ((q.num.toInt : ℚ) / (q.den.toNat : ℚ)) * (q.den.toNat : ℚ) :=
  50        mul_pos h hdenQ
  51      have hnumQ : 0 < (q.num.toInt : ℚ) := by
  52        field_simp [hden_ne] at hmul
  53        exact hmul
  54      exact_mod_cast hnumQ
  55    constructor
  56    · exact (SignedOrbit.nonneg_iff_toInt_nonneg q.num).mpr (by omega)
  57    · intro hbal
  58      have hnum_zero : q.num.toInt = 0 := by
  59        have := (SignedOrbit.balanced_iff_toInt_eq q.num SignedOrbit.zero).mp hbal
  60        simpa using this
  61      omega
  62
  63theorem positive_normalize {q : RatioOrbit}
  64    (h : positive q) : positive (DistinctionNat.normalizeRatio q) := by
  65  rw [positive_iff_toRat_pos, DistinctionNat.normalizeRatio_toRat]
  66  exact (positive_iff_toRat_pos q).mp h
  67
  68theorem positive_not_zero {q : RatioOrbit}
  69    (h : positive q) : q.toRat ≠ 0 := by
  70  exact ne_of_gt ((positive_iff_toRat_pos q).mp h)
  71
  72end RatioOrbit
  73
  74namespace PRCRat
  75
  76/-! ## Division and positive rationals -/
  77
  78/-- Division on PRC rationals, defined from PRC multiplication and reciprocal. -/
  79def div (a b : PRCRat) : PRCRat :=
  80  a * b⁻¹
  81
  82instance instDiv : Div PRCRat := ⟨div⟩
  83
  84@[simp] theorem div_eq (a b : PRCRat) : a / b = div a b := rfl
  85
  86theorem toRat_div (a b : PRCRat) :
  87    (a / b).toRat = a.toRat / b.toRat := by
  88  unfold HDiv.hDiv instHDiv Div.div instDiv div
  89  rw [toRat_mul', toRat_inv']
  90  rfl
  91
  92/-- A PRC rational is positive if it has a positive ratio-orbit representative. -/
  93def positive (q : PRCRat) : Prop :=
  94  ∃ r : RatioOrbit, q = mk r ∧ RatioOrbit.positive r
  95
  96theorem positive_iff_toRat_pos (q : PRCRat) :
  97    positive q ↔ 0 < q.toRat := by
  98  constructor
  99  · intro h
 100    rcases h with ⟨r, rfl, hr⟩
 101    rw [toRat_mk]
 102    exact (RatioOrbit.positive_iff_toRat_pos r).mp hr
 103  · refine Quot.induction_on q ?_
 104    intro r hr
 105    exact ⟨r, rfl, (RatioOrbit.positive_iff_toRat_pos r).mpr (by simpa using hr)⟩
 106
 107theorem positive_ne_zero {q : PRCRat}
 108    (h : positive q) : q.toRat ≠ 0 :=
 109  ne_of_gt ((positive_iff_toRat_pos q).mp h)
 110
 111/-! ## Operator-form field laws -/
 112
 113theorem add_assoc' (a b c : PRCRat) :
 114    (a + b) + c = a + (b + c) :=
 115  add_assoc a b c
 116
 117theorem zero_add' (a : PRCRat) :
 118    0 + a = a :=
 119  zero_add a
 120
 121theorem add_zero' (a : PRCRat) :
 122    a + 0 = a :=
 123  add_zero a
 124
 125theorem add_left_neg' (a : PRCRat) :
 126    -a + a = 0 :=
 127  negate_add a
 128
 129theorem add_right_neg' (a : PRCRat) :
 130    a + -a = 0 :=
 131  add_negate a
 132
 133theorem mul_assoc' (a b c : PRCRat) :
 134    (a * b) * c = a * (b * c) :=
 135  mul_assoc a b c
 136
 137theorem one_mul' (a : PRCRat) :
 138    1 * a = a :=
 139  one_mul a
 140
 141theorem mul_one' (a : PRCRat) :
 142    a * 1 = a :=
 143  mul_one a
 144
 145theorem zero_mul' (a : PRCRat) :
 146    0 * a = 0 :=
 147  zero_mul a
 148
 149theorem mul_zero' (a : PRCRat) :
 150    a * 0 = 0 :=
 151  mul_zero a
 152
 153theorem right_distrib' (a b c : PRCRat) :
 154    (a + b) * c = a * c + b * c :=
 155  right_distrib a b c
 156
 157theorem left_distrib' (a b c : PRCRat) :
 158    a * (b + c) = a * b + a * c :=
 159  left_distrib a b c
 160
 161/- `zero_ne_one` is proved structurally (choice-free) in `IntegerRational.lean`
 162via the `isZero` discriminator; the operator-form statement `(0 : PRCRat) ≠ 1`
 163is definitionally the same proposition. -/
 164
 165theorem inv_zero : (0 : PRCRat)⁻¹ = 0 :=
 166  recip_zero
 167
 168theorem inv_mul_cancel {a : PRCRat} (h : a.toRat ≠ 0) :
 169    a⁻¹ * a = 1 := by
 170  apply recip_mul_cancel₀
 171  intro hz
 172  apply h
 173  rw [hz, zero_toRat]
 174
 175theorem div_mul_cancel {a b : PRCRat} (h : b.toRat ≠ 0) :
 176    (a / b) * b = a := by
 177  apply toRat_injective
 178  rw [toRat_mul', toRat_div]
 179  field_simp [h]
 180
 181theorem mul_div_cancel {a b : PRCRat} (h : b.toRat ≠ 0) :
 182    a * b / b = a := by
 183  apply toRat_injective
 184  rw [toRat_div, toRat_mul']
 185  field_simp [h]
 186
 187end PRCRat
 188
 189namespace PRCJCost
 190
 191/-- PRC J-cost lifted from ratio-orbit representatives to the rational quotient. -/
 192def onPRCRat : PRCRat → PRCRat :=
 193  Quot.lift
 194    (fun q => PRCRat.mk (onRatioOrbit q))
 195    (by
 196      intro a b h
 197      apply PRCRat.toRat_injective
 198      rw [PRCRat.toRat_mk, PRCRat.toRat_mk, onRatioOrbit_toRat, onRatioOrbit_toRat]
 199      have hrat : a.toRat = b.toRat := (ratioOrbitEquiv_iff_toRat_eq a b).mp h
 200      rw [hrat])
 201
 202@[simp] theorem onPRCRat_mk (q : RatioOrbit) :
 203    onPRCRat (PRCRat.mk q) = PRCRat.mk (onRatioOrbit q) := by
 204  rfl
 205
 206theorem onPRCRat_toRat (q : PRCRat) :
 207    (onPRCRat q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1 := by
 208  refine Quot.induction_on q ?_
 209  intro r
 210  change (PRCRat.mk (onRatioOrbit r)).toRat =
 211    ((PRCRat.mk r).toRat + (PRCRat.mk r).toRat⁻¹) / 2 - 1
 212  rw [PRCRat.toRat_mk, PRCRat.toRat_mk, onRatioOrbit_toRat]
 213
 214theorem onPRCRat_normalized_representative (q : RatioOrbit) :
 215    onPRCRat (PRCRat.mk q) =
 216      onPRCRat (PRCRat.mk (DistinctionNat.normalizeRatio q)) := by
 217  apply PRCRat.toRat_injective
 218  rw [onPRCRat_toRat, onPRCRat_toRat, PRCRat.toRat_mk, PRCRat.toRat_mk,
 219    DistinctionNat.normalizeRatio_toRat]
 220
 221end PRCJCost
 222
 223/-! ## Bundled certificate -/
 224
 225structure RationalFieldCertificate : Prop where
 226  add_comm : ∀ a b : PRCRat, a + b = b + a
 227  add_assoc : ∀ a b c : PRCRat, (a + b) + c = a + (b + c)
 228  zero_add : ∀ a : PRCRat, 0 + a = a
 229  add_zero : ∀ a : PRCRat, a + 0 = a
 230  add_left_neg : ∀ a : PRCRat, -a + a = 0
 231  mul_comm : ∀ a b : PRCRat, a * b = b * a
 232  mul_assoc : ∀ a b c : PRCRat, (a * b) * c = a * (b * c)
 233  one_mul : ∀ a : PRCRat, 1 * a = a
 234  mul_one : ∀ a : PRCRat, a * 1 = a
 235  left_distrib : ∀ a b c : PRCRat, a * (b + c) = a * b + a * c
 236  right_distrib : ∀ a b c : PRCRat, (a + b) * c = a * c + b * c
 237  zero_ne_one : (0 : PRCRat) ≠ 1
 238  inv_zero : (0 : PRCRat)⁻¹ = 0
 239  mul_inv_cancel : ∀ a : PRCRat, a.toRat ≠ 0 → a * a⁻¹ = 1
 240  inv_mul_cancel : ∀ a : PRCRat, a.toRat ≠ 0 → a⁻¹ * a = 1
 241  div_display : ∀ a b : PRCRat, (a / b).toRat = a.toRat / b.toRat
 242  positive_display : ∀ q : PRCRat, PRCRat.positive q ↔ 0 < q.toRat
 243  ratio_positive_display : ∀ q : RatioOrbit, RatioOrbit.positive q ↔ 0 < q.toRat
 244  jcost_display :
 245    ∀ q : PRCRat, (PRCJCost.onPRCRat q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1
 246  jcost_normalized_representative :
 247    ∀ q : RatioOrbit,
 248      PRCJCost.onPRCRat (PRCRat.mk q) =
 249        PRCJCost.onPRCRat (PRCRat.mk (DistinctionNat.normalizeRatio q))
 250
 251theorem rational_field_certificate : RationalFieldCertificate where
 252  add_comm := PRCRat.add_comm
 253  add_assoc := PRCRat.add_assoc'
 254  zero_add := PRCRat.zero_add'
 255  add_zero := PRCRat.add_zero'
 256  add_left_neg := PRCRat.add_left_neg'
 257  mul_comm := PRCRat.mul_comm
 258  mul_assoc := PRCRat.mul_assoc'
 259  one_mul := PRCRat.one_mul'
 260  mul_one := PRCRat.mul_one'
 261  left_distrib := PRCRat.left_distrib'
 262  right_distrib := PRCRat.right_distrib'
 263  zero_ne_one := PRCRat.zero_ne_one
 264  inv_zero := PRCRat.inv_zero
 265  mul_inv_cancel := by
 266    intro a h
 267    exact PRCRat.mul_recip_cancel h
 268  inv_mul_cancel := by
 269    intro a h
 270    exact PRCRat.inv_mul_cancel h
 271  div_display := PRCRat.toRat_div
 272  positive_display := PRCRat.positive_iff_toRat_pos
 273  ratio_positive_display := RatioOrbit.positive_iff_toRat_pos
 274  jcost_display := PRCJCost.onPRCRat_toRat
 275  jcost_normalized_representative := PRCJCost.onPRCRat_normalized_representative
 276
 277end PrimitiveRecognitionCalculus
 278end Foundation
 279end IndisputableMonolith
 280