nx_lemma_import.nx

nx_lemma_import.nx -- Mass-ingestion bridge for imported lemmas. Per user 2026-05-15: "i mean wtf are we doing in preschool level when we can exceed". Reality: HOL Light has ~10K lemmas accumulated over 27 years. Lean Mathlib has 200K+ accumulated by hundreds of contributors. Coq stdlib + Mathcomp + UniMath have 50K+. Isabelle AFP has tens of thousands across hundreds of entries. Mizar has 70K+ theorems. We will not hand-write 10K NishiLang derivation chains. The realistic stomp path -- the same one Lean Mathlib used to grow past Coq stdlib in 5 years -- is INGESTION + PROVENANCE. This module is the bridge. Any external lemma can be imported as a v2 kernel axiom by calling nx_lemma_import(). Each imported axiom carries: - source system (sealed enum: HOL_LIGHT / COQ / LEAN / ISABELLE / MIZAR / NATIVE) - canonical name in the source system - the formal statement as a *Term (using nx_unify Term machinery) - sha256 of the statement bytes (for content-addressing / deduplication / provenance auditing) - import status: PROVED_NATIVE / IMPORTED_TRUSTED / IMPORTED_REPLAYED HONEST DISCLAIMER: IMPORTED_TRUSTED means we trust the source system's verification. The kernel itself does NOT re-verify the source's proof. This is the same approach Lean Mathport used to seed Mathlib4 from Mathlib3 and how every cross-system import works in practice. IMPORTED_REPLAYED means we re-derive the lemma natively in v2. This is the gold standard but expensive. Track the verification debt explicitly via the status field. PROVED_NATIVE means we have a v2 kernel chain for it. These are first-class.