Department of Redundancy Department
Read the 3-page note ↗

Case CDC-001 · double-checked, literally

Every edge deserves two good loops.

A playful field guide to the Cycle Double Cover proof: turn a bridgeless graph into cubic paperwork, assign tiny XOR gremlins, then watch closed cycles emerge.

The theorem: Every finite bridgeless undirected graph has a collection of cycles covering every edge exactly twice.

Audit a graph Show me the proof

Interactive explainer of the linked note, not an independent verification.

No edge left behind.
Also: no edge left alone.

Warm-up · the planar case

Audit the cube.

A cube has six face-boundary cycles. Stamp the faces and watch each of its twelve edges become exactly twice-covered. This is the friendly planar version of the theorem.

Interactive cube graph Twelve edges show how many selected face cycles cover them: zero, one, or two.

Each badge is an edge’s cycle count. Green “2” = fully chaperoned. Facial boundaries work here because the cube is planar.

The local trick · now with gremlins

No gremlin stands alone.

At a cubic junction, the nowhere-zero flow gives three nonzero 3-bit values with x ⊕ y ⊕ z = 000. The recipe below puts two passengers on each edge so every visible passenger appears exactly twice.

z = x ⊕ y = 011
edge a
edge b
edge c

These are {t, t+x}, {t+x, t+z}, and {t, t+z}. In this world, “+” is XOR.

The whole argument · four moves

Proof, translated from Mathematician.

The cube trick uses faces. The note’s general proof manufactures the same “zero or two at every vertex” behavior even when a graph has no polite planar faces.

  1. MOVE 01 / REDUCE

    Make the graph cubic.

    A standard reduction says it is enough to handle loopless cubic multigraphs. So every junction now has exactly three incident edges.

    general bridgeless G
    → loopless cubic G
    less graph, same problem
  2. MOVE 02 / LABEL

    Issue nonzero 3-bit IDs.

    Use a nowhere-zero flow in Γ = F₂³. At each vertex the incident labels satisfy x + y + z = 0, with addition meaning XOR.

    f(e) ≠ 000
    x ⊕ y ⊕ z = 000
    seven legal gremlins
  3. MOVE 03 / PAIR

    Give every edge two passengers.

    Construct a two-element set Pe so each symbol s appears on either zero or two edges at every vertex. Local pairs are easy; endpoint agreement is the hard bit below.

    |Pe| = 2
    local count(s) ∈ {0, 2}
    strict buddy system
  4. MOVE 04 / SORT

    Follow one passenger.

    For each s, collect edges carrying s. Every vertex has degree zero or two, so that collection is a union of cycles. Each edge carries two symbols, so it appears twice overall.

    Ms = {e : s ∈ Pe}
    degMₛ(v) ∈ {0, 2}
    cycles fall out
The bit that earns the theorem: endpoint couples therapy

The disagreement

The local recipe works at every vertex, but the two ends of an edge may assign it different passenger pairs. Give each vertex a shift tv, and each edge a one-bit “flip” εe. For e = uv, agreement becomes one linear equation:

tu + tv + εef(e) = de

Here de records the original mismatch. Solve all these equations at once and the local pairs glue into globally well-defined Pe’s.

Why a solution exists

Linear duality says the system can fail only if a dual witness η detects d while vanishing on every possible left-hand side. The local flow identities force each vertex’s contribution to equal the parity of its nonzero incident witnesses.

Now sum over all vertices: every nonzero edge witness appears once at each endpoint—twice. Over F₂, twice is zero. So no witness detects d, and the system is solvable.

Judge XOR’s ruling: “The prosecution counted every accusation twice. Case dismissed.”

Every edge gets two cycles. Nobody gets a bridge.

That is the proof’s shape. The paper has the exact bookkeeping in three brisk pages.

Open the serious version ↗