Summary:
- strict verifier boundary
- Lean verifier fixtures
- verified corpus and Lean project micro-ingestion
- Mathlib-style micro-subset
- real local Mathlib allowlist membrane
- declaration discovery and manifest builder
- proof-library demo pack
- public demo and release check
- curated real local Mathlib demo command and report workflow
- module-aware imported-declaration verification via explicit module
#check - robust minimal module-check requests plus qualification diagnostics/fallback
- real project execution mode selection, including
lake env leanfrom the supplied Mathlib/Lake project root - persistent Mathlib digest Lawbook with focused Nat pack, constructor and reason atlas exports, obstruction traces, and dry-run-safe accumulation
- no proof from advisory artifacts