Large Signal Model · Lean sources

Large Signal Model

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.

This inspector shows the 254 mathematical modules and their root import file. The full retained project, including rejection controls and test sources, remains available in the source downloads and through the work overview.

Source files 255

Source locations and editions

Files are shown relative to Lean/.

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

255 files

KomorebiLSM.lean
254 lines · 0 declaration locations
AffineObservationTransport.leanKomorebiLSM/
113 lines · 16 declaration locations
AtlasReconciliation.leanKomorebiLSM/
188 lines · 23 declaration locations
AveragedCongruence.leanKomorebiLSM/
348 lines · 24 declaration locations
BaseNorm.leanKomorebiLSM/
183 lines · 26 declaration locations
BaseNormIntegration.leanKomorebiLSM/
74 lines · 5 declaration locations
BaseNormModels.leanKomorebiLSM/
137 lines · 11 declaration locations
BaseNormTopology.leanKomorebiLSM/
117 lines · 11 declaration locations
BasisCoordinates.leanKomorebiLSM/
97 lines · 11 declaration locations
BasisDecoder.leanKomorebiLSM/
84 lines · 7 declaration locations
BayesianClosure.leanKomorebiLSM/
83 lines · 7 declaration locations
BayesianDefect.leanKomorebiLSM/
108 lines · 11 declaration locations
BehaviorMinimality.leanKomorebiLSM/
114 lines · 11 declaration locations
BehaviorProbability.leanKomorebiLSM/
86 lines · 10 declaration locations
BehaviorSpace.leanKomorebiLSM/
225 lines · 38 declaration locations
BernoulliRecordSeparation.leanKomorebiLSM/
318 lines · 38 declaration locations
BernsteinCellPositivity.leanKomorebiLSM/
155 lines · 11 declaration locations
BernsteinCoefficientError.leanKomorebiLSM/
227 lines · 16 declaration locations
BernsteinGridSearch.leanKomorebiLSM/
157 lines · 22 declaration locations
BernsteinKernel.leanKomorebiLSM/
365 lines · 45 declaration locations
BernsteinRationalBasis.leanKomorebiLSM/
149 lines · 17 declaration locations
Block10Examples.leanKomorebiLSM/
64 lines · 12 declaration locations
Block11Examples.leanKomorebiLSM/
43 lines · 8 declaration locations
Block12Examples.leanKomorebiLSM/
31 lines · 4 declaration locations
Block13Examples.leanKomorebiLSM/
65 lines · 5 declaration locations
Block14Examples.leanKomorebiLSM/
57 lines · 7 declaration locations
Block2Examples.leanKomorebiLSM/
171 lines · 31 declaration locations
Block3Examples.leanKomorebiLSM/
258 lines · 53 declaration locations
Block4Examples.leanKomorebiLSM/
374 lines · 62 declaration locations
Block5Examples.leanKomorebiLSM/
338 lines · 57 declaration locations
Block6Examples.leanKomorebiLSM/
350 lines · 60 declaration locations
Block7BoundaryExamples.leanKomorebiLSM/
137 lines · 24 declaration locations
Block7Examples.leanKomorebiLSM/
151 lines · 21 declaration locations
Block8ApproximationExamples.leanKomorebiLSM/
190 lines · 38 declaration locations
Block8Examples.leanKomorebiLSM/
160 lines · 26 declaration locations
Block9Examples.leanKomorebiLSM/
65 lines · 12 declaration locations
BoundedResponseNoise.leanKomorebiLSM/
133 lines · 7 declaration locations
CanonicalCone.leanKomorebiLSM/
136 lines · 21 declaration locations
CellDistance.leanKomorebiLSM/
110 lines · 7 declaration locations
CertificateLearning.leanKomorebiLSM/
489 lines · 34 declaration locations
CertifiedCorrection.leanKomorebiLSM/
67 lines · 6 declaration locations
CertifiedRepairUpper.leanKomorebiLSM/
40 lines · 2 declaration locations
CertifiedTemplate.leanKomorebiLSM/
504 lines · 44 declaration locations
CoefficientBox3.leanKomorebiLSM/
203 lines · 20 declaration locations
ComplexCoefficientBox.leanKomorebiLSM/
108 lines · 13 declaration locations
ConditionalBernoulli.leanKomorebiLSM/
53 lines · 2 declaration locations
ConditionalEventTV.leanKomorebiLSM/
102 lines · 5 declaration locations
ConditionalHoeffding.leanKomorebiLSM/
79 lines · 2 declaration locations
ConditionalRandomMultiplier.leanKomorebiLSM/
258 lines · 16 declaration locations
ConditionalStochasticCompletion.leanKomorebiLSM/
566 lines · 41 declaration locations
Conditioning.leanKomorebiLSM/
73 lines · 5 declaration locations
ContinuousBinnedRecords.leanKomorebiLSM/
453 lines · 46 declaration locations
ContinuousBins.leanKomorebiLSM/
204 lines · 17 declaration locations
ContinuousInstrument.leanKomorebiLSM/
195 lines · 26 declaration locations
ContinuousPopulationBridge.leanKomorebiLSM/
145 lines · 16 declaration locations
ContinuousRealizationP61.leanKomorebiLSM/
366 lines · 19 declaration locations
ContinuousRecordReference.leanKomorebiLSM/
146 lines · 12 declaration locations
ContinuousRecords.leanKomorebiLSM/
536 lines · 59 declaration locations
ContinuousReferenceChange.leanKomorebiLSM/
151 lines · 16 declaration locations
ContinuousTV.leanKomorebiLSM/
305 lines · 16 declaration locations
ContinuousTVDensity.leanKomorebiLSM/
88 lines · 5 declaration locations
ConvexMargin.leanKomorebiLSM/
188 lines · 17 declaration locations
ConvexRepairBracketing.leanKomorebiLSM/
157 lines · 17 declaration locations
CoreStability.leanKomorebiLSM/
92 lines · 10 declaration locations
CountableConfidence.leanKomorebiLSM/
57 lines · 4 declaration locations
CoveredActionBoundaries.leanKomorebiLSM/
79 lines · 16 declaration locations
CoveredAdaptiveActions.leanKomorebiLSM/
209 lines · 16 declaration locations
CoveredAdaptiveEvidence.leanKomorebiLSM/
153 lines · 8 declaration locations
CurvedMomentGeometry.leanKomorebiLSM/
162 lines · 21 declaration locations
CurvedMomentInstrument.leanKomorebiLSM/
148 lines · 16 declaration locations
CurvedMomentMarkov.leanKomorebiLSM/
165 lines · 17 declaration locations
CurvedMomentPolynomial.leanKomorebiLSM/
68 lines · 6 declaration locations
CurvedMomentRecordTV.leanKomorebiLSM/
217 lines · 18 declaration locations
CurvedMomentReferences.leanKomorebiLSM/
159 lines · 16 declaration locations
CurvedMomentTV.leanKomorebiLSM/
112 lines · 9 declaration locations
DataSelectedGeometry.leanKomorebiLSM/
154 lines · 18 declaration locations
DataSpan.leanKomorebiLSM/
82 lines · 7 declaration locations
DecoderMatrixFormula.leanKomorebiLSM/
46 lines · 5 declaration locations
DefectPropagation.leanKomorebiLSM/
111 lines · 9 declaration locations
DelayClosure.leanKomorebiLSM/
209 lines · 17 declaration locations
DyadicBernsteinCertificate.leanKomorebiLSM/
154 lines · 13 declaration locations
EllipsoidDiscovery.leanKomorebiLSM/
363 lines · 44 declaration locations
EllipsoidDiscoveryP63.leanKomorebiLSM/
153 lines · 7 declaration locations
EllipsoidDualCS.leanKomorebiLSM/
55 lines · 2 declaration locations
EllipsoidGeometry.leanKomorebiLSM/
218 lines · 25 declaration locations
EllipsoidPolynomial.leanKomorebiLSM/
273 lines · 31 declaration locations
EuclideanMatrixNorms.leanKomorebiLSM/
145 lines · 20 declaration locations
Examples.leanKomorebiLSM/
90 lines · 19 declaration locations
FacetRobustness.leanKomorebiLSM/
52 lines · 4 declaration locations
FilteringStability.leanKomorebiLSM/
142 lines · 11 declaration locations
FiniteBayes.leanKomorebiLSM/
225 lines · 32 declaration locations
FiniteInstrument.leanKomorebiLSM/
203 lines · 34 declaration locations
FiniteMomentIdentification.leanKomorebiLSM/
376 lines · 34 declaration locations
FinitePartitions.leanKomorebiLSM/
94 lines · 15 declaration locations
FinitePrefix.leanKomorebiLSM/
73 lines · 7 declaration locations
FiniteStochastic.leanKomorebiLSM/
199 lines · 22 declaration locations
FiniteTV.leanKomorebiLSM/
163 lines · 33 declaration locations
FiniteTableP32.leanKomorebiLSM/
36 lines · 1 declaration location
FiniteTestRows.leanKomorebiLSM/
69 lines · 3 declaration locations
GrammarAccounting.leanKomorebiLSM/
305 lines · 32 declaration locations
IdentificationBound.leanKomorebiLSM/
133 lines · 10 declaration locations
InstrumentCompletion.leanKomorebiLSM/
121 lines · 16 declaration locations
InstrumentContraction.leanKomorebiLSM/
153 lines · 14 declaration locations
InstrumentCoordinates.leanKomorebiLSM/
142 lines · 6 declaration locations
InstrumentRealization.leanKomorebiLSM/
111 lines · 10 declaration locations
InteriorRepair.leanKomorebiLSM/
299 lines · 23 declaration locations
InvariantCompletion.leanKomorebiLSM/
142 lines · 19 declaration locations
JointRefinement.leanKomorebiLSM/
206 lines · 29 declaration locations
KernelTVMeasurable.leanKomorebiLSM/
90 lines · 14 declaration locations
LearnedRealization.leanKomorebiLSM/
138 lines · 10 declaration locations
LeftSingularModes.leanKomorebiLSM/
66 lines · 5 declaration locations
LegendreCounterexample.leanKomorebiLSM/
397 lines · 53 declaration locations
LinearClosure.leanKomorebiLSM/
69 lines · 9 declaration locations
LinearRefinement.leanKomorebiLSM/
60 lines · 3 declaration locations
LorentzBaseNorm.leanKomorebiLSM/
226 lines · 42 declaration locations
LorentzBoundaryFragility.leanKomorebiLSM/
141 lines · 14 declaration locations
LorentzCylinder.leanKomorebiLSM/
124 lines · 13 declaration locations
MarkovMarginals.leanKomorebiLSM/
94 lines · 8 declaration locations
MarkovMinorization.leanKomorebiLSM/
133 lines · 6 declaration locations
MarkovRecords.leanKomorebiLSM/
107 lines · 13 declaration locations
MarkovWindows.leanKomorebiLSM/
131 lines · 11 declaration locations
MatrixEmbedding.leanKomorebiLSM/
236 lines · 34 declaration locations
MatrixOrderUnit.leanKomorebiLSM/
51 lines · 1 declaration location
MatrixRotation.leanKomorebiLSM/
330 lines · 53 declaration locations
MeasureTVCalculus.leanKomorebiLSM/
115 lines · 6 declaration locations
Memory.leanKomorebiLSM/
109 lines · 5 declaration locations
MemoryApproximation.leanKomorebiLSM/
153 lines · 10 declaration locations
MemoryBounds.leanKomorebiLSM/
112 lines · 7 declaration locations
MemoryStability.leanKomorebiLSM/
109 lines · 8 declaration locations
MissingIntervention.leanKomorebiLSM/
108 lines · 14 declaration locations
NoisySpectralSubspace.leanKomorebiLSM/
63 lines · 6 declaration locations
NoisySubspaceResidual.leanKomorebiLSM/
68 lines · 4 declaration locations
NormalizedDefect.leanKomorebiLSM/
127 lines · 14 declaration locations
Normed.leanKomorebiLSM/
73 lines · 7 declaration locations
ObservableCore.leanKomorebiLSM/
179 lines · 23 declaration locations
ObservableMomentAlgebra.leanKomorebiLSM/
126 lines · 7 declaration locations
ObservableMomentBoundaries.leanKomorebiLSM/
104 lines · 23 declaration locations
ObservableMomentConditional.leanKomorebiLSM/
297 lines · 16 declaration locations
ObservableMomentConfidence.leanKomorebiLSM/
153 lines · 10 declaration locations
ObservableMomentProcess.leanKomorebiLSM/
188 lines · 20 declaration locations
ObservableOperatorSets.leanKomorebiLSM/
207 lines · 19 declaration locations
ObservableRealization.leanKomorebiLSM/
132 lines · 9 declaration locations
ObservationEquivalence.leanKomorebiLSM/
124 lines · 13 declaration locations
ObservationLawComparison.leanKomorebiLSM/
157 lines · 13 declaration locations
ObservationLawKernels.leanKomorebiLSM/
102 lines · 18 declaration locations
ObservationPolicyTransport.leanKomorebiLSM/
68 lines · 6 declaration locations
ObservationTree.leanKomorebiLSM/
160 lines · 18 declaration locations
OneSidedSubspace.leanKomorebiLSM/
174 lines · 8 declaration locations
OrientedEllipsoid.leanKomorebiLSM/
115 lines · 16 declaration locations
OutwardConfidenceIntervals.leanKomorebiLSM/
62 lines · 8 declaration locations
PacketApproximation.leanKomorebiLSM/
160 lines · 12 declaration locations
PacketTree.leanKomorebiLSM/
186 lines · 19 declaration locations
PerturbedOperatorFixture.leanKomorebiLSM/
327 lines · 71 declaration locations
PolicyComparison.leanKomorebiLSM/
122 lines · 9 declaration locations
Polynomial.leanKomorebiLSM/
36 lines · 2 declaration locations
PolynomialGram.leanKomorebiLSM/
505 lines · 45 declaration locations
PolynomialGramP53.leanKomorebiLSM/
80 lines · 3 declaration locations
PositiveCellApproximation.leanKomorebiLSM/
251 lines · 26 declaration locations
PositiveCellP58.leanKomorebiLSM/
57 lines · 2 declaration locations
PositiveCellResolution.leanKomorebiLSM/
101 lines · 5 declaration locations
PositiveCellUniform.leanKomorebiLSM/
136 lines · 11 declaration locations
PositiveLift.leanKomorebiLSM/
215 lines · 24 declaration locations
PositiveLiftTopology.leanKomorebiLSM/
110 lines · 6 declaration locations
PositivePackets.leanKomorebiLSM/
184 lines · 13 declaration locations
PositivePolynomialApproximation.leanKomorebiLSM/
338 lines · 23 declaration locations
PositivePriors.leanKomorebiLSM/
78 lines · 8 declaration locations
PredictableResidual.leanKomorebiLSM/
295 lines · 21 declaration locations
PredictableResidualAffine.leanKomorebiLSM/
147 lines · 9 declaration locations
PredictableResidualAnytime.leanKomorebiLSM/
94 lines · 3 declaration locations
PredictableResidualGeneral.leanKomorebiLSM/
142 lines · 7 declaration locations
PredictableResidualP66.leanKomorebiLSM/
126 lines · 7 declaration locations
PredictiveClosure.leanKomorebiLSM/
115 lines · 11 declaration locations
PredictiveCompletion.leanKomorebiLSM/
198 lines · 22 declaration locations
ProgramRefinement.leanKomorebiLSM/
205 lines · 22 declaration locations
ProposalError.leanKomorebiLSM/
277 lines · 32 declaration locations
Pseudoinverse.leanKomorebiLSM/
85 lines · 15 declaration locations
RationalBernsteinMargin.leanKomorebiLSM/
187 lines · 20 declaration locations
RationalBernsteinTermination.leanKomorebiLSM/
85 lines · 6 declaration locations
RationalCertificateSearch.leanKomorebiLSM/
217 lines · 25 declaration locations
RationalCertificateSoundness.leanKomorebiLSM/
128 lines · 7 declaration locations
RationalConfidenceArithmetic.leanKomorebiLSM/
149 lines · 19 declaration locations
RationalFeasibility.leanKomorebiLSM/
196 lines · 4 declaration locations
RationalLorentzAlgebra.leanKomorebiLSM/
52 lines · 6 declaration locations
RationalLorentzMatrix.leanKomorebiLSM/
85 lines · 10 declaration locations
RationalRegressionConfidence.leanKomorebiLSM/
93 lines · 8 declaration locations
RationalSemicircle.leanKomorebiLSM/
153 lines · 15 declaration locations
RationalSqrtEnclosure.leanKomorebiLSM/
115 lines · 13 declaration locations
RationalTransform.leanKomorebiLSM/
294 lines · 47 declaration locations
Realization.leanKomorebiLSM/
131 lines · 22 declaration locations
ReconciliationHilbert.leanKomorebiLSM/
70 lines · 4 declaration locations
RecordedBernsteinFixture.leanKomorebiLSM/
16 lines · 1 declaration location
RegressionConfidence.leanKomorebiLSM/
93 lines · 5 declaration locations
RegressionExponential.leanKomorebiLSM/
284 lines · 21 declaration locations
RegressionGaussian.leanKomorebiLSM/
347 lines · 24 declaration locations
RegressionGeometry.leanKomorebiLSM/
243 lines · 27 declaration locations
RegressionRadius.leanKomorebiLSM/
48 lines · 2 declaration locations
RegularPolygon.leanKomorebiLSM/
103 lines · 13 declaration locations
RegularPolygonAngles.leanKomorebiLSM/
91 lines · 6 declaration locations
ResetCertificate.leanKomorebiLSM/
242 lines · 14 declaration locations
RobustFiniteDomains.leanKomorebiLSM/
115 lines · 12 declaration locations
RobustOrientedMargin.leanKomorebiLSM/
299 lines · 28 declaration locations
RotationApproximation.leanKomorebiLSM/
632 lines · 54 declaration locations
RotationConeGeometry.leanKomorebiLSM/
277 lines · 20 declaration locations
RotationDensity.leanKomorebiLSM/
81 lines · 11 declaration locations
RotationModel.leanKomorebiLSM/
245 lines · 55 declaration locations
RotationP46.leanKomorebiLSM/
52 lines · 1 declaration location
RotationRank.leanKomorebiLSM/
73 lines · 5 declaration locations
ScalarRegressionConfidence.leanKomorebiLSM/
97 lines · 12 declaration locations
Section88CertifiedRepair.leanKomorebiLSM/
245 lines · 22 declaration locations
Section88ComparisonBudget.leanKomorebiLSM/
107 lines · 11 declaration locations
Section88ComparisonDirectNegGap.leanKomorebiLSM/
264 lines · 30 declaration locations
Section88ComparisonDirectNegOrientation.leanKomorebiLSM/
382 lines · 42 declaration locations
Section88ComparisonDirectPosGap.leanKomorebiLSM/
264 lines · 30 declaration locations
Section88ComparisonDirectPosOrientation.leanKomorebiLSM/
344 lines · 42 declaration locations
Section88ComparisonRotatedNegGap.leanKomorebiLSM/
215 lines · 24 declaration locations
Section88ComparisonRotatedNegOrientation.leanKomorebiLSM/
295 lines · 36 declaration locations
Section88ComparisonRotatedPosGap.leanKomorebiLSM/
215 lines · 24 declaration locations
Section88ComparisonRotatedPosOrientation.leanKomorebiLSM/
295 lines · 36 declaration locations
Section88ProposedDirectNegGap.leanKomorebiLSM/
264 lines · 30 declaration locations
Section88ProposedDirectNegOrientation.leanKomorebiLSM/
344 lines · 42 declaration locations
Section88ProposedDirectPosGap.leanKomorebiLSM/
264 lines · 30 declaration locations
Section88ProposedDirectPosOrientation.leanKomorebiLSM/
344 lines · 42 declaration locations
Section88ProposedRotatedNegGap.leanKomorebiLSM/
215 lines · 24 declaration locations
Section88ProposedRotatedNegOrientation.leanKomorebiLSM/
295 lines · 36 declaration locations
Section88ProposedRotatedPosGap.leanKomorebiLSM/
215 lines · 24 declaration locations
Section88ProposedRotatedPosOrientation.leanKomorebiLSM/
295 lines · 36 declaration locations
Section88Reference.leanKomorebiLSM/
137 lines · 14 declaration locations
SequentialConfidence.leanKomorebiLSM/
94 lines · 5 declaration locations
SequentialLowerCertificate.leanKomorebiLSM/
184 lines · 14 declaration locations
SharpConditioning.leanKomorebiLSM/
69 lines · 12 declaration locations
SingularPerturbation.leanKomorebiLSM/
81 lines · 6 declaration locations
SpectralLowerBound.leanKomorebiLSM/
76 lines · 8 declaration locations
SpectralPseudoinverse.leanKomorebiLSM/
57 lines · 6 declaration locations
SpectralSharpness.leanKomorebiLSM/
67 lines · 5 declaration locations
SpectralSubspaces.leanKomorebiLSM/
90 lines · 8 declaration locations
SpectralTail.leanKomorebiLSM/
103 lines · 7 declaration locations
StatisticalRefinement.leanKomorebiLSM/
139 lines · 11 declaration locations
StrictRationalGeometry.leanKomorebiLSM/
98 lines · 4 declaration locations
StrictRationalSearch.leanKomorebiLSM/
271 lines · 31 declaration locations
StrongRefinement.leanKomorebiLSM/
124 lines · 8 declaration locations
StructuredLearning.leanKomorebiLSM/
188 lines · 20 declaration locations
StructuredLearningCapstone.leanKomorebiLSM/
121 lines · 6 declaration locations
StructuredRectangle.leanKomorebiLSM/
224 lines · 29 declaration locations
SubspaceCoordinates.leanKomorebiLSM/
76 lines · 5 declaration locations
TensorBernsteinCertificate.leanKomorebiLSM/
169 lines · 27 declaration locations
TestCones.leanKomorebiLSM/
210 lines · 28 declaration locations
TestTopology.leanKomorebiLSM/
65 lines · 5 declaration locations
TimeRecords.leanKomorebiLSM/
241 lines · 28 declaration locations
Transfer.leanKomorebiLSM/
71 lines · 6 declaration locations
TransferLearningCertificate.leanKomorebiLSM/
176 lines · 4 declaration locations
TreeEnergy.leanKomorebiLSM/
97 lines · 8 declaration locations
UniformAbsoluteMoments.leanKomorebiLSM/
40 lines · 3 declaration locations
UniformIntervalMoments.leanKomorebiLSM/
133 lines · 20 declaration locations
VilleInequality.leanKomorebiLSM/
91 lines · 7 declaration locations
WeightedReconciliation.leanKomorebiLSM/
165 lines · 17 declaration locations