totalSolidAngle_is_sphere_surface
plain-language theorem explainer
The theorem states that the total solid angle equals 4π steradians. Researchers deriving the 1/(4π) term in lepton generation steps cite this when normalizing the differential contribution of the active edge against the integrated passive-edge coupling. The proof is a one-line reflexivity that matches the definition of totalSolidAngle to the standard sphere surface area.
Claim. The total solid angle in three spatial dimensions equals $4π$ steradians.
background
The module derives the 1/(4π) factor in the lepton generation step formula step_e_mu = E_passive + 1/(4π) - α² from the distinction between discrete edge counting and continuous spherical averaging. Passive edges (11) contribute to the integrated coupling over all directions while the active edge supplies the differential mass transition. totalSolidAngle is defined as the surface area of the unit 2-sphere in ℝ³, a standard differential-geometry result given by S² = 2π^(3/2)/Γ(3/2) = 4π. The upstream definition totalSolidAngle : ℝ := 4 * Real.pi supplies the concrete value used here.
proof idea
One-line term proof applying reflexivity directly to the definition of totalSolidAngle.
why it matters
This equality supplies the normalization constant required for the fractional solid angle that appears in the generation-step derivation. It anchors the conversion from the 11 passive edges to the integrated 4π·11 term in the alpha formula while isolating the differential 1/(4π) contribution for the mass ratio. The result is consistent with D = 3 forced by the unified forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.