theorem
proved
Q3_trace
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CubeSpectrum on GitHub at line 53.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
50theorem Q3_eigenvalue_count : Q3_laplacian_eigenvalues.length = Q3_vertices := by
51 unfold Q3_laplacian_eigenvalues Q3_vertices; native_decide
52
53theorem Q3_trace : Q3_laplacian_eigenvalues.sum = Q3_degree * Q3_vertices := by
54 unfold Q3_laplacian_eigenvalues Q3_degree Q3_vertices; native_decide
55
56theorem Q3_max_eigenvalue_eq : Q3_max_eigenvalue = 2 * Q3_degree := by
57 unfold Q3_max_eigenvalue Q3_degree; omega
58
59/-- The multiplicities are {1, 3, 3, 1} = binomial coefficients C(3,k). -/
60def Q3_multiplicities : List ℕ := [1, 3, 3, 1]
61
62theorem Q3_multiplicities_sum : Q3_multiplicities.sum = Q3_vertices := by
63 unfold Q3_multiplicities Q3_vertices; native_decide
64
65theorem Q3_multiplicities_are_binomial :
66 Q3_multiplicities = [Nat.choose 3 0, Nat.choose 3 1, Nat.choose 3 2, Nat.choose 3 3] := by
67 unfold Q3_multiplicities; native_decide
68
69/-! ## Automorphism Group -/
70
71/-- |Aut(Q₃)| = 48 = |S₃| · |ℤ₂|³ · ... = 2³ · 3! = 8 · 6 = 48.
72 More precisely, Aut(Q_D) = S_D ⋊ ℤ₂^D, order D! · 2^D. -/
73def Q3_aut_order : ℕ := 48
74
75theorem Q3_aut_order_eq : Q3_aut_order = Nat.factorial Q3_degree * 2 ^ Q3_degree := by
76 unfold Q3_aut_order Q3_degree; native_decide
77
78/-- The face-pair count: 2D² = 18 for D = 3.
79 This is the structural number that appears in the η₂ correction. -/
80def Q3_face_pair_count : ℕ := 2 * Q3_degree ^ 2
81
82theorem Q3_face_pair_count_eq : Q3_face_pair_count = 18 := by
83 unfold Q3_face_pair_count Q3_degree; omega