Refactor Wang Z3 around shared edge terms

[xtraid]

Summary

• replace per-adjacency tile support implications with one finite edge-tuple relation per active cell
• share one Z3 color term across every active internal edge while keeping holes independent
• preserve the public SAT, UNSAT, UNKNOWN, dense witness, generic tileset, and duplicate-tile contracts
• document the model, controlled before/after measurement, and its limits

Verification

• make check: complete C suite and 69 Python tests
• focused edge identity, hole, generic tileset, brute-force differential, duplicate tile, and UNKNOWN tests
• independent witness validation
• Pages catalog check with 20 technical documents
• git diff --check and artifact/secret scans
• independent review with no open findings

Controlled measurement

Ryzen 5 3600, CPU 2, Python 3.13.5, Z3 4.16.0, one fresh SAT sample per scope:

• prepared Wang solve: 10.666 s to 2.605 s (-75.58%); RSS 88,396 to 87,060 KiB
• file-to-verified decision: 10.560 s to 2.620 s (-75.19%); RSS 88,580 to 86,984 KiB

This is a host-specific single-sample mechanism check, not a CI threshold or a claim about hard UNSAT and larger scaling.