def
definition
per_face_solid_angle
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 136.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
133
134/-- Per-face solid angle: by cubic symmetry, each of the 6 faces
135 subtends equal solid angle 4π/6 = 2π/3 from the cube center. -/
136noncomputable def per_face_solid_angle : ℝ :=
137 solid_angle_Q3 / (cube_faces D : ℝ)
138
139theorem per_face_solid_angle_eq :
140 per_face_solid_angle = 2 * Real.pi / 3 := by
141 have h6 : (cube_faces D : ℝ) = 6 := by exact_mod_cast faces_at_D3
142 simp only [per_face_solid_angle, solid_angle_Q3_eq, h6]; ring
143
144/-- Face solid angles reconstruct the total: 6 × (2π/3) = 4π. -/
145theorem face_solid_angle_sum :
146 (cube_faces D : ℝ) * per_face_solid_angle = 4 * Real.pi := by
147 have h6 : (cube_faces D : ℝ) = 6 := by exact_mod_cast faces_at_D3
148 rw [per_face_solid_angle_eq, h6]; ring
149
150/-! ## Part 4: Geometric Seed Assembly -/
151
152/-- The geometric seed factor is the passive edge count.
153 This is WHERE THE 11 COMES FROM. -/
154def geometric_seed_factor : ℕ := passive_field_edges D
155
156/-- Verify: geometric_seed_factor = 11 -/
157theorem geometric_seed_factor_eq_11 : geometric_seed_factor = 11 := by native_decide
158
159/-- The full geometric seed: Ω(∂Q₃) × E_passive.
160 Both factors derive from Q₃ geometry:
161 - 4π = Gauss-Bonnet total curvature of ∂Q₃ (Part 3)
162 - 11 = cube edges − 1 active edge (Part 2) -/
163noncomputable def geometric_seed : ℝ := solid_angle_Q3 * geometric_seed_factor
164
165/-- The geometric seed equals 4π·11. -/
166theorem geometric_seed_eq : geometric_seed = 4 * Real.pi * 11 := by