structure
definition
CrossPatternMatrixCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.CrossPatternMatrix on GitHub at line 101.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
113 D5_2cube := D5_times_2cube
114 twoCube_squared := twoCube_squared
115 full_turn := full_turn
116 gap_squared := gap_squared
117 cube_faces_squared := cube_faces_squared
118 face_pairs_minus_gap_is_D_sq := face_pairs_minus_gap
119 off_diag_count := offDiag_is_two_fourth
120
121end IndisputableMonolith.CrossDomain.CrossPatternMatrix