AlonTarsi.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 1 contain sorry, 0 declared as axioms

The Alon-Tarsi short cycle cover conjecture

References:

[AlTa85] Alon, N. and Tarsi, M., Covering multigraphs by simple circuits. SIAM J. Algebraic Discrete Methods (1985), 345--350.
arxiv/2607.06396 Some new results on Sylvester colorings of cubic graphs by Luca Ferrarini, Vahan Mkrtchyan, where this is Conjecture 4.

Every bridgeless graph has a list of cycles covering every edge whose lengths sum to at most $\frac{7}{5}|E|$.

Imports (1)

FormalConjecturesUtil

def Arxiv.«2607.06396».IsCycleCover C covers G: every edge of G lies on at least one cycle of C line 43 source
Source documentation
C covers G: every edge of G lies on at least one cycle of C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Multiset, SimpleGraph.Cycle
Proof uses: Sym2, Membership.mem, Finset, SimpleGraph.edgeFinset, Exists, And, List, SimpleGraph.Cycle.edges
6 instances, coercions and auxiliary constants left out.
```
def IsCycleCover (G : SimpleGraph V) [DecidableRel G.Adj] (C : Multiset (Cycle G)) : Prop :=
…
```
def Arxiv.«2607.06396».totalLength The total length of a family of cycles line 47 source
Source documentation
The total length of a family of cycles.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Multiset, SimpleGraph.Cycle, Nat
Proof uses: Multiset.sum, Multiset.map, SimpleGraph.Cycle.length
1 instances, coercions and auxiliary constants left out.
```
def totalLength {G : SimpleGraph V} (C : Multiset (Cycle G)) : ℕ := (C.map SimpleGraph.Cycle.length).sum
…
```
Mentions: SimpleGraph.Cycle.length
theorem Arxiv.«2607.06396».alon_tarsi_short_cycle_cover Conjecture 4 (Alon-Tarsi, 1985) sorry line 54 source
Source documentation
Conjecture 4 (Alon-Tarsi, 1985). Every bridgeless graph has a list of cycles covering every edge, with $\sum_{C} |E(C)| \leq \frac{7}{5}|E(G)|$.

depends on sorry what this means
Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsBridgeless, Exists, Multiset, SimpleGraph.Cycle, And, Arxiv.«2607.06396».IsCycleCover, LE.le, Rat, Arxiv.«2607.06396».totalLength, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Finset.card and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem alon_tarsi_short_cycle_cover :
    answer(sorry) ↔ ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
      [DecidableRel G.Adj], G.IsBridgeless →
      ∃ C : Multiset (Cycle G), IsCycleCover G C ∧
        (totalLength C : ℚ) ≤ 7 / 5 * #G.edgeFinset := by
…
```
Mentions: Arxiv.«2607.06396».IsCycleCover, Arxiv.«2607.06396».totalLength
theorem Arxiv.«2607.06396».exists_cover_of_edgeFinset_eq_empty The empty cover works when there are no edges, so the bound is attained with room to spare on edgeless graphs line 65 source
Source documentation
The empty cover works when there are no edges, so the bound is attained with room to spare on edgeless graphs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Finset, Sym2, SimpleGraph.edgeFinset, EmptyCollection.emptyCollection, Exists, Multiset, SimpleGraph.Cycle, And, Arxiv.«2607.06396».IsCycleCover, LE.le, Rat, Arxiv.«2607.06396».totalLength, HMul.hMul, HDiv.hDiv, OfNat.ofNat and 1 more
Proof uses: Exists.intro, And.intro, Membership.mem, absurd, List, SimpleGraph.Cycle.edges, Eq.mp, congrArg, Finset.notMem_empty, of_eq_true, Eq.trans, True, congr, CharP.cast_eq_zero, Nat, MulZeroClass.mul_zero
47 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem exists_cover_of_edgeFinset_eq_empty (G : SimpleGraph V) [DecidableRel G.Adj]
    (h : G.edgeFinset = ∅) :
    ∃ C : Multiset (Cycle G), IsCycleCover G C ∧
      (totalLength C : ℚ) ≤ 7 / 5 * #G.edgeFinset := by
…
```
Mentions: Arxiv.«2607.06396».IsCycleCover, Arxiv.«2607.06396».totalLength
theorem Arxiv.«2607.06396».exists_cover_of_isAcyclic Acyclic bridgeless graphs satisfy the conjecture, with the empty cover line 79 source
Source documentation
Acyclic bridgeless graphs satisfy the conjecture, with the empty cover. In a forest every edge is a bridge, so such a graph has no edges at all.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsAcyclic, SimpleGraph.IsBridgeless, Exists, Multiset, SimpleGraph.Cycle, And, Arxiv.«2607.06396».IsCycleCover, LE.le, Rat, Arxiv.«2607.06396».totalLength, HMul.hMul, HDiv.hDiv, OfNat.ofNat, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: Arxiv.«2607.06396».exists_cover_of_edgeFinset_eq_empty, SimpleGraph.edgeFinset_eq_empty_of_isBridgeless_of_isAcyclic
10 instances, coercions and auxiliary constants left out.
```
theorem exists_cover_of_isAcyclic (G : SimpleGraph V) [DecidableRel G.Adj]
    (hacyc : G.IsAcyclic) (hbr : G.IsBridgeless) :
    ∃ C : Multiset (Cycle G), IsCycleCover G C ∧
      (totalLength C : ℚ) ≤ 7 / 5 * #G.edgeFinset :=
…
```
Mentions: Arxiv.«2607.06396».IsCycleCover, Arxiv.«2607.06396».totalLength
theorem Arxiv.«2607.06396».three_le_length A cycle has at least three edges, so any cover of a graph with an edge has total length at least three line 90 source
Source documentation
A cycle has at least three edges, so any cover of a graph with an edge has total length at least three. This is what makes the 7/5 bound a real constraint rather than a formality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, SimpleGraph.Cycle, LE.le, Nat, OfNat.ofNat, SimpleGraph.Cycle.length
Proof uses: SimpleGraph.Walk.IsCircuit.three_le_length, SimpleGraph.Cycle.base, SimpleGraph.Cycle.walk, SimpleGraph.Walk.IsCycle.isCircuit, SimpleGraph.Cycle.isCycle
2 instances, coercions and auxiliary constants left out.
```
theorem three_le_length {G : SimpleGraph V} (c : Cycle G) : 3 ≤ c.length :=
…
```
Mentions: c