Mathematics · proofs · software

Paper II · Lean source

PaperII.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 (28)

KomorebiVerification/PaperII.lean46 lines

Original source pathformal/current/KomorebiVerification/PaperII.lean

Skip source text

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.PaperII.NestedRefinement
7 import KomorebiVerification.PaperII.ResidueFourierCRT
8 import KomorebiVerification.PaperII.WeightedTransfer
9 import KomorebiVerification.PaperII.TransferZeta
10 import KomorebiVerification.PaperII.ResultantSeparation
11 import KomorebiVerification.PaperII.SmithDyadic
12 import KomorebiVerification.PaperII.LinearDefects
13 import KomorebiVerification.PaperII.TypedLinearDefects
14 import KomorebiVerification.PaperII.CommonRefinementConsumers
15 import KomorebiVerification.PaperII.ReleaseCoordinatesConsumers
16 import KomorebiVerification.PaperII.ReleaseFilteredPaths
17 import KomorebiVerification.PaperII.ReleaseResultantIntegralPackets
18 import KomorebiVerification.PaperII.ReleaseResultantDVR
19 import KomorebiVerification.PaperII.ReleaseGluingBinary
20 import KomorebiVerification.PaperII.ReleaseGluingPrecisionBridge
21 import KomorebiVerification.PaperII.ReleaseGluingFinite
22 import KomorebiVerification.PaperII.ReleaseGluingEquivSmith
23 import KomorebiVerification.PaperII.ReleaseGluingMatrix
24 import KomorebiVerification.PaperII.ReleaseGluingPacketBridge
25 import KomorebiVerification.PaperII.ReleasePrecisionQuotient
26 import KomorebiVerification.PaperII.ReleaseDefectCompatibility
27 import KomorebiVerification.PaperII.ReleaseDefectPolynomial
28 import KomorebiVerification.PaperII.ReleaseAnalyticContourSup
29 import KomorebiVerification.PaperII.ReleaseTransferConsequences
30 import KomorebiVerification.PaperII.ReleaseSmithTransport
31 import KomorebiVerification.PaperII.ReleaseSmithSign
32 import KomorebiVerification.PaperII.ReleaseSmithCharacters
33 import KomorebiVerification.PaperII.ReleaseRectifiableCycle
34 
35 /-!
36 # Projector-Resolved Seed Calculus II
37 
38 Aggregate import for the current Paper II Lean development.
39 
40 The accompanying current manuscript correspondence records the scope of each
41 proved endpoint. General rectifiable-cycle Cauchy and canonical holomorphic
42 functional-calculus independence are not proved by this aggregate.
43 
44 The fail-closed trust audit is intentionally a separate build target:
45 `KomorebiVerification.PaperII.KernelAudit`.
46 -/

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: 2095e1fe4bda7524e1ff678a3c479806a99fcc86fb56e3e4a11b10293009256f

Original source on GitHub

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