IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic

   1/-
   2  PrimitiveRecognitionCalculus/OrbitArithmetic.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K4.5 (orbit arithmetic), K4.6 (balanced length), K4.7 (cross-multiplication)
   9
  10  Addition and multiplication on the δ-orbit, with the transport theorems
  11  to Lean Nat needed for the balanced and cross-multiplication
  12  characterizations of `PRCInt` and `PRCRat`.
  13
  14  Strength: δ-only. The construction uses only the inductive structure of
  15  the orbit and the verifier-level transport already established in
  16  `Orbit.lean`. No project-local axioms.
  17-/
  18
  19import Mathlib
  20import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace PrimitiveRecognitionCalculus
  25namespace DistinctionNat
  26
  27/-! ## Addition on the δ-orbit -/
  28
  29/-- K4.5. Addition of orbit positions: concatenation of repetition. -/
  30def add : DistinctionNat → DistinctionNat → DistinctionNat
  31  | a, zero => a
  32  | a, succ b => succ (add a b)
  33
  34instance : Add DistinctionNat := ⟨add⟩
  35
  36theorem add_def (a b : DistinctionNat) :
  37    a + b = add a b := rfl
  38
  39theorem add_zero_eq (a : DistinctionNat) :
  40    a + zero = a := rfl
  41
  42theorem add_succ_eq (a b : DistinctionNat) :
  43    a + succ b = succ (a + b) := rfl
  44
  45theorem zero_add_eq (a : DistinctionNat) :
  46    zero + a = a := by
  47  induction a with
  48  | zero => rfl
  49  | succ n ih =>
  50      show succ (zero + n) = succ n
  51      rw [ih]
  52
  53theorem succ_add_eq (a b : DistinctionNat) :
  54    succ a + b = succ (a + b) := by
  55  induction b with
  56  | zero => rfl
  57  | succ n ih =>
  58      show succ (succ a + n) = succ (succ (a + n))
  59      rw [ih]
  60
  61theorem add_comm (a b : DistinctionNat) :
  62    a + b = b + a := by
  63  induction a with
  64  | zero =>
  65      rw [zero_add_eq, add_zero_eq]
  66  | succ n ih =>
  67      rw [succ_add_eq, add_succ_eq, ih]
  68
  69theorem add_assoc (a b c : DistinctionNat) :
  70    (a + b) + c = a + (b + c) := by
  71  induction c with
  72  | zero => rfl
  73  | succ n ih =>
  74      show (a + b) + succ n = a + (b + succ n)
  75      rw [add_succ_eq, add_succ_eq, add_succ_eq, ih]
  76
  77/-! ## Transport to Lean Nat -/
  78
  79/-- K4.5. The verifier display of orbit addition matches Lean Nat addition. -/
  80theorem toNat_add (a b : DistinctionNat) :
  81    (a + b).toNat = a.toNat + b.toNat := by
  82  induction b with
  83  | zero =>
  84      rw [add_zero_eq, toNat_zero, Nat.add_zero]
  85  | succ n ih =>
  86      show (succ (a + n)).toNat = a.toNat + (succ n).toNat
  87      rw [toNat_succ, toNat_succ, ih]
  88      omega
  89
  90/-- The verifier display is injective: equal Nat displays come from equal
  91orbit positions. -/
  92theorem toNat_inj {a b : DistinctionNat} (h : a.toNat = b.toNat) :
  93    a = b := by
  94  have := congrArg DistinctionNat.ofNat h
  95  rwa [ofNat_toNat, ofNat_toNat] at this
  96
  97/-! ## Cancellation -/
  98
  99/-- K4.5. Left cancellation for orbit addition. -/
 100theorem add_left_cancel {a b c : DistinctionNat}
 101    (h : a + b = a + c) : b = c := by
 102  apply toNat_inj
 103  have h' : (a + b).toNat = (a + c).toNat := by rw [h]
 104  rw [toNat_add, toNat_add] at h'
 105  exact Nat.add_left_cancel h'
 106
 107/-- K4.5. Right cancellation for orbit addition. -/
 108theorem add_right_cancel {a b c : DistinctionNat}
 109    (h : a + c = b + c) : a = b := by
 110  apply add_left_cancel (a := c)
 111  rw [add_comm c a, add_comm c b]
 112  exact h
 113
 114/-! ## Multiplication on the δ-orbit -/
 115
 116/-- K4.7. Multiplication of orbit positions: nested repetition. -/
 117def mul : DistinctionNat → DistinctionNat → DistinctionNat
 118  | _, zero => zero
 119  | a, succ b => mul a b + a
 120
 121instance : Mul DistinctionNat := ⟨mul⟩
 122
 123theorem mul_def (a b : DistinctionNat) :
 124    a * b = mul a b := rfl
 125
 126theorem mul_zero_eq (a : DistinctionNat) :
 127    a * zero = zero := rfl
 128
 129theorem mul_succ_eq (a b : DistinctionNat) :
 130    a * succ b = a * b + a := rfl
 131
 132theorem zero_mul_eq (a : DistinctionNat) :
 133    zero * a = zero := by
 134  induction a with
 135  | zero => rfl
 136  | succ n ih =>
 137      show zero * n + zero = zero
 138      rw [add_zero_eq, ih]
 139
 140theorem succ_mul_eq (a b : DistinctionNat) :
 141    succ a * b = a * b + b := by
 142  induction b with
 143  | zero =>
 144      rw [mul_zero_eq, mul_zero_eq, add_zero_eq]
 145  | succ n ih =>
 146      show succ a * n + succ a = (a * n + a) + succ n
 147      rw [ih, add_succ_eq, add_succ_eq]
 148      congr 1
 149      rw [add_assoc, add_assoc, add_comm a n]
 150
 151theorem mul_comm (a b : DistinctionNat) :
 152    a * b = b * a := by
 153  induction a with
 154  | zero =>
 155      rw [zero_mul_eq, mul_zero_eq]
 156  | succ n ih =>
 157      rw [succ_mul_eq, mul_succ_eq, ih]
 158
 159/-- K4.7. The verifier display of orbit multiplication matches Lean Nat. -/
 160theorem toNat_mul (a b : DistinctionNat) :
 161    (a * b).toNat = a.toNat * b.toNat := by
 162  induction b with
 163  | zero =>
 164      show (a * zero).toNat = a.toNat * zero.toNat
 165      rw [mul_zero_eq, toNat_zero]
 166      omega
 167  | succ n ih =>
 168      show (a * n + a).toNat = a.toNat * (succ n).toNat
 169      rw [toNat_add, toNat_succ, ih, Nat.mul_succ]
 170
 171/-- K4.7. Product of nonzero orbit positions is nonzero. -/
 172theorem mul_ne_zero {a b : DistinctionNat}
 173    (ha : a ≠ zero) (hb : b ≠ zero) :
 174    a * b ≠ zero := by
 175  intro h
 176  have hnat : (a * b).toNat = zero.toNat := by rw [h]
 177  rw [toNat_mul, toNat_zero] at hnat
 178  rcases Nat.mul_eq_zero.mp hnat with hzero | hzero
 179  · have : a = zero := by
 180      apply toNat_inj
 181      rw [toNat_zero]
 182      exact hzero
 183    exact ha this
 184  · have : b = zero := by
 185      apply toNat_inj
 186      rw [toNat_zero]
 187      exact hzero
 188    exact hb this
 189
 190end DistinctionNat
 191
 192end PrimitiveRecognitionCalculus
 193end Foundation
 194end IndisputableMonolith
 195