Paper II · Lean source

KomorebiVerification.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 (14)

KomorebiVerification.lean16 lines

Original source path

formal/current/KomorebiVerification.lean

1 import KomorebiVerification.PaperII
2 
3 /- Imports for the rectifiable contour closeout of 19 October 2026. -/
4 import KomorebiVerification.PaperII.ReleaseRectifiableLength
5 import KomorebiVerification.PaperII.ReleaseRectifiableRSError
6 import KomorebiVerification.PaperII.ReleaseRectifiableDefect
7 import ReleaseCyclePrimitive
8 import KomorebiVerification.PaperII.ReleaseCycleParameter
9 import KomorebiVerification.PaperII.ReleaseCycleWinding
10 import KomorebiVerification.PaperII.ReleaseCycleDixon
11 import KomorebiVerification.PaperII.ReleaseCycleDSlope
12 import KomorebiVerification.PaperII.ReleaseCycleDecay
13 import KomorebiVerification.PaperII.ReleaseCycleCauchy
14 import KomorebiVerification.PaperII.ReleaseCanonicalHFC
15 import KomorebiVerification.PaperII.ReleaseCanonicalDefect
16 import KomorebiVerification.PaperII.ReleaseCanonicalNaturality

Back to source controls

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: c0c3dfa99d088c012ccc4cc68c83cc10bc1a4eb06705328216cf7e0611f08f19

Original source on GitHub

Back to Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets