theorem
proved
passive_edges_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.AlphaHigherOrder on GitHub at line 75.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 :
105 delta_1 = -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension) :=