Paper I · Lean source

PaperICompletion5.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 (3)

PaperICompletion5.lean3 lines

Original source path

formal/current/PaperICompletion5.lean

1 import PaperICompletion5.LinearPrimaryEigenspace
2 import PaperICompletion5.GeometricSeedFormula
3 import PaperICompletion5.CyclicGeometricCriterion

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: 722a398a88a9b9397a3f722731a285e4b32623a28293009881a0478a6f0f3f58

Original source on GitHub

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