IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   5
   6namespace IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
   7
   8open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   9open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  10
  11/-- Cross-multiplication order on `RatioOrbit`: `leQ p q` iff the signed orbit
  12    `p.num * q.den` is `≤` the signed orbit `q.num * p.den`, where the positive
  13    distinctions (dens) are cast in via `SignedOrbit.ofOrbit`. -/
  14def leQ (p q : RatioOrbit) : Prop :=
  15  SignedOrbit.le
  16    (SignedOrbit.mul p.num (SignedOrbit.ofOrbit q.den))
  17    (SignedOrbit.mul q.num (SignedOrbit.ofOrbit p.den))
  18
  19/-- Reflexivity of `leQ`: every rational is ≤ itself. Proved by `le_refl_cf`
  20    at the cross-product, which is literally the same signed orbit on both sides. -/
  21theorem leQ_refl (p : RatioOrbit) : leQ p p := by
  22  unfold leQ
  23  exact le_refl_cf _
  24
  25/-- Totality of `leQ`: for any two rationals, one is ≤ the other. Proved by
  26    `le_total_cf` at the two cross-products. -/
  27theorem leQ_total (p q : RatioOrbit) : leQ p q ∨ leQ q p := by
  28  unfold leQ
  29  exact le_total_cf _ _
  30
  31end IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
  32