Conway's 99-graph problem

Reference: Wikipedia

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

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

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

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

Equations

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

theorem Conway99Graph.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.

theorem Conway99Graph.triangle_locallyLinear_and_nonEdgesAreDiagonals : (completeGraph (Fin 3)).LocallyLinear ∧ NonEdgesAreDiagonals (completeGraph (Fin 3))

The triangle is an example with 3 vertices satisfying the condition.

def Conway99Graph.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

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

theorem Conway99Graph.conway9_nonEdgesAreDiagonals : NonEdgesAreDiagonals Conway9

theorem Conway99Graph.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}

theorem Conway99Graph.conway9_locallyLinear : Conway9.LocallyLinear