fractionalSolidAngle
plain-language theorem explainer
This definition sets the fractional solid angle to the reciprocal of the total solid angle 4π. Physicists deriving lepton generation steps from edge counting in the Recognition framework cite it to isolate the differential contribution of one active edge. It is a direct one-line definition that normalizes by the full sphere surface.
Claim. Let Ω denote the total solid angle in three dimensions. The fractional solid angle for a single direction is defined as Ω_f := 1/Ω.
background
In the Recognition framework a recognition event at each tick traverses one active edge while eleven passive edges dress the interaction. The total solid angle is the surface area of the unit 2-sphere in ℝ³, equal to 4π by the standard formula S² = 4π. The module derives the 1/(4π) term that appears in the generation-step formula step_e_mu = E_passive + 1/(4π) - α² from the distinction between integrated coupling (used for α) and differential transition (used for mass ratios).
proof idea
This is a one-line definition that applies the reciprocal directly to the upstream totalSolidAngle definition.
why it matters
The definition supplies the 1/(4π) factor required by generationStepDerived and thereby feeds alpha_step_relationship, fractional_step_is_forced, and same_ingredients. These theorems demonstrate that the same geometric ingredients (D=3 forcing 4π together with 11 passive edges from cube geometry) produce both the α seed via multiplication and the mass step via addition of the fractional term. It closes the structural derivation of the lepton generation formula from first principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.