  31/-- 12 = 3 × 4 = D × 2^(D-1). -/
  32theorem q3Edges_factored : q3Edges = 3 * 4 := by decide
  33
  34structure GraphTheoryCert where
  35  vertices_8 : q3Vertices = 8
  36  edges_12 : q3Edges = 12
  37  chromatic_2 : q3ChromaticNumber = 2
  38  edges_factored : q3Edges = 3 * 4
  39
  40def graphTheoryCert : GraphTheoryCert where
  41  vertices_8 := q3Vertices_eq
  42  edges_12 := q3Edges_eq
  43  chromatic_2 := q3Chromatic_eq
  44  edges_factored := q3Edges_factored
  45
  46end IndisputableMonolith.Mathematics.GraphTheoryFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.