A modular-storage proof of NP-completeness for chip-firing halting on simple digraphs

A complete attributed proof that ordinary conservative chip-firing HALTING is NP-complete under deterministic polynomial-time many-one reductions on finite loopless simple strongly connected digraphs with nonnegative binary configurations. Hardness holds with polynomial numerical total initial chips and a specified root whose deletion leaves an acyclic graph with no path of two arcs. The main construction permits antiparallel arcs; a separately proved oriented construction forbids them. The proof includes actual legal checkpoints, conservation, schedule-independent least action, polynomial output bounds, all preprocessing cases and a polynomial-bit NP certificate. The literal modular-bank formula and parallel primed-toppler mechanism are credited to Holroyd, Levine and Winkler, Abelian logic gates, arXiv:1511.00422v2, Lemma 4.1. The prime Boolean and local clause-product encoding is credited to Stockmeyer and Meyer, STOC 1973, Theorem 6.1, and its reconstruction by Gregor Gramlich alone, MFCS 2003, Fact 3. The allowed-predicate intersection is the complement of the classical invalid-variable or failed-clause union; extra local nonBoolean clause-complement residues are already variable-invalid. Neither ingredient nor avoiding global-period expansion is claimed as new. NP membership, capacity and the root-last viewpoint are prior Farrell-Levine/Farrell methods, and long simple-graph clocks are prior Eriksson. Full-result, conservative simple/oriented realization and remaining method priority, and preexisting worldwide openness, remain UNKNOWN after a bounded audit. AI tools were used extensively in solving, verification, source comparison, programming and writing. This is an unrefereed preprint, without external human peer review, journal acceptance or formal proof-assistant certification. No firstness is claimed. The support ZIP contains the complete TeX source, exact authored historical snapshots, bibliographic hashes/read scopes and fresh standard-library finite diagnostics with meaningful faults. No third-party source bodies are redistributed, no omitted historical program is claimed replayed, and finite tests do not certify the unbounded proof or the literature.