Lemma 12: eight_edges_well_defined - The 8-edge cover set is well-defined

[kavanaghpatrick]

Theorem Statement

Given a cycle_4 configuration with fan apexes, the 8-edge cover set is well-defined and has cardinality exactly 8 (assuming all edges are distinct).

Formal Statement (Lean)

def eightEdgeCover (cfg : Cycle4Config V) (x_A x_B x_C x_D : V) : Finset (Sym2 V) :=
  -- Cycle edges
  {s(cfg.vDA, cfg.vAB), s(cfg.vAB, cfg.vBC), s(cfg.vBC, cfg.vCD), s(cfg.vCD, cfg.vDA)} ∪
  -- Apex-private edges
  {s(cfg.a, x_A), s(cfg.b, x_B), s(cfg.c, x_C), s(cfg.d, x_D)}

theorem eight_edges_card
    (cfg : Cycle4Config V)
    (x_A x_B x_C x_D : V)
    (hx_distinct : [x_A, x_B, x_C, x_D].Nodup)
    (hx_not_M : x_A ∉ cfg.allMVertices ∧ x_B ∉ cfg.allMVertices ∧ 
                x_C ∉ cfg.allMVertices ∧ x_D ∉ cfg.allMVertices) :
    (eightEdgeCover cfg x_A x_B x_C x_D).card = 8 := by
  sorry

Why It Should Be True

The 8 edges are:

1. {v_DA, v_AB} - cycle edge for A
2. {v_AB, v_BC} - cycle edge for B
3. {v_BC, v_CD} - cycle edge for C
4. {v_CD, v_DA} - cycle edge for D
5. {a, x_A} - apex-private for A
6. {b, x_B} - apex-private for B
7. {c, x_C} - apex-private for C
8. {d, x_D} - apex-private for D

These are pairwise distinct because:

• Cycle edges use different vertex pairs (cfg has 8 distinct vertices)
• Apex-private edges use different private vertices
• No cycle edge equals an apex-private edge (cycle edges are between shared vertices, apex-private involve private vertices)

How It Helps

This establishes the cover set has the claimed size.

Dependencies

• Cycle4Config has 8 distinct vertices
• Fan apexes are outside M-vertices