Q3_simplex_vertices

formal source

  84
  85/-- The critical simplex vertex count: D + 1 = 4 for D = 3.
  86    This is the structural number that appears in the η₁ correction. -/
  87def Q3_simplex_vertices : ℕ := Q3_degree + 1
  88
  89theorem Q3_simplex_vertices_eq : Q3_simplex_vertices = 4 := by
  90  unfold Q3_simplex_vertices Q3_degree; omega
  91
  92/-! ## Spectral Ratios
  93
  94The ratios of consecutive eigenvalues determine the correction-to-scaling
  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