IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.IntegerDivisibility

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3
   4namespace IndisputableMonolith.PRCGrow.IntegerDivisibility
   5
   6open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   7
   8-- Choice-free bridges between `balanced` and the integer display, routed through
   9-- the Nat-level `balanced_iff_toNat_eq` (NOT the iff `balanced_iff_toInt_eq`),
  10-- so no order-typeclass / classical content leaks in.
  11
  12theorem balanced_toInt_eq {x y : SignedOrbit} (h : SignedOrbit.balanced x y) :
  13    x.toInt = y.toInt := by
  14  have hn := (SignedOrbit.balanced_iff_toNat_eq x y).mp h
  15  unfold SignedOrbit.toInt
  16  omega
  17
  18theorem balanced_of_toInt_eq {x y : SignedOrbit} (h : x.toInt = y.toInt) :
  19    SignedOrbit.balanced x y := by
  20  rw [SignedOrbit.balanced_iff_toNat_eq]
  21  unfold SignedOrbit.toInt at h
  22  omega
  23
  24def dvdZ (a b : SignedOrbit) : Prop :=
  25  ∃ c : SignedOrbit, SignedOrbit.balanced (SignedOrbit.mul a c) b
  26
  27theorem dvdZ_refl (a : SignedOrbit) : dvdZ a a := by
  28  refine ⟨SignedOrbit.one, balanced_of_toInt_eq ?_⟩
  29  rw [SignedOrbit.mul_toInt, SignedOrbit.one_toInt]
  30  omega
  31
  32theorem dvdZ_trans (a b c : SignedOrbit) (hab : dvdZ a b) (hbc : dvdZ b c) : dvdZ a c := by
  33  obtain ⟨w, hw⟩ := hab
  34  obtain ⟨v, hv⟩ := hbc
  35  refine ⟨SignedOrbit.mul w v, balanced_of_toInt_eq ?_⟩
  36  have hw' := balanced_toInt_eq hw
  37  have hv' := balanced_toInt_eq hv
  38  rw [SignedOrbit.mul_toInt] at hw' hv'
  39  rw [SignedOrbit.mul_toInt, SignedOrbit.mul_toInt]
  40  linear_combination v.toInt * hw' + hv'
  41
  42theorem dvdZ_add (a b c : SignedOrbit) (hab : dvdZ a b) (hac : dvdZ a c) :
  43    dvdZ a (SignedOrbit.add b c) := by
  44  obtain ⟨w, hw⟩ := hab
  45  obtain ⟨v, hv⟩ := hac
  46  refine ⟨SignedOrbit.add w v, balanced_of_toInt_eq ?_⟩
  47  have hw' := balanced_toInt_eq hw
  48  have hv' := balanced_toInt_eq hv
  49  rw [SignedOrbit.mul_toInt] at hw' hv'
  50  rw [SignedOrbit.mul_toInt, SignedOrbit.add_toInt, SignedOrbit.add_toInt]
  51  linear_combination hw' + hv'
  52
  53theorem one_dvdZ (a : SignedOrbit) : dvdZ SignedOrbit.one a := by
  54  refine ⟨a, balanced_of_toInt_eq ?_⟩
  55  rw [SignedOrbit.mul_toInt, SignedOrbit.one_toInt]
  56  omega
  57
  58theorem dvdZ_zero (a : SignedOrbit) : dvdZ a SignedOrbit.zero := by
  59  refine ⟨SignedOrbit.zero, balanced_of_toInt_eq ?_⟩
  60  rw [SignedOrbit.mul_toInt, SignedOrbit.zero_toInt]
  61  omega
  62
  63end IndisputableMonolith.PRCGrow.IntegerDivisibility
  64