Paper III · Lean sources
Typed Transfer, Nonlinear Packets, and Obstruction Theory
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.
Source files 161
Source locations and editions
Files are shown relative to formal/.
Historical editions keep their original paths. Package caches and build files are omitted.
161 files
BoundedPacketJetNorm.leanKomorebiPaperIII/ContinuousPacketJets.leanKomorebiPaperIII/CoordinateNaturality.leanKomorebiPaperIII/EdgeExtensions.leanKomorebiPaperIII/EdgeOperators.leanKomorebiPaperIII/HolonomyBlocks.leanKomorebiPaperIII/KernelAudit.leanKomorebiPaperIII/MultilinearPacketJets.leanKomorebiPaperIII/NonlinearObstructions.leanKomorebiPaperIII/NonlinearPacketCoordinates.leanKomorebiPaperIII/PacketCoordinates.leanKomorebiPaperIII/PacketDirectSum.leanKomorebiPaperIII/PacketJetComposition.leanKomorebiPaperIII/ReversibleConnections.leanKomorebiPaperIII/Transport.leanKomorebiPaperIII/InventoryOnly.leanaudit/OwnedAudit.leanaudit/ReplayClosure.leanaudit/AdmittedProof.leancontrols/AuditBadAxiom.leancontrols/AuditBadOpaque.leancontrols/AuditBadPartial.leancontrols/AuditBadUnsafe.leancontrols/AuditGoodForeign.leancontrols/BadAxiom.leancontrols/BadOpaque.leancontrols/BadPartial.leancontrols/BadUnsafe.leancontrols/BoundaryConsumers.leancontrols/FalseArithmetic.leancontrols/GoodForeign.leancontrols/source.leanverification/candidates_initial/000_KomorebiPaperIII_MultilinearPacketJets/source.leanverification/candidates_initial/001_KomorebiPaperIII_BoundedPacketJetNorm/source.leanverification/continuous_jets_corrected/000_KomorebiPaperIII_ContinuousPacketJets/source.leanverification/continuous_jets_initial/000_KomorebiPaperIII_ContinuousPacketJets/source.leanverification/continuous_release_audit/000_OwnedAudit/source.leanverification/continuous_release_controls/000_GoodForeign/source.leanverification/continuous_release_controls/001_AuditGoodForeign/source.leanverification/continuous_release_controls/002_BadAxiom/source.leanverification/continuous_release_controls/003_AuditBadAxiom/source.leanverification/continuous_release_controls/004_BadOpaque/source.leanverification/continuous_release_controls/005_AuditBadOpaque/source.leanverification/continuous_release_controls/006_BadUnsafe/source.leanverification/continuous_release_controls/007_AuditBadUnsafe/source.leanverification/continuous_release_controls/008_BadPartial/source.leanverification/continuous_release_controls/009_AuditBadPartial/source.leanverification/continuous_release_controls/010_FalseArithmetic/source.leanverification/continuous_release_controls/011_AdmittedProof/source.leanverification/continuous_release_controls/012_BoundaryConsumers/source.leanverification/continuous_release_controls/013_ReplayClosure/source.leanverification/continuous_release_full/000_KomorebiPaperIII_EdgeOperators/source.leanverification/continuous_release_full/001_KomorebiPaperIII_EdgeExtensions/source.leanverification/continuous_release_full/002_KomorebiPaperIII_Transport/source.leanverification/continuous_release_full/003_KomorebiPaperIII_ReversibleConnections/source.leanverification/continuous_release_full/004_KomorebiPaperIII_CoordinateNaturality/source.leanverification/continuous_release_full/005_KomorebiPaperIII_NonlinearObstructions/source.leanverification/continuous_release_full/006_KomorebiPaperIII_HolonomyBlocks/source.leanverification/continuous_release_full/007_KomorebiPaperIII_PacketCoordinates/source.leanverification/continuous_release_full/008_KomorebiPaperIII_NonlinearPacketCoordinates/source.leanverification/continuous_release_full/009_KomorebiPaperIII_PacketDirectSum/source.leanverification/continuous_release_full/010_KomorebiPaperIII/source.leanverification/continuous_release_full/011_KomorebiPaperIII_MultilinearPacketJets/source.leanverification/continuous_release_full/012_KomorebiPaperIII_BoundedPacketJetNorm/source.leanverification/continuous_release_full/013_KomorebiPaperIII_ContinuousPacketJets/source.leanverification/continuous_release_full/014_PaperIIIContinuation/source.leanverification/continuous_release_replay/000_ReplayClosure/source.leanverification/core_initial/000_KomorebiPaperIII_EdgeOperators/source.leanverification/core_initial/001_KomorebiPaperIII_EdgeExtensions/source.leanverification/core_initial/002_KomorebiPaperIII_Transport/source.leanverification/core_initial/003_KomorebiPaperIII_ReversibleConnections/source.leanverification/core_initial/004_KomorebiPaperIII_CoordinateNaturality/source.leanverification/core_initial/005_KomorebiPaperIII_NonlinearObstructions/source.leanverification/core_initial/006_KomorebiPaperIII_HolonomyBlocks/source.leanverification/core_initial/007_KomorebiPaperIII_PacketCoordinates/source.leanverification/core_initial/008_KomorebiPaperIII_NonlinearPacketCoordinates/source.leanverification/core_initial/009_KomorebiPaperIII_PacketDirectSum/source.leanverification/core_initial/010_KomorebiPaperIII/source.leanverification/core_initial/011_PaperIIIContinuation/source.leanverification/final_release_audit/000_OwnedAudit/source.leanverification/final_release_controls/000_GoodForeign/source.leanverification/final_release_controls/001_AuditGoodForeign/source.leanverification/final_release_controls/002_BadAxiom/source.leanverification/final_release_controls/003_AuditBadAxiom/source.leanverification/final_release_controls/004_BadOpaque/source.leanverification/final_release_controls/005_AuditBadOpaque/source.leanverification/final_release_controls/006_BadUnsafe/source.leanverification/final_release_controls/007_AuditBadUnsafe/source.leanverification/final_release_controls/008_BadPartial/source.leanverification/final_release_controls/009_AuditBadPartial/source.leanverification/final_release_controls/010_FalseArithmetic/source.leanverification/final_release_controls/011_AdmittedProof/source.leanverification/final_release_controls/012_BoundaryConsumers/source.leanverification/final_release_controls/013_ReplayClosure/source.leanverification/final_release_full/000_KomorebiPaperIII_EdgeOperators/source.leanverification/final_release_full/001_KomorebiPaperIII_EdgeExtensions/source.leanverification/final_release_full/002_KomorebiPaperIII_Transport/source.leanverification/final_release_full/003_KomorebiPaperIII_ReversibleConnections/source.leanverification/final_release_full/004_KomorebiPaperIII_CoordinateNaturality/source.leanverification/final_release_full/005_KomorebiPaperIII_NonlinearObstructions/source.leanverification/final_release_full/006_KomorebiPaperIII_HolonomyBlocks/source.leanverification/final_release_full/007_KomorebiPaperIII_PacketCoordinates/source.leanverification/final_release_full/008_KomorebiPaperIII_NonlinearPacketCoordinates/source.leanverification/final_release_full/009_KomorebiPaperIII_PacketDirectSum/source.leanverification/final_release_full/010_KomorebiPaperIII/source.leanverification/final_release_full/011_KomorebiPaperIII_MultilinearPacketJets/source.leanverification/final_release_full/012_KomorebiPaperIII_BoundedPacketJetNorm/source.leanverification/final_release_full/013_KomorebiPaperIII_ContinuousPacketJets/source.leanverification/final_release_full/014_KomorebiPaperIII_PacketJetComposition/source.leanverification/final_release_full/015_PaperIIIContinuation/source.leanverification/final_release_replay/000_ReplayClosure/source.leanverification/packet_composition_coercions/000_KomorebiPaperIII_PacketJetComposition/source.leanverification/packet_composition_corrected/000_KomorebiPaperIII_PacketJetComposition/source.leanverification/packet_composition_initial/000_KomorebiPaperIII_PacketJetComposition/source.leanverification/packet_composition_support/000_KomorebiPaperIII_PacketJetComposition/source.leanverification/packet_composition_support_corrected/000_KomorebiPaperIII_PacketJetComposition/source.leanverification/release_controls/000_GoodForeign/source.leanverification/release_controls/001_AuditGoodForeign/source.leanverification/release_controls/002_BadAxiom/source.leanverification/release_controls/003_AuditBadAxiom/source.leanverification/release_controls/004_BadOpaque/source.leanverification/release_controls/005_AuditBadOpaque/source.leanverification/release_controls/006_BadUnsafe/source.leanverification/release_controls/007_AuditBadUnsafe/source.leanverification/release_controls/008_BadPartial/source.leanverification/release_controls/009_AuditBadPartial/source.leanverification/release_controls/010_FalseArithmetic/source.leanverification/release_controls/011_AdmittedProof/source.leanverification/release_controls/012_BoundaryConsumers/source.leanverification/release_controls/013_ReplayClosure/source.leanverification/release_controls_corrected/000_GoodForeign/source.leanverification/release_controls_corrected/001_AuditGoodForeign/source.leanverification/release_controls_corrected/002_BadAxiom/source.leanverification/release_controls_corrected/003_AuditBadAxiom/source.leanverification/release_controls_corrected/004_BadOpaque/source.leanverification/release_controls_corrected/005_AuditBadOpaque/source.leanverification/release_controls_corrected/006_BadUnsafe/source.leanverification/release_controls_corrected/007_AuditBadUnsafe/source.leanverification/release_controls_corrected/008_BadPartial/source.leanverification/release_controls_corrected/009_AuditBadPartial/source.leanverification/release_controls_corrected/010_FalseArithmetic/source.leanverification/release_controls_corrected/011_AdmittedProof/source.leanverification/release_controls_corrected/012_BoundaryConsumers/source.leanverification/release_controls_corrected/013_ReplayClosure/source.leanverification/release_full/000_KomorebiPaperIII_EdgeOperators/source.leanverification/release_full/001_KomorebiPaperIII_EdgeExtensions/source.leanverification/release_full/002_KomorebiPaperIII_Transport/source.leanverification/release_full/003_KomorebiPaperIII_ReversibleConnections/source.leanverification/release_full/004_KomorebiPaperIII_CoordinateNaturality/source.leanverification/release_full/005_KomorebiPaperIII_NonlinearObstructions/source.leanverification/release_full/006_KomorebiPaperIII_HolonomyBlocks/source.leanverification/release_full/007_KomorebiPaperIII_PacketCoordinates/source.leanverification/release_full/008_KomorebiPaperIII_NonlinearPacketCoordinates/source.leanverification/release_full/009_KomorebiPaperIII_PacketDirectSum/source.leanverification/release_full/010_KomorebiPaperIII/source.leanverification/release_full/011_KomorebiPaperIII_MultilinearPacketJets/source.leanverification/release_full/012_KomorebiPaperIII_BoundedPacketJetNorm/source.leanverification/release_full/013_PaperIIIContinuation/source.leanverification/release_kernel_replay/000_ReplayClosure/source.leanverification/release_owned_audit/000_OwnedAudit/