nx_proof_sqrt2_v3_test.nx source
↩ module page · 29 lines · 1347 B
1// nx_proof_sqrt2_v3_test.nx -- exercise the CLOSED v3 proof.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_kernel_v2.nx"
7import "nx_proof_sqrt2_v3.nx"
8
9func main() -> nx_exit {
10 println("=== sqrt(2) irrational -- v3 (CLOSED theorem via NOT_INTRO) ===" as *u8)
11 let v: nx_int = nx_proof_sqrt2_v3()
12 print("nx_k2_verify -> " as *u8); print_i64(v); println("" as *u8)
13 if v == NX_K2_OK {
14 println("VERIFIED OK -- 16-node chain, 0 open hypotheses." as *u8)
15 println("THEOREM (closed): NOT (sqrt(2) = p/q in lowest terms)" as *u8)
16 println("which is propositionally sqrt(2) is irrational ∎" as *u8)
17 println("" as *u8)
18 println("Discharge step (the difference vs v2):" as *u8)
19 println(" step 14: contradiction -> false (still has open hyp ASSUME)" as *u8)
20 println(" step 15: NOT_INTRO(assume_idx, false_idx)" as *u8)
21 println(" |- NOT ASSUME (open hyps now empty)" as *u8)
22 println("nx_k2_mark_theorem ENFORCED closure: refuses to mark a node" as *u8)
23 println("with open hypotheses. This is the LCF discipline that turns" as *u8)
24 println("a development into a publishable theorem." as *u8)
25 return 0
26 }
27 print("VERIFY FAILED with code " as *u8); print_i64(v); println("" as *u8)
28 return 1
29}