Implement unknown outcome gate and diagnostics protections

[neysofu]

Summary

• add baseline-vs-candidate outcome gate tooling, diagnostic metadata, and strict transition enforcement so only unknown obligations can change outcome
• extend verification runner/bench-prove tooling for large-obligation retry gating, add JSON artifacts, and refresh lerched expectations
• document the new policies in AGENTS refs and keep solver/encoder semantics unchanged while refactoring bounded helpers with equivalence safeguards

Testing

• Not run (not requested)