README.md
Komorebi Space
README.md
1 # Komorebi Space
2
3 A Lean library for coherent realizations, constrained correction, obstruction, descent, and quantitative repair.
4
5 The formal development builds coherent objects from compatible observations and studies which defects can be removed while preserving designated information. It includes categorical descent, normed repair, Hilbert minimum corrections, attained budget profiles, sharp dual certificates, regularization limits, and coordinate invariant stopping certificates.
6
7 The accompanying monograph develops the mathematics. The Lean guide explains the formal interfaces and maps mathematical statements to exact declarations.
8
9 ## Use the library
10
11 From this directory, with the pinned Lean toolchain and dependencies available:
12
13 ```sh
14 lake build
15 ```
16
17 The configured default targets are `KomorebiSpaceCombined` and `KomorebiSpaceDiagonal`. A Lean file can import the complete development with
18
19 ```lean
20 import KomorebiSpaceCombined
21 import KomorebiSpaceDiagonal
22 ```
23
24 For smaller applications, import a specific module such as `KomorebiSpace.Correction`, `KomorebiSpace.BudgetDuality`, or `KomorebiSpace.CoordinateCovector`.
25
26 See `USAGE.md` for the environment, import entrypoints, inspection commands, and the distinction between a normal build and the full verification audit.
27
28 ## Formal coverage
29
30 The unchanged accepted formal development contains 162 production modules and four import entrypoints. It has 1,859 explicit theorem or lemma declarations and 5,339 exported project declarations. The exported-declaration inventory additionally counts definitions and generated helpers.
31
32 All sixteen principal analytic theorem groups have formal counterparts. Chapter 30's actual infinite diagonal model, certified tails, sharp all-budget asymptotic, and rounded noisy rate are available through `KomorebiSpaceDiagonal`. That entrypoint also imports the explicit inexact-solver rate in `DiagonalInexactRate` and the concrete nonclosed-range and closure/nonattainment results in `DiagonalRangeObstruction`. Both modules contribute declarations to `KomorebiSpace.DiagonalRegularization`. The selected theorem map is in `../verification/LEAN_THEOREM_MAP.json`. Exact hypotheses are given by the declaration types.
33
34 The accepted integrated replay freshly compiled all 166 project targets, exported all 5,339 project declarations by module provenance, and checked their recursive axiom dependencies. All 56 controls had the specified outcomes: 18 acceptances, 35 elaboration rejections, and three axiom-policy rejections. The historical cumulative audit's 44 controls and the accepted diagonal completion's eight controls were rerun together with four added controls for the two concrete connections. See [the runner guide](../verification/runner/README.md) for the acceptance conditions and evidence files.
35
36 For an executable rational example linked to the general theorem statements, read [WORKED_EXAMPLE.md](../examples/WORKED_EXAMPLE.md). The example's Python verifier is not a certified extraction from Lean.
37
38 ## Reproducibility
39
40 The required Lean version is `4.34.0-rc2`. The required mathlib revision is `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`. Preserve the toolchain file and dependency manifest together.
41
42 The source package does not bundle the multi-gigabyte compiler and dependency cache. A matching local environment may be reused. For the complete current replay, run the command in [USAGE.md](USAGE.md). The accepted earlier diagonal evidence is preserved intact in `../verification/DIAGONAL_ACCEPTED_EVIDENCE.zip`. Its `REPRODUCIBILITY.md` documents that historical audit and the compatibility detail used on its verification host. The separate Technical Record preserves the parent and continuation histories.
43
44 The publication's citation is in [CITATION.bib](../CITATION.bib). Original software uses MIT and original writing uses CC BY 4.0, with third-party terms preserved. See [REUSE.md](../REUSE.md) and [LICENSE.md](../LICENSE.md) for the current grant and exact scope.