Paper III · Lean source

PaperIIIContinuation.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 (8)

PaperIIIContinuation.lean8 lines

Original source path

formal/PaperIIIContinuation.lean

1 import KomorebiPaperIII
2 import KomorebiPaperIII.PacketCoordinates
3 import KomorebiPaperIII.NonlinearPacketCoordinates
4 import KomorebiPaperIII.PacketDirectSum
5 import KomorebiPaperIII.MultilinearPacketJets
6 import KomorebiPaperIII.BoundedPacketJetNorm
7 import KomorebiPaperIII.ContinuousPacketJets
8 import KomorebiPaperIII.PacketJetComposition

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: 71f39e42ac78376da9099ae226589645fb5fb134263d0397a7aecb99073a6c3e

Original source on GitHub

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