Grace/Cumulus/NumberTheory/PerfectNumbers.g17

Open in Workbench Download source

Imports

DivisorSum · Nat.ParityLemmas · Nat.SubtractionLemmas

Declarations

Source

1-- Perfect numbers: σ(n) = 2n. The divisors of 2^(k+1) are 1 and the doubles2-- of the divisors of 2^k, so σ(2^k) = 2^(k+1) − 1; Euclid's theorem that3-- 2^(p−1) · (2^p − 1) is perfect when 2^p − 1 is prime, and Euler's4-- converse that every even perfect number has this form5-- 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.PerfectNumbers11import DivisorSum12import Nat.ParityLemmas13import Nat.SubtractionLemmas1415-- The doubles of a set of naturals, and doubling as a bijection onto them.16def doubles (S : Set) : Set := { n ∈ ℕ | ∃ d ∈ S, n = mul(2, d) }1718defgraph doubleMap (S : Set) (d ∈ S) : doubles(S) := mul(2, d)19requires naturals : S ⊆ ℕ20proof21  have dIn := naturals with d, member22  have dNat := nat.omega.backward with dIn23  have doubleNat : Nat(mul(2, d)) by typecheck24  have doubleIn := nat.omega.forward with doubleNat25  have same : mul(2, d) = mul(2, d) by rfl26  exact doubles.membership.backward with ⟨doubleIn, d, member, same⟩2728theorem doubleMap.injective (S : Set)29  requires naturals : S ⊆ ℕ30  shows InjectiveBetween(doubleMap(S), S, doubles(S))31proof32  have function := doubleMap.function at S with naturals33  refine ⟨function, _⟩34  intros x hx y hy z hz relatesX relatesY35  have xNat := nat.omega.backward with (naturals with x, hx)36  have yNat := nat.omega.backward with (naturals with y, hy)37  have valueX := FunctionBetween.apply_value with function, hx, relatesX38  have valueY := FunctionBetween.apply_value with function, hy, relatesY39  have doubleX := doubleMap.value at S, x with naturals, hx40  have doubleY := doubleMap.value at S, y with naturals, hy41  have same : mul(2, x) = mul(2, y) by cc42  have twoNonzero : 2 ≠ 0 by arith43  exact mul.left_cancel_positive with twoNonzero, same4445theorem doubleMap.surjective (S : Set)46  requires naturals : S ⊆ ℕ47  shows SurjectiveBetween(doubleMap(S), S, doubles(S))48proof49  have function := doubleMap.function at S with naturals50  refine ⟨function, _⟩51  intros z hz52  have parts := doubles.membership.forward with hz53  obtain ⟨d, hd, shape⟩ := parts.right54  have relates := FunctionBetween.relates_apply with function, hd55  have value := doubleMap.value at S, d with naturals, hd56  rw [value, ← shape] at relates57  exact ⟨d, hd, relates⟩5859theorem doubleMap.bijective (S : Set)60  requires naturals : S ⊆ ℕ61  shows BijectiveBetween(doubleMap(S), S, doubles(S))62proof63  have injective := doubleMap.injective with naturals64  have surjective := doubleMap.surjective with naturals65  exact ⟨injective, surjective⟩6667theorem doubles.finite (S : Set)68  requires finite : Finite(S)69  requires naturals : S ⊆ ℕ70  shows Finite(doubles(S))71proof72  have bijective := doubleMap.bijective with naturals73  have equipotent : Equipotent(S, doubles(S)) := ⟨doubleMap(S), bijective⟩74  exact Finite.of_equipotent with finite, equipotent7576theorem doubles.weights (S : Set)77  requires naturals : S ⊆ ℕ78  shows ∀ t ∈ doubles(S), identity(ℕ)(t) ∈ ℕ79proof80  intros t ht81  have parts := doubles.membership.forward with ht82  have tNat := nat.omega.backward with parts.left83  exact identityWeight.natural at t8485-- The doubles sum to twice the sum.86theorem natSum.doubles (S : Set)87  requires finite : Finite(S)88  requires naturals : S ⊆ ℕ89  shows natSum(doubles(S), identity(ℕ)) =90    add(natSum(S, identity(ℕ)), natSum(S, identity(ℕ)))91proof92  have weights := doubles.weights with naturals93  have weightsS : ∀ s ∈ S, identity(ℕ)(s) ∈ ℕ94    intros s hs95    have sNat := nat.omega.backward with (naturals with s, hs)96    exact identityWeight.natural at s97  have function := doubleMap.function at S with naturals98  have bijective := doubleMap.bijective with naturals99  have values : ∀ s ∈ S, doubleMap(S)(s) = identity(ℕ)(doubleMap(S)(s))100    intros s hs101    have image := FunctionBetween.apply_closed with function, hs102    have parts := doubles.membership.forward with image103    symm104    exact identity.apply at doubleMap(S)(s), ℕ with parts.left105  have reindexed := natSum.reindex with finite, bijective, weights, values106  have agree : ∀ s ∈ S,107      doubleMap(S)(s) = add(identity(ℕ)(s), identity(ℕ)(s))108    intros s hs109    have sNat := nat.omega.backward with (naturals with s, hs)110    have value := doubleMap.value at S, s with naturals, hs111    have idValue := identityWeight.value at s112    rw [value, idValue]113    exact mul.two_left at s114  have correct := cardinality.correct with finite115  have cardNat := correct.left116  have size : cardinality(S) = cardinality(S) by rfl117  have pointwise := natSum.add_pointwise_of_size at doubleMap(S), identity(ℕ),118    identity(ℕ), cardinality(S)119  have added := pointwise with S, finite, size, weightsS, weightsS, agree120  rw [reindexed, added]121  rfl122123-- The divisors of 2^(k+1): 1 and the doubles of the divisors of 2^k.124theorem divisors.two_pow_succ (k : Nat)125  shows divisors(2 ^ (k + 1)) = insert(1, doubles(divisors(2 ^ k)))126proof127  have twoPositive : 0 < 2 by arith128  have twoNonzero : 2 ≠ 0 by arith129  have powPositive := pow.positive at 2, k with twoPositive130  have powNonzero := Less.ne_zero_of_positive with powPositive131  have succPositive := pow.positive at 2, k + 1 with twoPositive132  have succNonzero := Less.ne_zero_of_positive with succPositive133  have expanded := pow.add_one at 2, k134  have two := Prime.two135  ext d136  constructor137  . intro member138    have dNat := divisors.natural with member139    have factor := divisors.divides with member140    apply insert.membership.backward141    have parity := parity.exhaustive at d142    cases parity with even | odd143    . right144      have characterization := Even.iff_two_mul at d145      obtain ⟨c, cNat, shape⟩ := characterization.forward with even146      rw [shape, expanded] at factor147      have cancel := divides.mul_cancel_left at 2, c, 2 ^ k with twoNonzero148      have cDivides := cancel.forward with factor149      have cBelow := divides.le with cDivides, powNonzero150      have cCharacterization := divisors.membership_le at 2 ^ k, c151      have cMember := cCharacterization.backward with ⟨cBelow, cDivides⟩152      have dIn := nat.omega.forward with dNat153      have same : 2 * c = mul(2, c) by rfl154      rw shape at dIn155      rw shape156      exact doubles.membership.backward with ⟨dIn, c, cMember, same⟩157    . left158      have oddCharacterization := divides.not_two_iff_odd at d159      have notTwo := oddCharacterization.backward with odd160      have coprimeTwo := Prime.gcd_of_not_divides with two, notTwo161      have coprimePow := coprime.pow_left at 2, d, k + 1 with coprimeTwo162      have characterization := gcd.eq_one_iff at 2 ^ (k + 1), d163      have all := characterization.forward with coprimePow164      have selfDivides := divides.reflexive at d165      exact all with d, dNat, factor, selfDivides166  . intro member167    have split := insert.membership.forward with member168    cases split with one | double169    . rw one170      exact divisors.one_member at 2 ^ (k + 1) with succNonzero171    . have parts := doubles.membership.forward with double172      obtain ⟨c, hc, shape⟩ := parts.right173      have cNat := divisors.natural with hc174      have cDivides := divisors.divides with hc175      have twoSelf := divides.reflexive at 2176      have scaled := divides.mul_mono with twoSelf, cDivides177      rw ← expanded at scaled178      have below := divides.le with scaled, succNonzero179      have characterization := divisors.membership_le at 2 ^ (k + 1), 2 * c180      rw shape181      exact characterization.backward with ⟨below, scaled⟩182183-- σ(2^(k+1)) = 2 σ(2^k) + 1, hence σ(2^k) = 2^(k+1) − 1.184theorem sigma.two_pow_succ (k : Nat)185  shows sigma(2 ^ (k + 1)) = 2 * sigma(2 ^ k) + 1186proof187  have split := divisors.two_pow_succ at k188  have finite := divisors.finite at 2 ^ k189  have naturals := divisors.subset_naturals at 2 ^ k190  have finiteDoubles := doubles.finite with finite, naturals191  have weights := doubles.weights with naturals192  have doubled := natSum.doubles with finite, naturals193  rw ← sigma.definition at doubled194  have weightOne := identityWeight.natural at 1195  have valueOne := identityWeight.value at 1196  have fresh : ¬1 ∈ doubles(divisors(2 ^ k))197    intro inside198    have parts := doubles.membership.forward with inside199    obtain ⟨c, hc, shape⟩ := parts.right200    have cNat := divisors.natural with hc201    have even := Even.two_mul at c202    rw ← shape at even203    exact Even.not_one with even204  have inserted := natSum.insert with finiteDoubles, weights, weightOne, fresh205  have twice := mul.two_left at sigma(2 ^ k)206  rw [sigma.definition, split, inserted, doubled, valueOne, twice]207  rfl208209theorem sigma.two_pow_add_one (k : Nat)210  shows sigma(2 ^ k) + 1 = 2 ^ (k + 1)211proof212  induction k213  | zero =>214    rw [pow.zero, sigma.one, pow.add_one, pow.zero]215    ring216  | succ(j) using ih =>217    have step := sigma.two_pow_succ at j218    have asSucc := add.right_one at j219    rw asSucc at step220    rw [step, ← asSucc, pow.add_one, ← ih]221    ring222223theorem sigma.two_pow (k : Nat)224  shows sigma(2 ^ k) = 2 ^ (k + 1) - 1225proof226  have sum := sigma.two_pow_add_one at k227  symm228  exact sub.of_add_eq with sum229230-- A natural number is perfect when it is the sum of its proper divisors:231-- σ(n) = 2n.232predicate PerfectNumber (n : Nat) := 0 < n ∧ sigma(n) = 2 * n233234-- Euclid: 2^(p−1) · (2^p − 1) is perfect when 2^p − 1 is prime.235theorem perfectNumber.of_mersenne (p : Nat)236  requires prime : Prime(2 ^ p - 1)237  shows PerfectNumber(2 ^ (p - 1) * (2 ^ p - 1))238proof239  have qNonzero := Prime.nonzero with prime240  have pNonzero : p ≠ 0241    intro zero242    rw [zero, pow.zero, sub.self] at qNonzero243    apply qNonzero244    rfl245  have oneLeP : 1 ≤ p246    have characterization := LessEqual.one_iff_ne_zero at p247    exact characterization.backward with pNonzero248  have restored := sub.add_cancel at p, 1 with oneLeP249  have sum := sigma.two_pow_add_one at p - 1250  rw restored at sum251  have sigmaValue := sub.of_add_eq with sum252  have expanded := pow.add_one at 2, p - 1253  rw restored at expanded254  have oneLeTwo : 1 ≤ 2 by arith255  have powGeOne := pow.ge_one at 2, p with oneLeTwo256  have powRestored := sub.add_cancel at 2 ^ p, 1 with powGeOne257  have notTwo : 2 ^ p - 1 ≠ 2258    intro two259    have even := Even.two_mul at 2 ^ (p - 1)260    rw [← expanded, ← powRestored, two] at even261    have characterization := Even.iff_two_mul at 2 + 1262    obtain ⟨c, cNat, shape⟩ := characterization.forward with even263    have cBelow : c < 2 by arith264    have alternatives := natural.below_two with cBelow265    cases alternatives with zero | one266    . rw zero at shape267      arith268    . rw one at shape269      arith270  have odd := Prime.odd_of_ne_two with prime, notTwo271  have oddCharacterization := divides.not_two_iff_odd at 2 ^ p - 1272  have notDivides := oddCharacterization.backward with odd273  have two := Prime.two274  have coprimeTwo := Prime.gcd_of_not_divides with two, notDivides275  have coprime := coprime.pow_left at 2, 2 ^ p - 1, p - 1 with coprimeTwo276  have multiplicative := sigma.multiplicative with coprime277  have sigmaPrime := sigma.prime with prime278  have twoPositive : 0 < 2 by arith279  have powPositive := pow.positive at 2, p - 1 with twoPositive280  have powNonzero := Less.ne_zero_of_positive with powPositive281  have productNonzero := mul.nonzero with powNonzero, qNonzero282  have positive := Less.positive_of_ne_zero with productNonzero283  refine ⟨positive, _⟩284  rw [multiplicative, sigmaPrime, powRestored, sigmaValue, expanded]285  ring286287-- Every positive natural is a power of two times an odd number.288theorem natural.two_pow_odd_below (B : Nat)289  shows ∀ n, Nat(n) → 0 < n → n ≤ B →290    ∃ k ∈ ℕ, ∃ m ∈ ℕ, Odd(m) ∧ n = 2 ^ k * m291proof292  induction B293  | zero =>294    intros n nNat positive below295    exfalso296    arith297  | succ(b) using ih =>298    intros n nNat positive below299    have alternatives := LessEqual.cases at n, succ(b) with below300    cases alternatives with strict | same301    . have belowB : n ≤ b by arith302      exact ih with n, nNat, positive, belowB303    . have parity := parity.exhaustive at n304      cases parity with even | odd305      . have characterization := Even.iff_two_mul at n306        obtain ⟨c, cNat, shape⟩ := characterization.forward with even307        have cPositive : 0 < c by arith308        have cBelow : c ≤ b by arith309        obtain ⟨k, kIn, m, mIn, oddM, form⟩ :=310          ih with c, cNat, cPositive, cBelow311        have kNat := nat.omega.backward with kIn312        have mNat := nat.omega.backward with mIn313        have succNat : Nat(k + 1) by typecheck314        have succIn := nat.omega.forward with succNat315        have expanded := pow.add_one at 2, k316        have shapeN : n = 2 ^ (k + 1) * m317          rw [shape, form, expanded]318          ring319        exact ⟨k + 1, succIn, m, mIn, oddM, shapeN⟩320      . have zeroNat : Nat(0) by typecheck321        have zeroIn := nat.omega.forward with zeroNat322        have nIn := nat.omega.forward with nNat323        have shapeN : n = 2 ^ 0 * n324          rw [pow.zero, mul.left_unit]325          rfl326        exact ⟨0, zeroIn, n, nIn, odd, shapeN⟩327328theorem natural.two_pow_odd (n : Nat)329  requires positive : 0 < n330  shows ∃ k ∈ ℕ, ∃ m ∈ ℕ, Odd(m) ∧ n = 2 ^ k * m331proof332  have nNat : Nat(n) by typecheck333  have below := LessEqual.reflexive at n334  have all := natural.two_pow_odd_below at n335  exact all with n, nNat, positive, below336337-- Euler: an even perfect number is 2^(p−1) · (2^p − 1) with 2^p − 1338-- prime.339theorem perfectNumber.even_form (n : Nat)340  requires perfect : PerfectNumber(n)341  requires even : Even(n)342  shows ∃ p ∈ ℕ, Prime(2 ^ p - 1) ∧ n = 2 ^ (p - 1) * (2 ^ p - 1)343proof344  rcases perfect with ⟨positive, sum⟩345  obtain ⟨k, kIn, m, mIn, odd, form⟩ := natural.two_pow_odd with positive346  have kNat := nat.omega.backward with kIn347  have mNat := nat.omega.backward with mIn348  have mNonzero : m ≠ 0349    intro zero350    rw [zero, mul.right_zero] at form351    rw form at positive352    exact Less.irreflexive at 0 with positive353  have kNonzero : k ≠ 0354    intro zero355    rw [zero, pow.zero, mul.left_unit] at form356    rw form at even357    have notEven := Odd.not_even with odd358    exact notEven with even359  have two := Prime.two360  have oddCharacterization := divides.not_two_iff_odd at m361  have notTwo := oddCharacterization.backward with odd362  have coprimeTwo := Prime.gcd_of_not_divides with two, notTwo363  have coprime := coprime.pow_left at 2, m, k with coprimeTwo364  have multiplicative := sigma.multiplicative with coprime365  have powSum := sigma.two_pow_add_one at k366  have expanded := pow.add_one at 2, k367  rw [form, multiplicative] at sum368  -- With L = σ(2^k): L · σ(m) = (L + 1) · m.369  have key : sigma(2 ^ k) * sigma(m) = (sigma(2 ^ k) + 1) * m370    rw [powSum, expanded, sum]371    ring372  have kPositive := Less.positive_of_ne_zero with kNonzero373  have oneLeK : 1 ≤ k by arith374  have oneLeTwo : 1 ≤ 2 by arith375  have powMonotone := pow.exponent_monotone at 2, 1, k with oneLeTwo, oneLeK376  rw pow.one_right at powMonotone377  have threeLe : 3 ≤ sigma(2 ^ k)378    rw expanded at powSum379    arith380  have lPositive : 0 < sigma(2 ^ k) by arith381  have lNonzero := Less.ne_zero_of_positive with lPositive382  -- L divides m, since L is coprime to L + 1.383  have consecutive := gcd.consecutive at sigma(2 ^ k)384  have coprimeSucc := coprime.symmetric with consecutive385  have dividesProduct : sigma(2 ^ k) ∣ m * (sigma(2 ^ k) + 1)386    have commuted : m * (sigma(2 ^ k) + 1) = sigma(2 ^ k) * sigma(m)387      rw key388      ring389    rw commuted390    exact divides.mul_left_self at sigma(2 ^ k), sigma(m)391  have dividesM := coprime.cancel_right with coprimeSucc, dividesProduct392  obtain ⟨t, tNat, mForm⟩ := dividesM393  -- Then σ(m) = m + t, with t a divisor of m below m.394  have sigmaM : sigma(m) = m + t395    have scaled : sigma(2 ^ k) * sigma(m) = sigma(2 ^ k) * (m + t)396      rw [key, ← mForm]397      ring398    exact mul.left_cancel_positive with lNonzero, scaled399  have tNonzero : t ≠ 0400    intro zero401    rw [zero, mul.right_zero] at mForm402    apply mNonzero403    symm404    exact mForm405  have tPositive := Less.positive_of_ne_zero with tNonzero406  have tLess : t < m407    have scaled := LessEqual.mul_right at 3, sigma(2 ^ k), t with threeLe408    rw mForm at scaled409    arith410  have tNotSelf := Less.ne with tLess411  have tDivides : t ∣ m412    have commuted : t * sigma(2 ^ k) = m413      rw ← mForm414      ring415    exact divides.intro with commuted416  have tCases : t = 1 ∨ t ≠ 1 by tauto417  cases tCases with one | notOne418  . -- t = 1: m = L = 2^(k+1) − 1 and σ(m) = m + 1, so m is prime.419    rw [one, mul.right_unit] at mForm420    rw one at sigmaM421    have aboveOne : 1 < m by arith422    have primeM := Prime.of_sigma with aboveOne, sigmaM423    have succNat : Nat(k + 1) by typecheck424    have succIn := nat.omega.forward with succNat425    have predecessor := sub.add_one_right at k426    have mersenne : 2 ^ (k + 1) - 1 = m427      have value := sub.of_add_eq with powSum428      rw value429      exact mForm430    have primeMersenne : Prime(2 ^ (k + 1) - 1)431      rw mersenne432      exact primeM433    have shapeN : n = 2 ^ (k + 1 - 1) * (2 ^ (k + 1) - 1)434      rw [mersenne, predecessor]435      exact form436    exact ⟨k + 1, succIn, primeMersenne, shapeN⟩437  . -- t ≠ 1: t is a divisor strictly between, and σ(m) ≥ m + 1 + t.438    exfalso439    have member := innerDivisors.member with mNonzero, tDivides, notOne,440      tNotSelf441    have bound := innerDivisors.le_sum with member442    have aboveOne : 1 < m by arith443    have split := sigma.split with aboveOne444    rw sigmaM at split445    arith446447-- The even perfect numbers are exactly the Euclid numbers.448theorem perfectNumber.even_iff (n : Nat)449  requires even : Even(n)450  shows PerfectNumber(n) ↔451    ∃ p ∈ ℕ, Prime(2 ^ p - 1) ∧ n = 2 ^ (p - 1) * (2 ^ p - 1)452proof453  constructor454  . intro perfect455    exact perfectNumber.even_form with perfect, even456  . intro form457    obtain ⟨p, pIn, prime, shape⟩ := form458    have pNat := nat.omega.backward with pIn459    rw shape460    exact perfectNumber.of_mersenne with prime461