nx_proof_methods.nx source

1// nx_proof_methods.nx -- comprehensive sealed enum of proof methods 2// covering Wikipedia "Mathematical proof" + ATP technique families. 3// 4// Per user 2026-05-14: substrate must cover every reasonable proof 5// method from the literature and bridge entry-level to advanced math. 6 7// nx_safety_envelope: 8// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 9// sil_target: SIL1 10// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 11// verdict: NOT_YET_EVALUATED 12 13import "nx_syscalls.nx" 14import "nx_runtime.nx" 15import "nx_tier.nx" 16import "nx_axioms.nx" 17import "nx_derive.nx" 18 19// ===== Proof method codes (sealed enum) ============================= 20// Each maps to a category in Wikipedia "Mathematical proof". 21const NX_PROOF_METHOD_DIRECT: nx_int = 1 22const NX_PROOF_METHOD_INDUCTION: nx_int = 2 // weak/standard 23const NX_PROOF_METHOD_INDUCTION_STRONG: nx_int = 3 // strong/complete 24const NX_PROOF_METHOD_INDUCTION_STRUCT: nx_int = 4 // structural 25const NX_PROOF_METHOD_INFINITE_DESCENT: nx_int = 5 // Fermat-style 26const NX_PROOF_METHOD_CONTRAPOSITION: nx_int = 6 27const NX_PROOF_METHOD_CONTRADICTION: nx_int = 7 // reductio 28const NX_PROOF_METHOD_CONSTRUCTION: nx_int = 8 // constructive existence 29const NX_PROOF_METHOD_EXHAUSTION: nx_int = 9 // case analysis 30const NX_PROOF_METHOD_CLOSED_CHAIN: nx_int = 10 // pairwise equivalence 31const NX_PROOF_METHOD_PROBABILISTIC: nx_int = 11 32const NX_PROOF_METHOD_COMBINATORIAL: nx_int = 12 // bijection / double-count 33const NX_PROOF_METHOD_NONCONSTRUCTIVE: nx_int = 13 34const NX_PROOF_METHOD_COMPUTER_ASSIST: nx_int = 14 35const NX_PROOF_METHOD_VISUAL: nx_int = 15 // picture/diagram 36const NX_PROOF_METHOD_TWO_COLUMN: nx_int = 16 // US-HS geometry form 37const NX_PROOF_METHOD_ELEMENTARY: nx_int = 17 // restricted machinery 38const NX_PROOF_METHOD_STATISTICAL: nx_int = 18 // pure-math statistical 39const NX_PROOF_METHOD_AXIOM_CITATION: nx_int = 19 // single-axiom appeal 40 41func nx_proof_method_name(code: nx_int) -> *u8 { 42 if code == NX_PROOF_METHOD_DIRECT { return "direct" as *u8 } 43 if code == NX_PROOF_METHOD_INDUCTION { return "induction (weak)" as *u8 } 44 if code == NX_PROOF_METHOD_INDUCTION_STRONG { return "induction (strong)" as *u8 } 45 if code == NX_PROOF_METHOD_INDUCTION_STRUCT { return "structural induction" as *u8 } 46 if code == NX_PROOF_METHOD_INFINITE_DESCENT { return "infinite descent" as *u8 } 47 if code == NX_PROOF_METHOD_CONTRAPOSITION { return "contraposition" as *u8 } 48 if code == NX_PROOF_METHOD_CONTRADICTION { return "contradiction (reductio)" as *u8 } 49 if code == NX_PROOF_METHOD_CONSTRUCTION { return "construction (constructive)" as *u8 } 50 if code == NX_PROOF_METHOD_EXHAUSTION { return "exhaustion (case analysis)" as *u8 } 51 if code == NX_PROOF_METHOD_CLOSED_CHAIN { return "closed-chain inference" as *u8 } 52 if code == NX_PROOF_METHOD_PROBABILISTIC { return "probabilistic" as *u8 } 53 if code == NX_PROOF_METHOD_COMBINATORIAL { return "combinatorial (bijection/double-count)" as *u8 } 54 if code == NX_PROOF_METHOD_NONCONSTRUCTIVE { return "nonconstructive" as *u8 } 55 if code == NX_PROOF_METHOD_COMPUTER_ASSIST { return "computer-assisted" as *u8 } 56 if code == NX_PROOF_METHOD_VISUAL { return "visual (diagram)" as *u8 } 57 if code == NX_PROOF_METHOD_TWO_COLUMN { return "two-column (US-HS)" as *u8 } 58 if code == NX_PROOF_METHOD_ELEMENTARY { return "elementary" as *u8 } 59 if code == NX_PROOF_METHOD_STATISTICAL { return "statistical (pure math)" as *u8 } 60 if code == NX_PROOF_METHOD_AXIOM_CITATION { return "axiom citation" as *u8 } 61 return "(unknown method)" as *u8 62} 63 64// ===== ATP technique codes (sealed enum) ============================ 65const NX_ATP_RESOLUTION: nx_int = 101 66const NX_ATP_MODEL_ELIMINATION: nx_int = 102 67const NX_ATP_TABLEAUX: nx_int = 103 68const NX_ATP_SUPERPOSITION: nx_int = 104 // + term rewriting 69const NX_ATP_SAT_DPLL: nx_int = 105 70const NX_ATP_SMT_CDCL: nx_int = 106 71const NX_ATP_MODEL_CHECKING: nx_int = 107 72const NX_ATP_BDD: nx_int = 108 // binary decision diagram 73const NX_ATP_HIGHER_ORDER_UNIF: nx_int = 109 74const NX_ATP_QUANTIFIER_ELIM: nx_int = 110 75const NX_ATP_TACTIC_LCF: nx_int = 111 // LCF tradition 76const NX_ATP_PRESBURGER: nx_int = 112 // Presburger arithmetic decider 77 78func nx_atp_technique_name(code: nx_int) -> *u8 { 79 if code == NX_ATP_RESOLUTION { return "first-order resolution" as *u8 } 80 if code == NX_ATP_MODEL_ELIMINATION { return "model elimination" as *u8 } 81 if code == NX_ATP_TABLEAUX { return "analytic tableaux" as *u8 } 82 if code == NX_ATP_SUPERPOSITION { return "superposition + term rewriting" as *u8 } 83 if code == NX_ATP_SAT_DPLL { return "SAT via DPLL" as *u8 } 84 if code == NX_ATP_SMT_CDCL { return "SMT via CDCL" as *u8 } 85 if code == NX_ATP_MODEL_CHECKING { return "model checking" as *u8 } 86 if code == NX_ATP_BDD { return "binary decision diagram" as *u8 } 87 if code == NX_ATP_HIGHER_ORDER_UNIF { return "higher-order unification" as *u8 } 88 if code == NX_ATP_QUANTIFIER_ELIM { return "quantifier elimination" as *u8 } 89 if code == NX_ATP_TACTIC_LCF { return "tactic-based (LCF)" as *u8 } 90 if code == NX_ATP_PRESBURGER { return "Presburger arithmetic" as *u8 } 91 return "(unknown technique)" as *u8 92} 93 94// ===== End-of-proof marker ========================================== 95// Unicode U+220E (∎) or QED. 96func nx_proof_qed() -> *u8 { return "\xE2\x88\x8E" as *u8 } // ∎ 97func nx_proof_qed_text() -> *u8 { return "Q.E.D." as *u8 }