Grace/Cumulus/NumberTheory/InverseInvolution.g17

Open in Workbench Download source

Imports

Euler

Declarations

Source

1-- The modular inverse of a unit mod a prime, chosen once: it is a unit, it2-- is an involution, and its only fixed points are 1 and p − 13-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.NumberTheory.InverseInvolution9import Euler1011defunique modInverse (p x : Nat) (b ∈ p) := mul(x, b) % p = 112requires prime : Prime(p)13requires unit : gcd(x, p) = 114proof15  have aboveOne := Prime.greater_than_one at p with prime16  obtain ⟨b, bNat, bBelow, inverse⟩ := coprime.inverse at x, p with aboveOne, unit17  witness b18  constructor19  . exact membership.of_Less at b, p with *, *, bBelow20  . exact inverse2122uniqueness23  intros u uMember first v vMember second24  have nonzero := Prime.nonzero at p with prime25  have uNat := natural.member at p with uMember26  have vNat := natural.member at p with vMember27  have uBelow := Less.of_membership at u, p28  have vBelow := Less.of_membership at v, p29  have same : (x * u) % p = (x * v) % p30    rw [first, second]31    rfl32  have residues := coprime.mul_cancel_mod at x, p, u, v with nonzero, unit, same33  have uSelf := mod.of_less at p, u with (uBelow with uMember)34  have vSelf := mod.of_less at p, v with (vBelow with vMember)35  rw [uSelf, vSelf] at residues36  exact residues3738theorem modInverse.below (p x : Nat)39  requires prime : Prime(p)40  requires unit : gcd(x, p) = 141  shows modInverse(p, x) < p42proof43  have selected := modInverse.selected with prime, unit44  have bNat := natural.member at p with selected.left45  have below := Less.of_membership at modInverse(p, x), p46  exact below with selected.left4748theorem modInverse.natural (p x : Nat)49  requires prime : Prime(p)50  requires unit : gcd(x, p) = 151  shows Nat(modInverse(p, x))52proof53  have selected := modInverse.selected with prime, unit54  exact natural.member at p with selected.left5556theorem modInverse.product (p x : Nat)57  requires prime : Prime(p)58  requires unit : gcd(x, p) = 159  shows mul(x, modInverse(p, x)) % p = 160proof61  have selected := modInverse.selected with prime, unit62  exact selected.right6364theorem modInverse.unit (p x : Nat)65  requires prime : Prime(p)66  requires unit : gcd(x, p) = 167  shows gcd(modInverse(p, x), p) = 168proof69  have nonzero := Prime.nonzero with prime70  have bNat := modInverse.natural with prime, unit71  have product := modInverse.product with prime, unit72  exact units.inverse_coprime with nonzero, product7374-- Inverses are unique among residues below p.75theorem modInverse.unique_below (p x b : Nat)76  requires prime : Prime(p)77  requires unit : gcd(x, p) = 178  requires below : b < p79  requires product : (x * b) % p = 180  shows b = modInverse(p, x)81proof82  have nonzero := Prime.nonzero with prime83  have inverseNat := modInverse.natural with prime, unit84  have inverseBelow := modInverse.below with prime, unit85  have inverseProduct := modInverse.product with prime, unit86  have same : (x * b) % p = (x * modInverse(p, x)) % p87    rw [product, inverseProduct]88    rfl89  have residues := coprime.mul_cancel_mod with nonzero, unit, same90  have bSelf := mod.of_less with below91  have inverseSelf := mod.of_less with inverseBelow92  rwa [bSelf, inverseSelf] at residues9394theorem modInverse.involution (p x : Nat)95  requires prime : Prime(p)96  requires unit : gcd(x, p) = 197  requires below : x < p98  shows modInverse(p, modInverse(p, x)) = x99proof100  have inverseNat := modInverse.natural with prime, unit101  have inverseUnit := modInverse.unit with prime, unit102  have product := modInverse.product with prime, unit103  have commute := mul.commutative at modInverse(p, x), x with *104  rw commute at product105  have flipped : mul(modInverse(p, x), x) % p = 1 by exact product106  have same := modInverse.unique_below with prime, inverseUnit, below, flipped107  symm at same108  exact same109110theorem modInverse.positive (p x : Nat)111  requires prime : Prime(p)112  requires unit : gcd(x, p) = 1113  shows 0 < modInverse(p, x)114proof115  have aboveOne := Prime.greater_than_one with prime116  have inverseNat := modInverse.natural with prime, unit117  have product := modInverse.product with prime, unit118  have trichotomy := Less.trichotomy at 0, modInverse(p, x)119  rcases trichotomy with positive | zero | negative120  . exact positive121  . exfalso122    rw ← zero at product123    have vanish : x * 0 = 0 by ring124    rw [vanish, mod.zero_left] at product125    have impossible : ¬(0:N) = 1 by arith126    exact impossible with product127  . exfalso128    have impossible : ¬modInverse(p, x) < 0 by arith129    exact impossible with negative130131-- A residue below p is its own inverse only when it is 1 or p − 1.132theorem modInverse.fixed (p x : Nat)133  requires prime : Prime(p)134  requires positive : 0 < x135  requires below : x < p136  requires fixed : modInverse(p, x) = x137  shows x = 1 ∨ succ(x) = p138proof139  have nonzero := Prime.nonzero with prime140  have unit := prime.coprime_below with prime, positive, below141  have product := modInverse.product with prime, unit142  rw fixed at product143  have shape := natural.zero_or_successor at x144  cases shape with zero | successor145  . exfalso146    rw zero at positive147    exact Less.irreflexive with *, positive148  . obtain ⟨y, yNat, form⟩ := successor149    obtain ⟨q, qNat, equation⟩ := mod.equation at x * x, p with nonzero150    rw [product, form] at equation151    have expand : succ(y) * succ(y) = y * (y + 2) + 1 by ring152    rw expand at equation153    have cancel := add.right_cancel at y * (y + 2), p * q, 1154    have reduced := cancel with equation155    have dividesProduct : p ∣ y * (y + 2)156      witness q157      rw reduced158      rfl159    have split := Prime.divides_mul with prime, dividesProduct160    cases split with dividesY | dividesNext161    . left162      have yShape := natural.zero_or_successor at y163      cases yShape with yZero | ySucc164      . rw [form, yZero]165        rfl166      . exfalso167        have yNonzero : y ≠ 0168          intro zero169          obtain ⟨z, zNat, yForm⟩ := ySucc170          rw yForm at zero171          have impossible : succ(z) ≠ 0 by arith172          exact impossible with zero173        have le := divides.le with dividesY, yNonzero174        rw form at below175        have impossible : ¬p ≤ y by arith176        exact impossible with le177    . right178      have nextNonzero : y + 2 ≠ 0 by arith179      have le := divides.le with dividesNext, nextNonzero180      rw form at below181      have upper : y + 2 ≤ p182        have unfold : y + 2 = succ(succ(y)) by ring183        rw unfold184        exact below185      have same := LessEqual.antisymmetric with upper, le186      rw form187      have unfold : succ(succ(y)) = y + 2 by ring188      rwa unfold189