`twelve_is_D_4`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.CardinalitySpectrum on GitHub at line 61.

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

  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
  86
  87/-- 256 = 2⁸ = power set of Q₃. -/
  88theorem twoFiftySix_is_power_of_2cube : (256 : ℕ) = 2 ^ (2^3) := by decide
  89
  90/-- 360 = 8·45 (full turn = tick × gap). -/
  91theorem threeSixty_is_tick_gap : (360 : ℕ) = eightTick * gap45 := by decide

papers checked against this theorem

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