judge: trained ETP relation judge — library, CLI, training and eval

[karthikreddy-02]

Replaces the prompted-LLM judge with a trained artifact: known training data, a known split, and weights we own and can probe. Labels come from oracle/'s Lean-verified implication matrix, so the training signal has zero label noise and no prover runs at training time.

The split is by equivalence class, never by pair (1,064/140/211 of 1,415). Laws inside a class are mutually derivable, so a random pair split lets a lookup table score perfectly. The x = y class alone is 31.9% of the catalogue and is pinned into training. pairs_val minus classes_val is therefore the memorization measurement: 1.91 pp on Gemma-2-2B, 1.25 pp on Llama-3.1-8B. Both trained a judge, not a lookup table.

judge.py exposes both a CLI (compare / batch / rank) and a Judge class, with the live PeftModel reachable as .model so the interpretability work can attach hooks rather than shell out. Scoring restricts logits to the four label tokens before the argmax, so an invalid answer is impossible by construction rather than merely unlikely.

Results and ablations across two model families are in judge/README.md, including two findings that did NOT survive replication and should not be claimed: the attention/MLP asymmetry is a Gemma artifact, and the early-vs-middle layer ordering flips between families. What does replicate: rank saturates at or below 16, and late-layer-only adaptation collapses (5-6x worse than any other layer choice) in both models.

Neither base model can be contaminated: ETP launched 2024-09-25, while Gemma-2 shipped 2024-06-27 and Llama-3.1 on 2024-07-23.

Generated data and trained weights are gitignored; both are regenerable.