nx_eqsat_rule_proof_test.nx

nx_eqsat_rule_proof_test.nx -- SOVEREIGN soundness proof for the eqsat rewrite rules (algebraic-normal-form leg). Models nx_alu_divider_proof_test.nx: a machine-checked exhaustive small-width check + a width-independent induction argument (in comments/structure), cross-checked by triangulation legs that all run through nx_gsim (independent of NishiLang `*`/`<<` codegen via the netlist). WORKED EXAMPLE: certify mul x 8 == shl x 3 BY PROOF (not battery): build LHS netlist (MUL x 8) + RHS netlist (SHL x 3), sweep x over a representative width, assert outputs byte-identical EVERY vector. Known answer (FAIL LOUD): "<proven> <total> " printed; exit 0 iff proven==total.