solid_angle
plain-language theorem explainer
The solid_angle definition encodes the surface area of the unit sphere in D dimensions, returning exactly 4π when D equals 3. Researchers deriving sub-leading corrections to lepton masses cite it to normalize the spherical term 1/(4π) appearing in the electron-to-muon transition. The implementation is a direct pattern match on the dimension parameter that hard-codes the three-dimensional value and defaults all other cases to zero.
Claim. Let $Ω(d)$ denote the solid angle of the unit sphere $S^{d-1}$ in $d$ dimensions. Then $Ω(3) = 4π$ and $Ω(d) = 0$ for every natural number $d ≠ 3$.
background
The Lepton Sub-Leading Corrections module treats the integer cube counts {E_pass=11, F=6} as the leading structure and isolates geometric corrections of order 1 or smaller. The spherical correction 1/(4π) for the e→μ step is normalized by the surface measure of S² in three dimensions. Upstream results on empirical collision-free programs and simplicial edge lengths supply the broader forcing context, while the module itself records that the integer parts are already proved elsewhere as cube cell counts.
proof idea
The definition is realized by a single pattern match on the input dimension d. The case d=3 returns the literal 4 * Real.pi; every other case returns the placeholder 0.
why it matters
This definition supplies the geometric normalization required by the per_steradian and per_steradian_at_D3 siblings in the same module. It realizes the D=3 spatial dimension forced by the eight-tick octave in the Unified Forcing Chain. The module documentation notes that a complete uniqueness argument for the correction form remains open; the present object only constrains the coefficient via the known surface area.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.