def
definition
seam_denominator
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 201.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
224
225theorem curvature_fraction_is_103_over_102 :
226 curvature_fraction_num = 103 ∧ curvature_fraction_den = 102 := by
227 constructor <;> native_decide
228
229/-- The full curvature term: -103/(102π⁵).
230 The π⁵ comes from the 5-dimensional integration measure
231 (3 space + 1 time + 1 dual-balance). -/