nx_eqsat_membership_proof.nx

nx_eqsat_membership_proof.nx -- MEMBERSHIP-AS-PROOF CERTIFICATE for the eqsat e-graph (the sovereign analogue of ROVER's "verified rewriting": no external SMT oracle; the rewrite rules' soundness + e-class membership IS the proof). THE CLAIM BEING CERTIFIED: Two expressions a, b are equivalent-for-all-inputs (mod 2^W) iff (1) MEMBERSHIP: nx_eqsat_find(g, a) == nx_eqsat_find(g, b) (they landed in the same canonical e-class after saturation), AND (2) PROVENANCE: every union on the rewrite path that merged them used a rule from the PROVEN-SOUND set. When BOTH hold, a == b for all inputs -- membership is a rewrite-path equivalence PROOF, not a heuristic. LIVE CERTIFICATION (mp_certify_live): the engine (nx_eqsat.nx) now logs the citing rule-id of EVERY real merge at its single union chokepoint (nx_eqsat_union_cited) when provenance is enabled (nx_eqsat_enable_prov). The live certifier runs the REAL nx_eqsat_saturate and checks the GLOBAL property "every logged rule-id is in the proven-sound set" + find(a)==find(b) + the log did not overflow (fail-closed). Because every merge flows through the one function that mutates canon, a merge cannot happen without a rule-id being logged -- so an unlogged/un-cited merge (RULE_NONE) poisons the certificate. The gated recorder (mp_prov_admit_union) is RETAINED for the load-bearing negatives' belt-and-suspenders legs + the k<MP_W boundary side-condition. THE SOUND SET (justified, not asserted): a rule is admitted to the sound set ONLY after its W-bit (mod 2^W) algebraic identity is machine-checked EXHAUSTIVELY at a representative width W=8 -- the same width-independent exhaustive-small-width discipline as nx_alu_divider_proof_test.nx. Every evaluator output is MASKED to W bits before comparison (mask = (1<<W)-1) so we prove the true mod-2^W theorem, NOT a coincidental full-i64 identity (the truncation gap). The oracle is also reduced mod 2^W and is independent of both the MUL and SHL nodes (computed by repeated doubling), so the two netlist legs + oracle are three independent witnesses fed through nx_triangulate. LOAD-BEARING (defense in depth): the certificate must FAIL when (NEG-A) a NON-sound rule is used (it is not in the allow-list AND its W=8 battery DISAGREES, so it can never enter the sound set), or (NEG-B) the two endpoints are NOT in the same e-class (membership fails). Both negatives are exercised + asserted in the test (FAIL LOUD known answer).