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