totalSolidAngle
plain-language theorem explainer
The declaration defines the total solid angle in three dimensions as 4π steradians. Researchers deriving lepton generation steps or the 1/(4π) factor in mass ratios cite it to normalize the integrated coupling over all directions. The definition is a direct assignment to the standard surface measure on the unit sphere in R³, with the accompanying comment identifying the differential-geometry identity 2π^{3/2}/Γ(3/2).
Claim. The total solid angle subtended by the unit sphere in three-dimensional Euclidean space equals $4π$ steradians.
background
Recognition Science fixes D=3 spatial dimensions at T8 of the forcing chain. The present module derives the 1/(4π) term that appears in the lepton generation step step_e_mu = E_passive + 1/(4π) - α² by separating discrete edge counting from continuous spherical averaging. Passive edges (11) contribute to the integrated α seed while the single active edge contributes the differential fractional step. Upstream results supply the J-cost structure (PhiForcingDerived.of) and the seven-axiom reduction to four structural conditions (PrimitiveDistinction.from).
proof idea
One-line definition that directly assigns 4 * Real.pi. The attached comment recalls the standard evaluation S² = 2π^{3/2}/Γ(3/2) = 4π without invoking any Recognition-specific lemmas.
why it matters
This definition supplies the geometric factor used by alphaSeed := totalSolidAngle * passiveEdgeCount and by fractionalSolidAngle := 1/totalSolidAngle. It therefore enters the main theorem fractional_step_is_forced, which isolates the active-edge contribution (activeEdgeCount / totalSolidAngle) as the forced 1/(4π) term. The construction links the eight-tick octave and D=3 directly to the observed lepton mass hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.