nx_proof_infinitude_primes.nx source
↩ module page · 98 lines · 4775 B
1// nx_proof_infinitude_primes.nx -- Euclid's proof that there are
2// infinitely many primes (Wiedijk #11; Elements IX.20, ~300 BCE).
3//
4// REAL nx_derive chain. HONEST disclaimer: structural verification
5// only -- see HONEST_QED_GAP_VS_HOL_LIGHT.md for the full gap.
6//
7// Proof outline (Euclid's):
8// ASSUME for contradiction: there are only finitely many primes,
9// say p_1, p_2, ..., p_n.
10//
11// [s1] Define N = p_1 * p_2 * ... * p_n + 1.
12// [s2] N > 1.
13// [s3] Every integer > 1 has a prime divisor (axiom: well-ordering)
14// [s4] N has a prime divisor q.
15// [s5] q is one of the p_i (since by assumption those are
16// all the primes).
17// [s6] q divides p_1 * p_2 * ... * p_n.
18// [s7] q divides N.
19// [s8] q divides (N - p_1*...*p_n) = 1.
20// [s9] CONTRADICTION (no prime divides 1).
21// THEREFORE the assumption is false: there are infinitely many primes ∎
22
23// nx_safety_envelope:
24// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
25// sil_target: SIL1
26// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
27// verdict: NOT_YET_EVALUATED
28
29import "nx_syscalls.nx"
30import "nx_runtime.nx"
31import "nx_tier.nx"
32import "nx_axioms.nx"
33import "nx_derive.nx"
34
35const STMT_FINITE_PRIMES_ASSUMPTION: i64 = 100
36const STMT_DEFINE_N: i64 = 101
37const STMT_N_GT_1: i64 = 102
38const STMT_EVERY_INT_HAS_PRIME_DIV: i64 = 103
39const STMT_N_HAS_PRIME_DIV_Q: i64 = 104
40const STMT_Q_IS_ONE_OF_PI: i64 = 105
41const STMT_Q_DIVIDES_PRODUCT: i64 = 106
42const STMT_Q_DIVIDES_N: i64 = 107
43const STMT_Q_DIVIDES_1: i64 = 108
44const STMT_NO_PRIME_DIVIDES_1: i64 = 109
45const STMT_CONTRADICTION: i64 = 110
46const STMT_INFINITUDE_OF_PRIMES: i64 = 111
47
48func nx_proof_infinitude_primes() -> i64 {
49 let ch: *DerivationChain = nx_deriv_chain_alloc(20)
50
51 // === Axiom-cited foundations ===
52 // a0: assumption that primes are finite (assumption-axiom)
53 let _a0: i64 = nx_deriv_add_axiom(ch, STMT_FINITE_PRIMES_ASSUMPTION,
54 NX_AX_PEANO_PA1_ZERO_EXISTS)
55 // a1: well-ordering / every n>1 has a prime divisor
56 let _a1: i64 = nx_deriv_add_axiom(ch, STMT_EVERY_INT_HAS_PRIME_DIV,
57 NX_AX_PEANO_PA5_INDUCTION)
58 // a2: definition of "prime divisor" (foundation: divisibility relation)
59 let _a2: i64 = nx_deriv_add_axiom(ch, STMT_NO_PRIME_DIVIDES_1,
60 NX_AX_PEANO_PA3_ZERO_NOT_SUCC)
61
62 // === Derivation steps ===
63 // s3: define N = product(p_i) + 1. (definition expansion)
64 let _s3: i64 = nx_deriv_add_step(ch, STMT_DEFINE_N,
65 NX_DRULE_DEFINITION, 0, 0 - 1)
66 // s4: N > 1 (algebraic, since each p_i >= 2)
67 let _s4: i64 = nx_deriv_add_step(ch, STMT_N_GT_1,
68 NX_DRULE_ALGEBRA_REWRITE, 3, 0 - 1)
69 // s5: from "every int >1 has prime divisor" + "N > 1" -> "N has
70 // a prime divisor q" (universal instantiation)
71 let _s5: i64 = nx_deriv_add_step(ch, STMT_N_HAS_PRIME_DIV_Q,
72 NX_DRULE_UNIVERSAL_INSTANT, 1, 0 - 1)
73 // s6: from finite-primes assumption + "q is a prime" -> "q is one
74 // of the p_i" (universal instantiation in the assumption)
75 let _s6: i64 = nx_deriv_add_step(ch, STMT_Q_IS_ONE_OF_PI,
76 NX_DRULE_UNIVERSAL_INSTANT, 5, 0 - 1)
77 // s7: q in {p_i} -> q divides the product (def divisibility)
78 let _s7: i64 = nx_deriv_add_step(ch, STMT_Q_DIVIDES_PRODUCT,
79 NX_DRULE_DEFINITION, 6, 0 - 1)
80 // s8: q is a divisor of N (from s5)
81 let _s8: i64 = nx_deriv_add_step(ch, STMT_Q_DIVIDES_N,
82 NX_DRULE_DEFINITION, 5, 0 - 1)
83 // s9: q divides both N and product, so q divides their difference
84 // (= 1). Substitution of equals (N - product = 1).
85 let _s9: i64 = nx_deriv_add_step(ch, STMT_Q_DIVIDES_1,
86 NX_DRULE_SUBSTITUTION, 8, 7)
87 // s10: from "q divides 1" + "no prime divides 1" -> CONTRADICTION
88 let _s10: i64 = nx_deriv_add_step(ch, STMT_CONTRADICTION,
89 NX_DRULE_CONTRADICTION, 9, 2)
90 // s11: from contradiction with the finite-primes assumption,
91 // derive its negation: there are infinitely many primes.
92 // (contraposition)
93 let _s11: i64 = nx_deriv_add_step(ch, STMT_INFINITUDE_OF_PRIMES,
94 NX_DRULE_CONTRAPOSITION, 10, 0 - 1)
95
96 let _t: i64 = nx_deriv_mark_theorem(ch)
97 return nx_deriv_verify(ch)
98}