per_steradian_pos
plain-language theorem explainer
The declaration establishes that the spherical correction factor at three spatial dimensions is strictly positive. Researchers modeling sub-leading lepton mass corrections in Recognition Science would cite it to confirm the sign of the 1/(4π) term in the e to μ transition. The proof reduces the claim to the D=3 specialization via rewriting and applies a positivity tactic.
Claim. In three spatial dimensions the spherical correction factor satisfies $1/(4π) > 0$.
background
The Lepton Sub-Leading Corrections module treats the spherical term as the unique solid-angle normalization in D=3, where the surface area of S² equals 4π, so the per-steradian correction equals 1/(4π). This sits inside the broader lepton generation steps that add perturbative refinements to integer cube counts {E_pass=11, F=6}. Upstream results supply the J-cost convexity from PhysicsComplexityStructure.of and the forcing of exactly three generations from SpectralEmergence.of.
proof idea
The proof is a one-line wrapper that rewrites the expression using the D=3 specialization per_steradian_at_D3 and then applies the positivity tactic.
why it matters
This result secures the sign of the geometric correction required by the module's structural properties for the lepton mass ladder. It aligns with the Recognition Science forcing chain at T8 where D=3 is derived and supports the claim that both corrections remain O(1) or smaller. No downstream uses are recorded, leaving the positivity check as a local closure for numerical bounds on the α² and wallpaper terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.