Paper III · Lean source

source.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Local imports (7)

verification/release_full/010_KomorebiPaperIII/source.lean7 lines

Original source path

formal/verification/release_full/010_KomorebiPaperIII/source.lean

1 import KomorebiPaperIII.EdgeOperators
2 import KomorebiPaperIII.EdgeExtensions
3 import KomorebiPaperIII.Transport
4 import KomorebiPaperIII.ReversibleConnections
5 import KomorebiPaperIII.CoordinateNaturality
6 import KomorebiPaperIII.HolonomyBlocks
7 import KomorebiPaperIII.NonlinearObstructions

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

Original source on GitHub

Back to Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory