Paper I · Lean source
PaperIRelease.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 (70)
PaperIRelease.lean71 lines
Original source path
formal/current/PaperIRelease.lean1 /- Paper I release: complete current formal entry point. -/
2 import KomorebiVerification
3 import KomorebiVerification.KernelAudit
4 import PaperICompletion
5 import PaperICompletion3
6 import PaperICompletion4
7 import PaperICompletion5
8 import PaperICompletion6
9 import PaperICompletion7
10 import PaperICompletion8
11 import PaperIRelease.AlgebraClassGrouping
12 import PaperIRelease.AlgebraDiagonal
13 import PaperIRelease.AlgebraPreorder
14 import PaperIRelease.AlgebraQuotient
15 import PaperIRelease.AlgebraSupport
16 import PaperIRelease.AlgebraTransfer
17 import PaperIRelease.BoundedStar
18 import PaperIRelease.CategoryBoundaries
19 import PaperIRelease.CategoryExport
20 import PaperIRelease.CategoryPackets
21 import PaperIRelease.CategoryUniversal
22 import PaperIRelease.CoordinateTransport
23 import PaperIRelease.ExactSequences
24 import PaperIRelease.GeneralConditionedCoordinates
25 import PaperIRelease.GeneralFiniteCompletion
26 import PaperIRelease.GeneralNormedPackets
27 import PaperIRelease.GeneralPacketBounds
28 import PaperIRelease.GrammarAlgebra
29 import PaperIRelease.GrammarEquivalence
30 import PaperIRelease.GrammarFactorization
31 import PaperIRelease.GrammarIdeal
32 import PaperIRelease.GrammarModules
33 import PaperIRelease.GrammarPaths
34 import PaperIRelease.GrammarTyped
35 import PaperIRelease.GraphPropagation
36 import PaperIRelease.GraphReachability
37 import PaperIRelease.GraphSourceBoundary
38 import PaperIRelease.GraphSourceCount
39 import PaperIRelease.GraphSourceObstruction
40 import PaperIRelease.GraphSourceProjection
41 import PaperIRelease.GraphSources
42 import PaperIRelease.PacketAggregation
43 import PaperIRelease.PacketBoundaryTests
44 import PaperIRelease.PacketCorners
45 import PaperIRelease.PacketDescent
46 import PaperIRelease.PacketEquivalentNorm
47 import PaperIRelease.PacketExactSequence
48 import PaperIRelease.PacketLocalRank
49 import PaperIRelease.PacketPureBoundaryTests
50 import PaperIRelease.PacketPureRank
51 import PaperIRelease.PacketSourceLower
52 import PaperIRelease.PacketSourceRank
53 import PaperIRelease.PacketSourceUpper
54 import PaperIRelease.PacketTopology
55 import PaperIRelease.PacketTopologyGeneral
56 import PaperIRelease.PacketUniversal
57 import PaperIRelease.PolynomialModule
58 import PaperIRelease.PolynomialMonic
59 import PaperIRelease.ScalarExtension
60 import PaperIRelease.SeedOperations
61 import PaperIRelease.TensorPackets
62 import PaperIRelease.TopologyCategories
63 import PaperIRelease.TopologyCountablePackets
64 import PaperIRelease.TopologyDenseCompletion
65 import PaperIRelease.TopologyFiniteCompletion
66 import PaperIRelease.TopologyPresentations
67 import PaperIRelease.TopologySeedRank
68 import PaperIRelease.TopologySemilinearRank
69 import PaperIRelease.TopologyTransport
70 import PaperIRelease.TopologyUnconditional
71 import PaperIRelease.TopologyUnconditionalBridge
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: 9d64d25e637d05019cad6f01686d14013a7a61a135d6e52b5d630280132cad8e
Back to Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates