`passive_edges`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaHigherOrder
domain: Constants
line: 74 · 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 74.

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

  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). -/
  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 :

papers checked against this theorem

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