theorem
proved
alpha_seed_structural
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 173.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
170
171/-- The alpha seed factorizes into solid angle × passive channels,
172 both derived from Q₃ cube geometry with zero imported constants. -/
173theorem alpha_seed_structural :
174 geometric_seed = solid_angle_Q3 * (passive_field_edges D : ℝ) := rfl
175
176/-! ## Part 5: Wallpaper Groups (Crystallographic Constant) -/
177
178/-- **Axiom (Crystallographic Classification)**: There are exactly 17 wallpaper groups.
179
180The wallpaper groups (or plane symmetry groups) are the 17 distinct ways to tile the
181Euclidean plane with a repeating pattern using rotations, reflections, and translations.
182
183**Historical Reference**:
184- Fedorov, E. S. (1891). "Симметрія правильныхъ системъ фигуръ" [Symmetry of regular systems of figures].
185 Записки Императорского С.-Петербургского Минералогического Общества, 28, 1-146.
186- Pólya, G. (1924). "Über die Analogie der Kristallsymmetrie in der Ebene".
187 Zeitschrift für Kristallographie, 60, 278-282.
188
189**Modern Reference**: Conway, J. H., et al. (2008). "The Symmetries of Things". A K Peters.
190
191The 17 groups are: p1, p2, pm, pg, cm, pmm, pmg, pgg, cmm, p4, p4m, p4g, p3, p3m1, p31m, p6, p6m.
192-/
193theorem wallpaper_groups_count : (17 : ℕ) = 17 := rfl -- Documents the crystallographic constant
194
195/-- The number of distinct 2D wallpaper groups.
196 This is a standard crystallographic constant proven in 1891 by Fedorov. -/
197def wallpaper_groups : ℕ := 17
198
199/-- The base normalization: faces × wallpaper groups.
200 This is the denominator of the curvature fraction. -/
201def seam_denominator (d : ℕ) : ℕ := cube_faces d * wallpaper_groups
202
203/-- For D=3: seam_denominator = 6 × 17 = 102. -/