`Q3_faces`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 67.

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

  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
  90theorem measure_dimension_eq : measure_dimension = 5 := rfl
  91
  92/-! ## The Three Ingredients -/
  93
  94/-- Geometric seed: 4π × passive_edges. -/
  95def alpha_seed : ℝ := 4 * π * passive_edges
  96
  97/-- Gap weight (from DFT-8 projection — see Constants.GapWeight). -/

papers checked against this theorem

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