Q3_max_eigenvalue_eq

formal source

  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
  84
  85/-- The critical simplex vertex count: D + 1 = 4 for D = 3.
  86    This is the structural number that appears in the η₁ correction. -/