A clean cumulative run compiled all 79 modules, matched all 1,000 axiom reports, verified all nine dependency revisions, and correctly rejected all 37 invalid-proof controls. The statement-contract file separately checked the external parameter disjunction, integrality, positive threshold, and exact degree displacement. Warnings were treated as errors.
The capstone depends only on propext, Classical.choice, and Quot.sound. The 25 extension-infrastructure tests passed. Exact-rational checks passed 6,500 higher-difference cases in each dyadic normalization, 588 dyadic periods and 1,690 divisor-branch periods. These finite checks are not the universal proof. A fresh-extraction replay, when recorded in the separate release audit, is additional evidence beyond the source build.