IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeTransAntisymm

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4
   5namespace IndisputableMonolith.PRCGrow.RatioOrbitLeTransAntisymm
   6
   7open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   8open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
   9
  10/-- Transitivity of the delta-native cross-multiplication order `leQ` on `RatioOrbit`.
  11    From the two cross-product inequalities, multiply through by the (positive) outer
  12    denominators, chain, and cancel the shared positive denominator `q.den`.
  13    Choice-free: routed through the purified `SignedOrbit.le_iff_toInt_le` bridge and
  14    `Int` cancellation lemmas only. -/
  15theorem leQ_trans (p q r : RatioOrbit) (hpq : leQ p q) (hqr : leQ q r) : leQ p r := by
  16  unfold leQ at hpq hqr ⊢
  17  rw [SignedOrbit.le_iff_toInt_le] at hpq hqr ⊢
  18  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt] at hpq hqr ⊢
  19  -- hpq : p.num.toInt * q.den.toNat ≤ q.num.toInt * p.den.toNat
  20  -- hqr : q.num.toInt * r.den.toNat ≤ r.num.toInt * q.den.toNat
  21  -- goal: p.num.toInt * r.den.toNat ≤ r.num.toInt * p.den.toNat
  22  have hq : (0 : ℤ) < (q.den.toNat : ℤ) := by
  23    have := q.den_toNat_ne_zero
  24    omega
  25  have hp : (0 : ℤ) ≤ (p.den.toNat : ℤ) := Int.natCast_nonneg _
  26  have hr : (0 : ℤ) ≤ (r.den.toNat : ℤ) := Int.natCast_nonneg _
  27  have hchain : p.num.toInt * (r.den.toNat : ℤ) * (q.den.toNat : ℤ)
  28      ≤ r.num.toInt * (p.den.toNat : ℤ) * (q.den.toNat : ℤ) := by
  29    calc p.num.toInt * (r.den.toNat : ℤ) * (q.den.toNat : ℤ)
  30        = p.num.toInt * (q.den.toNat : ℤ) * (r.den.toNat : ℤ) := by ring
  31      _ ≤ q.num.toInt * (p.den.toNat : ℤ) * (r.den.toNat : ℤ) :=
  32          Int.mul_le_mul_of_nonneg_right hpq hr
  33      _ = q.num.toInt * (r.den.toNat : ℤ) * (p.den.toNat : ℤ) := by ring
  34      _ ≤ r.num.toInt * (q.den.toNat : ℤ) * (p.den.toNat : ℤ) :=
  35          Int.mul_le_mul_of_nonneg_right hqr hp
  36      _ = r.num.toInt * (p.den.toNat : ℤ) * (q.den.toNat : ℤ) := by ring
  37  exact Int.le_of_mul_le_mul_right hchain hq
  38
  39/-- Antisymmetry of `leQ` up to the rational equivalence `crossEq`: mutual `leQ`
  40    forces the cross products to be equal, which is exactly `crossEq` through the
  41    purified `crossEq_iff_toIntCross` bridge. Choice-free. -/
  42theorem leQ_antisymm (p q : RatioOrbit) (hpq : leQ p q) (hqp : leQ q p) :
  43    RatioOrbit.crossEq p q := by
  44  unfold leQ at hpq hqp
  45  rw [SignedOrbit.le_iff_toInt_le] at hpq hqp
  46  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt] at hpq hqp
  47  rw [RatioOrbit.crossEq_iff_toIntCross]
  48  exact Int.le_antisymm hpq hqp
  49
  50end IndisputableMonolith.PRCGrow.RatioOrbitLeTransAntisymm
  51