nx_proof_infinitude_primes_test.nx source
↩ module page · 32 lines · 1370 B
1// nx_proof_infinitude_primes_test.nx -- exercise Euclid IX.20.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_derive.nx"
7import "nx_proof_infinitude_primes.nx"
8
9func main() -> nx_exit {
10 println("=== Infinitude of Primes (Wiedijk #11, Euclid IX.20) ===" as *u8)
11
12 let v: i64 = nx_proof_infinitude_primes()
13 print("nx_deriv_verify -> " as *u8); print_i64(v); println("" as *u8)
14
15 if v == NX_DERIV_VERIFY_OK {
16 println("VERIFIED OK: 9-step derivation chain, axiom-rooted, kernel-passed." as *u8)
17 println("" as *u8)
18 println("Euclid's proof outline (Elements IX.20, ~300 BCE):" as *u8)
19 println(" ASSUME there are only finitely many primes p_1, p_2, ..., p_n." as *u8)
20 println(" Define N = p_1 * p_2 * ... * p_n + 1." as *u8)
21 println(" N > 1, so N has a prime divisor q." as *u8)
22 println(" By the assumption, q is one of the p_i." as *u8)
23 println(" So q divides p_1 * p_2 * ... * p_n." as *u8)
24 println(" But q also divides N." as *u8)
25 println(" So q divides N - (p_1 * ... * p_n) = 1." as *u8)
26 println(" No prime divides 1. CONTRADICTION." as *u8)
27 println(" THEREFORE the primes are not finite -- there are infinitely many ∎" as *u8)
28 return 0
29 }
30 println("VERIFY FAILED" as *u8)
31 return 1
32}