Paper I · Lean source

PaperICompletion.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 (4)

PaperICompletion.lean4 lines

Original source path

formal/current/PaperICompletion.lean

1 import KomorebiVerification
2 import PaperICompletion.CyclicClassification
3 import PaperICompletion.SpectralCertificates
4 import PaperICompletion.ConditionedCoordinates

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: b41e56dfb58c77e2f666399298377ecd876a4e43ebde44d1b2e2e85fe8e31ffa

Original source on GitHub

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