# P3062: Cycle Double Cover Conjecture

- ID: `P3062`
- Reference: `cycle-double-cover-conjecture`
- Page: https://theoremdb.org/statements/P3062
- Record maturity: Reviewed problem with recorded work

## Problem

Prove that every finite bridgeless loopless undirected multigraph admits a cycle double cover: a finite multiset of cycles in which every labelled edge occurs exactly \(2\) times, counting multiplicity.

### Context

A cycle double cover represents two copies of every edge as a multiset of cycles. The problem allows parallel edges and disconnected graphs while excluding bridges and loops.

### Problem setup

- **Definition (Cycle double cover).** A finite multiset of cycles in which each labelled edge has total multiplicity exactly two.
- **Convention.** Graphs may be disconnected and may have parallel edges. They are finite and loopless.

### What counts as a solution

- For every finite bridgeless loopless undirected multigraph, produce a finite multiset of cycles such that each labelled edge has total multiplicity exactly two.
- A formal certificate must pin the graph model, theorem endpoint, Lean version, mathlib revision, source revision, and axiom audit.

## The answer

The 2026 proof turns a nowhere-zero flow over the three-dimensional vector space over the two-element field into a family of cycles covering every edge twice. [1](#reference-1) [2](#reference-2) [3](#reference-3)

**Review status:** Supported.

**Lean verification:** not Lean-verified.

### Resolution argument

The standard reduction lets us work with a loopless cubic multigraph. Give it a nowhere-zero flow f with values in Gamma = F_2^3, whose existence follows from the Jaeger-Kilpatrick eight-flow theorem and Tutte's group-flow theorem. At a cubic vertex, write the three nonzero incident values as x, y, z, so x + y + z = 0. Choose local offsets g_(v,e) so that, after any common translation t_v, the two-element sets {t_v + g_(v,e), t_v + g_(v,e) + f(e)} have a parity property: each element of Gamma occurs on zero or two incident edges.

The local pairs must agree at the two ends of every edge. For e = uv, this is equivalent to finding vertex translations t_v in Gamma and bits epsilon_e in F_2 satisfying t_u + t_v + epsilon_e f(e) = g_(u,e) + g_(v,e). Regard the left side as a linear map L. A dual obstruction is a family of linear functionals eta_e in Gamma* with eta_e(f(e)) = 0 and the sum of eta_e over edges incident to v equal to 0 at each vertex. The local cubic calculation shows that the sum of eta_e(g_(v,e)) over incident edges is the parity of the nonzero incident eta_e. Summing over vertices counts each nonzero edge functional twice, so every obstruction annihilates the right side. Linear duality therefore gives the required t_v and epsilon_e.

Define the common edge pair P_e using either endpoint. For each s in Gamma, take the edges whose pair contains s. Every vertex has degree zero or two in this edge set, so it is a disjoint union of cycles. Each edge belongs to exactly two of these eight edge sets because P_e has two elements. Taking all cycle components with multiplicity gives a cycle double cover. The cubic reduction carries the cover back to the original bridgeless graph.

## Work

### Proof and evidence for the resolution

**Proposition 1 (Every finite bridgeless graph has a cycle double cover).** The 2026 proof turns a nowhere-zero flow over the three-dimensional vector space over the two-element field into a family of cycles covering every edge twice.

The standard reduction lets us work with a loopless cubic multigraph. Give it a nowhere-zero flow f with values in Gamma = F_2^3, whose existence follows from the Jaeger-Kilpatrick eight-flow theorem and Tutte's group-flow theorem. At a cubic vertex, write the three nonzero incident values as x, y, z, so x + y + z = 0. Choose local offsets g_(v,e) so that, after any common translation t_v, the two-element sets {t_v + g_(v,e), t_v + g_(v,e) + f(e)} have a parity property: each element of Gamma occurs on zero or two incident edges.

The local pairs must agree at the two ends of every edge. For e = uv, this is equivalent to finding vertex translations t_v in Gamma and bits epsilon_e in F_2 satisfying t_u + t_v + epsilon_e f(e) = g_(u,e) + g_(v,e). Regard the left side as a linear map L. A dual obstruction is a family of linear functionals eta_e in Gamma* with eta_e(f(e)) = 0 and the sum of eta_e over edges incident to v equal to 0 at each vertex. The local cubic calculation shows that the sum of eta_e(g_(v,e)) over incident edges is the parity of the nonzero incident eta_e. Summing over vertices counts each nonzero edge functional twice, so every obstruction annihilates the right side. Linear duality therefore gives the required t_v and epsilon_e.

Define the common edge pair P_e using either endpoint. For each s in Gamma, take the edges whose pair contains s. Every vertex has degree zero or two in this edge set, so it is a disjoint union of cycles. Each edge belongs to exactly two of these eight edge sets because P_e has two elements. Taking all cycle components with multiplicity gives a cycle double cover. The cubic reduction carries the cover back to the original bridgeless graph.

### Background and intake notes

- Original intake status: RESOLVED in July 2026 by the proof published by OpenAI. Independent expositions by Jim Geelen and Sang-il Oum were checked, and a public Lean formalization exists at a pinned commit.
- The primary preprint says the proof was entirely due to GPT-5.6 Sol Ultra and the writeup was prepared with Codex using GPT-5.6 Sol.
- The public Lean endpoint covers finite loopless bridgeless multigraphs, allows parallel edges, and does not assume connectedness.
- The pinned Lean repository records a clean upstream build and an axiom audit. TheoremDB has not yet rerun that source in its controlled verifier.

### Formalizations

- **Formalization 1** (reported): A public Lean 4.31.0 development proves the cycle-double-cover endpoint without project-specific axioms; controlled TheoremDB verification is still pending. [4](#reference-4)

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `cycle-double-cover-conjecture`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

120 declarations, with 0 open proof obligations.

### CDCLean.cycleDoubleCover_of_bridgeless

- State: source contains no sorry; verification pending
- Role: target declaration
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.FiniteGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.cycleDoubleCover_of_gammaFlow`, `CDCLean.CubicGraph.toFiniteGraph`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.CycleDoubleCover`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.NowhereZeroFlow`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.cubicExpansion`, `CDCLean.FiniteGraph.cubicExpansion_bridgeless`, `CDCLean.FiniteGraph.jaegerKilpatrickEightFlow`, `CDCLean.FiniteGraph.rotationSystemOfBridgeless`

```lean
theorem CDCLean.cycleDoubleCover_of_bridgeless
    {V E : Type u} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E]
    (G : FiniteGraph V E) (hb : G.Bridgeless) :
    Nonempty G.CycleDoubleCover
```

### CDCLean.FiniteGraph

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph.mk`

### CDCLean.CubicGraph

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph.mk`

### CDCLean.Gamma

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.F₂`

### CDCLean.F₂

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.HalfEdge

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.RotationSystem

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.RotationSystem.mk`

### CDCLean.FiniteGraph.ExpandedEdge

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.HalfEdge`

### CDCLean.FiniteGraph.ExpandedVertex

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.HalfEdge`

### CDCLean.FiniteGraph.Bridgeless

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.cut`

### CDCLean.FiniteGraph.NowhereZeroFlow

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.NowhereZeroFlow.mk`

### CDCLean.CubicGraph.toFiniteGraph

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.FiniteGraph`, `CDCLean.CubicGraph.endAt`, `CDCLean.CubicGraph.loopless`, `CDCLean.FiniteGraph.mk`

### CDCLean.FiniteGraph.cubicExpansion

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.FiniteGraph`, `CDCLean.CubicGraph.mk`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.expansionIncidence`, `CDCLean.FiniteGraph.cubicExpansion._proof_1`

### CDCLean.FiniteGraph.CycleDoubleCover

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.CycleDoubleCover.mk`

### CDCLean.cycleDoubleCover_of_gammaFlow

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.FiniteGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.IndexedEvenDoubleCover`, `CDCLean.cubic_even_double_cover`, `CDCLean.CubicGraph.gammaFlowOfNowhereZero`, `CDCLean.CubicGraph.toFiniteGraph`, `CDCLean.FiniteGraph.CycleDoubleCover`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover`, `CDCLean.FiniteGraph.NowhereZeroFlow`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.cubicExpansion`, `CDCLean.FiniteGraph.projectEvenDoubleCover`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover`

### CDCLean.FiniteGraph.cubicExpansion_bridgeless

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.CubicGraph.toFiniteGraph`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.cubicExpansion`, `CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq`, `CDCLean.FiniteGraph.expansionGraph`, `CDCLean.FiniteGraph.expansionGraph_bridgeless`

### CDCLean.FiniteGraph.jaegerKilpatrickEightFlow

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.NowhereZeroFlow`, `CDCLean.FiniteGraph.endAt`, `CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty`, `CDCLean.FiniteGraph.Crosses._proof_1`, `CDCLean.FiniteGraph.NowhereZeroFlow.mk`

### CDCLean.FiniteGraph.rotationSystemOfBridgeless

- State: source contains no sorry; verification pending
- Role: dependency depth 1
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.degree_ne_one_of_bridgeless`, `CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne`

### CDCLean.FiniteGraph.endAt

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`

### CDCLean.FiniteGraph.Crosses._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.IndexedEvenDoubleCover

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.IndexedEvenDoubleCover.mk`

### CDCLean.FiniteGraph.cut

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.Crosses`

### CDCLean.FiniteGraph.expansionGraph

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.mk`, `CDCLean.FiniteGraph.RotationSystem.next`, `CDCLean.FiniteGraph.expansionGraph._proof_1`, `CDCLean.FiniteGraph.expansionGraph.match_1`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_2`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.mk`

### CDCLean.FiniteGraph.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`

### CDCLean.FiniteGraph.NowhereZeroFlow.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.IsFlow`, `CDCLean.FiniteGraph.IsNowhereZero`, `CDCLean.FiniteGraph.NowhereZeroFlow`

### CDCLean.CubicGraph.endAt

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.CubicGraph.incidence`

### CDCLean.CubicGraph.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`

### CDCLean.FiniteGraph.CycleDoubleCover.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.Cycle`, `CDCLean.FiniteGraph.CycleDoubleCover`, `CDCLean.FiniteGraph.Cycle.edges`

### CDCLean.FiniteGraph.expansionIncidence

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.RotationSystem`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionFromEnd`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansion_left_inverse`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansion_right_inverse`

### CDCLean.FiniteGraph.RotationSystem.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.vertex`

### CDCLean.cubic_even_double_cover

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.CubicLabeling`, `CDCLean.Gamma`, `CDCLean.GammaFlow`, `CDCLean.IndexedEvenDoubleCover`, `CDCLean.cubic_labeling`, `CDCLean.pairIndicator`, `CDCLean.CubicLabeling.base`, `CDCLean.CubicLabeling.vertexParity`, `CDCLean.GammaFlow.val`, `CDCLean.IndexedEvenDoubleCover.mk`, `CDCLean.cubic_even_double_cover._proof_2`

### CDCLean.CubicGraph.gammaFlowOfNowhereZero

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.GammaFlow`, `CDCLean.CubicGraph.toFiniteGraph`, `CDCLean.FiniteGraph.NowhereZeroFlow`, `CDCLean.GammaFlow.mk`, `CDCLean.CubicGraph.gammaFlowOfNowhereZero._proof_1`, `CDCLean.CubicGraph.gammaFlowOfNowhereZero._proof_2`, `CDCLean.FiniteGraph.NowhereZeroFlow.val`

### CDCLean.CubicGraph.loopless

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.CubicGraph.incidence`

### CDCLean.FiniteGraph.cubicExpansion_toFiniteGraph_eq

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.CubicGraph.toFiniteGraph`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.cubicExpansion`, `CDCLean.FiniteGraph.endAt`, `CDCLean.FiniteGraph.expansionGraph`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.finiteGraph_eq_of_endAt_eq`

### CDCLean.FiniteGraph.cubicExpansion._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.expansionIncidence`, `CDCLean.FiniteGraph.RotationSystem.next`, `CDCLean.FiniteGraph.RotationSystem.next_ne`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_1`, `_private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_2`

### CDCLean.FiniteGraph.degree_ne_one_of_bridgeless

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.Crosses`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.cut`, `CDCLean.FiniteGraph.degree`, `CDCLean.FiniteGraph.endAt`, `CDCLean.FiniteGraph.halfEdgesAt`, `CDCLean.FiniteGraph.instFintypeHalfEdgesAt`, `CDCLean.FiniteGraph.loopless`, `CDCLean.FiniteGraph.vertex`, `CDCLean.FiniteGraph.Crosses._proof_1`, `CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._proof_1_6`, `CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_2`, `CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_3`, `CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_4`

### CDCLean.FiniteGraph.expansionGraph_bridgeless

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.F₂`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.Crosses`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.cut`, `CDCLean.FiniteGraph.endAt`, `CDCLean.FiniteGraph.expansionGraph`, `CDCLean.FiniteGraph.expansionGraph_ring_endAt_one`, `CDCLean.FiniteGraph.expansionGraph_ring_endAt_zero`, `CDCLean.FiniteGraph.expansionGraph_spoke_endAt`, `CDCLean.FiniteGraph.vertex`, `CDCLean.FiniteGraph.Crosses._proof_1`, `CDCLean.FiniteGraph.RotationSystem.fiberTransitive`, `CDCLean.FiniteGraph.RotationSystem.next`, `CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_3`, `CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_4`, `CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_5`, `CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_6`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.FiniteGraph.Cycle`, `CDCLean.FiniteGraph.CycleDoubleCover`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover`, `CDCLean.FiniteGraph.Cycle.edges`, `CDCLean.FiniteGraph.CycleDoubleCover.mk`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.support`, `CDCLean.FiniteGraph.edgeIncidence._proof_1`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_1`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_2`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_3`

### CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_of_nonempty

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.FiniteGraph.Bridgeless`, `CDCLean.FiniteGraph.ComponentEdge`, `CDCLean.FiniteGraph.ComponentVertex`, `CDCLean.FiniteGraph.NowhereZeroFlow`, `CDCLean.FiniteGraph.componentEdgeFintype`, `CDCLean.FiniteGraph.componentGraph`, `CDCLean.FiniteGraph.componentGraph_bridgeless`, `CDCLean.FiniteGraph.componentGraph_connects_univ`, `CDCLean.FiniteGraph.componentSetoid`, `CDCLean.FiniteGraph.componentVertexFintype`, `CDCLean.FiniteGraph.component_eq_of_endAt_eq`, `CDCLean.FiniteGraph.endAt`, `CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_connected`, `CDCLean.FiniteGraph.Crosses._proof_1`, `CDCLean.FiniteGraph.NowhereZeroFlow.conservation`, `CDCLean.FiniteGraph.NowhereZeroFlow.mk`, `CDCLean.FiniteGraph.NowhereZeroFlow.nowhereZero`, `CDCLean.FiniteGraph.NowhereZeroFlow.val`, `CDCLean.FiniteGraph.componentGraph._proof_1`, `CDCLean.FiniteGraph.componentGraph._proof_2`, `CDCLean.FiniteGraph.doubleGraph._proof_1`

### CDCLean.FiniteGraph.projectEvenDoubleCover

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.Gamma`, `CDCLean.IndexedEvenDoubleCover`, `CDCLean.FiniteGraph.ExpandedEdge`, `CDCLean.FiniteGraph.ExpandedVertex`, `CDCLean.FiniteGraph.HalfEdge`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.cubicExpansion`, `CDCLean.FiniteGraph.projected_vertex_even`, `CDCLean.IndexedEvenDoubleCover.member`, `CDCLean.FiniteGraph.IndexedEvenDoubleCover.mk`, `CDCLean.FiniteGraph.projectEvenDoubleCover._proof_1`

### CDCLean.FiniteGraph.rotationSystemOfDegreeNeOne

- State: source contains no sorry; verification pending
- Role: dependency depth 2
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.FiniteGraph`, `CDCLean.FiniteGraph.RotationSystem`, `CDCLean.FiniteGraph.degree`, `CDCLean.FiniteGraph.rotationPerm`, `CDCLean.FiniteGraph.rotationPerm_fiberTransitive`, `CDCLean.FiniteGraph.rotationPerm_ne`, `CDCLean.FiniteGraph.rotationPerm_sameVertex`, `CDCLean.FiniteGraph.RotationSystem.mk`

### CDCLean.GammaFlow

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.GammaFlow.mk`

### CDCLean.CubicLabeling

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.GammaFlow`, `CDCLean.CubicLabeling.mk`

### CDCLean.FiniteGraph.Crosses

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.RotationSystem.next

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.vertex

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.GammaFlow.val

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.Gamma`, `CDCLean.GammaFlow`

### CDCLean.pairIndicator

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.F₂`, `CDCLean.Gamma`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_2

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.CubicGraph.incidence

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.CubicLabeling.base

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.CubicLabeling`, `CDCLean.Gamma`, `CDCLean.GammaFlow`

### CDCLean.FiniteGraph.Cycle

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.Cycle.edges

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.degree

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.NowhereZeroFlow.val

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.GammaFlow.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.IndexedEvenDoubleCover.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.IndexedEvenDoubleCover`, `CDCLean.CubicGraph.edgeAt`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansion_left_inverse

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansion_right_inverse

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionFromEnd

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.expansionToEnd._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### _private.CDCLean.Expansion.0.CDCLean.FiniteGraph.finiteGraph_eq_of_endAt_eq

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.cubic_even_double_cover._proof_2

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.GammaFlow`

### CDCLean.cubic_labeling

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.CubicLabeling`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.GammaFlow`, `CDCLean.compatibilityMap`, `CDCLean.pairIndicator`, `CDCLean.CubicGraph.endAt`, `CDCLean.CubicLabeling.mk`, `CDCLean.GammaFlow.val`

### CDCLean.CubicGraph.gammaFlowOfNowhereZero._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.CubicGraph.gammaFlowOfNowhereZero._proof_2

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.CubicLabeling.vertexParity

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`
- Depends on: `CDCLean.CubicGraph`, `CDCLean.CubicLabeling`, `CDCLean.F₂`, `CDCLean.Gamma`, `CDCLean.GammaFlow`, `CDCLean.pairIndicator`, `CDCLean.CubicGraph.edgeAt`, `CDCLean.CubicLabeling.base`, `CDCLean.GammaFlow.val`

### CDCLean.FiniteGraph.component_eq_of_endAt_eq

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.ComponentEdge

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentEdgeFintype

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentGraph

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentGraph_bridgeless

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentGraph_connects_univ

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentGraph._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentGraph._proof_2

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentSetoid

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.ComponentVertex

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.componentVertexFintype

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._proof_1_6

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_2

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_3

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.degree_ne_one_of_bridgeless._simp_1_4

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.doubleGraph._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.edgeIncidence._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_3

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_4

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_5

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_bridgeless._simp_1_6

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_ring_endAt_one

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_ring_endAt_zero

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph_spoke_endAt

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.expansionGraph.match_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.halfEdgesAt

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover.support

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_2

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IndexedEvenDoubleCover.toCycleDoubleCover._proof_3

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.instFintypeHalfEdgesAt

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IsFlow

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.IsNowhereZero

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.jaegerKilpatrickEightFlow_connected

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.loopless

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.NowhereZeroFlow.conservation

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.NowhereZeroFlow.nowhereZero

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.projected_vertex_even

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.projectEvenDoubleCover._proof_1

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.rotationPerm

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.rotationPerm_fiberTransitive

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.rotationPerm_ne

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.rotationPerm_sameVertex

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.RotationSystem.fiberTransitive

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.FiniteGraph.RotationSystem.next_ne

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.IndexedEvenDoubleCover.member

- State: source contains no sorry; verification pending
- Role: dependency depth 3
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.CubicGraph.edgeAt

- State: source contains no sorry; verification pending
- Role: dependency depth 4
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.CubicLabeling.mk

- State: source contains no sorry; verification pending
- Role: dependency depth 4
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### CDCLean.compatibilityMap

- State: source contains no sorry; verification pending
- Role: dependency depth 4
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+cdc-lean@577e9d9ea326d520f80672ee69b830bf1d513df5`

### Continue Lean verification

Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.

[Continue Lean verification with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20cycle-double-cover-conjecture%0A%0AExact%20title%3A%20Cycle%20Double%20Cover%20Conjecture%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fcycle-double-cover-conjecture%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>OpenAI, A Proof of the Cycle Double Cover Conjecture, preprint (July 2026). Theorem 1.1 and Statement of AI use, page 1; proof, pages 1-3 https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf
   - Also cited at Theorem 1.1 and Section 2, pages 1-3, cross-checked against the expositions by Geelen and Oum
   - preprint; primary source; July 2026; checked 2026-08-01
   - Source use: original_summary
   - States the theorem, gives the proof, attributes the result to GPT-5.6 Sol Ultra, and credits Codex with GPT-5.6 Sol for the writeup.
   - Source used to formulate or check the problem record.
   - States and proves the theorem, attributes the conjecture to W. T. Tutte, Alon Itai, Michael Rodeh, George Szekeres, and Paul D. Seymour, credits GPT-5.6 Sol Ultra with the proof, and credits Codex with GPT-5.6 Sol for the writeup.
   - Source named by the research packet.
2. <a id="reference-2"></a>Sang-il Oum, A proof of the cycle double cover conjecture by OpenAI: An exposition, arXiv:2607.16356v2 (2026). Abstract and full exposition https://arxiv.org/abs/2607.16356v2
   - preprint; independent_check source; v2; checked 2026-08-01
   - Source use: original_summary
   - Independent human exposition of the proof with accessibility modifications.
3. <a id="reference-3"></a>Jim Geelen, OpenAI's proof of the Cycle Double Cover Theorem, arXiv:2607.15399v1 (2026). Abstract and full exposition https://arxiv.org/abs/2607.15399v1
   - preprint; independent_check source; v1; checked 2026-08-01
   - Source use: original_summary
   - Independent human exposition intended to clarify the proof.
4. <a id="reference-4"></a>Boris Alexeev and Cheuk Hei Chu, cdc-lean, OpenAI, commit 577e9d9ea326d520f80672ee69b830bf1d513df5 (2026). CDCLean/Main.lean, theorem cycleDoubleCover_of_bridgeless; VERIFICATION.md https://github.com/openai/cdc-lean/tree/577e9d9ea326d520f80672ee69b830bf1d513df5
   - Also cited at CDCLean/Main.lean, theorem cycleDoubleCover_of_bridgeless; VERIFICATION.md; contributor commits
   - Also cited at CDCLean/Main.lean theorem CDCLean.cycleDoubleCover_of_bridgeless and VERIFICATION.md
   - software; software source; 577e9d9ea326d520f80672ee69b830bf1d513df5; checked 2026-08-01
   - Source use: citation_only
   - Pinned Lean 4.31.0 formalization and upstream verification record.
5. <a id="reference-5"></a>François Jaeger, A Survey of the Cycle Double Cover Conjecture, in Cycles in Graphs, North-Holland Mathematics Studies 115 (1985), 1-12. Survey; Proposition 4 for the cubic reduction https://doi.org/10.1016/S0304-0208(08)72993-1
   - proceedings_article; reference source
   - Source use: original_summary
   - Historical background and the standard reduction to loopless cubic graphs.
6. <a id="reference-6"></a>Alon Itai and Michael Rodeh, Covering a Graph by Circuits, in Automata, Languages and Programming, LNCS 62 (1978), 289-299. Problem attribution and early formulation https://doi.org/10.1007/3-540-08860-1_21
   - proceedings_article; reference source
   - Source use: citation_only
   - One of the independent historical formulations credited by the proof paper.
7. <a id="reference-7"></a>George Szekeres, Polyhedral Decompositions of Cubic Graphs, Bulletin of the Australian Mathematical Society 8 (1973), 367-387. Page 367 and conjecture attribution https://doi.org/10.1017/S0004972700042660
   - journal_article; reference source
   - Source use: citation_only
   - Historical formulation and the 3-edge-colourable cubic case.
8. <a id="reference-8"></a>Paul D. Seymour, Sums of Circuits, in Graph Theory and Related Topics, Academic Press (1979), 341-355. Conjecture attribution https://www.sciencedirect.com/science/article/pii/B9780121473504500319
   - proceedings_article; reference source
   - Source use: citation_only
   - Historical formulation credited by the proof paper.