Remove UnlinkPool Lean axioms from specs

[Th0rgal]

Summary

• remove the unused Poseidon field-bound Lean axioms from the pool specs
• reword pool review and source metadata around opaque/linkage boundaries instead of axioms
• refresh proof comments now that the ZK entry points are translated

Verification

• rg -n '^\s*axiom\b|\bsorry\b|\badmit\b' Benchmark/Cases/UnlinkXyz/Pool cases/unlink_xyz/pool -S
• git diff --check
• lake build Benchmark.Cases.UnlinkXyz.Pool.Compile
• python3 scripts/check_reference_solutions.py

---

Note

Low Risk
Mostly comment/documentation and spec-boundary declaration tweaks; functional behavior is unchanged, with only a small risk that future proofs relied on the removed field-bound axioms.

Overview
Updates Benchmark/Cases/UnlinkXyz/Pool/Specs.lean to treat Poseidon boundaries as purely opaque (dropping the unused in-field axiom constraints) and adjusts surrounding wording to emphasize opaque/linked trust boundaries rather than Lean axioms.

Refreshes related documentation/metadata (case.yaml, spec-review.md, source-metadata.md, Proofs.lean, and a comment in InternalLazyIMT.lean) to match the current translated entrypoints and the updated boundary framing.

^{Reviewed by Cursor Bugbot for commit ce8f854. Bugbot is set up for automated code reviews on this repo. Configure here.}