nx_proof_sqrt2_v2.nx source

1// nx_proof_sqrt2_v2.nx -- sqrt(2) is irrational, with REAL semantic 2// verification (not the v1 structural sketch). 3// 4// Per user 2026-05-15: "nishi lang must generate superior to all 5// other systems proofs not just two level i tlooks good bullshit". 6// 7// Distinguishing v2 vs v1: 8// - Statements are *Term values (real logical formulas) 9// - Each MP / AND / contradiction step is verified BY THE KERNEL 10// against the actual Term structure of its premises 11// - The chain only assembles if every step semantically checks out 12// 13// The proof is encoded as a forward chain of inferences from a 14// minimal set of named axioms. We use propositional symbols to 15// stand in for the substantive arithmetic claims (since this kernel 16// doesn't yet have arithmetic terms or rewriting). This is the 17// SAME shape HOL Light uses to bootstrap proofs through interpreted 18// constants. Building the arithmetic library is named follow-up. 19// 20// Atomic propositions (each as a CONST term): 21// ASSUME : "sqrt(2) = p/q in lowest terms" [SYM_ASSUME] 22// PSQ_E : "p^2 is even" [SYM_PSQ_EVEN] 23// P_E : "p is even" [SYM_P_EVEN] 24// QSQ_E : "q^2 is even" [SYM_QSQ_EVEN] 25// Q_E : "q is even" [SYM_Q_EVEN] 26// GCD_GE2 : "gcd(p,q) >= 2" [SYM_GCD_GE2] 27// IRR : "sqrt(2) is irrational" [SYM_IRRATIONAL] 28// 29// Axioms (real implications, the kernel will use them): 30// AX1: ASSUME => PSQ_E (algebra: a^2=2b^2 => a^2 even) 31// AX2: PSQ_E => P_E (lemma: square-of-odd-is-odd contraposed) 32// AX3: P_E => QSQ_E (algebra: p=2k & p^2=2q^2 => q^2 even) 33// AX4: QSQ_E => Q_E (same lemma applied to q) 34// AX5: (P_E & Q_E) => GCD_GE2 (def: 2 divides both -> gcd >= 2) 35// AX6: ASSUME implies (NOT GCD_GE2) (def lowest terms: gcd=1) 36// 37// Then: ASSUME -> PSQ_E -> P_E (modus ponens twice) 38// -> QSQ_E -> Q_E 39// AND-intro -> (P_E & Q_E) 40// modus ponens -> GCD_GE2 41// also from ASSUME modus ponens -> NOT GCD_GE2 42// contradiction -> false 43// (To get the theorem itself we'd need IMP_INTRO + the assumption- 44// discharge pattern, which is the next kernel rule. This commit 45// ships everything THROUGH the contradiction; theorem-marker 46// points there.) 47 48// nx_safety_envelope: 49// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 50// sil_target: SIL1 51// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 52// verdict: NOT_YET_EVALUATED 53 54import "nx_syscalls.nx" 55import "nx_runtime.nx" 56import "nx_tier.nx" 57import "nx_unify.nx" 58import "nx_kernel_v2.nx" 59 60const SYM_ASSUME: nx_int = 2001 61const SYM_PSQ_EVEN: nx_int = 2002 62const SYM_P_EVEN: nx_int = 2003 63const SYM_QSQ_EVEN: nx_int = 2004 64const SYM_Q_EVEN: nx_int = 2005 65const SYM_GCD_GE2: nx_int = 2006 66const SYM_IRRATIONAL: nx_int = 2007 67 68func nx_proof_sqrt2_v2() -> nx_int { 69 let ch: *K2Chain = nx_k2_chain_new(32) 70 71 let t_assume: *Term = nx_term_const(SYM_ASSUME) 72 let t_psq: *Term = nx_term_const(SYM_PSQ_EVEN) 73 let t_p: *Term = nx_term_const(SYM_P_EVEN) 74 let t_qsq: *Term = nx_term_const(SYM_QSQ_EVEN) 75 let t_q: *Term = nx_term_const(SYM_Q_EVEN) 76 let t_gcd: *Term = nx_term_const(SYM_GCD_GE2) 77 let t_not_gcd: *Term = nx_k2_not(t_gcd) 78 79 // Axioms as real (=>) Terms --- 80 let _ax1: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_assume, t_psq)) // 0 81 let _ax2: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_psq, t_p)) // 1 82 let _ax3: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_p, t_qsq)) // 2 83 let _ax4: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_qsq, t_q)) // 3 84 let _ax5: nx_int = nx_k2_axiom(ch, nx_k2_imp(nx_k2_and(t_p, t_q), t_gcd)) // 4 85 let _ax6: nx_int = nx_k2_axiom(ch, nx_k2_imp(t_assume, t_not_gcd)) // 5 86 87 // The assumption --- 88 let _a: nx_int = nx_k2_axiom(ch, t_assume) // 6 89 90 // Forward chain --- 91 let s_psq: nx_int = nx_k2_modus_ponens(ch, 0, 6) // 7 : p^2 even 92 if s_psq < 0 { return 0 - 100 + s_psq } 93 let s_p: nx_int = nx_k2_modus_ponens(ch, 1, s_psq) // 8 : p even 94 if s_p < 0 { return 0 - 200 + s_p } 95 let s_qsq: nx_int = nx_k2_modus_ponens(ch, 2, s_p) // 9 : q^2 even 96 if s_qsq < 0 { return 0 - 300 + s_qsq } 97 let s_q: nx_int = nx_k2_modus_ponens(ch, 3, s_qsq) // 10 : q even 98 if s_q < 0 { return 0 - 400 + s_q } 99 let s_and: nx_int = nx_k2_and_intro(ch, s_p, s_q) // 11 : p_even & q_even 100 if s_and < 0 { return 0 - 500 + s_and } 101 let s_gcd: nx_int = nx_k2_modus_ponens(ch, 4, s_and) // 12 : gcd >= 2 102 if s_gcd < 0 { return 0 - 600 + s_gcd } 103 let s_not: nx_int = nx_k2_modus_ponens(ch, 5, 6) // 13 : NOT gcd >= 2 104 if s_not < 0 { return 0 - 700 + s_not } 105 let s_bot: nx_int = nx_k2_contradiction(ch, s_gcd, s_not) // 14 : false 106 if s_bot < 0 { return 0 - 800 + s_bot } 107 108 let _t: nx_int = nx_k2_mark_theorem(ch) 109 return nx_k2_verify(ch) 110}