Large Signal Model · Lean source
KomorebiLSM.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 (254)
KomorebiLSM.lean254 lines
Original source path
Lean/KomorebiLSM.lean1 import KomorebiLSM.Realization
2 import KomorebiLSM.PredictiveClosure
3 import KomorebiLSM.Transfer
4 import KomorebiLSM.LinearClosure
5 import KomorebiLSM.LinearRefinement
6 import KomorebiLSM.Normed
7 import KomorebiLSM.Polynomial
8 import KomorebiLSM.Memory
9 import KomorebiLSM.MemoryBounds
10 import KomorebiLSM.Examples
11 import KomorebiLSM.PacketTree
12 import KomorebiLSM.TreeEnergy
13 import KomorebiLSM.InvariantCompletion
14 import KomorebiLSM.PredictiveCompletion
15 import KomorebiLSM.Block2Examples
16 import KomorebiLSM.FiniteBayes
17 import KomorebiLSM.BayesianClosure
18 import KomorebiLSM.BayesianDefect
19 import KomorebiLSM.FinitePartitions
20 import KomorebiLSM.JointRefinement
21 import KomorebiLSM.FiniteStochastic
22 import KomorebiLSM.Block3Examples
23 import KomorebiLSM.FiniteInstrument
24 import KomorebiLSM.PositivePriors
25 import KomorebiLSM.NormalizedDefect
26 import KomorebiLSM.InstrumentCompletion
27 import KomorebiLSM.InstrumentCoordinates
28 import KomorebiLSM.InstrumentRealization
29 import KomorebiLSM.Block4Examples
30 import KomorebiLSM.BehaviorSpace
31 import KomorebiLSM.BehaviorMinimality
32 import KomorebiLSM.ObservableCore
33 import KomorebiLSM.ObservableRealization
34 import KomorebiLSM.BehaviorProbability
35 import KomorebiLSM.PositivePackets
36 import KomorebiLSM.Block5Examples
37 import KomorebiLSM.TestCones
38 import KomorebiLSM.TestTopology
39 import KomorebiLSM.CanonicalCone
40 import KomorebiLSM.FiniteTestRows
41 import KomorebiLSM.PositiveLift
42 import KomorebiLSM.PositiveLiftTopology
43 import KomorebiLSM.RobustFiniteDomains
44 import KomorebiLSM.FacetRobustness
45 import KomorebiLSM.CertifiedCorrection
46 import KomorebiLSM.Block6Examples
47 import KomorebiLSM.BaseNorm
48 import KomorebiLSM.BaseNormTopology
49 import KomorebiLSM.InstrumentContraction
50 import KomorebiLSM.FiniteTV
51 import KomorebiLSM.Conditioning
52 import KomorebiLSM.SharpConditioning
53 import KomorebiLSM.ObservationTree
54 import KomorebiLSM.PolicyComparison
55 import KomorebiLSM.BaseNormModels
56 import KomorebiLSM.Block7Examples
57 import KomorebiLSM.Block7BoundaryExamples
58 import KomorebiLSM.DefectPropagation
59 import KomorebiLSM.StrongRefinement
60 import KomorebiLSM.MemoryStability
61 import KomorebiLSM.MemoryApproximation
62 import KomorebiLSM.PacketApproximation
63 import KomorebiLSM.WeightedReconciliation
64 import KomorebiLSM.AtlasReconciliation
65 import KomorebiLSM.ReconciliationHilbert
66 import KomorebiLSM.Block8Examples
67 import KomorebiLSM.Block8ApproximationExamples
68 import KomorebiLSM.DataSpan
69 import KomorebiLSM.DelayClosure
70 import KomorebiLSM.Pseudoinverse
71 import KomorebiLSM.IdentificationBound
72 import KomorebiLSM.FinitePrefix
73 import KomorebiLSM.LearnedRealization
74 import KomorebiLSM.Block9Examples
75 import KomorebiLSM.RationalFeasibility
76 import KomorebiLSM.RationalCertificateSearch
77 import KomorebiLSM.RationalCertificateSoundness
78 import KomorebiLSM.Block10Examples
79 import KomorebiLSM.CoreStability
80 import KomorebiLSM.FilteringStability
81 import KomorebiLSM.SubspaceCoordinates
82 import KomorebiLSM.Block11Examples
83 import KomorebiLSM.OneSidedSubspace
84 import KomorebiLSM.NoisySubspaceResidual
85 import KomorebiLSM.Block12Examples
86 import KomorebiLSM.SpectralLowerBound
87 import KomorebiLSM.SpectralPseudoinverse
88 import KomorebiLSM.SpectralSharpness
89 import KomorebiLSM.Block13Examples
90 import KomorebiLSM.SpectralSubspaces
91 import KomorebiLSM.SpectralTail
92 import KomorebiLSM.SingularPerturbation
93 import KomorebiLSM.LeftSingularModes
94 import KomorebiLSM.NoisySpectralSubspace
95 import KomorebiLSM.BasisCoordinates
96 import KomorebiLSM.BasisDecoder
97 import KomorebiLSM.DecoderMatrixFormula
98 import KomorebiLSM.FiniteTableP32
99 import KomorebiLSM.Block14Examples
100 import KomorebiLSM.StatisticalRefinement
101 import KomorebiLSM.ProgramRefinement
102 import KomorebiLSM.GrammarAccounting
103 import KomorebiLSM.MissingIntervention
104 import KomorebiLSM.ResetCertificate
105 import KomorebiLSM.SequentialConfidence
106 import KomorebiLSM.ConditionalStochasticCompletion
107 import KomorebiLSM.AveragedCongruence
108 import KomorebiLSM.SequentialLowerCertificate
109 import KomorebiLSM.PredictableResidual
110 import KomorebiLSM.RotationDensity
111 import KomorebiLSM.RotationModel
112 import KomorebiLSM.RotationRank
113 import KomorebiLSM.LorentzBaseNorm
114 import KomorebiLSM.RotationConeGeometry
115 import KomorebiLSM.RotationP46
116 import KomorebiLSM.RegularPolygonAngles
117 import KomorebiLSM.RegularPolygon
118 import KomorebiLSM.RotationApproximation
119 import KomorebiLSM.CertificateLearning
120 import KomorebiLSM.MatrixOrderUnit
121 import KomorebiLSM.MatrixEmbedding
122 import KomorebiLSM.MatrixRotation
123 import KomorebiLSM.UniformIntervalMoments
124 import KomorebiLSM.ContinuousInstrument
125 import KomorebiLSM.ContinuousReferenceChange
126 import KomorebiLSM.ContinuousRecords
127 import KomorebiLSM.ContinuousRecordReference
128 import KomorebiLSM.PolynomialGram
129 import KomorebiLSM.PolynomialGramP53
130 import KomorebiLSM.FiniteMomentIdentification
131 import KomorebiLSM.LegendreCounterexample
132 import KomorebiLSM.ContinuousBins
133 import KomorebiLSM.ContinuousBinnedRecords
134 import KomorebiLSM.BaseNormIntegration
135 import KomorebiLSM.BernsteinKernel
136 import KomorebiLSM.CellDistance
137 import KomorebiLSM.PositiveCellApproximation
138 import KomorebiLSM.TimeRecords
139 import KomorebiLSM.ContinuousTVDensity
140 import KomorebiLSM.ContinuousTV
141 import KomorebiLSM.PositivePolynomialApproximation
142 import KomorebiLSM.BernsteinCoefficientError
143 import KomorebiLSM.CertifiedTemplate
144 import KomorebiLSM.ConditionalEventTV
145 import KomorebiLSM.ContinuousPopulationBridge
146 import KomorebiLSM.PositiveCellResolution
147 import KomorebiLSM.PositiveCellUniform
148 import KomorebiLSM.PositiveCellP58
149 import KomorebiLSM.ContinuousRealizationP61
150 import KomorebiLSM.EllipsoidDiscovery
151 import KomorebiLSM.EllipsoidGeometry
152 import KomorebiLSM.EllipsoidDualCS
153 import KomorebiLSM.OrientedEllipsoid
154 import KomorebiLSM.EllipsoidPolynomial
155 import KomorebiLSM.EllipsoidDiscoveryP63
156 import KomorebiLSM.ObservationEquivalence
157 import KomorebiLSM.ObservationPolicyTransport
158 import KomorebiLSM.AffineObservationTransport
159 import KomorebiLSM.MeasureTVCalculus
160 import KomorebiLSM.MarkovMinorization
161 import KomorebiLSM.MarkovMarginals
162 import KomorebiLSM.BernoulliRecordSeparation
163 import KomorebiLSM.BernsteinRationalBasis
164 import KomorebiLSM.TensorBernsteinCertificate
165 import KomorebiLSM.BernsteinCellPositivity
166 import KomorebiLSM.DyadicBernsteinCertificate
167 import KomorebiLSM.BernsteinGridSearch
168 import KomorebiLSM.ConditionalBernoulli
169 import KomorebiLSM.ConditionalHoeffding
170 import KomorebiLSM.PredictableResidualAffine
171 import KomorebiLSM.ConditionalRandomMultiplier
172 import KomorebiLSM.BoundedResponseNoise
173 import KomorebiLSM.LorentzCylinder
174 import KomorebiLSM.RobustOrientedMargin
175 import KomorebiLSM.InteriorRepair
176 import KomorebiLSM.ConvexRepairBracketing
177 import KomorebiLSM.RationalSemicircle
178 import KomorebiLSM.RationalBernsteinMargin
179 import KomorebiLSM.CertifiedRepairUpper
180 import KomorebiLSM.CoefficientBox3
181 import KomorebiLSM.ComplexCoefficientBox
182 import KomorebiLSM.ConvexMargin
183 import KomorebiLSM.CountableConfidence
184 import KomorebiLSM.CoveredAdaptiveActions
185 import KomorebiLSM.CoveredActionBoundaries
186 import KomorebiLSM.PredictableResidualGeneral
187 import KomorebiLSM.PredictableResidualAnytime
188 import KomorebiLSM.PredictableResidualP66
189 import KomorebiLSM.CoveredAdaptiveEvidence
190 import KomorebiLSM.CurvedMomentGeometry
191 import KomorebiLSM.CurvedMomentInstrument
192 import KomorebiLSM.CurvedMomentPolynomial
193 import KomorebiLSM.CurvedMomentMarkov
194 import KomorebiLSM.KernelTVMeasurable
195 import KomorebiLSM.CurvedMomentTV
196 import KomorebiLSM.ObservationLawKernels
197 import KomorebiLSM.ObservationLawComparison
198 import KomorebiLSM.CurvedMomentRecordTV
199 import KomorebiLSM.CurvedMomentReferences
200 import KomorebiLSM.EuclideanMatrixNorms
201 import KomorebiLSM.DataSelectedGeometry
202 import KomorebiLSM.LorentzBoundaryFragility
203 import KomorebiLSM.MarkovRecords
204 import KomorebiLSM.MarkovWindows
205 import KomorebiLSM.ObservableMomentConditional
206 import KomorebiLSM.RegressionGeometry
207 import KomorebiLSM.ObservableMomentAlgebra
208 import KomorebiLSM.ObservableMomentProcess
209 import KomorebiLSM.ObservableOperatorSets
210 import KomorebiLSM.RegressionGaussian
211 import KomorebiLSM.RegressionRadius
212 import KomorebiLSM.RegressionExponential
213 import KomorebiLSM.VilleInequality
214 import KomorebiLSM.RegressionConfidence
215 import KomorebiLSM.ObservableMomentConfidence
216 import KomorebiLSM.ObservableMomentBoundaries
217 import KomorebiLSM.RationalSqrtEnclosure
218 import KomorebiLSM.RationalConfidenceArithmetic
219 import KomorebiLSM.OutwardConfidenceIntervals
220 import KomorebiLSM.RationalLorentzMatrix
221 import KomorebiLSM.PerturbedOperatorFixture
222 import KomorebiLSM.ProposalError
223 import KomorebiLSM.RationalBernsteinTermination
224 import KomorebiLSM.RationalLorentzAlgebra
225 import KomorebiLSM.ScalarRegressionConfidence
226 import KomorebiLSM.RationalRegressionConfidence
227 import KomorebiLSM.RationalTransform
228 import KomorebiLSM.RecordedBernsteinFixture
229 import KomorebiLSM.Section88ProposedDirectPosOrientation
230 import KomorebiLSM.Section88ProposedDirectPosGap
231 import KomorebiLSM.Section88ProposedDirectNegOrientation
232 import KomorebiLSM.Section88ProposedDirectNegGap
233 import KomorebiLSM.Section88ProposedRotatedPosOrientation
234 import KomorebiLSM.Section88ProposedRotatedPosGap
235 import KomorebiLSM.Section88ProposedRotatedNegOrientation
236 import KomorebiLSM.Section88ProposedRotatedNegGap
237 import KomorebiLSM.Section88ComparisonDirectPosOrientation
238 import KomorebiLSM.Section88ComparisonDirectPosGap
239 import KomorebiLSM.Section88ComparisonDirectNegOrientation
240 import KomorebiLSM.Section88ComparisonDirectNegGap
241 import KomorebiLSM.Section88ComparisonRotatedPosOrientation
242 import KomorebiLSM.Section88ComparisonRotatedPosGap
243 import KomorebiLSM.Section88ComparisonRotatedNegOrientation
244 import KomorebiLSM.Section88ComparisonRotatedNegGap
245 import KomorebiLSM.Section88Reference
246 import KomorebiLSM.UniformAbsoluteMoments
247 import KomorebiLSM.Section88ComparisonBudget
248 import KomorebiLSM.Section88CertifiedRepair
249 import KomorebiLSM.StrictRationalGeometry
250 import KomorebiLSM.StrictRationalSearch
251 import KomorebiLSM.StructuredLearning
252 import KomorebiLSM.StructuredRectangle
253 import KomorebiLSM.StructuredLearningCapstone
254 import KomorebiLSM.TransferLearningCertificate
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: ba6de148a8565c671c9a9b91cd3442efcd2457abae11929c27f44440f9d319ae