Paper II · Lean sources
Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets
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.
Source files 75
Source locations and editions
Files are shown relative to formal/current/.
Historical editions keep their original paths. Package caches and build files are omitted.
75 files
ExactCoordinates.leanKomorebiVerification/FibreRefinement.leanKomorebiVerification/PaperII.leanKomorebiVerification/CommonRefinement.leanKomorebiVerification/PaperII/CommonRefinementConsumers.leanKomorebiVerification/PaperII/FiniteCommonRefinement.leanKomorebiVerification/PaperII/KernelAudit.leanKomorebiVerification/PaperII/LinearDefects.leanKomorebiVerification/PaperII/NestedRefinement.leanKomorebiVerification/PaperII/ReleaseAnalyticContour.leanKomorebiVerification/PaperII/ReleaseAnalyticContourSup.leanKomorebiVerification/PaperII/ReleaseAnalyticExponential.leanKomorebiVerification/PaperII/ReleaseArcLength.leanKomorebiVerification/PaperII/ReleaseCanonicalDefect.leanKomorebiVerification/PaperII/ReleaseCanonicalHFC.leanKomorebiVerification/PaperII/ReleaseCanonicalNaturality.leanKomorebiVerification/PaperII/ReleaseCoordinatesAlgebra.leanKomorebiVerification/PaperII/ReleaseCoordinatesConsumers.leanKomorebiVerification/PaperII/ReleaseCoordinatesFourier.leanKomorebiVerification/PaperII/ReleaseCoordinatesHilbert.leanKomorebiVerification/PaperII/ReleaseCoordinatesResidue.leanKomorebiVerification/PaperII/ReleaseCycleCauchy.leanKomorebiVerification/PaperII/ReleaseCycleDSlope.leanKomorebiVerification/PaperII/ReleaseCycleDecay.leanKomorebiVerification/PaperII/ReleaseCycleDixon.leanKomorebiVerification/PaperII/ReleaseCycleParameter.leanKomorebiVerification/PaperII/ReleaseCycleWinding.leanKomorebiVerification/PaperII/ReleaseDefectCompatibility.leanKomorebiVerification/PaperII/ReleaseDefectKernelAudit.leanKomorebiVerification/PaperII/ReleaseDefectPolynomial.leanKomorebiVerification/PaperII/ReleaseDefectTower.leanKomorebiVerification/PaperII/ReleaseFiltered.leanKomorebiVerification/PaperII/ReleaseFilteredPaths.leanKomorebiVerification/PaperII/ReleaseGluing.leanKomorebiVerification/PaperII/ReleaseGluingBinary.leanKomorebiVerification/PaperII/ReleaseGluingDVR.leanKomorebiVerification/PaperII/ReleaseGluingEquivSmith.leanKomorebiVerification/PaperII/ReleaseGluingFinite.leanKomorebiVerification/PaperII/ReleaseGluingMatrix.leanKomorebiVerification/PaperII/ReleaseGluingPacketBridge.leanKomorebiVerification/PaperII/ReleaseGluingPrecisionBridge.leanKomorebiVerification/PaperII/ReleaseGluingSmith.leanKomorebiVerification/PaperII/ReleasePrecision.leanKomorebiVerification/PaperII/ReleasePrecisionQuotient.leanKomorebiVerification/PaperII/ReleaseRectifiable.leanKomorebiVerification/PaperII/ReleaseRectifiableCycle.leanKomorebiVerification/PaperII/ReleaseRectifiableDefect.leanKomorebiVerification/PaperII/ReleaseRectifiableLength.leanKomorebiVerification/PaperII/ReleaseRectifiableRSError.leanKomorebiVerification/PaperII/ReleaseResultantDVR.leanKomorebiVerification/PaperII/ReleaseResultantIntegralPackets.leanKomorebiVerification/PaperII/ReleaseResultantPackets.leanKomorebiVerification/PaperII/ReleaseResultantPolynomial.leanKomorebiVerification/PaperII/ReleaseSmithCharacters.leanKomorebiVerification/PaperII/ReleaseSmithDVR.leanKomorebiVerification/PaperII/ReleaseSmithRectangular.leanKomorebiVerification/PaperII/ReleaseSmithSign.leanKomorebiVerification/PaperII/ReleaseSmithTransport.leanKomorebiVerification/PaperII/ReleaseTransferConsequences.leanKomorebiVerification/PaperII/ReleaseTransferMatrix.leanKomorebiVerification/PaperII/ReleaseTransferMultigraded.leanKomorebiVerification/PaperII/ReleaseTransferMultigradedRational.leanKomorebiVerification/PaperII/ReleaseTransferScalar.leanKomorebiVerification/PaperII/ResidueFourierCRT.leanKomorebiVerification/PaperII/ResultantSeparation.leanKomorebiVerification/PaperII/SmithDyadic.leanKomorebiVerification/PaperII/TransferZeta.leanKomorebiVerification/PaperII/TypedLinearDefects.leanKomorebiVerification/PaperII/WeightedTransfer.leanKomorebiVerification/PaperII/ProjectorCore.leanKomorebiVerification/ResidueProjectors.leanKomorebiVerification/