Lemma 15: tau_le_8_cycle4 - MAIN THEOREM: τ ≤ 8 for cycle_4

[kavanaghpatrick]

Theorem Statement

For any graph G with ν(G) = 4 in cycle_4 configuration, τ(G) ≤ 8.

Formal Statement (Lean)

theorem tau_le_8_cycle4
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (M : Finset (Finset V)) (hM : isMaxPacking G M) (hM4 : M.card = 4)
    (hMaximal : ∀ T, isTriangle G T → T ∉ M → ∃ A ∈ M, sharesEdge T A)
    (cfg : Cycle4Config V) (hM_eq : M = {cfg.A, cfg.B, cfg.C, cfg.D})
    (hG_triangles : ∀ A ∈ M, isTriangle G A) :
    ∃ cover : Finset (Sym2 V), cover.card ≤ 8 ∧ 
      (∀ T, isTriangle G T → ∃ e ∈ cover, e ∈ T.sym2) := by
  -- Get fan apexes (Lemma 4)
  obtain ⟨x_A, hx_A⟩ := fan_apex_exists G M hM hM4 cfg.A ...
  obtain ⟨x_B, hx_B⟩ := fan_apex_exists G M hM hM4 cfg.B ...
  obtain ⟨x_C, hx_C⟩ := fan_apex_exists G M hM hM4 cfg.C ...
  obtain ⟨x_D, hx_D⟩ := fan_apex_exists G M hM hM4 cfg.D ...
  -- Construct cover
  use eightEdgeCover cfg x_A x_B x_C x_D
  constructor
  · -- Size bound (Lemma 12)
    exact eight_edges_card ...
  · -- Coverage (Lemmas 11, 13, 14)
    intro T hT
    rcases all_triangles_M_or_external ... with hT_M | ⟨A, hA, hT_ext⟩
    · exact cover_hits_all_M_elements ...
    · exact cover_hits_all_externals ...

Why It Should Be True

This assembles all the previous lemmas:

1. Fan apexes exist (Lemma 4)
2. Cover has size 8 (Lemma 12)
3. All triangles are M or external (Lemma 11)
4. Cover hits all M-elements (Lemma 13)
5. Cover hits all externals (Lemma 14)

How It Helps

This IS the main theorem - proving τ ≤ 2ν for the cycle_4 case of ν = 4.

Dependencies

• ALL previous lemmas (1-14)
• This is the final assembly

Notes

This proves Tuza's conjecture for the hardest remaining case of ν = 4. Combined with the other 6 cases (star, path, scattered, etc.), this completes the proof for ν = 4.