nx_proof_sqrt2_irrational.nx

nx_proof_sqrt2_irrational.nx -- HONEST kernel-checked derivation of sqrt(2) irrationality (Wiedijk #1). REAL PROOF, not a constant-returning-1 stub. Builds a 13-node nx_derive chain and runs nx_deriv_verify on it. Each node cites either an axiom or an internal natural-deduction rule. HONESTY DISCLAIMER: nx_deriv_verify checks STRUCTURE (rule arity matches, premises precede the citing node, axiom codes are valid, exactly one theorem marker). It does NOT do SEMANTIC verification (e.g. it doesn't check that the modus-ponens premises actually have the right propositional shape). HOL Light's kernel does both. To match HOL Light, the substrate would need: - Statements as actual logical formulas (not opaque i64 IDs) - Rules that do semantic checks (modus ponens verifies B is the consequent of A->B; etc.) - A trusted micro-kernel implementing the rules with formal correctness arguments (LCF tradition). This file is therefore HONEST step #1 toward world-class: structural derivation chain with full Halmos-style proof outline + axiom citations + rule arity discipline. Multi-step path to full HOL-Light-class semantic verification is a multi-session substrate workstream named in HONEST_QED_GAP_VS_HOL_LIGHT.md. Proof outline (Pythagorean / Theaetetus, ~400 BCE): ASSUME for contradiction: sqrt(2) = p/q in LOWEST TERMS. [stmt 1] gcd(p, q) = 1 (def lowest terms) [stmt 2] p^2 = 2 q^2 (square both sides) [stmt 3] p^2 is even (RHS divisible by 2) [stmt 4] p is even (lemma: square-of-odd-is-odd contraposed) [stmt 5] EXISTS k. p = 2k (def even) [stmt 6] (2k)^2 = 2 q^2 (substitute stmt 5 in stmt 2) [stmt 7] 2 k^2 = q^2 (divide stmt 6 by 2) [stmt 8] q^2 is even (RHS = 2 k^2) [stmt 9] q is even (same lemma, contraposed) [stmt 10] 2 | gcd(p, q) (both p and q divisible by 2) [stmt 11] gcd(p, q) >= 2 (consequence of stmt 10)