Komorebi Space · Lean source

KomorebiSpaceRegularization.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 (3)

KomorebiSpaceRegularization.lean3 lines

Original source path

lean/KomorebiSpaceRegularization.lean

1 import KomorebiSpace.RegularizedHilbertRepair
2 import KomorebiSpace.RegularizationCertificates
3 import KomorebiSpace.ProtectedRegularizedRepair

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: e2395cfc307fe3a5a6d1ea35173de605689f8f04befa9b2ac02bdb83fe9d28f7