per_steradian_at_D3
plain-language theorem explainer
The theorem fixes the per-steradian correction at three spatial dimensions to exactly one over four pi. Researchers deriving sub-leading geometric factors in lepton mass ladders cite it to normalize the spherical term in the e-to-mu step. The proof reduces the claim by unfolding the two supporting definitions and applying algebraic normalization.
Claim. In three spatial dimensions the per-steradian correction equals $1/(4π)$.
background
The module derives structural constraints on the sub-leading corrections that appear after the integer cube counts in the lepton ladder. The spherical term is introduced as the inverse solid angle of the two-sphere: solid_angle(3) is defined to be 4π and per_steradian(d) is defined as its reciprocal. Module documentation states that this supplies the unique solid-angle normalization in D=3, with Surface(S²)=4π. Upstream definitions supply the explicit case split in solid_angle and the reciprocal construction in per_steradian.
proof idea
The term-mode proof unfolds per_steradian and solid_angle, then invokes the ring tactic to discharge the resulting algebraic identity.
why it matters
The result anchors the 1/(4π) factor inside the e→μ correction of the lepton sub-leading forcing module. It is invoked directly by the downstream positivity theorem for the spherical correction. Module documentation links the normalization to the D=3 outcome of the unified forcing chain and to the requirement that corrections remain O(1) relative to the integer rung structure. The declaration thereby closes one geometric constraint needed before numerical bounds on the full corrections can be checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.