nx_eqsat_congruence_test.nx

nx_eqsat_congruence_test.nx -- STRUCTURAL-WITNESS GATE for the egg-style deferred CONGRUENCE CLOSURE newly integrated into nx_eqsat.nx. THE PROOF (the new organ actually MEETS egg's congruence rebuild): Congruence axiom of equality: if a == b (same canonical e-class) then for any deterministic function f, f(...a...) == f(...b...). The pre-MEET engine had a real hashcons-by-linear-scan + union-find, but NO rebuild: after a union it never re-merged congruent PARENTS, so f(a) and f(b) stayed in distinct classes. This gate builds exactly that witness and proves the rebuild closes it. CASE 1 (POSITIVE -- congruence FIRES, cited + logged sound): Build a, b as two DISTINCT vars; build g_a = NEG(a) and g_b = NEG(b) (so the two parent e-nodes are genuinely different nodes). Pre-merge a~b via the SOUND mul_pow2 path is overkill; instead we drive the canonical congruence trigger through the real saturator: a=(mul x 8), b=(shl x 3) -> mul_pow2 merges them, then NEG(a) and NEG(b) MUST become congruent via the rebuild (same op NEG, same payload, canonically-equal child). Assert: (1a) find(NEG a) == find(NEG b) -- congruence detected (1b) the prov log contains id 8 (CONGRUENCE) -- the merge was CITED (1c) every logged id is in the proven-sound allow-list (0..8, !=NONE-as-bad) (1d) RULE_NONE (id 0) count == 0 -- no back-door (2-arg) merge CASE 2 (NEGATIVE control -- WITHOUT rebuild the gap is REAL): Same graph, but provenance/meet OFF on a plain engine run (rebuild disabled): mul_pow2 still merges (mul x 8)~(shl x 3), but the parents NEG(mul8)/NEG(shl3) are NOT merged -> find(NEG a) != find(NEG b). This proves the rebuild is the load-bearing organ (a passing CASE 1 is not vacuous). CASE 3 (NEGATIVE -- non-congruent nodes are NOT merged): NEG(a) vs NOT(a): same single child class but DIFFERENT op -> distinct fingerprints -> never congruence-merged. Asserts the fingerprint folds op (a fingerprint that ignored op would wrongly merge them and cite CONGRUENCE). KNOWN ANSWER (FAIL LOUD), one line: "<case1_member> <cong_logged> <none_count> <case2_member> <case3_member>" = "1 1 0 0 0 " exit 0 iff every assertion holds. SOVEREIGN: no SMT, no .sh; runs on the pinned NishiLang compiler. The exit code IS the verdict. license_tier: ORIGINAL