Paper I · Lean source

KomorebiVerification.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 (17)

KomorebiVerification.lean19 lines

Original source path

formal/current/KomorebiVerification.lean

1 import KomorebiVerification.Basic
2 import KomorebiVerification.ProjectorCore
3 import KomorebiVerification.FibreRefinement
4 import KomorebiVerification.ExactCoordinates
5 import KomorebiVerification.ResidueProjectors
6 import KomorebiVerification.PaperITransport
7 import KomorebiVerification.PaperIBlockCompletion
8 import KomorebiVerification.SeedRankBasics
9 import KomorebiVerification.SeedRankOperations
10 import KomorebiVerification.SemisimpleSeedRank
11 import KomorebiVerification.SemisimpleCompletion
12 import KomorebiVerification.FullMatrixCyclicity
13 import KomorebiVerification.PathGraphKrylov
14 import KomorebiVerification.SingleOperatorGraph
15 import KomorebiVerification.PacketNaturalityCompletion
16 import KomorebiVerification.TopologicalCompletion
17 import KomorebiVerification.EllipticAlgorithms
18 
19 -- `KernelAudit` is a standalone release gate, invoked explicitly by both runners.

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: 292bc683670b4cec1c82c52d643a54fd6dd3598681401cdc451f52bc5b78b8bf

Original source on GitHub

Back to Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates