nx_proof_sqrt2_v2.nx

nx_proof_sqrt2_v2.nx -- sqrt(2) is irrational, with REAL semantic verification (not the v1 structural sketch). Per user 2026-05-15: "nishi lang must generate superior to all other systems proofs not just two level i tlooks good bullshit". Distinguishing v2 vs v1: - Statements are *Term values (real logical formulas) - Each MP / AND / contradiction step is verified BY THE KERNEL against the actual Term structure of its premises - The chain only assembles if every step semantically checks out The proof is encoded as a forward chain of inferences from a minimal set of named axioms. We use propositional symbols to stand in for the substantive arithmetic claims (since this kernel doesn't yet have arithmetic terms or rewriting). This is the SAME shape HOL Light uses to bootstrap proofs through interpreted constants. Building the arithmetic library is named follow-up. Atomic propositions (each as a CONST term): ASSUME : "sqrt(2) = p/q in lowest terms" [SYM_ASSUME] PSQ_E : "p^2 is even" [SYM_PSQ_EVEN] P_E : "p is even" [SYM_P_EVEN] QSQ_E : "q^2 is even" [SYM_QSQ_EVEN] Q_E : "q is even" [SYM_Q_EVEN] GCD_GE2 : "gcd(p,q) >= 2" [SYM_GCD_GE2] IRR : "sqrt(2) is irrational" [SYM_IRRATIONAL] Axioms (real implications, the kernel will use them): AX1: ASSUME => PSQ_E (algebra: a^2=2b^2 => a^2 even) AX2: PSQ_E => P_E (lemma: square-of-odd-is-odd contraposed) AX3: P_E => QSQ_E (algebra: p=2k & p^2=2q^2 => q^2 even) AX4: QSQ_E => Q_E (same lemma applied to q) AX5: (P_E & Q_E) => GCD_GE2 (def: 2 divides both -> gcd >= 2) AX6: ASSUME implies (NOT GCD_GE2) (def lowest terms: gcd=1) Then: ASSUME -> PSQ_E -> P_E (modus ponens twice) -> QSQ_E -> Q_E AND-intro -> (P_E & Q_E) modus ponens -> GCD_GE2