nx_rule_soundness_test.nx

nx_rule_soundness_test.nx -- FAIL-LOUD driver that PROVES the nx_eqsat rewrite rules SOUND (algebraic identities mod 2^W) via nx_rule_soundness.nx. Strategy (winning): width-independent induction (reuses the divider-proof template) + EXHAUSTIVE small-width at W=8, with nx_triangulate as the independent cross-check, and TWO independent witnesses per vector ANDed. CERTIFIED-LIVE SET (this rung): the SIX width-trivial unary rules {add_zero, sub_self, add_self, and_self, or_zero, mul_one} swept exhaustively over x in [0,2^8). They have NO k boundary and ZERO owed guards, so they are fully certifiable now. Known answer: total_unary == 1536 (= 6 * 256), all certified. mul_pow2 (NEXT rung -- theorem proven here but NOT in the certified-live set): IN-RANGE: for all x in [0,2^8) and all k in [0,8), MUL(x,2^k) == SHL(x,k) mod 2^8. Known answer: in_range == 2048 (= 256 * 8), all certified. BOUNDARY (k>=W): the rule MUST NOT fire -- the identity is FALSE. We PROVE unsoundness for k in [8,16) over all x (the owed k<W guard's location). Known answer: neg_caught == neg_total == 2048 (= 256 * 8). mul_pow2 stays OUT of the live-certified set until the k<W guard lands in nx_eqsat.nx. EXIT CODES (FAIL LOUD): 1 a certified-unary rule vector failed (proven_unary != total_unary) 2 unary total mismatch (total_unary != 1536) 3 a mul_pow2 in-range vector failed (proven_ir != in_range) 4 mul_pow2 in-range total mismatch (in_range != 2048) 5 a mul_pow2 boundary vector did NOT demonstrate unsoundness (neg_caught != neg_total) 6 boundary total mismatch (neg_total != 2048) 0 ALL pass. KNOWN-ANSWER LINE printed (FAIL LOUD): the per-rule pass counts then the exhaustive totals: "<add_zero> <sub_self> <add_self> <and_self> <or_zero> <mul_one> | <rules_proven> <proven_unary> <total_unary> | <proven_ir> <in_range> | <neg_caught> <neg_total>" SOVEREIGN: no SMT, no .sh, no foreign oracle -- runs on the pinned compiler.