Komorebi Space · Lean source
KomorebiSpaceDiagonal.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (4)
KomorebiSpaceDiagonal.lean7 lines
Original source path
lean/KomorebiSpaceDiagonal.lean1 import KomorebiSpace.DiagonalTheorems
2 import KomorebiSpace.DiagonalAsymptotic
3 import KomorebiSpace.DiagonalInexactRate
4 import KomorebiSpace.DiagonalRangeObstruction
5
6 /-! The infinite diagonal regularization model, certified tails, sharp budget
7 asymptotic, rounded noisy and inexact rates, and the concrete range obstruction. -/
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 258b19da6e9d8aa29728d37cb254fb1782c7f99ad77dff4c1e285d7c9f8d5d79