benchmarks: add squarefree-class obstruction audit

[yuelgrace1810-ops]

Summary

• add one independent Regression-family Harbor task from FineProofs-SFT default train row 4
• require the full reduction from square products to squarefree-kernel classes and squared class counts
• independently enumerate the modulo-8 three-square obstruction and reconstruct the four-class transversal

Quality gate

• score: 86/100
• primary objective: structural theorem reduction
• difficulty: Hard (provisional; no empirical baseline yet)
• shortcut audit: four arbitrary integers, the public conclusion, and the isolated congruence 2023 ≡ 7 (mod 8) cannot pass without the kernel equivalence, count identity, at-most-three-class reduction, complete residue table, and transversal reconstruction
• discrimination estimate: weaker agents may find the modular fact but omit the class reduction; stronger agents should preserve the full chain; tool-less agents remain viable
• assurance ceiling: COMPUTED

Validation

• make harbor-check: 456 passed
• generic malformed/evidence/scope/unsupported-VERIFIED adversarial suite: passed
• clean-room one/two/three-square residue enumeration: passed
• Ruff lint and format: passed
• git diff --check: passed
• local Docker Oracle unavailable; GitHub Oracle is required before health is confirmed

Provenance

• lm-provers/FineProofs-SFT
• revision 73661e62811cf2940a0d3f82788a4f4332204c2f
• default train row 4
• Apache-2.0

Portfolio contribution

This adds a multi-stage structural reduction from multiplicative parity classes to a combinatorial transversal through a representation obstruction. It differs from bounded modular searches and standalone counterexample certificates because no concrete source set is available or sufficient.

[yuelgrace1810-ops]

Closing this draft because the refreshed active-PR audit found it is an exact duplicate of #313: the same FineProofs revision, train row 4, row digest, theorem, squarefree-kernel reduction, three-square obstruction, and transversal conclusion. #313 is the canonical benchmark and has the more open verifier contract (agent-selected modulus). No code from this PR should be merged.