Paper I · Lean source

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

PaperICompletion4.lean4 lines

Original source path

formal/current/PaperICompletion4.lean

1 import PaperICompletion4.ResidueQuotient
2 import PaperICompletion4.IntrinsicPrimary
3 import PaperICompletion4.GroupedPrimary
4 import PaperICompletion4.OperatorIntrinsicFormula

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: 9a72da00fb06db5204b4eae3d978d8308337260973b3d43436bca4a46ecfc34f

Original source on GitHub

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