IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitMulPos

   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.RatioOrbitMulPos
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
  11open IndisputableMonolith.PRCGrow.RatioOrbitLtTrichotomy
  12open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  13
  14theorem mul_strictpos_cf (a b : SignedOrbit) (ha : a.neg.toNat < a.pos.toNat) (hb : b.neg.toNat < b.pos.toNat) : (SignedOrbit.mul a b).neg.toNat < (SignedOrbit.mul a b).pos.toNat := by
  15  have hpos : (SignedOrbit.mul a b).pos.toNat = a.pos.toNat * b.pos.toNat + a.neg.toNat * b.neg.toNat := by
  16    show (a.pos * b.pos + a.neg * b.neg).toNat = _
  17    rw [DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul]
  18  have hneg : (SignedOrbit.mul a b).neg.toNat = a.pos.toNat * b.neg.toNat + a.neg.toNat * b.pos.toNat := by
  19    show (a.pos * b.neg + a.neg * b.pos).toNat = _
  20    rw [DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul]
  21  rw [hpos, hneg]; obtain ⟨s, hs⟩ := Nat.exists_eq_add_of_lt ha; obtain ⟨t, ht⟩ := Nat.exists_eq_add_of_lt hb; rw [hs, ht]; ring_nf; omega
  22
  23theorem zero_ltQ_iff_num (r : RatioOrbit) : ltQ RatioOrbit.zero r ↔ r.num.neg.toNat < r.num.pos.toNat := by
  24  unfold ltQ leQ RatioOrbit.crossEq
  25  constructor
  26  · rintro ⟨hle, hne⟩
  27    rw [le_iff_toNat_cf] at hle
  28    rw [SignedOrbit.balanced_iff_toNat_eq] at hne
  29    simp only [RatioOrbit.zero, SignedOrbit.mul, SignedOrbit.ofOrbit, SignedOrbit.zero, SignedOrbit.scaleByNat, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero, DistinctionNat.toNat_succ] at hle hne
  30    omega
  31  · intro h
  32    refine ⟨?_, ?_⟩
  33    · rw [le_iff_toNat_cf]
  34      simp only [RatioOrbit.zero, SignedOrbit.mul, SignedOrbit.ofOrbit, SignedOrbit.zero, SignedOrbit.scaleByNat, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero, DistinctionNat.toNat_succ]
  35      omega
  36    · intro hbal
  37      rw [SignedOrbit.balanced_iff_toNat_eq] at hbal
  38      simp only [RatioOrbit.zero, SignedOrbit.mul, SignedOrbit.ofOrbit, SignedOrbit.zero, SignedOrbit.scaleByNat, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero, DistinctionNat.toNat_succ] at hbal
  39      omega
  40
  41theorem ltQ_mul_pos (p q : RatioOrbit) (hp : ltQ RatioOrbit.zero p) (hq : ltQ RatioOrbit.zero q) : ltQ RatioOrbit.zero (RatioOrbit.mul p q) := by
  42  rw [zero_ltQ_iff_num] at hp hq ⊢
  43  have h : (RatioOrbit.mul p q).num = SignedOrbit.mul p.num q.num := rfl
  44  rw [h]
  45  exact mul_strictpos_cf p.num q.num hp hq
  46
  47end IndisputableMonolith.PRCGrow.RatioOrbitMulPos
  48