`Dconfig`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.CardinalitySpectrum on GitHub at line 27.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  24/-! ## Generators (primitive RS numbers) -/
  25
  26def Dspatial : ℕ := 3
  27def Dconfig : ℕ := 5
  28def twoFace : ℕ := 2        -- binary face count
  29def gap45 : ℕ := 45
  30def eightTick : ℕ := 8       -- 2^Dspatial
  31def cubeFaces : ℕ := 6       -- 2 * Dspatial
  32
  33theorem eightTick_eq : eightTick = 2 ^ Dspatial := by decide
  34theorem gap45_eq : gap45 = Dspatial^2 * Dconfig := by decide
  35theorem cubeFaces_eq : cubeFaces = twoFace * Dspatial := by decide
  36
  37/-! ## Spectrum members with RS decompositions -/
  38
  39/-- 3 = D_spatial. -/
  40theorem three_is_Dspatial : (3 : ℕ) = Dspatial := rfl
  41
  42/-- 4 = 2². -/
  43theorem four_is_2sq : (4 : ℕ) = 2^2 := by decide
  44
  45/-- 5 = D_config. -/
  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. -/

papers checked against this theorem

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