`alphaInv_derived_eq_formula`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaDerivation
domain: Constants
line: 247 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.AlphaDerivation on GitHub at line 247.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 244noncomputable def alphaInv_derived : ℝ := geometric_seed - (f_gap + curvature_term)
 245
 246/-- Main theorem: The derived α⁻¹ matches the formula in Constants.Alpha. -/
 247theorem alphaInv_derived_eq_formula :
 248    alphaInv_derived = 4 * Real.pi * 11 - (f_gap + (-(103 : ℝ) / (102 * Real.pi ^ 5))) := by
 249  simp only [alphaInv_derived, geometric_seed_eq, curvature_term_eq]
 250
 251/-! ## Part 9: Summary Theorems (Closing the Gap) -/
 252
 253/-- The number 11 is not arbitrary: it is the passive edge count of Q₃. -/
 254theorem eleven_is_forced : (11 : ℕ) = cube_edges 3 - 1 := by native_decide
 255
 256/-- The number 103 is not arbitrary: it is 6×17 + 1. -/
 257theorem one_oh_three_is_forced : (103 : ℕ) = 2 * 3 * 17 + 1 := by native_decide
 258
 259/-- The number 102 is not arbitrary: it is 6×17. -/
 260theorem one_oh_two_is_forced : (102 : ℕ) = 2 * 3 * 17 := by native_decide
 261
 262/-- Complete provenance: all magic numbers are derived from D=3 cube geometry. -/
 263theorem alpha_ingredients_from_D3_cube :
 264    geometric_seed_factor = cube_edges D - active_edges_per_tick ∧
 265    seam_numerator D = cube_faces D * wallpaper_groups + euler_closure ∧
 266    seam_denominator D = cube_faces D * wallpaper_groups := by
 267  constructor
 268  · rfl
 269  constructor
 270  · rfl
 271  · rfl
 272
 273end AlphaDerivation
 274end Constants
 275end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.