theorem
proved
wallpaper_groups_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 193.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
204theorem seam_denominator_at_D3 : seam_denominator D = 102 := by native_decide
205
206/-! ## Part 6: Topological Closure -/
207
208/-- The Euler characteristic contribution for manifold closure.
209 For a closed orientable 3-manifold patched from cubes, this is 1. -/
210def euler_closure : ℕ := 1
211
212/-- The seam numerator: base + closure.
213 This is WHERE 103 COMES FROM. -/
214def seam_numerator (d : ℕ) : ℕ := seam_denominator d + euler_closure
215
216/-- For D=3: seam_numerator = 102 + 1 = 103. -/
217theorem seam_numerator_at_D3 : seam_numerator D = 103 := by native_decide
218
219/-! ## Part 7: Curvature Term Derivation -/
220
221/-- The curvature fraction (without π^5 and sign). -/
222def curvature_fraction_num : ℕ := seam_numerator D
223def curvature_fraction_den : ℕ := seam_denominator D