`six_is_cubeFaces`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CardinalitySpectrum
domain: CrossDomain
line: 49 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.CardinalitySpectrum on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  46theorem five_is_Dconfig : (5 : ℕ) = Dconfig := rfl
  47
  48/-- 6 = 2·3 = cube faces. -/
  49theorem six_is_cubeFaces : (6 : ℕ) = cubeFaces := rfl
  50
  51/-- 7 = 2³ − 1 (working memory). -/
  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

papers checked against this theorem

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