solid_angle
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.
claimLet $Ω(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 in Recognition Science
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.
scope and limits
- Does not derive 4π from Recognition Science axioms.
- Does not compute solid angles for any dimension other than 3.
- Does not prove that 1/(4π) is the unique possible spherical correction.
- Does not address higher-order curvature or non-spherical geometries.
Lean usage
theorem per_steradian_at_D3 : per_steradian 3 = 1 / (4 * Real.pi) := by unfold per_steradian solid_angle; ringformal statement (Lean)
54noncomputable def solid_angle (d : ℕ) : ℝ :=
proof body
Definition body.
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. -/