Paper I · Lean source

PaperICompletion3.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)

PaperICompletion3.lean4 lines

Original source path

formal/current/PaperICompletion3.lean

1 import PaperICompletion
2 import PaperICompletion3.PrimarySeedFormula
3 import PaperICompletion3.OperatorPrimaryAPI
4 import PaperICompletion3.InvariantFactorCount

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: 22cf28d8018044fc3006608012fce5b7b7aa4b62979eeb576a8ce9eafb3b967f

Original source on GitHub

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