Reuse verified Lean proofs across release platforms

[Polarnova]

Summary

• elaborate and audit the complete proof library once on Ubuntu
• reject native files from the proof seed archive
• rehash and validate the full 8,852-job DAG without rebuilding on native Linux and macOS runners
• run the axiom audit on both platforms before creating their Lake archives
• retain post-publication consumer verification on both platforms

Evidence

The previous macOS release job timed out after 120 minutes at 8,840/8,852 jobs, before the 2,302-second Linux CandidateCertificates tail. The verified Linux Lake archive contains no native artifacts. Unpacking it into an isolated macOS arm64 release-builder workspace and running lake --rehash --no-build reports all 8,852 jobs up to date; the macOS axiom audit then passes all 2,452 declarations.

Static checks: actionlint, shellcheck, bash syntax, forbidden-token scan, Blueprint statement style, and diff whitespace.