import Mathlib.Data.Fin.Basic

/-!
# Conway's 99-graph problem

The statement uses arbitrary binary relations rather than a particular graph
data structure. Finite cardinalities are represented by injective enumerations
whose ranges are exactly the predicates being counted.
-/

namespace Conway99

/-- An irreflexive, symmetric graph relation. -/
def IsSimple {n : Nat} (G : Fin n → Fin n → Prop) : Prop :=
  (∀ v, ¬G v v) ∧ (∀ u v, G u v ↔ G v u)

/-- Exactly `count` vertices satisfy `P`. -/
def HasCardinality {n : Nat} (count : Nat) (P : Fin n → Prop) : Prop :=
  ∃ elements : Fin count → Fin n,
    Function.Injective elements ∧
      ∀ vertex, P vertex ↔ ∃ index, elements index = vertex

/-- A graph relation has the strongly regular parameters `(n,k,lambda,mu)`. -/
def IsSRG {n : Nat} (k lambda mu : Nat) (G : Fin n → Fin n → Prop) : Prop :=
  IsSimple G ∧
    (∀ vertex, HasCardinality k (G vertex)) ∧
      ∀ u v, u ≠ v →
        (G u v → HasCardinality lambda (fun w => G u w ∧ G v w)) ∧
        (¬G u v → HasCardinality mu (fun w => G u w ∧ G v w))

/-- There exists a strongly regular graph with Conway's parameters. -/
def HasConway99 : Prop :=
  ∃ G : Fin 99 → Fin 99 → Prop, IsSRG 14 1 2 G

/-- The formal nonexistence alternative accepted by the challenge. -/
def NoConway99 : Prop :=
  ¬HasConway99

end Conway99
