theorem
proved
hyperoctahedral_D3
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.CubicSymmetryGroupFromRS on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24/-- B₃ order = 2^D × D! at D=3. -/
25def hyperoctahedralOrder (D : ℕ) : ℕ := 2 ^ D * Nat.factorial D
26
27theorem hyperoctahedral_D3 : hyperoctahedralOrder 3 = 48 := by decide
28
29/-- The (3,2,1) subgroup rank structure. -/
30def rankDecomposition : List ℕ := [3, 2, 1]
31theorem rank_sum : rankDecomposition.sum = 6 := by decide
32theorem rank_length : rankDecomposition.length = 3 := by decide
33
34structure CubicSymmetryCert where
35 b3_order : b3Order = 48
36 hyperoctahedral : hyperoctahedralOrder 3 = 48
37 rank_sum : rankDecomposition.sum = 6
38
39def cubicSymmetryCert : CubicSymmetryCert where
40 b3_order := b3Order_eq_48
41 hyperoctahedral := hyperoctahedral_D3
42 rank_sum := rank_sum
43
44end IndisputableMonolith.Mathematics.CubicSymmetryGroupFromRS