Paper I · Lean sources

Typed Operator Systems, Seed Rank, and Exact Packet Coordinates

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 116

Source locations and editions

Files are shown relative to formal/current/.

Historical editions keep their original paths. Package caches and build files are omitted.

116 files

KomorebiVerification.lean
19 lines · 0 declaration locations
Basic.leanKomorebiVerification/
34 lines · 2 declaration locations
EllipticAlgorithms.leanKomorebiVerification/
667 lines · 73 declaration locations
ExactCoordinates.leanKomorebiVerification/
104 lines · 10 declaration locations
FibreRefinement.leanKomorebiVerification/
103 lines · 5 declaration locations
FullMatrixCyclicity.leanKomorebiVerification/
40 lines · 2 declaration locations
KernelAudit.leanKomorebiVerification/
196 lines · 4 declaration locations
MathlibImports.leanKomorebiVerification/
41 lines · 0 declaration locations
PacketNaturalityCompletion.leanKomorebiVerification/
1370 lines · 121 declaration locations
PaperIBlockCompletion.leanKomorebiVerification/
155 lines · 8 declaration locations
PaperITransport.leanKomorebiVerification/
99 lines · 6 declaration locations
PathGraphKrylov.leanKomorebiVerification/
238 lines · 25 declaration locations
ProjectorCore.leanKomorebiVerification/
606 lines · 68 declaration locations
ResidueProjectors.leanKomorebiVerification/
105 lines · 8 declaration locations
SeedRankBasics.leanKomorebiVerification/
296 lines · 35 declaration locations
SeedRankOperations.leanKomorebiVerification/
643 lines · 22 declaration locations
SemisimpleCompletion.leanKomorebiVerification/
459 lines · 24 declaration locations
SemisimpleSeedRank.leanKomorebiVerification/
168 lines · 7 declaration locations
SingleOperatorGraph.leanKomorebiVerification/
1158 lines · 61 declaration locations
TopologicalCompletion.leanKomorebiVerification/
624 lines · 54 declaration locations
PaperICompletion.lean
4 lines · 0 declaration locations
ConditionedCoordinates.leanPaperICompletion/
94 lines · 12 declaration locations
CyclicClassification.leanPaperICompletion/
206 lines · 15 declaration locations
SpectralCertificates.leanPaperICompletion/
184 lines · 18 declaration locations
PaperICompletion3.lean
4 lines · 0 declaration locations
InvariantFactorCount.leanPaperICompletion3/
68 lines · 2 declaration locations
OperatorPrimaryAPI.leanPaperICompletion3/
156 lines · 17 declaration locations
PrimarySeedFormula.leanPaperICompletion3/
393 lines · 24 declaration locations
PaperICompletion4.lean
4 lines · 0 declaration locations
GroupedPrimary.leanPaperICompletion4/
114 lines · 5 declaration locations
IntrinsicPrimary.leanPaperICompletion4/
118 lines · 9 declaration locations
OperatorIntrinsicFormula.leanPaperICompletion4/
197 lines · 20 declaration locations
ResidueQuotient.leanPaperICompletion4/
183 lines · 13 declaration locations
PaperICompletion5.lean
3 lines · 0 declaration locations
CyclicGeometricCriterion.leanPaperICompletion5/
121 lines · 9 declaration locations
GeometricSeedFormula.leanPaperICompletion5/
137 lines · 17 declaration locations
LinearPrimaryEigenspace.leanPaperICompletion5/
99 lines · 8 declaration locations
PaperICompletion6.lean
1 line · 0 declaration locations
OneInvariantFactor.leanPaperICompletion6/
113 lines · 9 declaration locations
PrimaryCyclicCriterion.leanPaperICompletion6/
101 lines · 6 declaration locations
ScalarExtension.leanPaperICompletion6/
101 lines · 11 declaration locations
SixWayCyclicCriterion.leanPaperICompletion6/
74 lines · 3 declaration locations
PaperICompletion7.lean
4 lines · 0 declaration locations
LocalResidue.leanPaperICompletion7/
69 lines · 6 declaration locations
ModuleTop.leanPaperICompletion7/
124 lines · 11 declaration locations
Nakayama.leanPaperICompletion7/
81 lines · 10 declaration locations
PaperICompletion8.lean
2 lines · 0 declaration locations
DivisionBlock.leanPaperICompletion8/
107 lines · 6 declaration locations
DivisionProduct.leanPaperICompletion8/
175 lines · 10 declaration locations
DivisionRows.leanPaperICompletion8/
165 lines · 7 declaration locations
ProductPresentation.leanPaperICompletion8/
101 lines · 3 declaration locations
RegularMultiplicity.leanPaperICompletion8/
208 lines · 18 declaration locations
SemisimpleExistence.leanPaperICompletion8/
93 lines · 4 declaration locations
SemisimpleFormula.leanPaperICompletion8/
143 lines · 11 declaration locations
PaperIRelease.lean
71 lines · 0 declaration locations
AlgebraClassGrouping.leanPaperIRelease/
172 lines · 20 declaration locations
AlgebraDiagonal.leanPaperIRelease/
145 lines · 13 declaration locations
AlgebraPreorder.leanPaperIRelease/
274 lines · 23 declaration locations
AlgebraQuotient.leanPaperIRelease/
108 lines · 5 declaration locations
AlgebraSupport.leanPaperIRelease/
129 lines · 7 declaration locations
AlgebraTransfer.leanPaperIRelease/
163 lines · 16 declaration locations
BoundedStar.leanPaperIRelease/
255 lines · 19 declaration locations
CategoryBoundaries.leanPaperIRelease/
85 lines · 7 declaration locations
CategoryExport.leanPaperIRelease/
107 lines · 8 declaration locations
CategoryPackets.leanPaperIRelease/
309 lines · 26 declaration locations
CategoryUniversal.leanPaperIRelease/
75 lines · 6 declaration locations
CoordinateTransport.leanPaperIRelease/
48 lines · 3 declaration locations
ExactSequences.leanPaperIRelease/
99 lines · 3 declaration locations
GeneralConditionedCoordinates.leanPaperIRelease/
113 lines · 12 declaration locations
GeneralFiniteCompletion.leanPaperIRelease/
81 lines · 3 declaration locations
GeneralNormedPackets.leanPaperIRelease/
165 lines · 14 declaration locations
GeneralPacketBounds.leanPaperIRelease/
71 lines · 6 declaration locations
GrammarAlgebra.leanPaperIRelease/
216 lines · 30 declaration locations
GrammarEquivalence.leanPaperIRelease/
208 lines · 23 declaration locations
GrammarFactorization.leanPaperIRelease/
60 lines · 2 declaration locations
GrammarIdeal.leanPaperIRelease/
138 lines · 17 declaration locations
GrammarModules.leanPaperIRelease/
125 lines · 17 declaration locations
GrammarPaths.leanPaperIRelease/
88 lines · 9 declaration locations
GrammarTyped.leanPaperIRelease/
172 lines · 19 declaration locations
GraphPropagation.leanPaperIRelease/
147 lines · 11 declaration locations
GraphReachability.leanPaperIRelease/
99 lines · 7 declaration locations
GraphSourceBoundary.leanPaperIRelease/
52 lines · 7 declaration locations
GraphSourceCount.leanPaperIRelease/
182 lines · 8 declaration locations
GraphSourceObstruction.leanPaperIRelease/
33 lines · 1 declaration location
GraphSourceProjection.leanPaperIRelease/
94 lines · 6 declaration locations
GraphSources.leanPaperIRelease/
132 lines · 20 declaration locations
PacketAggregation.leanPaperIRelease/
152 lines · 11 declaration locations
PacketBoundaryTests.leanPaperIRelease/
137 lines · 16 declaration locations
PacketCorners.leanPaperIRelease/
70 lines · 5 declaration locations
PacketDescent.leanPaperIRelease/
291 lines · 26 declaration locations
PacketEquivalentNorm.leanPaperIRelease/
41 lines · 2 declaration locations
PacketExactSequence.leanPaperIRelease/
154 lines · 10 declaration locations
PacketLocalRank.leanPaperIRelease/
149 lines · 10 declaration locations
PacketPureBoundaryTests.leanPaperIRelease/
76 lines · 6 declaration locations
PacketPureRank.leanPaperIRelease/
113 lines · 8 declaration locations
PacketSourceLower.leanPaperIRelease/
120 lines · 5 declaration locations
PacketSourceRank.leanPaperIRelease/
58 lines · 1 declaration location
PacketSourceUpper.leanPaperIRelease/
64 lines · 1 declaration location
PacketTopology.leanPaperIRelease/
317 lines · 31 declaration locations
PacketTopologyGeneral.leanPaperIRelease/
155 lines · 16 declaration locations
PacketUniversal.leanPaperIRelease/
104 lines · 9 declaration locations
PolynomialModule.leanPaperIRelease/
90 lines · 8 declaration locations
PolynomialMonic.leanPaperIRelease/
61 lines · 7 declaration locations
ScalarExtension.leanPaperIRelease/
167 lines · 5 declaration locations
SeedOperations.leanPaperIRelease/
96 lines · 9 declaration locations
TensorPackets.leanPaperIRelease/
166 lines · 11 declaration locations
TopologyCategories.leanPaperIRelease/
160 lines · 17 declaration locations
TopologyCountablePackets.leanPaperIRelease/
260 lines · 36 declaration locations
TopologyDenseCompletion.leanPaperIRelease/
250 lines · 21 declaration locations
TopologyFiniteCompletion.leanPaperIRelease/
81 lines · 3 declaration locations
TopologyPresentations.leanPaperIRelease/
74 lines · 5 declaration locations
TopologySeedRank.leanPaperIRelease/
103 lines · 9 declaration locations
TopologySemilinearRank.leanPaperIRelease/
163 lines · 15 declaration locations
TopologyTransport.leanPaperIRelease/
131 lines · 7 declaration locations
TopologyUnconditional.leanPaperIRelease/
255 lines · 34 declaration locations
TopologyUnconditionalBridge.leanPaperIRelease/
72 lines · 6 declaration locations