module module

`IndisputableMonolith.Physics.CubeSpectrum`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.ThermalFixedPoint module_import
IndisputableMonolith.Physics.UniversalityClasses module_import

declarations in this module (25)

def Q3_vertices L20
def Q3_edges L21
def Q3_faces L22
def Q3_degree L23
theorem Q3_euler L25
theorem Q3_edge_count L28
theorem Q3_vertices_eq L31
def Q3_laplacian_eigenvalues L45
def Q3_spectral_gap L47
def Q3_max_eigenvalue L48
theorem Q3_eigenvalue_count L50
theorem Q3_trace L53
theorem Q3_max_eigenvalue_eq L56
def Q3_multiplicities L60
theorem Q3_multiplicities_sum L62
theorem Q3_multiplicities_are_binomial L65
def Q3_aut_order L73
theorem Q3_aut_order_eq L75
def Q3_face_pair_count L80
theorem Q3_face_pair_count_eq L82
def Q3_simplex_vertices L87
theorem Q3_simplex_vertices_eq L89
theorem Q3_eigenvalue_ratio L98
structure Q3Cert L103
def q3Cert L113