fractionalSolidAngle_eq
plain-language theorem explainer
The equality fixes the fractional solid angle at one over four pi for use in lepton generation steps. Researchers constructing mass ratios between electron and muon generations cite this when normalizing the differential edge contribution against the full sphere. The proof is a one-line term that unfolds the reciprocal definition and applies reflexivity.
Claim. The fractional solid angle, defined as the reciprocal of the total solid angle over the sphere, equals $1/(4π)$.
background
The module derives the $1/(4π)$ term in the lepton generation step formula from the distinction between discrete edge counting and continuous spherical averaging in three dimensions. One active edge drives the transition while eleven passive edges dress the integrated coupling; the alpha formula integrates over the full sphere times the passive count, but the generation step isolates the per-direction fractional contribution. The total solid angle is the surface area of the unit sphere, and the fractional version normalizes it to a single direction.
proof idea
The proof is a one-line wrapper that unfolds the definition of the fractional solid angle as the reciprocal of the total solid angle and the total solid angle as the sphere surface area, then applies reflexivity.
why it matters
This result supplies the normalization constant required for the differential contribution in the generation step formula. It underpins the structural derivation of mass ratios between lepton generations and aligns with the forced three spatial dimensions in the unified forcing chain. The theorem closes the account of the $1/(4π)$ term without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.