The Erdős–Gyárfás conjecture

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem GT003 — The Erdős–Gyárfás conjecture

Does every graph with minimum degree three contain a cycle of length a power of two?

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : ∀ (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
    (∀ v : V, 3 ≤ G.degree v) → ∃ k : ℕ, HasCycleLength G (2 ^ k) := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.GT003.Statement

namespace Submission

theorem solution : Conjectura.GT003.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### has a cycle of length `k`

A graph has a cycle of length `k` when some closed walk of that length repeats no vertex or edge. Which cycle lengths a graph must contain is the subject of a large family of extremal questions.

```lean
Conjectura.GraphTheory.HasCycleLength
-- unfolds to:
def HasCycleLength {V : Type*} (G : SimpleGraph V) (k : ℕ) : Prop :=
  ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length = k
```
Defined in this corpus.

### length

The length of a subset $s$ of $\mathbb{C}$ is defined to be its 1-dimensional Hausdorff measure $\mathcal{H}^1(s)$.

```lean
Conjectura.EP0003.length
-- unfolds to:
noncomputable def length (s : Set ℂ) : ℝ≥0∞ := μH[1] s
```
Defined in this corpus.

### Fintype

class

```lean
Fintype
```
Defined in Mathlib.

### Adj

structure

```lean
G.Adj
```
Defined in Mathlib.

### degree

def

```lean
G.degree
```
Defined in Mathlib.

### Walk

inductive

```lean
G.Walk
```
Defined in Mathlib.

### IsCycle

structure

```lean
w.IsCycle
```
Defined in Mathlib.

### Set

abbrev

```lean
Set
```
Defined in Mathlib.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.