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

verification/release_full/013_PaperIIIContinuation/source.lean6 lines

Original source pathformal/verification/release_full/013_PaperIIIContinuation/source.lean

Skip source text

1 import KomorebiPaperIII
2 import KomorebiPaperIII.PacketCoordinates
3 import KomorebiPaperIII.NonlinearPacketCoordinates
4 import KomorebiPaperIII.PacketDirectSum
5 import KomorebiPaperIII.MultilinearPacketJets
6 import KomorebiPaperIII.BoundedPacketJetNorm

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: 78a148c5e9017d533ef7e0c8f9c33659af76ccf52bdebe104b0c5421dab5f1c7

Original source on GitHub

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