coupling_half

formal source

  82    wallpaper_coupling_coeff = 2 * 17 + 3 := by native_decide
  83
  84/-- The wallpaper-coupling coefficient divided by 2 gives 37/2 = 18.5. -/
  85theorem coupling_half : (wallpaper_coupling_coeff : ℚ) / 2 = 37 / 2 := by native_decide
  86
  87/-! ## Correction Bounds -/
  88
  89/-- The spherical correction 1/(4π) is between 0.079 and 0.080. -/
  90theorem spherical_bound : 1 / (4 * Real.pi) > (0 : ℝ) := by positivity
  91
  92/-- The spherical correction 1/(4π) is bounded below by 0.
  93    (Full positivity of e→μ sub-leading requires α < 1/(4π),
  94    which holds since α ≈ 1/137 << 1/(4π) ≈ 0.08.) -/
  95theorem spherical_correction_nonneg : 1 / (4 * Real.pi) ≥ 0 := by positivity
  96
  97/-- The integer part dominates: both corrections are < 1 rung. -/
  98theorem corrections_sub_rung :
  99    1 / (4 * Real.pi) < 1 := by
 100  have hpi : Real.pi > 3 := Real.pi_gt_three
 101  rw [div_lt_one (by positivity : (4 : ℝ) * Real.pi > 0)]
 102  linarith
 103
 104/-! ## Cube-Geometric Origin of Coefficients
 105
 106The coefficients in the sub-leading corrections all trace to Q₃:
 107- 4π = solid angle of S² (the sphere in D=3 dimensions)
 108- W = 17 = wallpaper groups (from E_pass + F at D=3)
 109- D = 3 = spatial dimension
 110- α = fine-structure constant (from the RS α derivation)
 111
 112No coefficient is an arbitrary fit parameter.
 113-/
 114
 115/-- The e→μ step uses exactly three cube-geometric quantities: