IndisputableMonolith.CrossDomain.CardinalitySpectrum

   1import Mathlib
   2
   3/-!
   4# C21: RS Cardinality Spectrum — Wave 63 Cross-Domain
   5
   6Structural claim: across the RS stack, the cardinalities of canonical
   7domain types fall into a specific spectrum:
   8
   9  {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, ...}
  10
  11These are not arbitrary. Each is reachable by multiplying, summing, or
  12taking powers/combinations of the small cube-generators {2, 3}, the
  13configDim 5, and gap45. This module collects exemplar witnesses.
  14
  15The point: show that RS produces a *structured* numerical spectrum, not
  16a random one. Specifically, every member of the spectrum admits a
  17decomposition into RS primitives.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith.CrossDomain.CardinalitySpectrum
  23
  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. -/
  58theorem ten_is_2_D : (10 : ℕ) = 2 * Dconfig := by decide
  59
  60/-- 12 = 3·4 = D · 2² (cube edges). -/
  61theorem twelve_is_D_4 : (12 : ℕ) = Dspatial * 4 := by decide
  62
  63/-- 15 = 3·5 = 3 nested configDim (planet strata). -/
  64theorem fifteen_is_3_D : (15 : ℕ) = 3 * Dconfig := by decide
  65
  66/-- 16 = 2⁴. -/
  67theorem sixteen_is_2_fourth : (16 : ℕ) = 2^4 := by decide
  68
  69/-- 25 = D². -/
  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
 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
 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
 141  D_cubed := oneTwentyFive_is_Dcubed
 142  D_fifth := threeOne25_is_D_fifth
 143  spectrum_length := rsSpectrum_length
 144  spectrum_pairwise := rsSpectrum_pairwise_lt
 145  spectrum_bounded := rsSpectrum_bounded
 146
 147end IndisputableMonolith.CrossDomain.CardinalitySpectrum
 148