solidAngle_is_sphere_area
plain-language theorem explainer
The declaration shows that the solid angle factor equals the surface area of the unit sphere in three dimensions. Derivations of the fine-structure constant in Recognition Science cite it to fix the 4π prefactor in the α inverse expression. The proof is a one-line wrapper that unfolds the solid angle definition and rewrites via the pre-proved D=3 case of the unit sphere surface formula.
Claim. The solid angle in three dimensions equals the surface area of the unit sphere: $4π = 2π^{3/2} / Γ(3/2)$.
background
The module establishes that the geometric seed 4π in the α derivation is the total solid angle for isotropic coupling in D=3. The solid angle is defined directly as 4π. The unit sphere surface is given by the general formula S_{D-1} = 2π^{D/2} / Γ(D/2) for the (D-1)-sphere in ℝ^D. The upstream theorem unitSphereSurface_D3 proves that this formula evaluates to 4π when D=3, using the Gamma function identity Γ(3/2) = √π/2.
proof idea
The proof is a one-line wrapper. It unfolds the solid angle definition to expose 4π, then rewrites the right-hand side via the D=3 unit sphere surface theorem.
why it matters
This result anchors the 4π factor inside the α^{-1} = 4π·11 - f_gap - δ_κ expression required by isotropic coupling and D=3 (T8). It supplies the geometric normalization that feeds the passive-edge count in the ledger. No open scaffolding remains; the equality is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.