pith. machine review for the scientific record. sign in
def

wallpaper_groups

definition
show as:
view math explainer →
module
IndisputableMonolith.Constants.AlphaHigherOrder
domain
Constants
line
78 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 78.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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.