nx_proof_sqrt2_irrational_test.nx source
↩ module page · 46 lines · 2559 B
1// nx_proof_sqrt2_irrational_test.nx -- exercise the honest sqrt(2) proof.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_derive.nx"
7import "nx_proof_sqrt2_irrational.nx"
8
9func main() -> nx_exit {
10 println("=== sqrt(2) irrationality -- HONEST kernel-checked proof ===" as *u8)
11
12 let v: i64 = nx_proof_sqrt2_irrational()
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: 12-step derivation chain, axiom-rooted, kernel-passed." as *u8)
17 println("" as *u8)
18 println("Halmos-style proof outline (Theaetetus, ~400 BCE):" as *u8)
19 println(" ASSUME sqrt(2) = p/q in lowest terms (gcd(p,q)=1)." as *u8)
20 println(" [s1] p^2 = 2 q^2 (square both sides)" as *u8)
21 println(" [s2] p^2 is even (RHS divisible by 2)" as *u8)
22 println(" [s3] p is even (lemma: n^2 even -> n even)" as *u8)
23 println(" [s4] EXISTS k. p = 2k (def even)" as *u8)
24 println(" [s5] (2k)^2 = 2 q^2 (substitute s4 into s1)" as *u8)
25 println(" [s6] 2 k^2 = q^2 (divide both sides by 2)" as *u8)
26 println(" [s7] q^2 is even" as *u8)
27 println(" [s8] q is even (same lemma)" as *u8)
28 println(" [s9] 2 | gcd(p,q) (both p, q divisible by 2)" as *u8)
29 println(" [s10] gcd(p,q) >= 2" as *u8)
30 println(" [s11] CONTRADICTION (s10 vs assumption gcd=1)" as *u8)
31 println(" THEREFORE no such p, q exist, so sqrt(2) is irrational Halmos-tombstone" as *u8)
32 println("" as *u8)
33 println("HONESTY DISCLAIMER: nx_deriv_verify checks STRUCTURE." as *u8)
34 println(" - rule-arity discipline matches each natural-deduction rule" as *u8)
35 println(" - all premises precede their citing nodes (DAG topology)" as *u8)
36 println(" - all axiom citations reference valid NX_AX_* codes" as *u8)
37 println(" - exactly one node is marked the theorem" as *u8)
38 println("It does NOT do SEMANTIC verification (the verifier doesn't" as *u8)
39 println("interpret the statement-IDs). HOL Light's kernel does both." as *u8)
40 println("Path to full HOL-Light-class semantic verification is named" as *u8)
41 println("in docs/HONEST_QED_GAP_VS_HOL_LIGHT.md." as *u8)
42 return 0
43 }
44 println("VERIFY FAILED" as *u8)
45 return 1
46}