IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitDenseMediant

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLtTrichotomy
   5import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   6
   7namespace IndisputableMonolith.PRCGrow.RatioOrbitDenseMediant
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
  11open IndisputableMonolith.PRCGrow.RatioOrbitLtTrichotomy
  12open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  13
  14def mediant (p q : RatioOrbit) : RatioOrbit where
  15  num := SignedOrbit.add p.num q.num
  16  den := p.den + q.den
  17  den_ne_zero := by
  18    intro h
  19    have hp := RatioOrbit.den_toNat_ne_zero p
  20    have hq := RatioOrbit.den_toNat_ne_zero q
  21    have hadd : (p.den + q.den).toNat = p.den.toNat + q.den.toNat :=
  22      DistinctionNat.toNat_add p.den q.den
  23    have h2 : DistinctionNat.zero.toNat = p.den.toNat + q.den.toNat := by
  24      rw [← h]; exact hadd
  25    have h0 : DistinctionNat.zero.toNat = 0 := rfl
  26    rw [h0] at h2
  27    omega
  28
  29theorem ltQ_iff_toNat (p q : RatioOrbit) :
  30    ltQ p q ↔
  31    p.num.pos.toNat * q.den.toNat + q.num.neg.toNat * p.den.toNat <
  32    q.num.pos.toNat * p.den.toNat + p.num.neg.toNat * q.den.toNat := by
  33  unfold ltQ leQ RatioOrbit.crossEq
  34  rw [le_iff_toNat_cf, SignedOrbit.balanced_iff_toNat_eq]
  35  simp only [SignedOrbit.mul_pos, SignedOrbit.mul_neg, SignedOrbit.scaleByNat_pos,
  36             SignedOrbit.scaleByNat_neg, SignedOrbit.ofOrbit,
  37             DistinctionNat.toNat_add, DistinctionNat.toNat_mul]
  38  constructor
  39  · intro h
  40    have hz : DistinctionNat.zero.toNat = 0 := rfl
  41    simp only [hz, Nat.mul_zero, Nat.add_zero, Nat.zero_add] at *
  42    obtain ⟨h1, h2⟩ := h
  43    omega
  44  · intro h
  45    have hz : DistinctionNat.zero.toNat = 0 := rfl
  46    simp only [hz, Nat.mul_zero, Nat.add_zero, Nat.zero_add] at *
  47    refine ⟨?_, ?_⟩
  48    · omega
  49    · omega
  50
  51theorem ltQ_mediant : ∀ p q, ltQ p q → ltQ p (mediant p q) ∧ ltQ (mediant p q) q := by
  52  intro p q h
  53  rw [ltQ_iff_toNat] at h
  54  refine ⟨?_, ?_⟩
  55  · rw [ltQ_iff_toNat]
  56    simp only [mediant, SignedOrbit.add_pos, SignedOrbit.add_neg,
  57               DistinctionNat.toNat_add, Nat.mul_add, Nat.add_mul]
  58    generalize p.num.pos.toNat * p.den.toNat = e1 at *
  59    generalize p.num.pos.toNat * q.den.toNat = e2 at *
  60    generalize p.num.neg.toNat * p.den.toNat = e3 at *
  61    generalize q.num.neg.toNat * p.den.toNat = e4 at *
  62    generalize q.num.pos.toNat * p.den.toNat = e5 at *
  63    generalize p.num.neg.toNat * q.den.toNat = e6 at *
  64    omega
  65  · rw [ltQ_iff_toNat]
  66    simp only [mediant, SignedOrbit.add_pos, SignedOrbit.add_neg,
  67               DistinctionNat.toNat_add, Nat.mul_add, Nat.add_mul]
  68    generalize p.num.pos.toNat * q.den.toNat = e2 at *
  69    generalize q.num.pos.toNat * q.den.toNat = e7 at *
  70    generalize q.num.neg.toNat * p.den.toNat = e4 at *
  71    generalize q.num.neg.toNat * q.den.toNat = e8 at *
  72    generalize q.num.pos.toNat * p.den.toNat = e5 at *
  73    generalize p.num.neg.toNat * q.den.toNat = e6 at *
  74    omega
  75
  76end IndisputableMonolith.PRCGrow.RatioOrbitDenseMediant
  77