Komorebi Space · Lean sources

Komorebi Space

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.

Edit and run in your browser

Source files 166

Source locations and editions

Files are shown relative to lean/.

Historical editions keep their original paths. Package caches and build files are omitted.

166 files

KomorebiSpace.lean
139 lines · 0 declaration locations
AdditiveCocycleBridge.leanKomorebiSpace/
92 lines · 6 declaration locations
AdjacentResolution.leanKomorebiSpace/
88 lines · 10 declaration locations
AmplifiedExamples.leanKomorebiSpace/
172 lines · 23 declaration locations
AmplifiedHolonomy.leanKomorebiSpace/
215 lines · 33 declaration locations
AmplifiedRepair.leanKomorebiSpace/
249 lines · 31 declaration locations
AmplifiedTransport.leanKomorebiSpace/
251 lines · 35 declaration locations
AmplifiedViews.leanKomorebiSpace/
114 lines · 12 declaration locations
BanachBlocks.leanKomorebiSpace/
197 lines · 22 declaration locations
BanachReindexing.leanKomorebiSpace/
122 lines · 15 declaration locations
BanachTowerExactification.leanKomorebiSpace/
140 lines · 9 declaration locations
BanachTowers.leanKomorebiSpace/
181 lines · 26 declaration locations
BanachViewBridge.leanKomorebiSpace/
63 lines · 9 declaration locations
BoundedApproximateRealization.leanKomorebiSpace/
105 lines · 5 declaration locations
BoundedParity.leanKomorebiSpace/
148 lines · 25 declaration locations
BudgetDuality.leanKomorebiSpace/
139 lines · 8 declaration locations
BudgetProfile.leanKomorebiSpace/
197 lines · 21 declaration locations
BudgetProfileGeometry.leanKomorebiSpace/
113 lines · 6 declaration locations
BudgetRobustness.leanKomorebiSpace/
113 lines · 8 declaration locations
CascadeBoundaryExamples.leanKomorebiSpace/
86 lines · 11 declaration locations
CascadeDensity.leanKomorebiSpace/
110 lines · 11 declaration locations
CascadeLimits.leanKomorebiSpace/
207 lines · 22 declaration locations
CascadeProjections.leanKomorebiSpace/
173 lines · 25 declaration locations
CayleyHolonomyConditioning.leanKomorebiSpace/
132 lines · 17 declaration locations
CoarseningCascade.leanKomorebiSpace/
107 lines · 16 declaration locations
CocycleDescent.leanKomorebiSpace/
166 lines · 14 declaration locations
CocycleExamples.leanKomorebiSpace/
222 lines · 30 declaration locations
CocycleGaugeGroupoid.leanKomorebiSpace/
181 lines · 25 declaration locations
Cofinal.leanKomorebiSpace/
113 lines · 14 declaration locations
CofinalTransports.leanKomorebiSpace/
177 lines · 19 declaration locations
Cohomology.leanKomorebiSpace/
99 lines · 12 declaration locations
CompositionSite.leanKomorebiSpace/
171 lines · 23 declaration locations
CompositionSiteExamples.leanKomorebiSpace/
71 lines · 7 declaration locations
CompositionStack.leanKomorebiSpace/
191 lines · 14 declaration locations
ConstantTower.leanKomorebiSpace/
95 lines · 8 declaration locations
CoordinateBasisChange.leanKomorebiSpace/
174 lines · 17 declaration locations
CoordinateCovector.leanKomorebiSpace/
367 lines · 34 declaration locations
Correction.leanKomorebiSpace/
90 lines · 11 declaration locations
DescentClosedRange.leanKomorebiSpace/
107 lines · 10 declaration locations
DescentComparison.leanKomorebiSpace/
124 lines · 15 declaration locations
DescentDataGroupoid.leanKomorebiSpace/
140 lines · 13 declaration locations
DescentEquivalence.leanKomorebiSpace/
116 lines · 12 declaration locations
DiagonalAsymptotic.leanKomorebiSpace/
348 lines · 47 declaration locations
DiagonalDefinitions.leanKomorebiSpace/
22 lines · 10 declaration locations
DiagonalInexactRate.leanKomorebiSpace/
53 lines · 1 declaration location
DiagonalNoisyRate.leanKomorebiSpace/
166 lines · 14 declaration locations
DiagonalRangeObstruction.leanKomorebiSpace/
102 lines · 13 declaration locations
DiagonalSeriesBounds.leanKomorebiSpace/
385 lines · 46 declaration locations
DiagonalTheorems.leanKomorebiSpace/
35 lines · 2 declaration locations
DyadicDetailExamples.leanKomorebiSpace/
93 lines · 17 declaration locations
DyadicInfiniteReconstruction.leanKomorebiSpace/
218 lines · 19 declaration locations
DyadicResidualDetails.leanKomorebiSpace/
269 lines · 28 declaration locations
DyadicResidualHierarchy.leanKomorebiSpace/
85 lines · 7 declaration locations
DyadicResidualSplit.leanKomorebiSpace/
214 lines · 31 declaration locations
DyadicSupport.leanKomorebiSpace/
93 lines · 5 declaration locations
EffectiveCocycleDescent.leanKomorebiSpace/
146 lines · 15 declaration locations
EffectiveDescentExamples.leanKomorebiSpace/
130 lines · 21 declaration locations
EuclideanCertificateCoordinates.leanKomorebiSpace/
44 lines · 6 declaration locations
EventualCategory.leanKomorebiSpace/
104 lines · 18 declaration locations
Exactification.leanKomorebiSpace/
175 lines · 11 declaration locations
ExtensionChoiceExample.leanKomorebiSpace/
193 lines · 26 declaration locations
ExtensionFibers.leanKomorebiSpace/
133 lines · 17 declaration locations
FiniteObservation.leanKomorebiSpace/
116 lines · 14 declaration locations
FinitePrefixBoundary.leanKomorebiSpace/
49 lines · 7 declaration locations
FiniteRealizationExistence.leanKomorebiSpace/
99 lines · 13 declaration locations
FramingBoundaryExamples.leanKomorebiSpace/
123 lines · 10 declaration locations
GaugeDescent.leanKomorebiSpace/
158 lines · 15 declaration locations
GroupViewSystems.leanKomorebiSpace/
174 lines · 17 declaration locations
GrowingTower.leanKomorebiSpace/
223 lines · 38 declaration locations
HilbertHolonomyRepair.leanKomorebiSpace/
251 lines · 31 declaration locations
HilbertKernelProjection.leanKomorebiSpace/
251 lines · 32 declaration locations
HolonomyConditioningExample.leanKomorebiSpace/
127 lines · 11 declaration locations
HolonomyCoordinates.leanKomorebiSpace/
203 lines · 27 declaration locations
HolonomyExamples.leanKomorebiSpace/
220 lines · 28 declaration locations
HolonomyGapCertificate.leanKomorebiSpace/
101 lines · 7 declaration locations
HolonomyProjection.leanKomorebiSpace/
182 lines · 30 declaration locations
HolonomyRepair.leanKomorebiSpace/
152 lines · 12 declaration locations
HolonomyTransport.leanKomorebiSpace/
168 lines · 21 declaration locations
HolonomyViews.leanKomorebiSpace/
99 lines · 11 declaration locations
IdentityTowerObstruction.leanKomorebiSpace/
85 lines · 9 declaration locations
InfiniteDiagonalModel.leanKomorebiSpace/
302 lines · 54 declaration locations
KernelProjectionBounds.leanKomorebiSpace/
180 lines · 26 declaration locations
LinearExactification.leanKomorebiSpace/
77 lines · 5 declaration locations
MarkedBoundaryChange.leanKomorebiSpace/
76 lines · 9 declaration locations
MarkedRealization.leanKomorebiSpace/
91 lines · 11 declaration locations
MarkedTransport.leanKomorebiSpace/
135 lines · 13 declaration locations
MonotoneBudgetAsymptotic.leanKomorebiSpace/
100 lines · 7 declaration locations
MovingDescent.leanKomorebiSpace/
77 lines · 4 declaration locations
MovingKernelBounds.leanKomorebiSpace/
179 lines · 10 declaration locations
MovingKernelExamples.leanKomorebiSpace/
238 lines · 34 declaration locations
NestedMinimumCorrections.leanKomorebiSpace/
241 lines · 19 declaration locations
NonabelianExtension.leanKomorebiSpace/
134 lines · 11 declaration locations
NonabelianExtensionFibers.leanKomorebiSpace/
131 lines · 8 declaration locations
NormedDefects.leanKomorebiSpace/
92 lines · 8 declaration locations
ObstructionFloor.leanKomorebiSpace/
49 lines · 6 declaration locations
ObstructionRestriction.leanKomorebiSpace/
86 lines · 9 declaration locations
OverlapExamples.leanKomorebiSpace/
193 lines · 26 declaration locations
OverlapPathRepair.leanKomorebiSpace/
169 lines · 30 declaration locations
OverlapResidualImage.leanKomorebiSpace/
115 lines · 15 declaration locations
OverlapTransport.leanKomorebiSpace/
124 lines · 30 declaration locations
OverlapViewBridge.leanKomorebiSpace/
181 lines · 21 declaration locations
PatchViewEquivalence.leanKomorebiSpace/
97 lines · 10 declaration locations
PatchViewSystem.leanKomorebiSpace/
100 lines · 12 declaration locations
Profiles.leanKomorebiSpace/
71 lines · 8 declaration locations
ProjectiveExample.leanKomorebiSpace/
44 lines · 9 declaration locations
ProtectedBoundedRealization.leanKomorebiSpace/
43 lines · 1 declaration location
ProtectedHilbertRepair.leanKomorebiSpace/
218 lines · 28 declaration locations
ProtectedLinearCertificates.leanKomorebiSpace/
214 lines · 20 declaration locations
ProtectedRegularizedRepair.leanKomorebiSpace/
86 lines · 12 declaration locations
QuantitativeDescent.leanKomorebiSpace/
184 lines · 24 declaration locations
Realization.leanKomorebiSpace/
113 lines · 20 declaration locations
RealizationFaithfulness.leanKomorebiSpace/
121 lines · 13 declaration locations
RegularizationCertificates.leanKomorebiSpace/
120 lines · 12 declaration locations
RegularizationLimits.leanKomorebiSpace/
121 lines · 10 declaration locations
RegularizationNoiseLimits.leanKomorebiSpace/
208 lines · 16 declaration locations
RegularizationStrongLimit.leanKomorebiSpace/
132 lines · 7 declaration locations
RegularizedHilbertRepair.leanKomorebiSpace/
254 lines · 37 declaration locations
ReindexedTransports.leanKomorebiSpace/
151 lines · 20 declaration locations
ReindexingExamples.leanKomorebiSpace/
118 lines · 18 declaration locations
RelativeAmbiguity.leanKomorebiSpace/
93 lines · 6 declaration locations
RelativeCocycleRealization.leanKomorebiSpace/
97 lines · 9 declaration locations
RelativeSections.leanKomorebiSpace/
123 lines · 11 declaration locations
RepairDynamics.leanKomorebiSpace/
123 lines · 14 declaration locations
RepairExamples.leanKomorebiSpace/
64 lines · 5 declaration locations
RepairProjection.leanKomorebiSpace/
164 lines · 23 declaration locations
ResidualAliasing.leanKomorebiSpace/
210 lines · 32 declaration locations
ResidualNaturality.leanKomorebiSpace/
155 lines · 22 declaration locations
ResidualPerturbation.leanKomorebiSpace/
150 lines · 11 declaration locations
ResidualProfiles.leanKomorebiSpace/
73 lines · 3 declaration locations
ResidualSampling.leanKomorebiSpace/
153 lines · 19 declaration locations
ResolutionViews.leanKomorebiSpace/
77 lines · 11 declaration locations
SamplingRepair.leanKomorebiSpace/
95 lines · 9 declaration locations
ScheduleNormObstruction.leanKomorebiSpace/
99 lines · 15 declaration locations
SectionExactSequence.leanKomorebiSpace/
157 lines · 19 declaration locations
SectionExtensionExample.leanKomorebiSpace/
90 lines · 11 declaration locations
SectionExtensionFibers.leanKomorebiSpace/
108 lines · 10 declaration locations
SectionExtensionStages.leanKomorebiSpace/
66 lines · 7 declaration locations
SectionGluing.leanKomorebiSpace/
120 lines · 15 declaration locations
SectionObstruction.leanKomorebiSpace/
150 lines · 17 declaration locations
SectionViewEquivalence.leanKomorebiSpace/
101 lines · 12 declaration locations
SequenceCascade.leanKomorebiSpace/
278 lines · 32 declaration locations
SiteDescent.leanKomorebiSpace/
110 lines · 8 declaration locations
SplitDefectCharts.leanKomorebiSpace/
256 lines · 36 declaration locations
SplitKernelPerturbation.leanKomorebiSpace/
247 lines · 31 declaration locations
SplitTowerCanonicity.leanKomorebiSpace/
137 lines · 18 declaration locations
SplitTowerCoordinates.leanKomorebiSpace/
128 lines · 12 declaration locations
SplitTowerPerturbation.leanKomorebiSpace/
134 lines · 9 declaration locations
SplitTowerRepair.leanKomorebiSpace/
224 lines · 32 declaration locations
SplitTowerSemantics.leanKomorebiSpace/
219 lines · 23 declaration locations
SplittingDependence.leanKomorebiSpace/
140 lines · 20 declaration locations
Squares.leanKomorebiSpace/
52 lines · 6 declaration locations
StandardDescentBridge.leanKomorebiSpace/
140 lines · 9 declaration locations
SurjectiveKernelMotion.leanKomorebiSpace/
85 lines · 10 declaration locations
TowerCorrection.leanKomorebiSpace/
81 lines · 9 declaration locations
Towers.leanKomorebiSpace/
120 lines · 22 declaration locations
ViewBoundaryExamples.leanKomorebiSpace/
122 lines · 16 declaration locations
ViewCorrespondence.leanKomorebiSpace/
117 lines · 10 declaration locations
ViewDuplication.leanKomorebiSpace/
142 lines · 19 declaration locations
ViewEquivalence.leanKomorebiSpace/
182 lines · 17 declaration locations
ViewPullback.leanKomorebiSpace/
85 lines · 8 declaration locations
ViewSections.leanKomorebiSpace/
176 lines · 30 declaration locations
ViewSiteTransport.leanKomorebiSpace/
100 lines · 9 declaration locations
WeightedGeometry.leanKomorebiSpace/
84 lines · 12 declaration locations
KomorebiSpaceCombined.lean
15 lines · 0 declaration locations
KomorebiSpaceDiagonal.lean
7 lines · 0 declaration locations
KomorebiSpaceRegularization.lean
3 lines · 0 declaration locations