Paper II · Lean source
PaperIIRefinement.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 (1)
PaperIIRefinement.lean1 line
Original source path
formal/current/PaperIIRefinement.lean1 import KomorebiVerification.PaperII.CommonRefinementConsumers
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: 2ed19f210c6a40b3896104326eb3fecc8c08ed3f563666d7c622ffc05b421f42
Back to Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets