theorem
proved
Q3_aut_order_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CubeSpectrum on GitHub at line 75.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
84
85/-- The critical simplex vertex count: D + 1 = 4 for D = 3.
86 This is the structural number that appears in the η₁ correction. -/
87def Q3_simplex_vertices : ℕ := Q3_degree + 1
88
89theorem Q3_simplex_vertices_eq : Q3_simplex_vertices = 4 := by
90 unfold Q3_simplex_vertices Q3_degree; omega
91
92/-! ## Spectral Ratios
93
94The ratios of consecutive eigenvalues determine the correction-to-scaling
95structure. The key ratio λ₂/λ₁ = 4/2 = 2 governs the subleading RG eigenvalue.
96-/
97
98theorem Q3_eigenvalue_ratio : Q3_max_eigenvalue / Q3_spectral_gap = Q3_degree := by
99 unfold Q3_max_eigenvalue Q3_spectral_gap Q3_degree; omega
100
101/-! ## Certificate -/
102
103structure Q3Cert where
104 vertices : Q3_vertices = 8
105 edges : Q3_edges = 12