IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitOrderAddMono

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   5
   6namespace IndisputableMonolith.PRCGrow.RatioOrbitOrderAddMono
   7
   8open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   9open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
  10open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  11
  12/-- Choice-free unfold of `toInt` to its pos/neg Nat-cast difference. -/
  13private lemma toInt_eq (a : SignedOrbit) :
  14    a.toInt = (a.pos.toNat : ℤ) - (a.neg.toNat : ℤ) := by
  15  cases a with
  16  | mk pos neg => exact SignedOrbit.toInt_mk pos neg
  17
  18/-- Choice-free Int order bridge, routed through the CF Nat bridge `le_iff_toNat_cf`
  19    (never through the choice-tainted `SignedOrbit.le_iff_toInt_le`). -/
  20private lemma le_iff_toInt_le_cf (a b : SignedOrbit) :
  21    SignedOrbit.le a b ↔ a.toInt ≤ b.toInt := by
  22  rw [le_iff_toNat_cf, toInt_eq a, toInt_eq b]
  23  constructor
  24  · intro hh; omega
  25  · intro hh; omega
  26
  27/-- Translation invariance of the delta-native ratio order: the order on `RatioOrbit`
  28    is compatible with addition. -/
  29theorem leQ_add_right (p q r : RatioOrbit) (h : leQ p q) :
  30    leQ (RatioOrbit.add p r) (RatioOrbit.add q r) := by
  31  unfold leQ at h ⊢
  32  rw [le_iff_toInt_le_cf] at h ⊢
  33  unfold RatioOrbit.add
  34  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt, SignedOrbit.scaleByNat_toInt,
  35             SignedOrbit.add_toInt, DistinctionNat.toNat_mul] at h ⊢
  36  push_cast at h ⊢
  37  rw [← Int.sub_nonneg] at h ⊢
  38  have hc : (0:ℤ) ≤ (r.den.toNat : ℤ) * (r.den.toNat : ℤ) :=
  39    Int.mul_nonneg (by omega) (by omega)
  40  have hprod := Int.mul_nonneg h hc
  41  convert hprod using 1 <;> ring
  42
  43end IndisputableMonolith.PRCGrow.RatioOrbitOrderAddMono
  44