Paper I · Lean source

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

PaperICompletion7.lean4 lines

Original source path

formal/current/PaperICompletion7.lean

1 import PaperICompletion6
2 import PaperICompletion7.Nakayama
3 import PaperICompletion7.ModuleTop
4 import PaperICompletion7.LocalResidue

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: 2806b9e504b0698929e1c45577fd437322781cbc419751b8c6d696cc08c0f27f