nx_eqsat_bw_witness_gate.nx

nx_eqsat_bw_witness_gate.nx -- the BOUNDED-WIDTH TRUNCATION GATE underneath the whole mul_pow2 rule. CLAIM, proven exhaustively: for a W-bit machine with mask = 2^W - 1, ((x * 2^k) & mask) == ((x << k) & mask) for ALL x in [0, 2^W) and ALL k in [0, W). That is the mul-to-shl identity in mod-2^W arithmetic, which is the form the shipping optimizer actually needs: real registers truncate, so an identity holding only over the integers is not the one being relied on. PROMOTED FROM A THROWAWAY 2026-08-14 and RENAMED in the same pass. Its own header called it a throwaway witness, it had NEVER BEEN COMPILED, and its verdict was an exit code nothing could read. A 1,048,576-vector exhaustive check of the semantics every other eqsat proof leans on is not throwaway work -- it is the floor those proofs stand on, and it was treated as scaffolding because of a word in a comment. WHY THE NAME CHANGED: /api/gate_run executes verifiers ONLY and requires a name ending in gate, test or kat -- the bound that stops that route reaching a daemon or deployer. The old name could be built and promoted but never RUN through the gate door, so it would have joined the promoted-but-uninvokable pile. The predecessor path is retired, not deleted. ANTI-VACUITY, WHICH THE ORIGINAL LACKED: `agree == total` is TRUE OVER AN EMPTY SWEEP, and also for a degenerate run where every value is zero -- an equality between two always-zero quantities proves nothing about multiplying or shifting. So the sweep length is asserted against its own arithmetic AND the run must produce non-zero values that COULD have differed. license_tier: ORIGINAL expect_exit: 0