Grace/Cumulus/NumberTheory/Prime.g17

Imports

Declarations

Source

1-- Prime natural numbers2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.NumberTheory.Prime8import Divisibility9import Set.Ordinal1011-- For von Neumann naturals, `1 in p` is literally the strict inequality 1 < p.12-- A prime has no proper natural divisor other than one.13-- The soft-typed binder is part of the predicate's meaning: Prime(p) entails14-- Nat(p), including when Prime is used inside Separation over omega.15predicate Prime (p : Nat) :=16  1 ∈ p ∧17  (∀ d, Nat(d) → d ∈ p → d ∣ p → d = 1)1819-- The primes form a set because they are separated from omega.20def primes : Set := { p ∈ ℕ | Prime(p) }2122theorem Prime.natural (p : Set)23  requires hp : Prime(p)24  shows Nat(p)25proof26  simp [Prime]2728lemma Prime.greater_than_one_membership (p : Set)29  requires hp : Prime(p)30  shows 1 ∈ p31proof32  simp [Prime]3334-- Representation bridge used internally by factorial arguments: a prime is35-- positive as a von Neumann natural.  The public comparison theorem remains36-- `Prime.greater_than_one` below.37lemma Prime.positive_membership (p : Set)38  requires hp : Prime(p)39  shows 0 ∈ p40proof41  have hpNat := Prime.natural with hp42  have hpOrdinal := Ordinal.natural with hpNat43  have transitive := Ordinal.transitive with hpOrdinal44  have oneSubset := transitive at 145  have oneMember := Prime.greater_than_one_membership with hp46  specialize oneSubset with oneMember47  have zeroMember := oneSubset at 048  have zeroInOne := membership.self_successor with Naturals.constructor.zero49  exact zeroMember with zeroInOne5051theorem Prime.greater_than_one (p : Set)52  requires hp : Prime(p)53  shows 1 < p54proof55  have member := Prime.greater_than_one_membership with hp56  exact Less.of_membership with member5758theorem Prime.divisor (p d : Set)59  requires hp : Prime(p)60  requires hd : Nat(d)61  requires hproper : d ∈ p62  requires hdivides : d ∣ p63  shows d = 164proof65  rcases hp with ⟨hpAbove, hpDivisors⟩66  exact hpDivisors with d, hd, hproper, hdivides6768theorem primes.contains (p : Set)69  requires hp : Prime(p)70  shows p ∈ primes71proof72  apply primes.membership.backward73  constructor74  . have natural := Prime.natural with hp75    simp [nat.omega]76  . exact hp7778-- Foundation induction on the von Neumann membership order is strong79-- induction on naturals. A hypothetical number with no prime divisor would80-- itself be prime: every proper divisor above one already has a smaller prime81-- divisor, contradicting the hypothesis.82lemma natural.exists_prime_divisor_membership (m : Set)83  shows Nat(m) → 1 ∈ m → ∃ p, Prime(p) ∧ p ∣ m84proof85  induction m using membership86  intros current ih hCurrentNat hAboveOne87  by_contra hNoPrimeDivisor88  apply hNoPrimeDivisor89  witness current90  constructor91    constructor92    . exact hAboveOne93    . intros d hdNat hdProper hdDivides94      have cases := natural.zero_one_or_above_one with hdNat95      cases cases with hdZero | hdRest96      . exfalso97        rw hdZero at hdDivides98        have currentZero := zero.divides_only_zero with hCurrentNat, hdDivides99        rw currentZero at hAboveOne100        simp101      . cases hdRest with hdOne | hdAboveOne102        . exact hdOne103        . have smaller := ih at d with hdProper, hdNat, hdAboveOne104          obtain ⟨p, hpPrime, hpDividesD⟩ := smaller105          exfalso106          apply hNoPrimeDivisor107          witness p108          constructor109          . exact hpPrime110          . have hpNat := Prime.natural with hpPrime111            exact divides.transitive with hdNat, hCurrentNat, hpDividesD, hdDivides112  . exact divides.reflexive with hCurrentNat113114-- Public Nat-order form. The membership-induction lemma above is the115-- representation bridge; elementary number theory uses this interface.116theorem natural.exists_prime_divisor (m : Nat)117  requires hAboveOne : 1 < m118  shows ∃ p, Prime(p) ∧ p ∣ m119proof120  apply natural.exists_prime_divisor_membership121  . assumption122  . apply membership.of_Less at 1, m123    . exact hAboveOne124125lemma prime_divisor.factorial_successor_not_bounded (p n : Set)126  requires hnNat : Nat(n)127  requires hp : Prime(p)128  requires hDivides : p ∣ succ(n!)129  requires hpBound : p ∈ succ(n)130  shows false131proof132  have hpPositive := Prime.positive_membership with hp133  have dividesFactorial := factorial.divisible_through with hnNat, hpPositive, hpBound134  have common := divides.consecutive_one with dividesFactorial, hDivides135  have aboveOne := Prime.greater_than_one_membership with hp136  rw common at aboveOne137  have oneMember := membership.one.forward with aboveOne138  arith139140lemma prime_divisor.factorial_successor_above_membership (p n : Set)141  requires hnNat : Nat(n)142  requires hp : Prime(p)143  requires hDivides : p ∣ succ(n!)144  shows n ∈ p145proof146  have hpNat := Prime.natural with hp147  have hnOrdinal := Ordinal.natural with hnNat148  have hpOrdinal := Ordinal.natural with hpNat149  have comparison := Ordinal.trichotomy with hnOrdinal, p, hpOrdinal150  cases comparison with hnInP | hRest151  . exact hnInP152  . exfalso153    apply prime_divisor.factorial_successor_not_bounded154    . exact hnNat155    . exact hp156    . exact hDivides157    . cases hRest with hnEqP | hpInN158      . apply membership.successor_backward{n := n} at p159        right160        simp161      . apply membership.successor_backward{n := n} at p162        left163        exact hpInN164165lemma factorial.successor_above_one_membership (n : Set)166  requires hnNat : Nat(n)167  shows 1 ∈ succ(n!)168proof169  have factorialNatural := factorial.closed with hnNat170  have factorialCases := natural.zero_one_or_above_one with factorialNatural171  cases factorialCases with hZero | hRest172  . exfalso173    have nonzero := factorial.nonzero with hnNat174    apply nonzero175    exact hZero176  . cases hRest with hOne | hAbove177    . apply membership.successor_backward{n := n!} at 1178      right179      simp180    . apply membership.successor_backward{n := n!} at 1181      left182      exact hAbove183184theorem factorial.successor_greater_than_one (n : Nat)185  shows 1 < succ(n!)186proof187  apply Less.of_membership188  . apply factorial.successor_above_one_membership at n189190-- Public Nat-level form of the factorial argument. Its implementation bridge191-- to von Neumann membership is confined to this proof.192theorem prime_divisor.factorial_successor_greater (p n : Nat)193  requires hp : Prime(p)194  requires hDivides : p ∣ succ(n!)195  shows n < p196proof197  apply Less.of_membership198  . apply prime_divisor.factorial_successor_above_membership at p, n199    . exact hp200    . exact hDivides201202-- The Euclid number has a prime divisor.  This is the natural arithmetic203-- witness lemma; its proof alone crosses to the von Neumann representation to204-- use the foundational prime-divisor existence result.205lemma factorial_successor.exists_prime_divisor (n : Nat)206  shows ∃ p, Prime(p) ∧ p ∣ succ(n!)207proof208  have aboveOne := factorial.successor_greater_than_one at n209  exact natural.exists_prime_divisor with aboveOne210211-- Euclid's theorem as elementary number theory: the visible statement and212-- proof mention only naturals, primes, divisibility, factorial, and order.213theorem Euclid.larger_prime (n : Nat)214  shows ∃ p, Prime(p) ∧ n < p215proof216  obtain ⟨p, hpPrime, hpDivides⟩ := factorial_successor.exists_prime_divisor at n with assumption217  witness p218  constructor219  . exact hpPrime220  . apply prime_divisor.factorial_successor_greater at p, n221    . exact hpPrime222    . exact hpDivides223224theorem primes.unbounded (n : Nat)225  shows ∃ p, Prime(p) ∧ n < p226proof227  apply Euclid.larger_prime228