Paper II · Lean source
ReleaseDefectKernelAudit.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 (5)
KomorebiVerification/PaperII/ReleaseDefectKernelAudit.lean22 lines
Original source path
formal/current/KomorebiVerification/PaperII/ReleaseDefectKernelAudit.lean1 import KomorebiVerification.PaperII.ReleaseDefectPolynomial
2 import KomorebiVerification.PaperII.ReleaseDefectTower
3 import KomorebiVerification.PaperII.ReleaseAnalyticExponential
4 import KomorebiVerification.PaperII.ReleaseAnalyticContourSup
5 import KomorebiVerification.PaperII.ReleaseDefectCompatibility
6
7 set_option autoImplicit false
8 #print axioms Komorebi.PaperII.ReleaseDefectPolynomial.polynomial_defect
9 #print axioms Komorebi.PaperII.ReleaseDefectPolynomial.continuous_polynomial_defect
10 #print axioms Komorebi.PaperII.ReleaseDefectTower.multilevel_defect
11 #print axioms Komorebi.PaperII.ReleaseDefectTower.continuous_multilevel_defect
12 #print axioms Komorebi.PaperII.ReleaseDefectTower.continuous_norm_multilevel_defect_le
13 #print axioms Komorebi.PaperII.ReleaseDefectTower.continuous_multilevel_polynomial_compatible
14 #print axioms Komorebi.PaperII.ReleaseDefectTower.continuous_multilevel_resolvents_compatible
15 #print axioms Komorebi.PaperII.ReleaseAnalyticExponential.exponential_defect_real
16 #print axioms Komorebi.PaperII.ReleaseAnalyticExponential.exponential_defect_segment
17 #print axioms Komorebi.PaperII.ReleaseAnalyticExponential.norm_exponential_defect_real_le
18 #print axioms Komorebi.PaperII.ReleaseAnalyticContour.resolvent_defect_actual
19 #print axioms Komorebi.PaperII.ReleaseAnalyticContour.dunfordIntegral_defect
20 #print axioms Komorebi.PaperII.ReleaseAnalyticContour.dunfordIntegral_norm_defect_le_sup
21 #print axioms Komorebi.PaperII.ReleaseDefectCompatibility.multilevel_exponential_compatible
22 #print axioms Komorebi.PaperII.ReleaseDefectCompatibility.multilevel_dunfordIntegral_compatible
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: 471acbb95239b444647bc18ece05da922dbf52ce3c77b114a0e3faded1718b61
Back to Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets