theorem
proved
fourColors_eq_DplusOne
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.FourColorTheoremFromRS on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26def fourColors : ℕ := 4
27def spatialDimPlusOne : ℕ := 3 + 1
28
29theorem fourColors_eq_DplusOne : fourColors = spatialDimPlusOne := by decide
30theorem fourColors_eq_2sq : fourColors = 2 ^ 2 := by decide
31
32/-- 4 colors = |F₂²| (2-bit space). -/
33def f2sq_card : ℕ := 2 ^ 2
34theorem four_eq_F2sq : fourColors = f2sq_card := by decide
35
36structure FourColorCert where
37 four_eq_Dp1 : fourColors = spatialDimPlusOne
38 four_eq_2sq : fourColors = 2 ^ 2
39 f2sq : fourColors = f2sq_card
40
41def fourColorCert : FourColorCert where
42 four_eq_Dp1 := fourColors_eq_DplusOne
43 four_eq_2sq := fourColors_eq_2sq
44 f2sq := four_eq_F2sq
45
46end IndisputableMonolith.Mathematics.FourColorTheoremFromRS