D_times_double_cube

formal source

  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
  77/-- Cube faces × cube faces = 36 (face pairings on Q₃). -/
  78theorem cube_faces_squared : (6 : ℕ) * 6 = 36 := by decide
  79
  80/-- 36 + 8 = 44 = 2 · gap45 - 46 (relation between face-pairs and the
  81    gap-45 structure: 36 = gap45 - 9 = 45 - 9 = 45 - D²). -/
  82theorem face_pairs_minus_gap : (45 : ℕ) - 6 * 6 = 9 := by decide
  83
  84/-- 9 = D² (spatial dimension squared). -/
  85theorem nine_is_D_sq : (9 : ℕ) = 3^2 := by decide
  86
  87/-! ## Information-theoretic content. -/
  88
  89/-- The full cross-pattern matrix has 25 entries (5×5 patterns). The
  90    non-trivial off-diagonal entries (excluding J=0 row/col which is null)
  91    are 4×4 = 16. -/
  92def matrixSize : ℕ := 5
  93def offDiagSize : ℕ := 4
  94def offDiagEntries : ℕ := offDiagSize * offDiagSize
  95
  96theorem offDiagEntries_eq : offDiagEntries = 16 := by decide