nx_theorem_ingest.nx

nx_theorem_ingest.nx -- ingest machine-readable theorem corpora. Strategy doc: docs/THEOREM_INGESTION_STRATEGY.md Phase P0 implementation: minimal MetaMath-style tokenizer + chain builder + ingestion driver. Reads a corpus from disk via sys_read_file, parses statements, translates proof tokens into DerivationChain objects, runs nx_deriv_verify, emits ledger entry. MetaMath statement grammar (subset we accept in P0): $c c1 c2 ... $. declare constants $v v1 v2 ... $. declare variables $f label v term $. variable-type hypothesis $e label term $. logical hypothesis $a label term $. axiom assertion $p label term $= proof-tokens $. provable theorem with proof $( comment $) comment block ${ ... $} scope block We focus on $a / $p / $e since those carry the substrate-relevant structure. $c / $v / $f are tracked as a symbol table. genealogy_id: megill_metamath_1992 + russell_whitehead_1910 (formal_proof) lineage_id: formal_proof_theory + token_substitution