`fortyfive_is_gap`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CardinalitySpectrum
domain: CrossDomain
line: 73 · 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 73.

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

formal source

  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
  92
  93/-- 3125 = D⁵. -/
  94theorem threeOne25_is_D_fifth : (3125 : ℕ) = Dconfig^5 := by decide
  95
  96/-! ## Non-primitives (integers that don't decompose cleanly) -/
  97
  98/-- 11 = 2³ + D − 2 is a less-clean decomposition (a prime close to cube). -/
  99theorem eleven_check : (11 : ℕ) ≠ Dconfig ∧ (11 : ℕ) ≠ eightTick := by
 100  refine ⟨?_, ?_⟩ <;> decide
 101
 102/-- 13 = F(7), a Fibonacci number (cleanly interpretable via φ-ladder). -/
 103theorem thirteen_is_fib_7 : (13 : ℕ) = Nat.fib 7 := by decide

papers checked against this theorem

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