Large Signal Model · Lean source
RecordedBernsteinFixture.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 (2)
KomorebiLSM/RecordedBernsteinFixture.lean16 lines
Original source path
Lean/KomorebiLSM/RecordedBernsteinFixture.leanSkip declarations and read code
1 import KomorebiLSM.RationalLorentzMatrix
2 import KomorebiLSM.DyadicBernsteinCertificate
3
4 /-! Arithmetic records retain the submitted lower bound as well as the exact sound certificate. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.RecordedBernsteinFixture
7 open TensorBernsteinCertificate
8
9 structure RecordedLeaf (p : Polynomial₂) (R : Rectangle) where
10 certificate : LocalCertificate p R
11 lowerBound : ℚ
12 lower_nonnegative : 0≤lowerBound
13 lower_valid : ∀ i j,lowerBound≤certificate.coefficient i j
14 lower_attained : ∃ i j,certificate.coefficient i j=lowerBound
15
16 end Komorebi.LSM.RecordedBernsteinFixture
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: f54ffbfafd413060b81806d444883572dd6a2090eb39467646e751fd22914265