oneTwentyFive_is_Dcubed

formal source

  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
 104
 105/-! ## The spectrum: list of first 20 canonical RS cardinalities. -/
 106
 107def rsSpectrum : List ℕ :=
 108  [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]
 109
 110theorem rsSpectrum_length : rsSpectrum.length = 20 := by decide
 111
 112/-- The spectrum is strictly increasing (pairwise). -/