Slim spec comparison script down to pure static analysis

Remove the executable witness tie-breaker (value pool, rejection
sampling, doctest mining) and its TermMember membership model. It
executed stdlib functions with sampled arguments -- too much surface
for a CI script -- and upgraded no verdicts on the current tree. The
gate semantics are unchanged for practical purposes: lattice
contradictions and unacknowledged residue entries still fail the run.
443 lines smaller, fully deterministic, no code execution.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: lukaszsamson