8.1. Checked proof snapshot🔗

The completed proof is at immutable revision ff645fa. At that revision the library build passes 3757 jobs. The standard-axiom audit passes for 282 project declarations, including private helpers.

Theorem status: proved. The exact unconditional infinitude statement is present.

Full Comparator: passed locally. The unchanged frozen challenge and the solution were accepted. The check includes statement comparison, permitted axioms, and Lean kernel replay. The macOS run has no process sandbox.

Hosted full gate: passed at the completed proof revision. See the full theorem run. The workflow passed the library audit and full Comparator check in the Linux sandbox. It accepted the exact frozen statement and replayed the proof in Lean's kernel.