gap_squared

formal source

  43theorem twoCube_squared : (2 : ℕ)^3 * 2^3 = 64 := by decide
  44theorem twoCube_times_gap : (2 : ℕ)^3 * 45 = 360 := by decide
  45
  46theorem gap_squared : (45 : ℕ) * 45 = 2025 := by decide
  47
  48/-- Full turn: 2³ × 45 = 360 degrees. -/
  49theorem full_turn : (2 : ℕ)^3 * 45 = 360 := twoCube_times_gap
  50
  51/-- Each entry corresponds to a unique integer (no two non-trivial entries
  52    coincide). -/
  53theorem entries_distinct :
  54    25 ≠ 40 ∧ 40 ≠ 64 ∧ 64 ≠ 360 ∧ 360 ≠ 2025 ∧
  55    25 ≠ 64 ∧ 25 ≠ 360 ∧ 25 ≠ 2025 ∧
  56    40 ≠ 360 ∧ 40 ≠ 2025 ∧
  57    64 ≠ 2025 := by
  58  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide
  59
  60/-! ## Pattern combinations across cardinalities. -/
  61
  62/-- D² · 2³ = 200 (D-pair × cube period). -/
  63theorem D_sq_times_cube : (5 : ℕ)^2 * 2^3 = 200 := by decide
  64
  65/-- D · 2⁶ = 320 (D × double-cube). -/
  66theorem D_times_double_cube : (5 : ℕ) * 2^6 = 320 := by decide
  67
  68/-- (2³)² + 2³ = 72 (cube squared + cube; appears in some RS bounds). -/
  69theorem cube_sq_plus_cube : (2 : ℕ)^3 * 2^3 + 2^3 = 72 := by decide
  70
  71/-- D × cube faces = 30 (configDim × cube-face count). -/
  72theorem D_times_cube_faces : (5 : ℕ) * 6 = 30 := by decide
  73
  74/-- D² × cube faces = 150 — a quantity that exceeds gap45 by exactly D²·D - 1·45 = 5·D = 25. -/
  75theorem D_sq_cube_faces_minus_gap : (5 : ℕ)^2 * 6 - 45 = 105 := by decide
  76