Mathematics · proofs · software

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 (4)

verification/core_initial/011_PaperIIIContinuation/source.lean4 lines

Original source pathformal/verification/core_initial/011_PaperIIIContinuation/source.lean

Skip source text

1 import KomorebiPaperIII
2 import KomorebiPaperIII.PacketCoordinates
3 import KomorebiPaperIII.NonlinearPacketCoordinates
4 import KomorebiPaperIII.PacketDirectSum

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

Original source on GitHub

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