def
definition
solid_angle
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.LeptonSubLeadingForcing on GitHub at line 54.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
51
52/-- The solid angle of S^{D-1} in D dimensions.
53 For D=3: Surface(S²) = 4π. -/
54noncomputable def solid_angle (d : ℕ) : ℝ :=
55 match d with
56 | 3 => 4 * Real.pi
57 | _ => 0 -- placeholder for other dimensions
58
59/-- The "per-steradian" correction is the inverse solid angle. -/
60noncomputable def per_steradian (d : ℕ) : ℝ := 1 / solid_angle d
61
62/-- At D=3: per_steradian = 1/(4π). -/
63theorem per_steradian_at_D3 : per_steradian 3 = 1 / (4 * Real.pi) := by
64 unfold per_steradian solid_angle
65 ring
66
67/-- The spherical correction is positive. -/
68theorem per_steradian_pos : per_steradian 3 > 0 := by
69 rw [per_steradian_at_D3]
70 positivity
71
72/-! ## Structural Properties of the Wallpaper-Coupling Term -/
73
74/-- The wallpaper-coupling coefficient: 2W + D. -/
75def wallpaper_coupling_coeff : ℕ := 2 * wallpaper_groups + D
76
77theorem wallpaper_coupling_coeff_eq : wallpaper_coupling_coeff = 37 := by
78 native_decide
79
80/-- The mu→tau coupling coefficient uses W=17 and D=3. -/
81theorem coupling_coeff_decomposition :
82 wallpaper_coupling_coeff = 2 * 17 + 3 := by native_decide
83
84/-- The wallpaper-coupling coefficient divided by 2 gives 37/2 = 18.5. -/