Speed up PrintAxioms audit

[Th0rgal]

Summary

• Replace generated #print axioms commands with a repo-local memoized Lean axiom audit command.
• Keep PrintAxioms.lean generated and reproducible via scripts/generate_print_axioms.py.
• Add Lean.ofReduceBool to the builtin Lean axiom allowlist; existing docs already treat it as a foundational Lean axiom.
• Preserve the existing check_axioms.py --report input format while emitting one normalized line per theorem.

Benchmarks

Measured with warmed Lake artifacts.

Host	Command	Before	After	Speedup
DGX Spark ARM64	lake env lean PrintAxioms.lean	1:20.33	0:02.67	30.1x
DGX Spark ARM64	lake build PrintAxioms	1:20.92	0:03.07	26.4x
Local x64 checkout	lake env lean PrintAxioms.lean	3:03.71	0:05.02	36.6x
Local x64 checkout	lake build PrintAxioms	not separately captured before	0:05.36	n/a

The new audit also reports all 2,782 generated public theorem checks as one-line records. The old parser only captured 1,197 old #print records in my local comparison because Lean wrapped many axiom lists across lines.

Validation

• lake build PrintAxioms
• lake env lean PrintAxioms.lean + python3 scripts/check_axioms.py --report
• python3 scripts/generate_print_axioms.py --check
• python3 -m unittest scripts.test_check_axioms scripts.test_profile_ci_resources scripts.test_check_verify_sync
• python3 -m unittest discover scripts
• make check

---

Note

Low Risk
Low risk: changes are confined to the Lean axiom-audit generator and its Python parsing/allowlist, primarily affecting CI verification output and performance rather than runtime behavior.

Overview
Speeds up the axiom-dependency audit by replacing generated per-theorem #print axioms commands with a repo-local, memoized Lean command (#verity_print_axioms) that caches axiom results across dependencies.

Keeps PrintAxioms.lean reproducible via scripts/generate_print_axioms.py, and updates scripts/check_axioms.py --report to parse the new one-theorem-per-line output while expanding the builtin allowlist to include Lean.ofReduceBool.

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

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit deb7011. Configure here.}