  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). -/
  98def f_gap (w8 : ℝ) : ℝ := w8 * Real.log φ where
  99  φ := (1 + Real.sqrt 5) / 2
 100
 101/-- First-order curvature correction. -/
 102def delta_1 : ℝ := -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension)
 103
 104theorem delta_1_structure :
 105    delta_1 = -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension) :=
 106  rfl
 107
 108theorem delta_1_numerator : (curvature_numerator : ℕ) = 103 := curvature_numerator_eq

papers checked against this theorem

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