theorem
proved
eleven_check
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.CardinalitySpectrum on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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). -/
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