Reproduce and inspect the authoritative files
On this page · Permalink · Source line 354
COMMANDS AND SOURCE IDENTITY From source/komorebi-circuit-obstructions-v1.2.0, run
python scripts/check_integrity.py
python scripts/verify.py --all
python scripts/verify_lean.py --toolchain /path/to/toolchainThe integrity check needs Python; the full scientific replay also needs a C++17 compiler. The last command needs the pinned Lean toolchain supplied separately. The verification scripts do not download it. A missing toolchain fails before proof checking. The current completion pass restored the pinned runtime and successfully executed this verification.
From the publication-set root, regenerate the exact declaration appendix and the explanatory guide source with
python scripts/build_lean_register.py
python scripts/build_lean_guide.py
python scripts/build_documents.py
python scripts/verify_publication.pyThe register generator verifies all 115 source hashes and declaration lines against the archived catalog, then copies each complete elaborated type. The guide generator preserves the archived explanatory proof route and adds this edition's evidence distinctions. Neither script compiles Lean.
The unmodified source ZIP's SHA-256 is
88628c8274660bd20e11fec83249fdc04960403b9d64d1e5068a476b8c025936The complete publication package preserves that ZIP, the repository bundle, original companions and current evidence. Its new manifest binds the revised papers, generators and figure assets. Hash consistency is not an authorship certificate or mathematical proof.
The declaration register follows. It includes the 40 inherited results and 75 Block 02 additions. The ten non-ASCII logical glyphs in its exact type text are rendered as mathematical glyphs for readability. The unchanged UTF-8 sidecar is manuscripts/lean_statements_utf8.txt; the original authoritative catalog is reference/lean-block02/declaration_catalog.json in the source release. Imported library declarations and explanatory prose are not counted as new project theorems.