 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). -/
 113theorem rsSpectrum_pairwise_lt : rsSpectrum.Pairwise (· < ·) := by decide
 114
 115/-- All RS spectrum members are ≤ 3125 = D⁵. -/
 116theorem rsSpectrum_bounded : ∀ n ∈ rsSpectrum, n ≤ 3125 := by
 117  decide
 118
 119structure CardinalitySpectrumCert where
 120  Dspatial_is_3 : Dspatial = 3
 121  Dconfig_is_5 : Dconfig = 5
 122  gap_as_D : gap45 = Dspatial^2 * Dconfig
 123  eightTick_as_D : eightTick = 2 ^ Dspatial
 124  cubeFaces_as_D : cubeFaces = twoFace * Dspatial
 125  full_turn : (360 : ℕ) = eightTick * gap45
 126  choose_central : (70 : ℕ) = Nat.choose 8 4
 127  D_cubed : (125 : ℕ) = Dconfig^3
 128  D_fifth : (3125 : ℕ) = Dconfig^5
 129  spectrum_length : rsSpectrum.length = 20
 130  spectrum_pairwise : rsSpectrum.Pairwise (· < ·)
 131  spectrum_bounded : ∀ n ∈ rsSpectrum, n ≤ 3125
 132
 133def cardinalitySpectrumCert : CardinalitySpectrumCert where
 134  Dspatial_is_3 := rfl
 135  Dconfig_is_5 := rfl
 136  gap_as_D := gap45_eq
 137  eightTick_as_D := eightTick_eq
 138  cubeFaces_as_D := cubeFaces_eq
 139  full_turn := threeSixty_is_tick_gap
 140  choose_central := seventy_is_choose_8_4

papers checked against this theorem

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