Komorebi Space · Lean source

KomorebiSpaceCombined.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 (14)

KomorebiSpaceCombined.lean15 lines

Original source path

lean/KomorebiSpaceCombined.lean

1 -- Combined entrypoint; inherited module bytes are unchanged.
2 import KomorebiSpace
3 import KomorebiSpaceRegularization
4 import KomorebiSpace.BoundedApproximateRealization
5 import KomorebiSpace.NestedMinimumCorrections
6 import KomorebiSpace.ProtectedBoundedRealization
7 import KomorebiSpace.BudgetDuality
8 import KomorebiSpace.BudgetProfile
9 import KomorebiSpace.BudgetProfileGeometry
10 import KomorebiSpace.BudgetRobustness
11 import KomorebiSpace.RegularizationLimits
12 import KomorebiSpace.RegularizationNoiseLimits
13 import KomorebiSpace.RegularizationStrongLimit
14 import KomorebiSpace.CoordinateBasisChange
15 import KomorebiSpace.CoordinateCovector

Back to source controls

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

Original source on GitHub

Back to Komorebi Space