First-party checked source

Source for Bondy's Minimum-Degree Longest-Cycle Conjecture

The companion paper presents a candidate proof of Bondy's minimum-degree longest-cycle conjecture. Paper-to-formal-statement alignment is under review. Lean checks only the exact displayed endpoint Bondy.bondy_longest_cycle at the audited source commit; its 204-module first-party cone reports only standard classical foundations. Download the complete checked closure, open the endpoint, or browse its supporting modules to study the proof or develop an extension.

Read the theorem overview Complete checked Lean source · 204 Lean files · 1 evidence record · Download ZIP Open Main.lean

Immutable source commit: 9e13b044d8821b587935fa3019d913699eadffa2

License and notice commit: 9134da370295ac4c1989070c341ba101ac3d9c17

Each ZIP contains the checked first-party local Lean import closure, exact statements and boundaries, license, notice, evidence, a source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled; this is not a portable whole-repository release.

Proof and source

What is checked—and how much source supports it

Browse the counted source

Declarations covered by evidence: 1
First-party Lean files: 204
Lean source lines: 101,839
Main recorded file: 48 lines

How the source is counted

Line counts exclude blank lines; comments and documentation count. The total is the deduplicated, commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded. Declaration count means names covered by the artifact's recorded evidence, not every declaration in the source. Source footprint is not a difficulty or proof-quality score.

Exact theorem evidence

Bondy's Minimum-Degree Longest-Cycle Conjecture

Bondy.bondy_longest_cycle

This is the hash-matched main Lean file. Its complete tracked local Lean import closure is browsable once below; checker evidence remains separate for this exact theorem.

Commit: 9e13b044d8821b587935fa3019d913699eadffa2
Main Lean file: Bondy/Main.lean
Main-file footprint: 48 lines
File SHA-256: sha256:39f30c64552384723952a7a5db99d1254ac0dc72658b71b71e6b75d0d59bf85a
Complete Lean closure: 204 files · 101,839 lines
Toolchain: leanprover/lean4:v4.30.0-rc2

Open main Lean file Download main Lean file Download checker evidence (JSON)Download Apache-2.0 license Download Lech Mazur notice

Deduplicated checked source

Complete Lean import closure

This closure supports the theorem evidence record above.

Complete checked Lean closure

204 Lean files are available here

Start with the principal theorem and proof-architecture files below, or search the complete commit-pinned closure.

204Lean files

Search and browse all 204 checked Lean files

Every listed file is read from the same pinned Git commit. File links open raw source in a new tab; use the ZIP download for the complete package. External Mathlib modules are dependency-locked but are not copied into this first-party source tree.

Filter all 204 Lean files

Showing all 204 files

Bondy2 files · 57 lines

Bondy/Main.lean48 lines
Bondy/Setup.lean9 lines

Bondy/Basic14 files · 6,373 lines

Bondy/Basic/Arithmetic.lean2,448 lines
Bondy/Basic/Case12FourBadAwayMatching.lean813 lines
Bondy/Basic/ContactTransition.lean293 lines
Bondy/Basic/CyclicProtectedRun.lean207 lines
Bondy/Basic/CyclicTwoExceptional.lean458 lines
Bondy/Basic/DisjointContactCount.lean162 lines
Bondy/Basic/FiniteLine.lean621 lines
Bondy/Basic/FiniteMaximizer.lean70 lines
Bondy/Basic/IncreasingEnumeration.lean671 lines
Bondy/Basic/MaxCardThenWeight.lean211 lines
Bondy/Basic/NatDegree.lean156 lines
Bondy/Basic/OrderedGap.lean43 lines
Bondy/Basic/SecondMinimum.lean162 lines
Bondy/Basic/SpecialGenericConflict.lean58 lines

Bondy/Components4 files · 569 lines

Bondy/Components/ComponentOf.lean111 lines
Bondy/Components/Components.lean83 lines
Bondy/Components/LongestPath.lean313 lines
Bondy/Components/ResidualPiece.lean62 lines

Bondy/Connectivity6 files · 584 lines

Bondy/Connectivity/CrossingEdge.lean44 lines
Bondy/Connectivity/Induced.lean115 lines
Bondy/Connectivity/MinimumDegree.lean78 lines
Bondy/Connectivity/Reachability.lean70 lines
Bondy/Connectivity/TwoConnectedOn.lean172 lines
Bondy/Connectivity/VertexConnected.lean105 lines

Bondy/InternalMazur29 files · 6,126 lines

Bondy/InternalMazur/Allowance.lean66 lines
Bondy/InternalMazur/AttachmentBridge.lean280 lines
Bondy/InternalMazur/BranchAccounting.lean337 lines
Bondy/InternalMazur/BranchArithmetic.lean155 lines
Bondy/InternalMazur/BranchBoundsInstantiation.lean404 lines
Bondy/InternalMazur/BranchCover.lean78 lines
Bondy/InternalMazur/BranchCycleBounds.lean410 lines
Bondy/InternalMazur/BranchEndpointBounds.lean372 lines
Bondy/InternalMazur/BranchIncidenceLine.lean323 lines
Bondy/InternalMazur/BranchSummation.lean224 lines
Bondy/InternalMazur/Core.lean176 lines
Bondy/InternalMazur/CoreNormalization.lean35 lines
Bondy/InternalMazur/CycleIncidence.lean139 lines
Bondy/InternalMazur/DegreeBudget.lean225 lines
Bondy/InternalMazur/DegreeDecomposition.lean172 lines
Bondy/InternalMazur/Geometry.lean235 lines
Bondy/InternalMazur/LastPathAncestor.lean154 lines
Bondy/InternalMazur/Linkage.lean252 lines
Bondy/InternalMazur/LinkedAttachment.lean266 lines
Bondy/InternalMazur/Localization.lean320 lines
Bondy/InternalMazur/OrderedAttachments.lean19 lines
Bondy/InternalMazur/PathLinkage.lean94 lines
Bondy/InternalMazur/PathLinkageSplice.lean152 lines
Bondy/InternalMazur/PathPosition.lean461 lines
Bondy/InternalMazur/RepresentativeBudget.lean85 lines
Bondy/InternalMazur/RepresentativeSelection.lean218 lines
Bondy/InternalMazur/TypeOne.lean236 lines
Bondy/InternalMazur/TypeTwoSelection.lean165 lines
Bondy/InternalMazur/TypeTwoUniverse.lean73 lines

Bondy/NormalTree9 files · 1,649 lines

Bondy/NormalTree/AncestorData.lean93 lines
Bondy/NormalTree/ComponentInduction.lean286 lines
Bondy/NormalTree/DeepestLeaf.lean149 lines
Bondy/NormalTree/ExtendsPath.lean141 lines
Bondy/NormalTree/Glue.lean360 lines
Bondy/NormalTree/Graft.lean116 lines
Bondy/NormalTree/OffPath.lean25 lines
Bondy/NormalTree/Parent.lean256 lines
Bondy/NormalTree/TreeSegment.lean223 lines

Bondy/PathCycle21 files · 17,049 lines

Bondy/PathCycle/AdjacentContactCellBridge.lean949 lines
Bondy/PathCycle/AdjacentPairCrossDetour.lean558 lines
Bondy/PathCycle/AdjacentPairExternalBridgeDetour.lean1,652 lines
Bondy/PathCycle/AdjacentPairExternalExtension.lean1,047 lines
Bondy/PathCycle/AlternatingHubExternalBridge.lean1,661 lines
Bondy/PathCycle/CrossingExternalBridge.lean885 lines
Bondy/PathCycle/CycleArc.lean491 lines
Bondy/PathCycle/EndpointNeighborDetour.lean291 lines
Bondy/PathCycle/ExternalCycleBridge.lean304 lines
Bondy/PathCycle/ExternalDetour.lean371 lines
Bondy/PathCycle/ExternalJoin.lean88 lines
Bondy/PathCycle/HubParityExtension.lean2,151 lines
Bondy/PathCycle/Join.lean632 lines
Bondy/PathCycle/LastContact.lean3,669 lines
Bondy/PathCycle/ListBuilder.lean137 lines
Bondy/PathCycle/Segment.lean283 lines
Bondy/PathCycle/StationaryFan.lean798 lines
Bondy/PathCycle/TwoGapReplacement.lean624 lines
Bondy/PathCycle/TwoPathCycle.lean159 lines
Bondy/PathCycle/VCycle.lean130 lines
Bondy/PathCycle/VPath.lean169 lines

Bondy/RequiredResidual119 files · 69,432 lines

Bondy/RequiredResidual/BondyResidualCap.lean107 lines
Bondy/RequiredResidual/Cap.lean27 lines
Bondy/RequiredResidual/CapBridge.lean21 lines
Bondy/RequiredResidual/Case12MultiSpecialArcChain.lean148 lines
Bondy/RequiredResidual/Case12MultiSpecialChain.lean110 lines
Bondy/RequiredResidual/Case12PhysicalGapSelectedOwners.lean200 lines
Bondy/RequiredResidual/Case12SelectedSpecialGapOrder.lean301 lines
Bondy/RequiredResidual/Case12SelectedSpecialPlainConnectorChain.lean119 lines
Bondy/RequiredResidual/Case12TerminalGeometry.lean526 lines
Bondy/RequiredResidual/ChargedCleanGap.lean240 lines
Bondy/RequiredResidual/CollisionEscapePath.lean72 lines
Bondy/RequiredResidual/CycleExtensionNInfrastructure.lean127 lines
Bondy/RequiredResidual/CycleExtensionNMiddle.lean80 lines
Bondy/RequiredResidual/CycleSpreading.lean341 lines
Bondy/RequiredResidual/CycleSpreadingAbsorb.lean314 lines
Bondy/RequiredResidual/CycleSpreadingBudget.lean220 lines
Bondy/RequiredResidual/CycleSpreadingCompensation.lean450 lines
Bondy/RequiredResidual/CycleSpreadingConfined.lean359 lines
Bondy/RequiredResidual/CycleSpreadingCyclic.lean788 lines
Bondy/RequiredResidual/CycleSpreadingDegree.lean223 lines
Bondy/RequiredResidual/CycleSpreadingDegreeSelection.lean124 lines
Bondy/RequiredResidual/CycleSpreadingExtreme.lean389 lines
Bondy/RequiredResidual/CycleSpreadingFan.lean235 lines
Bondy/RequiredResidual/CycleSpreadingHigh.lean100 lines
Bondy/RequiredResidual/CycleSpreadingHighBudget.lean195 lines
Bondy/RequiredResidual/CycleSpreadingIncidentBridge.lean375 lines
Bondy/RequiredResidual/CycleSpreadingLemmaTwo.lean728 lines
Bondy/RequiredResidual/CycleSpreadingLemmaTwoBridge.lean759 lines
Bondy/RequiredResidual/CycleSpreadingLemmaTwoConclusion.lean158 lines
Bondy/RequiredResidual/CycleSpreadingMaximality.lean463 lines
Bondy/RequiredResidual/CycleSpreadingOneEdgeActive.lean115 lines
Bondy/RequiredResidual/CycleSpreadingOneEdgeOmittedGap.lean482 lines
Bondy/RequiredResidual/CycleSpreadingOneEdgePath.lean2,316 lines
Bondy/RequiredResidual/CycleSpreadingOneHigh.lean156 lines
Bondy/RequiredResidual/CycleSpreadingOneHighBudget.lean171 lines
Bondy/RequiredResidual/CycleSpreadingOneHighConclusion.lean110 lines
Bondy/RequiredResidual/CycleSpreadingOrderTwo.lean190 lines
Bondy/RequiredResidual/CycleSpreadingPivot.lean466 lines
Bondy/RequiredResidual/CycleSpreadingPivots.lean228 lines
Bondy/RequiredResidual/CycleSpreadingReroute.lean390 lines
Bondy/RequiredResidual/CycleSpreadingTwoHigh.lean466 lines
Bondy/RequiredResidual/Dirac.lean79 lines
Bondy/RequiredResidual/DiracAlignedPaths.lean2,572 lines
Bondy/RequiredResidual/DiracCircumferenceTail.lean2,715 lines
Bondy/RequiredResidual/DiracCycleThroughPath.lean164 lines
Bondy/RequiredResidual/DiracEndpointSets.lean137 lines
Bondy/RequiredResidual/DiracNonspanning.lean41 lines
Bondy/RequiredResidual/LongestCycleConnectivity.lean68 lines
Bondy/RequiredResidual/Packing.lean49 lines
Bondy/RequiredResidual/PositiveHighGlobalSize.lean395 lines
Bondy/RequiredResidual/RepairedThetaBetaSharp.lean206 lines
Bondy/RequiredResidual/RepairedThetaClaim4BlockIncidence.lean353 lines
Bondy/RequiredResidual/RepairedThetaCollisionAdjacentPairs.lean412 lines
Bondy/RequiredResidual/RepairedThetaCollisionAssignment.lean359 lines
Bondy/RequiredResidual/RepairedThetaCollisionChargedCycle.lean641 lines
Bondy/RequiredResidual/RepairedThetaCollisionChargedGap.lean193 lines
Bondy/RequiredResidual/RepairedThetaCollisionCyclicOrder.lean447 lines
Bondy/RequiredResidual/RepairedThetaCollisionEscape.lean236 lines
Bondy/RequiredResidual/RepairedThetaCollisionI1Assembler.lean355 lines
Bondy/RequiredResidual/RepairedThetaCollisionRooting.lean1,429 lines
Bondy/RequiredResidual/RepairedThetaConfinedNonSpecialG6.lean5,778 lines
Bondy/RequiredResidual/RepairedThetaConflictFreeGenericSelection.lean1,516 lines
Bondy/RequiredResidual/RepairedThetaCoveredRouteProtection.lean296 lines
Bondy/RequiredResidual/RepairedThetaCoveredSelectedGapChain.lean294 lines
Bondy/RequiredResidual/RepairedThetaCoveredTerminalFamily.lean1,159 lines
Bondy/RequiredResidual/RepairedThetaDefinition39ChargedGap.lean754 lines
Bondy/RequiredResidual/RepairedThetaDefinition39GapPair.lean284 lines
Bondy/RequiredResidual/RepairedThetaDefinition39State.lean1,613 lines
Bondy/RequiredResidual/RepairedThetaEarTrace.lean104 lines
Bondy/RequiredResidual/RepairedThetaFullHallChargedCycle.lean196 lines
Bondy/RequiredResidual/RepairedThetaFullHallI1Assembler.lean265 lines
Bondy/RequiredResidual/RepairedThetaGamma.lean357 lines
Bondy/RequiredResidual/RepairedThetaLowSpecialConnector.lean1,275 lines
Bondy/RequiredResidual/RepairedThetaLowSpecialCoveredData.lean445 lines
Bondy/RequiredResidual/RepairedThetaLowSpecialDeficiency.lean604 lines
Bondy/RequiredResidual/RepairedThetaLowSpecialDensity.lean326 lines
Bondy/RequiredResidual/RepairedThetaLowSpecialInterpolation.lean234 lines
Bondy/RequiredResidual/RepairedThetaLowSpecialProtectedRunParametric.lean253 lines
Bondy/RequiredResidual/RepairedThetaNonSpecialConnector.lean258 lines
Bondy/RequiredResidual/RepairedThetaNonSpecialExit.lean548 lines
Bondy/RequiredResidual/RepairedThetaOutcome.lean347 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionConnector.lean841 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionI1.lean1,089 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionI1MixedCase32.lean3,389 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionI1Moving.lean8,873 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionI1Stationary.lean1,231 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionI3.lean273 lines
Bondy/RequiredResidual/RepairedThetaPlainCollisionLowerBound.lean315 lines
Bondy/RequiredResidual/RepairedThetaProtectedRunParametric.lean220 lines
Bondy/RequiredResidual/RepairedThetaProtectedRunSurplus.lean635 lines
Bondy/RequiredResidual/RepairedThetaPureGenericParametric.lean170 lines
Bondy/RequiredResidual/RepairedThetaSaturationConfinement.lean889 lines
Bondy/RequiredResidual/RepairedThetaSpecialCardHigh.lean342 lines
Bondy/RequiredResidual/RepairedThetaSpecialClassification.lean99 lines
Bondy/RequiredResidual/RepairedThetaSpreading.lean187 lines
Bondy/RequiredResidual/RepairedThetaStationaryWitness.lean51 lines
Bondy/RequiredResidual/RepairedThetaTopHallHighAdapter.lean796 lines
Bondy/RequiredResidual/RepairedThetaTopHallI1Assembler.lean79 lines
Bondy/RequiredResidual/RepairedThetaTraceExtraction.lean554 lines
Bondy/RequiredResidual/RepairedThetaTransformedPathProvenance.lean1,190 lines
Bondy/RequiredResidual/RepairedThetaWeakA2.lean1,434 lines
Bondy/RequiredResidual/ResidualComponentSeparation.lean66 lines
Bondy/RequiredResidual/ResidualCyclicCarrier.lean372 lines
Bondy/RequiredResidual/ResidualGCycle.lean131 lines
Bondy/RequiredResidual/ResidualHighBoundary.lean103 lines
Bondy/RequiredResidual/ResidualLinkageEnumeration.lean565 lines
Bondy/RequiredResidual/ResidualLinkageSplice.lean603 lines
Bondy/RequiredResidual/ResidualMaximum.lean117 lines
Bondy/RequiredResidual/SetLinkage.lean72 lines
Bondy/RequiredResidual/SetLinkageContactWord.lean333 lines
Bondy/RequiredResidual/SetLinkageFamilySelection.lean342 lines
Bondy/RequiredResidual/SetLinkageMap.lean124 lines
Bondy/RequiredResidual/SetLinkageSeparation.lean272 lines
Bondy/RequiredResidual/SetMenger.lean704 lines
Bondy/RequiredResidual/SetMengerContraction.lean934 lines
Bondy/RequiredResidual/SetMengerLinkage.lean273 lines
Bondy/RequiredResidual/TerminalRouteFamilyConnectivity.lean212 lines
Bondy/RequiredResidual/TerminalRouteFamilySelection.lean229 lines
Bondy/RequiredResidual/ThetaSpecialSaturation.lean177 lines

Source hashMatches checked record

Lean buildPassed in recorded evidence

LicenseApache-2.0 · Lech Mazur

Provenance and reproducibility

Exact checked source, with reuse terms

The endpoint and every listed local import come from the exact recorded Git commit, and the endpoint matches the stored source hash byte for byte. The locally authored package material is licensed under Apache-2.0 by Lech Mazur; Mathlib and cited third-party material remain under their own terms. Machine-readable checker evidence is included.