def
definition
q3Edges
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.GraphTheoryFromRS on GitHub at line 23.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
20namespace IndisputableMonolith.Mathematics.GraphTheoryFromRS
21
22def q3Vertices : ℕ := 2 ^ 3
23def q3Edges : ℕ := 3 * 2 ^ (3 - 1)
24def q3ChromaticNumber : ℕ := 2
25
26theorem q3Vertices_eq : q3Vertices = 8 := by decide
27theorem q3Edges_eq : q3Edges = 12 := by decide
28theorem q3Chromatic_eq : q3ChromaticNumber = 2 := rfl
29theorem q3Bipartite : q3ChromaticNumber = 2 := rfl
30
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