theorem
proved
eight_is_2cube
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.CardinalitySpectrum on GitHub at line 55.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
52theorem seven_is_cube_minus_one : (7 : ℕ) = 2^3 - 1 := by decide
53
54/-- 8 = 2³. -/
55theorem eight_is_2cube : (8 : ℕ) = eightTick := rfl
56
57/-- 10 = 2·5. -/
58theorem ten_is_2_D : (10 : ℕ) = 2 * Dconfig := by decide
59
60/-- 12 = 3·4 = D · 2² (cube edges). -/
61theorem twelve_is_D_4 : (12 : ℕ) = Dspatial * 4 := by decide
62
63/-- 15 = 3·5 = 3 nested configDim (planet strata). -/
64theorem fifteen_is_3_D : (15 : ℕ) = 3 * Dconfig := by decide
65
66/-- 16 = 2⁴. -/
67theorem sixteen_is_2_fourth : (16 : ℕ) = 2^4 := by decide
68
69/-- 25 = D². -/
70theorem twentyfive_is_Dsq : (25 : ℕ) = Dconfig^2 := by decide
71
72/-- 45 = gap. -/
73theorem fortyfive_is_gap : (45 : ℕ) = gap45 := rfl
74
75/-- 64 = 2⁶ = 8·8. -/
76theorem sixtyfour_is_2sixth : (64 : ℕ) = 2^6 := by decide
77
78/-- 70 = C(8,4) = max central binomial. -/
79theorem seventy_is_choose_8_4 : (70 : ℕ) = Nat.choose 8 4 := by decide
80
81/-- 125 = D³. -/
82theorem oneTwentyFive_is_Dcubed : (125 : ℕ) = Dconfig^3 := by decide
83
84/-- 216 = 6³. -/
85theorem twoSixteen_is_six_cubed : (216 : ℕ) = cubeFaces^3 := by decide