Nat.lean — FrcCore

1/-!2# FrcCore.Nat — the arithmetic the shells stand on, from first principles34No Mathlib, no `simp`, no `omega`: every theorem here is checked by `#print axioms` to depend on no5axiom at all. Lean's own core library proves most of these with `propext` for convenience (see6`reports/lean-axioms-probe-20260917/core_probe.log`); they are re-derived here by induction from the7axiom-free primitives (`Nat.rec`, `Nat.add_comm`, `Nat.mul_comm`, `Nat.left_distrib`, `Nat.mod_lt`,8`Nat.le.dest`, `ite_eq_left`, `ite_eq_right`, `Decidable.em`).910The division algorithm is obtained from the definition of `Nat.mod` in `Init.Prelude` (the wrapper11around `Nat.modCore`, itself a fuel recursion): `mod_eq_of_lt`, `mod_eq_sub_mod`, `mod_spec`12(`x = p·q + x % p`) and `mod_unique` (the remainder is determined by any such decomposition). Everything13about residues mod `p` follows from those four.1415Since the ledger migration (task LM17) it also holds `isPrime`, primality by trial division (from 10-dimensions),16and since task LM22 `isPrime_of_bounded`, trial division up to the square root (from 14-entropy).17-/1819namespace FRC.Nat2021/-! ## Cancellation and subtraction -/2223theorem add_left_cancel {a b c : Nat} (h : a + b = a + c) : b = c := by24  induction a with25  | zero => rw [Nat.zero_add, Nat.zero_add] at h; exact h26  | succ a ih =>27    apply ih28    rw [Nat.succ_add, Nat.succ_add] at h29    exact Nat.succ.inj h3031theorem add_right_cancel {a b c : Nat} (h : a + c = b + c) : a = b :=32  add_left_cancel (a := c) (by rw [Nat.add_comm c a, Nat.add_comm c b]; exact h)3334theorem add_sub_cancel (n m : Nat) : n + m - m = n := by35  induction m with36  | zero => rfl37  | succ m ih => rw [Nat.add_succ, Nat.succ_sub_succ]; exact ih3839theorem add_sub_cancel_left (n m : Nat) : n + m - n = m := by40  rw [Nat.add_comm]; exact add_sub_cancel m n4142theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by43  match Nat.le.dest h with44  | ⟨k, hk⟩ => rw [← hk, add_sub_cancel_left, Nat.add_comm]4546theorem sub_add_self_eq_zero (m : Nat) : ∀ k, m - (m + k) = 047  | 0 => Nat.sub_self m48  | k + 1 => by show Nat.pred (m - (m + k)) = 0; rw [sub_add_self_eq_zero m k]; rfl4950theorem sub_eq_zero_of_le {m n : Nat} (h : m ≤ n) : m - n = 0 :=51  match Nat.le.dest h with52  | ⟨k, hk⟩ => by rw [← hk]; exact sub_add_self_eq_zero m k5354theorem add_sub_of_le {n m : Nat} (h : m ≤ n) : m + (n - m) = n := by55  rw [Nat.add_comm]; exact sub_add_cancel h5657theorem sub_lt_of_lt_add {x y z : Nat} (h : x < y + z) (hy : y ≤ x) : x - y < z := by58  refine Nat.lt_of_add_lt_add_right (n := y) ?_59  rw [sub_add_cancel hy, Nat.add_comm z y]60  exact h6162theorem le_of_add_le_add_left {a b c : Nat} (h : a + b ≤ a + c) : b ≤ c := by63  induction a with64  | zero => rw [Nat.zero_add, Nat.zero_add] at h; exact h65  | succ a ih => apply ih; rw [Nat.succ_add, Nat.succ_add] at h; exact Nat.le_of_succ_le_succ h6667theorem le_of_add_le_add_right {a b c : Nat} (h : b + a ≤ c + a) : b ≤ c :=68  le_of_add_le_add_left (a := a) (by rw [Nat.add_comm a b, Nat.add_comm a c]; exact h)6970theorem sub_le_of_le_add {a b c : Nat} (h : a ≤ c + b) : a - b ≤ c := by71  have := Nat.sub_le_sub_right h b72  rw [add_sub_cancel] at this; exact this7374theorem le_add_of_sub_le {a b c : Nat} (hb : b ≤ a) (h : a - b ≤ c) : a ≤ c + b := by75  have := Nat.add_le_add_right h b76  rw [sub_add_cancel hb] at this; exact this7778theorem le_sub_of_add_le {a b c : Nat} (h : c + b ≤ a) : c ≤ a - b := by79  have := Nat.sub_le_sub_right h b80  rw [add_sub_cancel] at this; exact this8182theorem succ_ne_zero (n : Nat) : n + 1 ≠ 0 := fun h => Nat.noConfusion h8384theorem pos_of_lt {a b : Nat} (h : a < b) : 0 < b :=85  Nat.lt_of_le_of_lt (Nat.zero_le a) h8687/-! ## Multiplication -/8889theorem mul_assoc (a b c : Nat) : a * b * c = a * (b * c) := by90  induction c with91  | zero => rfl92  | succ c ih => rw [Nat.mul_succ, Nat.mul_succ, ih, Nat.left_distrib]9394theorem add_mul (a b c : Nat) : (a + b) * c = a * c + b * c := by95  rw [Nat.mul_comm, Nat.left_distrib, Nat.mul_comm c a, Nat.mul_comm c b]9697theorem add_add_add_comm (a b c d : Nat) : a + b + (c + d) = a + c + (b + d) := by98  rw [Nat.add_assoc, Nat.add_assoc, Nat.add_left_comm b]99100theorem mul_left_comm (a b c : Nat) : a * (b * c) = b * (a * c) := by101  rw [← mul_assoc, Nat.mul_comm a b, mul_assoc]102103theorem mul_lt_mul_of_lt_of_pos {a b c : Nat} (h : a < b) (hc : 0 < c) : a * c < b * c := by104  rw [Nat.mul_comm a c, Nat.mul_comm b c]105  exact Nat.mul_lt_mul_of_pos_left h hc106107/-! ## The division algorithm, from the definition of `Nat.mod` -/108109section mod110111/-- The fuel of `Nat.modCore.go` does not matter once it exceeds the dividend. -/112theorem modCore_go_fuel {y : Nat} (hy : 0 < y) : ∀ (f1 f2 x : Nat) (h1 : x < f1) (h2 : x < f2),113    Nat.modCore.go y hy f1 x h1 = Nat.modCore.go y hy f2 x h2 := by114  intro f1115  induction f1 with116  | zero => intro f2 x h1; exact absurd h1 (Nat.not_lt_zero x)117  | succ f1 ih =>118    intro f2 x h1 h2119    cases f2 with120    | zero => exact absurd h2 (Nat.not_lt_zero x)121    | succ f2 =>122      show (if h : y ≤ x then Nat.modCore.go y hy f1 (x - y) _ else x)123          = (if h : y ≤ x then Nat.modCore.go y hy f2 (x - y) _ else x)124      exact match Nat.decLe y x with125        | .isTrue h => by rw [dite_eq_left h, dite_eq_left h]; exact ih f2 (x - y) _ _126        | .isFalse h => by rw [dite_eq_right h, dite_eq_right h]127128theorem modCore_eq' (x y : Nat) (hy : 0 < y) :129    Nat.modCore x y = if y ≤ x then Nat.modCore (x - y) y else x := by130  unfold Nat.modCore131  rw [dite_eq_left hy]132  show (if h : y ≤ x then Nat.modCore.go y hy x (x - y) _ else x) = _133  exact match Nat.decLe y x with134    | .isTrue h => by135        rw [dite_eq_left h, ite_eq_left h, dite_eq_left hy]136        exact modCore_go_fuel hy x (x - y + 1) (x - y) _ _137    | .isFalse h => by rw [dite_eq_right h, ite_eq_right h]138139theorem modCore_eq_mod' (n m : Nat) (hm : 0 < m) : Nat.modCore n m = n % m := by140  cases n with141  | zero =>142    show Nat.modCore 0 m = 0143    rw [modCore_eq' 0 m hm, ite_eq_right (Nat.not_le_of_lt hm)]144  | succ n =>145    show Nat.modCore (n + 1) m = ite (m ≤ n + 1) (Nat.modCore (n + 1) m) (n + 1)146    exact match Nat.decLe m (n + 1) with147      | .isTrue h => by rw [ite_eq_left h]148      | .isFalse h => by rw [ite_eq_right h, modCore_eq' _ _ hm, ite_eq_right h]149150theorem mod_eq_of_lt {x y : Nat} (h : x < y) : x % y = x := by151  cases x with152  | zero => rfl153  | succ n =>154    show ite (y ≤ n + 1) (Nat.modCore (n + 1) y) (n + 1) = n + 1155    rw [ite_eq_right (Nat.not_le_of_lt h)]156157theorem mod_eq_sub_mod {x y : Nat} (hy : 0 < y) (h : y ≤ x) : x % y = (x - y) % y := by158  rw [← modCore_eq_mod' x y hy, modCore_eq' x y hy, ite_eq_left h, modCore_eq_mod' _ _ hy]159160/-- The division algorithm: `x = p·q + x % p` for some `q`. -/161theorem mod_spec (p : Nat) (hp : 0 < p) : ∀ x : Nat, ∃ q, x = p * q + x % p := by162  intro x163  induction x using Nat.strongRecOn with164  | _ x ih =>165    exact match Nat.decLe p x with166      | .isTrue h =>167          match ih (x - p) (Nat.sub_lt (Nat.lt_of_lt_of_le hp h) hp) with168          | ⟨q, hq⟩ => ⟨q + 1, by169              rw [mod_eq_sub_mod hp h, Nat.mul_succ, Nat.add_assoc, Nat.add_comm p, ← Nat.add_assoc,170                ← hq, sub_add_cancel h]⟩171      | .isFalse h => ⟨0, by rw [mod_eq_of_lt (Nat.lt_of_not_le h), Nat.mul_zero, Nat.zero_add]⟩172173/-- Uniqueness of the decomposition: the quotients agree. -/174theorem quot_unique {p q q' r r' : Nat} (hr : r < p) (hr' : r' < p) (h : p * q + r = p * q' + r') :175    q = q' := by176  have key : ∀ {q q' r r' : Nat}, r < p → r' < p → p * q + r = p * q' + r' → ¬ q < q' := by177    intro q q' r r' hr hr' h hlt178    have h1 : p * (q + 1) ≤ p * q' := Nat.mul_le_mul_left p hlt179    have h2 : p * q + r < p * q + p := Nat.add_lt_add_left hr _180    rw [Nat.mul_succ] at h1181    have h3 : p * q + r < p * q' + r' := Nat.lt_of_lt_of_le h2 (Nat.le_trans h1 (Nat.le_add_right _ _))182    rw [h] at h3183    exact Nat.lt_irrefl _ h3184  exact match Nat.lt_or_ge q q' with185    | .inl hlt => absurd hlt (key hr hr' h)186    | .inr hge => match Nat.lt_or_ge q' q with187      | .inl hlt => absurd hlt (key hr' hr h.symm)188      | .inr hge' => Nat.le_antisymm hge' hge189190/-- The remainder is determined: if `x = p·q + r` with `r < p`, then `r = x % p`. -/191theorem mod_unique {p x q r : Nat} (hr : r < p) (h : x = p * q + r) : x % p = r := by192  have hp : 0 < p := pos_of_lt hr193  match mod_spec p hp x with194  | ⟨q', hq'⟩ =>195    have hqq : q' = q := quot_unique (Nat.mod_lt x hp) hr (by rw [← hq', ← h])196    rw [hqq] at hq'197    rw [h] at hq'198    rw [h]199    exact (add_left_cancel hq').symm200201theorem mod_mod (x p : Nat) (hp : 0 < p) : x % p % p = x % p :=202  mod_eq_of_lt (Nat.mod_lt x hp)203204theorem add_mod (a b p : Nat) (hp : 0 < p) : (a + b) % p = (a % p + b % p) % p := by205  match mod_spec p hp a, mod_spec p hp b, mod_spec p hp (a % p + b % p) with206  | ⟨qa, ha⟩, ⟨qb, hb⟩, ⟨qc, hc⟩ =>207    apply mod_unique (q := qa + qb + qc) (Nat.mod_lt _ hp)208    rw [Nat.left_distrib, Nat.left_distrib, Nat.add_assoc, ← hc]209    rw [Nat.add_assoc, Nat.add_left_comm (p * qb), ← Nat.add_assoc, ← ha, ← hb]210211theorem add_mul_mod_self_left (x k p : Nat) (hp : 0 < p) : (p * k + x) % p = x % p := by212  match mod_spec p hp x with213  | ⟨q, hq⟩ =>214    apply mod_unique (q := k + q) (Nat.mod_lt x hp)215    rw [Nat.left_distrib, Nat.add_assoc, ← hq]216217theorem mul_mod_left' (a b p : Nat) (hp : 0 < p) : (a * b) % p = (a % p * b) % p := by218  match mod_spec p hp a with219  | ⟨qa, ha⟩ =>220    have e : a * b = p * (qa * b) + a % p * b := by221      rw [← mul_assoc, ← add_mul, ← ha]222    rw [e, add_mul_mod_self_left _ _ _ hp]223224theorem mul_mod (a b p : Nat) (hp : 0 < p) : (a * b) % p = (a % p * (b % p)) % p := by225  rw [mul_mod_left' a b p hp, Nat.mul_comm (a % p) b, mul_mod_left' b (a % p) p hp,226    Nat.mul_comm (b % p) (a % p)]227228theorem mod_self (p : Nat) (hp : 0 < p) : p % p = 0 :=229  mod_unique hp (by rw [Nat.mul_one, Nat.add_zero])230231theorem zero_mod (p : Nat) : 0 % p = 0 := rfl232233theorem mod_add_mod (a b p : Nat) (hp : 0 < p) : (a % p + b) % p = (a + b) % p := by234  rw [add_mod a b p hp, add_mod (a % p) b p hp, mod_mod _ _ hp]235236theorem add_mod_mod (a b p : Nat) (hp : 0 < p) : (a + b % p) % p = (a + b) % p := by237  rw [add_mod a b p hp, add_mod a (b % p) p hp, mod_mod _ _ hp]238239theorem mod_mul_mod (a b p : Nat) (hp : 0 < p) : (a % p * b) % p = (a * b) % p :=240  (mul_mod_left' a b p hp).symm241242theorem mul_mod_mod (a b p : Nat) (hp : 0 < p) : (a * (b % p)) % p = (a * b) % p := by243  rw [mul_mod a (b % p) p hp, mod_mod _ _ hp, ← mul_mod a b p hp]244245theorem mod_lt' (x : Nat) {p : Nat} (hp : 0 < p) : x % p < p := Nat.mod_lt x hp246247end mod248249/-! ## Powers -/250251theorem pow_succ' (a n : Nat) : a ^ (n + 1) = a ^ n * a := rfl252253theorem pow_add (a m n : Nat) : a ^ (m + n) = a ^ m * a ^ n := by254  induction n with255  | zero => rw [Nat.add_zero, Nat.pow_zero, Nat.mul_one]256  | succ n ih => rw [Nat.add_succ, Nat.pow_succ, ih, Nat.pow_succ, mul_assoc]257258theorem pow_mul (a m n : Nat) : a ^ (m * n) = (a ^ m) ^ n := by259  induction n with260  | zero => rw [Nat.mul_zero, Nat.pow_zero, Nat.pow_zero]261  | succ n ih => rw [Nat.mul_succ, pow_add, ih, Nat.pow_succ]262263theorem pos_pow_of_pos {a : Nat} (n : Nat) (h : 0 < a) : 0 < a ^ n := Nat.pow_pos h264265/-! ## Primality (10-dimensions' predicate, moved by task LM17) -/266267/-- Primality by trial division, decidable. -/268def isPrime (n : Nat) : Prop := 2 ≤ n ∧ ∀ d, d < n → 2 ≤ d → n % d ≠ 0269instance (n : Nat) : Decidable (isPrime n) := by unfold isPrime; exact inferInstance270271/-- Trial division up to `B` decides primality when `n < (B + 1)²`: a divisor `d ≥ 2` of `n` with272`d > B` has a cofactor `q = n/d` with `2 ≤ q ≤ B`, itself a divisor. (From 14-entropy, moved by task LM22.) -/273theorem isPrime_of_bounded (n B : Nat) (h2 : 2 ≤ n) (hB : n < (B + 1) * (B + 1))274    (hd : ∀ d, d < B + 1 → 2 ≤ d → n % d ≠ 0) : isPrime n := by275  refine ⟨h2, fun d hdn hd2 hmod => ?_⟩276  have hd0 : 0 < d := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hd2277  obtain ⟨q, hq⟩ := mod_spec d hd0 n278  rw [hmod, Nat.add_zero] at hq279  match Nat.lt_or_ge d (B + 1) with280  | .inl hlt => exact hd d hlt hd2 hmod281  | .inr hge =>282    -- the cofactor `q`: `n = d q`, `q ≥ 2` (else `n = 0` or `n = d`), and `q ≤ B` (else `d q ≥ (B+1)²`)283    have hq2 : 2 ≤ q := by284      match q with285      | 0 => rw [Nat.mul_zero] at hq; exact absurd (hq ▸ h2) (Nat.not_succ_le_zero 1)286      | 1 => rw [Nat.mul_one] at hq; exact absurd (hq ▸ hdn) (Nat.lt_irrefl d)287      | q + 2 => exact Nat.le_add_left 2 q288    have hqB : q < B + 1 := by289      match Nat.lt_or_ge q (B + 1) with290      | .inl h => exact h291      | .inr hqge =>292        have : (B + 1) * (B + 1) ≤ d * q := Nat.mul_le_mul hge hqge293        exact absurd (Nat.lt_of_lt_of_le hB this) (hq ▸ Nat.lt_irrefl n)294    have hq0 : 0 < q := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hq2295    have hmodq : n % q = 0 :=296      mod_unique hq0 (by rw [hq, Nat.mul_comm d q, Nat.add_zero])297    exact hd q hqB hq2 hmodq298299end FRC.Nat300