IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitOrderMulNonneg

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4
   5namespace IndisputableMonolith.PRCGrow.RatioOrbitOrderMulNonneg
   6
   7open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   8open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
   9
  10/-- Choice-free characterization of nonnegativity in the `leQ` order:
  11    `zero ≤ r` iff the numerator's signed-orbit integer is nonnegative.
  12    Routed through the purified `SignedOrbit.le_iff_toInt_le` bridge; the
  13    zero side collapses because `RatioOrbit.zero` has numerator integer `0`
  14    and denominator `1`. -/
  15theorem zero_leQ_iff (r : RatioOrbit) :
  16    leQ RatioOrbit.zero r ↔ (0 : ℤ) ≤ r.num.toInt := by
  17  unfold leQ
  18  rw [SignedOrbit.le_iff_toInt_le]
  19  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt, RatioOrbit.zero,
  20    SignedOrbit.zero_toInt, DistinctionNat.toNat_succ, DistinctionNat.toNat_zero]
  21  constructor
  22  · intro h
  23    omega
  24  · intro h
  25    omega
  26
  27/-- The ordered-ring law for the delta-native rational order: multiplying both
  28    sides of a `leQ` inequality on the right by a nonnegative ratio orbit
  29    preserves the order. Expand `RatioOrbit.mul` on representatives, reduce the
  30    cross-products to integer arithmetic through the choice-free `toInt`
  31    bridge (casts moved by the axiom-free `Int.natCast_mul`, never `push_cast`,
  32    which smuggles `Classical.choice` on this goal shape), and close with
  33    `Int.mul_le_mul_of_nonneg_right` after a `ring` regrouping that isolates
  34    the common nonnegative factor `r.num.toInt * r.den.toNat`. Choice-free:
  35    `#print axioms` is `{propext, Quot.sound}`. -/
  36theorem leQ_mul_nonneg_right (p q r : RatioOrbit)
  37    (hr : leQ RatioOrbit.zero r) (hpq : leQ p q) :
  38    leQ (RatioOrbit.mul p r) (RatioOrbit.mul q r) := by
  39  rw [zero_leQ_iff] at hr
  40  unfold leQ at hpq ⊢
  41  rw [SignedOrbit.le_iff_toInt_le] at hpq ⊢
  42  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt, RatioOrbit.mul,
  43    DistinctionNat.toNat_mul] at hpq ⊢
  44  -- hpq : p.num.toInt * q.den.toNat ≤ q.num.toInt * p.den.toNat
  45  -- goal: p.num.toInt * r.num.toInt * (q.den.toNat * r.den.toNat)
  46  --     ≤ q.num.toInt * r.num.toInt * (p.den.toNat * r.den.toNat)
  47  rw [Int.natCast_mul, Int.natCast_mul]
  48  have hrd : (0 : ℤ) ≤ (r.den.toNat : ℤ) := Int.natCast_nonneg _
  49  have hfac : (0 : ℤ) ≤ r.num.toInt * (r.den.toNat : ℤ) :=
  50    Int.mul_nonneg hr hrd
  51  have hstep : p.num.toInt * (q.den.toNat : ℤ) * (r.num.toInt * (r.den.toNat : ℤ))
  52      ≤ q.num.toInt * (p.den.toNat : ℤ) * (r.num.toInt * (r.den.toNat : ℤ)) :=
  53    Int.mul_le_mul_of_nonneg_right hpq hfac
  54  calc p.num.toInt * r.num.toInt * ((q.den.toNat : ℤ) * (r.den.toNat : ℤ))
  55      = p.num.toInt * (q.den.toNat : ℤ) * (r.num.toInt * (r.den.toNat : ℤ)) := by ring
  56    _ ≤ q.num.toInt * (p.den.toNat : ℤ) * (r.num.toInt * (r.den.toNat : ℤ)) := hstep
  57    _ = q.num.toInt * r.num.toInt * ((p.den.toNat : ℤ) * (r.den.toNat : ℤ)) := by ring
  58
  59end IndisputableMonolith.PRCGrow.RatioOrbitOrderMulNonneg
  60