Berge–Fulkerson C(24)

Complete Lean proof of C(24), including the class-2 strengthening. Both final theorem targets and their exact axiom audits passed locally on 2026-09-05. No sorry or user-supplied axiom is used. The finite computation uses Lean’s native evaluator and compiler; its trust boundary and recorded evidence are in FORMALIZATION.md.

Let a graph consist of two disjoint simple cycles of equal length, joined by a perfect matching M. If it has a simple M-alternating circuit of length at most 24, it admits six perfect matchings covering every edge exactly twice. The cycle length is unbounded; repeated matchings are allowed.

The formal target is:

C24.c24 : C24.C24Statement

The additional target C24.c24_with_prescribed_matchings specifies that, in class 2, the cover contains both M and M △ E(Q). Both this target and the main existence theorem have passed Lean.

See PROOF.md for the mathematical proof and FORMALIZATION.md for the exact Lean statements and trust boundary.

Verify with Lean

Use the pinned Lean 4.28.0 toolchain. Mathlib 4.28.0 is pinned in the manifest. The scripts require Python 3.9+ on Linux or macOS.

lake exe cache get Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.Data.List.FinRange
lake build

The default build checks the unbounded graph deduction. To check the complete theorem, including all native computations:

python3 verify_lean.py --jobs 4

Equivalently, lake build C24Theorem C24DistinguishedTheorem builds both complete targets. The Python driver bounds the number of simultaneous expensive shards, records logs under out/lean/, and enforces the exact final axiom whitelist. A clean run is a substantial computation; benchmark figures and the recorded run belong in FORMALIZATION.md.

For a partial reproduction:

python3 verify_lean.py --jobs 1 --modules Head1_2

The new k = 12 finite theorem covers 40,874,803,200 states: every D-order beginning with zero and every pair of odd flags. It uses neither domino connectivity nor flag-rotation reduction. The proof is split into 110 twelve-spoke shards. Nine additional shards handle k = 10; smaller cases are in C24MatchingSmall.lean.

No C++ result is imported into Lean. The finite proofs use native_decide, with explicit native-evaluator and compiler trust. The graph deduction and checker-soundness proofs use only the standard logical axioms.

Separate C++ certificate replay

bash verify.sh --jobs 2

This regenerates and replays the original symmetry-reduced length-24 census: 2,831,155,200 states, with 1,048,849,560 four-partition certificates. About 8.4 GB pass through pipes; the binary stream is regenerated instead of committed. The driver then checks 1000 physical lifts and the supplied example. A C++17 compiler is required.

To audit the retained file hashes and logs without recomputing:

python3 verify.py --audit-only
python3 audit_lean_evidence.py

The Lean and C++ state counts differ because their enumeration domains differ. Both are documented explicitly.

Repository layout

• C24Statement.lean, C24Theorem.lean: exact graph statement and final theorem.
• C24Distinguished.lean, C24DistinguishedTheorem.lean: class-2 strengthening and exact symmetric-difference matching.
• C24Assemble.lean and the structural C24*.lean modules: compression, normalization, parity, expansion, and cover assembly.
• C24BoundaryMatching.lean: literal matching-row equations and their soundness.
• C24FastMatching.lean: checked caches, relabeling, bitwise partition verification, and streaming exhaustive coverage.
• C24MatchingSmall.lean, C24MatchingFinite/, C24MatchingFinite.lean: closed finite computations and their assembly.
• exhaustive_local.cpp, replay_certificate.cpp, verify_physical_lifts.py: separate computational evidence.
• logs/, census.json, finite-census.json, SHA256SUMS: recorded evidence and reproducibility metadata.

prepare-finite-workspace.sh creates a finite-only workspace using bundled Std, without Mathlib. The inherited experimental modules C24Finite, C24NativeFinite, and KernelProbe are not dependencies of the final theorem.

The 1026-vertex example has alternating girth exactly 24 for its specified spoke matching. Its six matchings are explicit in example24-cover.json. No claim is made that the example is a snark or falls outside every previously known Berge–Fulkerson class. C(24) remains a sufficient condition, not a proof of the general conjecture.