per_steradian
plain-language theorem explainer
The declaration defines the per-steradian factor as the reciprocal of the solid angle in d dimensions. Researchers modeling lepton mass corrections in Recognition Science cite it to normalize the spherical term in the e to mu transition. The definition is a direct one-line wrapper around the solid_angle function.
Claim. Let $S(d)$ denote the solid angle of the unit sphere in $d$ dimensions. The per-steradian correction is defined by $P(d) := 1/S(d)$.
background
In the lepton sub-leading corrections module the integer cube counts for generation steps receive geometric refinements. The solid_angle definition returns 4π for d=3, matching the surface area of the 2-sphere, and returns zero otherwise as a placeholder. The per-steradian term is introduced as its reciprocal to normalize the spherical correction 1/(4π) in the mass formula for the e to μ step.
proof idea
The definition is a one-line wrapper that applies the solid_angle definition by taking its reciprocal.
why it matters
This definition supplies the normalization factor used in per_steradian_at_D3, which establishes the value 1/(4π) at D=3, and in per_steradian_pos, which confirms positivity. It fills the geometric normalization step in the lepton correction structure described in the module, consistent with D=3 fixed at forcing-chain step T8. The open question of full uniqueness of corrections remains outside this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.