face_pairs_minus_gap

formal source

  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
  97
  98/-- 16 = 2⁴ (the off-diagonal entry count is a power of 2). -/
  99theorem offDiag_is_two_fourth : offDiagEntries = 2^4 := by decide
 100
 101structure CrossPatternMatrixCert where
 102  D5_squared : (5 : ℕ) * 5 = 25
 103  D5_2cube : (5 : ℕ) * 2^3 = 40
 104  twoCube_squared : (2 : ℕ)^3 * 2^3 = 64
 105  full_turn : (2 : ℕ)^3 * 45 = 360
 106  gap_squared : (45 : ℕ) * 45 = 2025
 107  cube_faces_squared : (6 : ℕ) * 6 = 36
 108  face_pairs_minus_gap_is_D_sq : (45 : ℕ) - 6 * 6 = 9
 109  off_diag_count : offDiagEntries = 2^4
 110
 111def crossPatternMatrixCert : CrossPatternMatrixCert where
 112  D5_squared := D5_squared