Q3_laplacian_eigenvalues

formal source

  42- λ₃ = 6 (multiplicity 1, the parity function)
  43-/
  44
  45def Q3_laplacian_eigenvalues : List ℕ := [0, 2, 2, 2, 4, 4, 4, 6]
  46
  47def Q3_spectral_gap : ℕ := 2
  48def Q3_max_eigenvalue : ℕ := 6
  49
  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