unitSphereSurface
plain-language theorem explainer
The declaration supplies the classical formula for the surface area of the unit (D-1)-sphere in D-dimensional Euclidean space. Researchers deriving the fine structure constant in Recognition Science cite it to fix the geometric seed as exactly 4π under isotropic coupling in three dimensions. The definition is a direct transcription of the standard expression 2π^{D/2}/Γ(D/2) with no additional lemmas.
Claim. The surface area of the unit sphere in Euclidean space of dimension D is given by $S_{D-1} = 2π^{D/2} / Γ(D/2)$.
background
The module derives the uniqueness of the 4π factor in the α seed α^{-1} = 4π·11 - f_gap - δ_κ from the requirement of isotropic coupling. The surface area supplies the total solid angle that any rotationally invariant measure on the sphere must integrate to. The formula is the standard hypersurface measure on S^{D-1} expressed via the gamma function.
proof idea
The definition is a direct one-line encoding of the classical formula using the real exponentiation and gamma primitives from the mathematics library. No upstream lemmas from the listed depends_on edges are invoked; the body simply assembles the expression 2 * Real.pi ^ ((D : ℝ) / 2) / Real.Gamma ((D : ℝ) / 2).
why it matters
This definition is invoked by four_pi_unique_for_D3 to conclude that the geometric seed must be exactly 4π when D=3, and by isotropic_measure_unique_principle to establish uniqueness of the Haar measure on the sphere. It supplies the concrete normalization required by the T8 forcing of three spatial dimensions and the isotropic-coupling condition in the α derivation. The module doc-comment explicitly ties the construction to the three physical requirements of isotropy, normalization to the passive edge count, and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.