`Q3_vertices`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.CubeSpectrum
domain: Physics
line: 20 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.CubeSpectrum on GitHub at line 20.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  17
  18/-! ## Q₃ Combinatorics -/
  19
  20def Q3_vertices : ℕ := 8
  21def Q3_edges : ℕ := 12
  22def Q3_faces : ℕ := 6
  23def Q3_degree : ℕ := 3
  24
  25theorem Q3_euler : Q3_vertices + Q3_faces = Q3_edges + 2 := by
  26  unfold Q3_vertices Q3_edges Q3_faces; omega
  27
  28theorem Q3_edge_count : Q3_edges = Q3_degree * Q3_vertices / 2 := by
  29  unfold Q3_edges Q3_degree Q3_vertices; omega
  30
  31theorem Q3_vertices_eq : Q3_vertices = 2 ^ Q3_degree := by
  32  unfold Q3_vertices Q3_degree; omega
  33
  34/-! ## Q₃ Laplacian Spectrum
  35
  36The graph Laplacian L = D − A of Q₃ has eigenvalues determined by the
  37Hamming weight of binary vectors in {0,1}³. For vertex v with Hamming
  38weight w(v), the eigenvalue is 2·w(v). The spectrum is:
  39- λ₀ = 0 (multiplicity 1, the all-ones eigenvector)
  40- λ₁ = 2 (multiplicity 3, the three coordinate functions)
  41- λ₂ = 4 (multiplicity 3, the three pairwise products)
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.