Conway's 99-graph problem

Reference: Wikipedia

theorem completeGraphIsClique {V : Type} (s : Finset V) : ⊤.IsClique ↑s

theorem completeGraph_cliqueSet {V : Type} [Fintype V] : ⊤.cliqueSet (Fintype.card V) = {Set.univ.toFinset}

def NonEdgesAreDiagonals {V : Type} (G : SimpleGraph V) : Prop

Each two non-adjacent vertices have exactly two common neighbors.

Equations

• NonEdgesAreDiagonals G = Pairwise fun (i j : V) => ¬G.Adj i j → (G.neighborSet i ∩ G.neighborSet j).ncard = 2

theorem Conway99Graph : (∃ (G : SimpleGraph (Fin 99)), G.LocallyLinear ∧ NonEdgesAreDiagonals G) ↔ sorry

Does there exist an undirected graph with 99 vertices, in which each two adjacent vertices have exactly one common neighbor, and in which each two non-adjacent vertices have exactly two common neighbors? Equivalently, every edge should be part of a unique triangle and every non-adjacent pair should be one of the two diagonals of a unique 4-cycle. The first condition is equivalent to being locally linear.

def Conway9 : SimpleGraph (Fin 3 × Fin 3)

The box product of two triangles is an example with 9 vertices satisfying the condition. (This graph is the complement of the one described in https://vimeo.com/109815595 and it is also isomorphic to it and to the Paley graph and the graph of the 3-3 duoprism)

Equations

• Conway9 = completeGraph (Fin 3) □ completeGraph (Fin 3)

theorem completeGraph_boxProd_completeGraph_cliqueSet : (completeGraph (Fin 3) □ completeGraph (Fin 3)).cliqueSet 3 = {x : Finset (Fin 3 × Fin 3) | ∃ (q : Fin 3), Finset.filter (fun (x : Fin 3 × Fin 3) => ∃ (p : Fin 3), (p, q) = x) Finset.univ = x} ∪ {x : Finset (Fin 3 × Fin 3) | ∃ (q : Fin 3), Finset.filter (fun (x : Fin 3 × Fin 3) => ∃ (p : Fin 3), (q, p) = x) Finset.univ = x}