Komorebi Sufficient Resolution v0.16.0
Cumulative Lean 4/Mathlib formalization of exact/approximate sufficient representation, hidden-return dynamics, globalization obstruction, reconstruction and regularization, discrepancy certification, uncertain forward operators, source-bound-free discrepancy, and calibration-generated operator-error certification.
Current inventory: 998 theorem/lemma declarations, 93 production proof modules,
1159 enumerated named declarations. Counts include helpers/examples and are not novelty
counts. See PROGRESS.md, BLOCK_16_THEOREMS.md, and VERIFICATION_SUMMARY.md.
Final-edition replay and provenance
All 93 production Lean files are unchanged from the frozen checkpoint. The generic
verification driver and top-level metadata are amended for this paper edition.
Read PORTABLE_REPLAY.md and the current VERIFICATION_SUMMARY.md. Original
metadata and the original generic driver are preserved in inherited_provenance.
Current bounded finite evidence is in the release-level verification directory.
No fresh Lean build is claimed because the separately required runtime could not
be recovered in this session.