`Q3_vertices`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaHigherOrder
domain: Constants
line: 59 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 59.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  56/-! ## Cube Combinatorics -/
  57
  58/-- Vertices of Q₃. -/
  59def Q3_vertices : ℕ := 2^3
  60theorem Q3_vertices_eq : Q3_vertices = 8 := rfl
  61
  62/-- Edges of Q₃. -/
  63def Q3_edges : ℕ := 3 * 2^2
  64theorem Q3_edges_eq : Q3_edges = 12 := rfl
  65
  66/-- Faces of Q₃. -/
  67def Q3_faces : ℕ := 2 * 3
  68theorem Q3_faces_eq : Q3_faces = 6 := rfl
  69
  70/-- Active edges per tick. -/
  71def active_edges : ℕ := 1
  72
  73/-- Passive edges = total - active. -/
  74def passive_edges : ℕ := Q3_edges - active_edges
  75theorem passive_edges_eq : passive_edges = 11 := rfl
  76
  77/-- Number of wallpaper groups (Fedorov 1891). -/
  78def wallpaper_groups : ℕ := 17
  79
  80/-- Face-wallpaper pairs. -/
  81def face_wallpaper_pairs : ℕ := Q3_faces * wallpaper_groups
  82theorem face_wallpaper_pairs_eq : face_wallpaper_pairs = 102 := rfl
  83
  84/-- Curvature numerator: face-wallpaper + active edge (Euler closure). -/
  85def curvature_numerator : ℕ := face_wallpaper_pairs + active_edges
  86theorem curvature_numerator_eq : curvature_numerator = 103 := rfl
  87
  88/-- Integration measure dimension: D + 1 (temporal) + 1 (conservation). -/
  89def measure_dimension : ℕ := 3 + 1 + 1

papers checked against this theorem

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