`Q3_eigenvalue_ratio`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.CubeSpectrum
domain: Physics
line: 98 · 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 98.

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

formal source

  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
 106  faces : Q3_faces = 6
 107  euler : Q3_vertices + Q3_faces = Q3_edges + 2
 108  trace : Q3_laplacian_eigenvalues.sum = Q3_degree * Q3_vertices
 109  aut_order : Q3_aut_order = 48
 110  face_pairs : Q3_face_pair_count = 18
 111  simplex_verts : Q3_simplex_vertices = 4
 112
 113def q3Cert : Q3Cert where
 114  vertices := rfl
 115  edges := rfl
 116  faces := rfl
 117  euler := Q3_euler
 118  trace := Q3_trace
 119  aut_order := rfl
 120  face_pairs := Q3_face_pair_count_eq
 121  simplex_verts := Q3_simplex_vertices_eq
 122
 123end CubeSpectrum
 124end Physics
 125end IndisputableMonolith

papers checked against this theorem

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