nx_classical.nx

nx_classical.nx -- classical-logic axioms. Closes the named blocker for nonconstructive proofs (currently PARTIAL in the audit). Per user 2026-05-15: "no losses". Adds two axioms that are sound in CLASSICAL but not INTUITIONISTIC logic. The kernel core (nx_kernel_v2) stays intuitionistic; classical proofs explicitly cite these axioms so the audit trail always shows whether classical logic was used. LEM: for any A, A | ~A DNE: for any A, ~~A => A LEM and DNE are interderivable in classical logic; we ship both because each saves a step in different proof shapes. HOL Light derives the rest from these (Peirce's law, RAA, etc.) via the engine + the existing v2 rules.