nx_derive.nx

nx_derive.nx -- verifiable derivation chains from axioms to theorems. "A mathematician can start from zero and build all the way into what they are proposing or proving." -- user, 2026-05-10 This primitive enforces that discipline: every theorem the substrate claims must show a derivation chain rooted in the foundational axioms (nx_axioms.nx). Substrate runs nx_derive_verify on each chain; any chain with an unrecognized axiom OR an unsupported rule is REJECTED. A derivation is a DAG of DerivationNode nodes: - LEAF nodes cite an axiom (axiom_code != 0) - INTERNAL nodes cite a rule_id + premise_ids - One node is marked as the THEOREM (the derivation's conclusion) Rules supported (closed enum): modus_ponens A, A->B |- B modus_tollens ~B, A->B |- ~A universal_instant forall x P(x) |- P(t) existential_gen P(t) |- exists x P(x) substitution A=B, P(A) |- P(B) induction P(0), P(n)->P(n+1) |- forall n P(n) conjunction_intro A, B |- A^B conjunction_elim A^B |- A (or B) disjunction_intro A |- A v B contradiction A, ~A |- false contraposition A->B |- ~B->~A transitivity_eq A=B, B=C |- A=C trans_inequality A<=B, B<=C |- A<=C genealogy_id: hilbert_1899 + frege_1879 + russell_whitehead_1910 lineage_id: formal_proof_theory