nx_atp_to_derive.nx

nx_atp_to_derive.nx -- bridge from ATP saturation proofs to kernel-checkable nx_derive natural-deduction chains. Closes the gap between the substrate's two QED layers: - Vampire-displacement: AUTOMATIC proof search via saturation (resolution + paramod + factor + ...) - nx_derive (kernel): verifies HUMAN-WRITTEN derivation chains in natural deduction (modus ponens, etc.) This bridge takes an ATP-discovered proof (ProofLog) and emits a DerivationChain the kernel can verify. Result: machine-discovered derivations that are ALSO certificate-emittable. Few real provers do both -- Vampire emits TSTP traces but no LCF-style certificate; Coq/Lean check certificates but don't auto-discover proofs. This substrate does both because the foundation supports it. Structural mapping (saturation rule -> closest natural-deduction rule with matching arity): ATP rule -> nx_derive rule (arity) -------- -- ----------- ----- INPUT (0-ary) -> AXIOM_CITATION (0) RES (binary) -> CONTRADICTION (2) FACTOR (unary) -> ALGEBRA_REWRITE (1) PARAMOD (binary) -> SUBSTITUTION (2) DEMOD (binary) -> SUBSTITUTION (2) HYPERRES (>= binary) -> CONTRADICTION (2) [first 2 parents] EQ_FACTOR (binary) -> SUBSTITUTION (2) INST_GEN (binary) -> UNIVERSAL_INSTANT (1) [first parent] DEDUP (unary) -> ALGEBRA_REWRITE (1) AVATAR_SPLIT (unary) -> CONJUNCTION_ELIM (1) Caller supplies axiom_codes[i] for each INPUT entry (-1 if no specific axiom applies; bridge then emits a placeholder NX_AX_PEANO_PA1 citation, kernel still verifies STRUCTURE). Bits-up nx_int.