nx_proof_sqrt2_v3.nx source
↩ module page · 78 lines · 3603 B
1// nx_proof_sqrt2_v3.nx -- sqrt(2) is irrational, RESULT IS A CLOSED
2// THEOREM (no open hypotheses).
3//
4// Difference vs v2: v2 stopped at "ASSUME |- false". v3 properly
5// DISCHARGES the assumption via NOT_INTRO to produce the actual
6// theorem "|- NOT (sqrt(2) = p/q in lowest terms)" with zero open
7// hypotheses. This is what HOL Light publishes as a theorem; v2 was
8// only an intermediate sequent.
9
10// nx_safety_envelope:
11// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
12// sil_target: SIL1
13// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
14// verdict: NOT_YET_EVALUATED
15
16import "nx_syscalls.nx"
17import "nx_runtime.nx"
18import "nx_tier.nx"
19import "nx_unify.nx"
20import "nx_kernel_v2.nx"
21
22const SYM_ASSUME: nx_int = 2001
23const SYM_PSQ_EVEN: nx_int = 2002
24const SYM_P_EVEN: nx_int = 2003
25const SYM_QSQ_EVEN: nx_int = 2004
26const SYM_Q_EVEN: nx_int = 2005
27const SYM_GCD_GE2: nx_int = 2006
28
29func nx_proof_sqrt2_v3() -> nx_int {
30 let ch: *K2Chain = nx_k2_chain_new(32)
31
32 let t_assume: *Term = nx_term_const(SYM_ASSUME)
33 let t_psq: *Term = nx_term_const(SYM_PSQ_EVEN)
34 let t_p: *Term = nx_term_const(SYM_P_EVEN)
35 let t_qsq: *Term = nx_term_const(SYM_QSQ_EVEN)
36 let t_q: *Term = nx_term_const(SYM_Q_EVEN)
37 let t_gcd: *Term = nx_term_const(SYM_GCD_GE2)
38 let t_not_gcd: *Term = nx_k2_not(t_gcd)
39
40 // Foundation axioms 0..5 (no hypotheses):
41 let _ax1: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_assume, t_psq)) // 0
42 let _ax2: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_psq, t_p)) // 1
43 let _ax3: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_p, t_qsq)) // 2
44 let _ax4: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_qsq, t_q)) // 3
45 let _ax5: nx_int = nx_k2_axiom(ch, nx_k2_imp(nx_k2_and(t_p, t_q), t_gcd)) // 4
46 let _ax6: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_assume, t_not_gcd)) // 5
47
48 // Introduce the assumption (open hyp: ASSUME):
49 let a_idx: nx_int = nx_k2_assume(ch, t_assume) // 6
50
51 // Forward chain under hypothesis ASSUME:
52 let s_psq: nx_int = nx_k2_modus_ponens(ch, 0, a_idx) // 7
53 if s_psq < 0 { return 0 - 100 + s_psq }
54 let s_p: nx_int = nx_k2_modus_ponens(ch, 1, s_psq) // 8
55 if s_p < 0 { return 0 - 200 + s_p }
56 let s_qsq: nx_int = nx_k2_modus_ponens(ch, 2, s_p) // 9
57 if s_qsq < 0 { return 0 - 300 + s_qsq }
58 let s_q: nx_int = nx_k2_modus_ponens(ch, 3, s_qsq) // 10
59 if s_q < 0 { return 0 - 400 + s_q }
60 let s_and: nx_int = nx_k2_and_intro(ch, s_p, s_q) // 11
61 if s_and < 0 { return 0 - 500 + s_and }
62 let s_gcd: nx_int = nx_k2_modus_ponens(ch, 4, s_and) // 12
63 if s_gcd < 0 { return 0 - 600 + s_gcd }
64 let s_not: nx_int = nx_k2_modus_ponens(ch, 5, a_idx) // 13
65 if s_not < 0 { return 0 - 700 + s_not }
66 let s_bot: nx_int = nx_k2_contradiction(ch, s_gcd, s_not) // 14 false (hyp ASSUME)
67 if s_bot < 0 { return 0 - 800 + s_bot }
68
69 // *** THE DISCHARGE -- closes the proof ***
70 // ASSUME |- false becomes |- NOT ASSUME (no open hyps)
71 let s_thm: nx_int = nx_k2_not_intro(ch, a_idx, s_bot) // 15 NOT ASSUME (closed)
72 if s_thm < 0 { return 0 - 900 + s_thm }
73
74 // mark_theorem refuses non-closed theorems -- this checks closure.
75 let m: nx_int = nx_k2_mark_theorem(ch)
76 if m != NX_K2_OK { return 0 - 1000 + m }
77 return nx_k2_verify(ch)
78}