Grace/Cumulus/NumberTheory/ModularMore.g17

Open in Workbench Download source

Imports

Euler · DivisibilityMore

Declarations

Source

1-- More modular arithmetic: remainders of multiples and sums, powers, the2-- exhaustive small remainders, congruence modulo n as a predicate with its3-- equivalence and compatibility laws, cancellation of a coprime factor, and4-- the congruence forms of Euler's and Fermat's theorems5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.NumberTheory.ModularMore11import Euler12import DivisibilityMore1314theorem mod.self (n : Nat)15  shows n % n = 016proof17  have reflexive := divides.reflexive at n18  have characterization := divides.iff_mod_zero at n, n19  exact characterization.forward with reflexive2021theorem mod.mul_self_left (n k : Nat)22  shows (n * k) % n = 023proof24  have multiple := divides.mul_left_self at n, k25  have characterization := divides.iff_mod_zero at n, n * k26  exact characterization.forward with multiple2728theorem mod.mul_self_right (n k : Nat)29  shows (k * n) % n = 030proof31  have multiple := divides.mul_right_self at n, k32  have characterization := divides.iff_mod_zero at n, k * n33  exact characterization.forward with multiple3435theorem mod.of_divides (d a : Nat)36  requires hda : d ∣ a37  shows a % d = 038proof39  have characterization := divides.iff_mod_zero at d, a40  exact characterization.forward with hda4142theorem mod.add_self (n a : Nat)43  requires nonzero : n ≠ 044  shows (a + n) % n = a % n45proof46  have shifted := mod.add_multiple at n, a, 1 with nonzero47  have one : a + n * 1 = a + n by ring48  rw one at shifted49  exact shifted5051theorem mod.self_add (n a : Nat)52  requires nonzero : n ≠ 053  shows (n + a) % n = a % n54proof55  have commute : n + a = a + n by ring56  rw commute57  exact mod.add_self at n, a with nonzero5859theorem mod.multiple_add (n a s : Nat)60  requires nonzero : n ≠ 061  shows (n * s + a) % n = a % n62proof63  have commute : n * s + a = a + n * s by ring64  rw commute65  exact mod.add_multiple at n, a, s with nonzero6667theorem mod.le (n a : Nat)68  shows a % n ≤ a69proof70  have split : n = 0 ∨ n ≠ 0 by tauto71  cases split with zero | nonzero72  . rw zero73    have value := mod.zero_right at a74    rw value75    exact LessEqual.reflexive at a76  . obtain ⟨q, qNat, equation⟩ := mod.equation at a, n with nonzero77    witness n * q78    symm79    linear_combination equation8081theorem mod.eq_self_iff (n a : Nat)82  requires nonzero : n ≠ 083  shows a % n = a ↔ a < n84proof85  constructor86  . intro same87    have bound := mod.less at a, n with nonzero88    rw same at bound89    exact bound90  . intro below91    exact mod.of_less with below9293theorem mod.one_left (n : Nat)94  requires above : 1 < n95  shows 1 % n = 196proof97  exact mod.of_less with above9899theorem mod.add_mod_left (n a b : Nat)100  requires nonzero : n ≠ 0101  shows (a % n + b) % n = (a + b) % n102proof103  have first := mod.add at n, a % n, b with nonzero104  have second := mod.add at n, a, b with nonzero105  have idempotent := mod.mod at n, a with nonzero106  rw [first, idempotent, second]107  rfl108109theorem mod.add_mod_right (n a b : Nat)110  requires nonzero : n ≠ 0111  shows (a + b % n) % n = (a + b) % n112proof113  have first := mod.add at n, a, b % n with nonzero114  have second := mod.add at n, a, b with nonzero115  have idempotent := mod.mod at n, b with nonzero116  rw [first, idempotent, second]117  rfl118119theorem mod.pow (n a k : Nat)120  requires nonzero : n ≠ 0121  shows (a ^ k) % n = ((a % n) ^ k) % n122proof123  induction k124  | zero =>125    have left := pow.zero at a126    have right := pow.zero at a % n127    rw [left, right]128    rfl129  | j + 1 using ih =>130    have left := pow.add_one at a, j131    have right := pow.add_one at a % n, j132    rw [left, right]133    have first := mod.mul at n, a, a ^ j with nonzero134    rw [first, ih]135    exact mod.mul_right at n, a % n, (a % n) ^ j with nonzero136137theorem natural.below_two (r : Nat)138  requires below : r < 2139  shows r = 0 ∨ r = 1140proof141  have le1 : r ≤ 1 by arith142  have alternatives := LessEqual.cases at r, 1 with le1143  cases alternatives with lt1 | eq1144  . left145    have le0 : r ≤ 0 by arith146    exact LessEqual.eq_zero with le0147  . right148    exact eq1149150theorem natural.below_three (r : Nat)151  requires below : r < 3152  shows r = 0 ∨ r = 1 ∨ r = 2153proof154  have le2 : r ≤ 2 by arith155  have alternatives := LessEqual.cases at r, 2 with le2156  cases alternatives with lt2 | eq2157  . have small := natural.below_two with lt2158    cases small with zero | one159    . left160      exact zero161    . right162      left163      exact one164  . right165    right166    exact eq2167168theorem natural.below_four (r : Nat)169  requires below : r < 4170  shows r = 0 ∨ r = 1 ∨ r = 2 ∨ r = 3171proof172  have le3 : r ≤ 3 by arith173  have alternatives := LessEqual.cases at r, 3 with le3174  cases alternatives with lt3 | eq3175  . have small := natural.below_three with lt3176    rcases small with zero | one | two177    . left178      exact zero179    . right180      left181      exact one182    . right183      right184      left185      exact two186  . right187    right188    right189    exact eq3190191theorem mod.two_cases (a : Nat)192  shows a % 2 = 0 ∨ a % 2 = 1193proof194  have two : 2 ≠ 0 by arith195  have bound := mod.less at a, 2 with two196  exact natural.below_two with bound197198theorem mod.three_cases (a : Nat)199  shows a % 3 = 0 ∨ a % 3 = 1 ∨ a % 3 = 2200proof201  have three : 3 ≠ 0 by arith202  have bound := mod.less at a, 3 with three203  exact natural.below_three with bound204205theorem mod.four_cases (a : Nat)206  shows a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3207proof208  have four : 4 ≠ 0 by arith209  have bound := mod.less at a, 4 with four210  exact natural.below_four with bound211212-- Adding d preserves the remainder exactly when n divides d.213theorem mod.add_eq_iff (n a d : Nat)214  shows (a + d) % n = a % n ↔ n ∣ d215proof216  have split : n = 0 ∨ n ≠ 0 by tauto217  cases split with zero | nonzero218  . rw zero219    have left := mod.zero_right at a + d220    have right := mod.zero_right at a221    rw [left, right]222    constructor223    . intro same224      have le0 : d ≤ 0 by arith225      have dZero := LessEqual.eq_zero with le0226      rw dZero227      exact divides.zero at 0228    . intro h229      have dZero := zero.divides_only_zero with h230      rw dZero231      ring232  . constructor233    . intro same234      exact mod.add_cancel at n, a, d with nonzero, same235    . intro h236      obtain ⟨s, sNat, equation⟩ := h237      rw ← equation238      exact mod.add_multiple at n, a, s with nonzero239240theorem mod.eq_iff_divides_natDist (n a b : Nat)241  shows a % n = b % n ↔ n ∣ natDist(a, b)242proof243  have total := LessEqual.total at a, b244  cases total with below | above245  . obtain ⟨d, dNat, split⟩ := LessEqual.exists_add with below246    have distance : natDist(a, b) = d247      have value := natDist.of_le at a, b with below248      have sum := split249      symm at sum250      have difference := sub.of_add_eq_left at a, d, b with sum251      rw [value, difference]252      rfl253    rw [distance, split]254    have shifted := mod.add_eq_iff at n, a, d255    constructor256    . intro same257      symm at same258      exact shifted.forward with same259    . intro h260      symm261      exact shifted.backward with h262  . obtain ⟨d, dNat, split⟩ := LessEqual.exists_add with above263    have distance : natDist(a, b) = d264      have value := natDist.of_ge at a, b with above265      have sum := split266      symm at sum267      have difference := sub.of_add_eq_left at b, d, a with sum268      rw [value, difference]269      rfl270    rw [distance, split]271    exact mod.add_eq_iff at n, b, d272273predicate CongruentMod (a b n : Nat) := a % n = b % n274275theorem CongruentMod.reflexive (a n : Nat)276  shows CongruentMod(a, a, n)277proof278  unfold CongruentMod279  rfl280281theorem CongruentMod.symmetric (a b n : Nat)282  requires congruent : CongruentMod(a, b, n)283  shows CongruentMod(b, a, n)284proof285  unfold CongruentMod at congruent286  unfold CongruentMod287  symm288  exact congruent289290theorem CongruentMod.transitive (a b c n : Nat)291  requires first : CongruentMod(a, b, n)292  requires second : CongruentMod(b, c, n)293  shows CongruentMod(a, c, n)294proof295  unfold CongruentMod at first296  unfold CongruentMod at second297  unfold CongruentMod298  rw [first, second]299  rfl300301theorem CongruentMod.of_eq (a b n : Nat)302  requires same : a = b303  shows CongruentMod(a, b, n)304proof305  rw same306  exact CongruentMod.reflexive at b, n307308theorem CongruentMod.zero_modulus (a b : Nat)309  shows CongruentMod(a, b, 0) ↔ a = b310proof311  have left := mod.zero_right at a312  have right := mod.zero_right at b313  constructor314  . intro congruent315    unfold CongruentMod at congruent316    rw [left, right] at congruent317    exact congruent318  . intro same319    unfold CongruentMod320    rw [left, right]321    exact same322323theorem CongruentMod.one_modulus (a b : Nat)324  shows CongruentMod(a, b, 1)325proof326  unfold CongruentMod327  have left := mod.one at a328  have right := mod.one at b329  rw [left, right]330  rfl331332theorem CongruentMod.iff_divides_natDist (a b n : Nat)333  shows CongruentMod(a, b, n) ↔ n ∣ natDist(a, b)334proof335  have characterization := mod.eq_iff_divides_natDist at n, a, b336  constructor337  . intro congruent338    unfold CongruentMod at congruent339    exact characterization.forward with congruent340  . intro distance341    unfold CongruentMod342    exact characterization.backward with distance343344theorem CongruentMod.divides_natDist (a b n : Nat)345  requires congruent : CongruentMod(a, b, n)346  shows n ∣ natDist(a, b)347proof348  have characterization := CongruentMod.iff_divides_natDist at a, b, n349  exact characterization.forward with congruent350351theorem CongruentMod.of_divides_natDist (a b n : Nat)352  requires distance : n ∣ natDist(a, b)353  shows CongruentMod(a, b, n)354proof355  have characterization := CongruentMod.iff_divides_natDist at a, b, n356  exact characterization.backward with distance357358theorem CongruentMod.of_add (a d n : Nat)359  requires multiple : n ∣ d360  shows CongruentMod(a + d, a, n)361proof362  unfold CongruentMod363  have shifted := mod.add_eq_iff at n, a, d364  exact shifted.backward with multiple365366theorem CongruentMod.zero_right_iff (a n : Nat)367  shows CongruentMod(a, 0, n) ↔ n ∣ a368proof369  have characterization := CongruentMod.iff_divides_natDist at a, 0, n370  have value := natDist.zero_right at a371  rw value at characterization372  exact characterization373374theorem CongruentMod.mod_right (a n : Nat)375  shows CongruentMod(a, a % n, n)376proof377  unfold CongruentMod378  have split : n = 0 ∨ n ≠ 0 by tauto379  cases split with zero | nonzero380  . rw zero381    have value := mod.zero_right at a382    rw value383    rw value384    rfl385  . have idempotent := mod.mod at n, a with nonzero386    rw idempotent387    rfl388389theorem CongruentMod.mod_left (a n : Nat)390  shows CongruentMod(a % n, a, n)391proof392  have right := CongruentMod.mod_right at a, n393  exact CongruentMod.symmetric with right394395theorem CongruentMod.divides_modulus (a b m n : Nat)396  requires hmn : m ∣ n397  requires congruent : CongruentMod(a, b, n)398  shows CongruentMod(a, b, m)399proof400  have distance := CongruentMod.divides_natDist with congruent401  have smaller := divides.transitive at m, n, natDist(a, b) with hmn, distance402  exact CongruentMod.of_divides_natDist with smaller403404theorem CongruentMod.add (a b c d n : Nat)405  requires first : CongruentMod(a, b, n)406  requires second : CongruentMod(c, d, n)407  shows CongruentMod(a + c, b + d, n)408proof409  have split : n = 0 ∨ n ≠ 0 by tauto410  cases split with zero | nonzero411  . rw zero at first412    rw zero at second413    rw zero414    have firstEq := CongruentMod.zero_modulus at a, b415    have secondEq := CongruentMod.zero_modulus at c, d416    have ab := firstEq.forward with first417    have cd := secondEq.forward with second418    rw [ab, cd]419    exact CongruentMod.reflexive at b + d, 0420  . unfold CongruentMod at first421    unfold CongruentMod at second422    unfold CongruentMod423    have left := mod.add at n, a, c with nonzero424    have right := mod.add at n, b, d with nonzero425    rw [left, right, first, second]426    rfl427428theorem CongruentMod.mul (a b c d n : Nat)429  requires first : CongruentMod(a, b, n)430  requires second : CongruentMod(c, d, n)431  shows CongruentMod(a * c, b * d, n)432proof433  have split : n = 0 ∨ n ≠ 0 by tauto434  cases split with zero | nonzero435  . rw zero at first436    rw zero at second437    rw zero438    have firstEq := CongruentMod.zero_modulus at a, b439    have secondEq := CongruentMod.zero_modulus at c, d440    have ab := firstEq.forward with first441    have cd := secondEq.forward with second442    rw [ab, cd]443    exact CongruentMod.reflexive at b * d, 0444  . unfold CongruentMod at first445    unfold CongruentMod at second446    unfold CongruentMod447    have left := mod.mul at n, a, c with nonzero448    have right := mod.mul at n, b, d with nonzero449    rw [left, right, first, second]450    rfl451452theorem CongruentMod.add_left (a b c n : Nat)453  requires congruent : CongruentMod(a, b, n)454  shows CongruentMod(c + a, c + b, n)455proof456  have reflexive := CongruentMod.reflexive at c, n457  exact CongruentMod.add at c, c, a, b, n with reflexive, congruent458459theorem CongruentMod.add_right (a b c n : Nat)460  requires congruent : CongruentMod(a, b, n)461  shows CongruentMod(a + c, b + c, n)462proof463  have reflexive := CongruentMod.reflexive at c, n464  exact CongruentMod.add at a, b, c, c, n with congruent, reflexive465466theorem CongruentMod.mul_left (a b c n : Nat)467  requires congruent : CongruentMod(a, b, n)468  shows CongruentMod(c * a, c * b, n)469proof470  have reflexive := CongruentMod.reflexive at c, n471  exact CongruentMod.mul at c, c, a, b, n with reflexive, congruent472473theorem CongruentMod.mul_right (a b c n : Nat)474  requires congruent : CongruentMod(a, b, n)475  shows CongruentMod(a * c, b * c, n)476proof477  have reflexive := CongruentMod.reflexive at c, n478  exact CongruentMod.mul at a, b, c, c, n with congruent, reflexive479480theorem CongruentMod.pow (a b k n : Nat)481  requires congruent : CongruentMod(a, b, n)482  shows CongruentMod(a ^ k, b ^ k, n)483proof484  induction k485  | zero =>486    have left := pow.zero at a487    have right := pow.zero at b488    rw [left, right]489    exact CongruentMod.reflexive at 1, n490  | j + 1 using ih =>491    have left := pow.add_one at a, j492    have right := pow.add_one at b, j493    rw [left, right]494    exact CongruentMod.mul at a, b, a ^ j, b ^ j, n with congruent, ih495496theorem CongruentMod.add_right_cancel (a b c n : Nat)497  requires congruent : CongruentMod(a + c, b + c, n)498  shows CongruentMod(a, b, n)499proof500  have distance := CongruentMod.divides_natDist with congruent501  have shift := natDist.add_right at a, b, c502  rw shift at distance503  exact CongruentMod.of_divides_natDist with distance504505theorem CongruentMod.add_left_cancel (a b c n : Nat)506  requires congruent : CongruentMod(c + a, c + b, n)507  shows CongruentMod(a, b, n)508proof509  have distance := CongruentMod.divides_natDist with congruent510  have shift := natDist.add_left at a, b, c511  rw shift at distance512  exact CongruentMod.of_divides_natDist with distance513514theorem CongruentMod.mul_cancel_coprime (a x y n : Nat)515  requires coprimeAN : gcd(a, n) = 1516  requires congruent : CongruentMod(a * x, a * y, n)517  shows CongruentMod(x, y, n)518proof519  have split : n = 0 ∨ n ≠ 0 by tauto520  cases split with zero | nonzero521  . rw zero at congruent522    rw zero at coprimeAN523    rw zero524    have value := gcd.zero_right at a525    rw value at coprimeAN526    have products := CongruentMod.zero_modulus at a * x, a * y527    have same := products.forward with congruent528    rw coprimeAN at same529    have left : 1 * x = x by ring530    have right : 1 * y = y by ring531    rw [left, right] at same532    have characterization := CongruentMod.zero_modulus at x, y533    exact characterization.backward with same534  . unfold CongruentMod at congruent535    unfold CongruentMod536    exact coprime.mul_cancel_mod at a, n, x, y537      with nonzero, coprimeAN, congruent538539theorem CongruentMod.euler (a n : Nat)540  requires aboveOne : 1 < n541  requires coprimeAN : gcd(a, n) = 1542  shows CongruentMod(a ^ totient(n), 1, n)543proof544  unfold CongruentMod545  have power := euler.theorem with aboveOne, coprimeAN546  have one := mod.one_left at n with aboveOne547  rw [power, one]548  rfl549550theorem CongruentMod.pow_totient_period (a k n : Nat)551  requires aboveOne : 1 < n552  requires coprimeAN : gcd(a, n) = 1553  shows CongruentMod(a ^ (k + totient(n)), a ^ k, n)554proof555  have expand := pow.add at a, totient(n), k556  rw expand557  have unit := CongruentMod.euler with aboveOne, coprimeAN558  have scaled := CongruentMod.mul_left at a ^ totient(n), 1, a ^ k, n with unit559  have one : a ^ k * 1 = a ^ k by ring560  rw one at scaled561  exact scaled562563theorem CongruentMod.fermat (a p : Nat)564  requires prime : Prime(p)565  requires notDivides : ¬(p ∣ a)566  shows CongruentMod(a ^ (p - 1), 1, p)567proof568  unfold CongruentMod569  have power := fermat.little with prime, notDivides570  have aboveOne := Prime.greater_than_one with prime571  have one := mod.one_left at p with aboveOne572  rw [power, one]573  rfl574575theorem CongruentMod.fermat_pow (a p : Nat)576  requires prime : Prime(p)577  shows CongruentMod(a ^ p, a, p)578proof579  have aboveOne := Prime.greater_than_one with prime580  have positive : 1 ≤ p by arith581  have predecessor := sub.add_cancel at p, 1 with positive582  have expand := pow.add_one at a, p - 1583  rw predecessor at expand584  rw expand585  have split : p ∣ a ∨ ¬(p ∣ a) by tauto586  cases split with yes | no587  . have left : p ∣ a * a ^ (p - 1)588      exact divides.multiply_right at p, a, a ^ (p - 1) with yes589    have zeroLeft := CongruentMod.zero_right_iff at a * a ^ (p - 1), p590    have zeroRight := CongruentMod.zero_right_iff at a, p591    have first := zeroLeft.backward with left592    have second := zeroRight.backward with yes593    have swapped := CongruentMod.symmetric with second594    exact CongruentMod.transitive at a * a ^ (p - 1), 0, a, p595      with first, swapped596  . have unit := CongruentMod.fermat with prime, no597    have scaled := CongruentMod.mul_left at a ^ (p - 1), 1, a, p with unit598    have one : a * 1 = a by ring599    rw one at scaled600    exact scaled601