unitSphereSurface_D3
plain-language theorem explainer
Unit sphere surface area in three dimensions equals four pi. Derivations of the fine structure constant from isotropic recognition coupling cite this to fix the geometric seed. The tactic proof unfolds the general hypersurface formula, evaluates the gamma function at three halves via its recurrence relation, and reduces the resulting algebraic expression to four pi with field simplification and ring tactics.
Claim. The surface area of the unit sphere in three-dimensional Euclidean space satisfies $S_2 = 4π$.
background
The SolidAngleExclusivity module proves that the geometric seed in the fine structure constant derivation must be four pi because it equals the surface area of the unit sphere in three dimensions. The general definition computes this area as two pi to the D over two divided by gamma of D over two. For D set to three this yields exactly four pi, as required by isotropy in the recognition ledger.
proof idea
The proof first unfolds unitSphereSurface. It then proves the gamma identity at three halves by applying the recurrence Gamma(s+1) equals s times Gamma(s) at s equals one half, together with the known value Gamma one half equals square root of pi. A separate calculation shows pi to the three halves equals pi times square root of pi. The main simplification applies these equalities, coerces the natural number three, clears the denominator with field_simp, and finishes with ring.
why it matters
This theorem supplies the concrete value needed by four_pi_unique_for_D3 to conclude that four pi is the unique factor for D equals three. It likewise discharges the rewrite in solidAngle_is_sphere_area. Within the framework it confirms the solid angle term in the alpha seed expression alpha inverse equals four pi times eleven minus gap terms, aligning with the D equals three forcing from the unified chain and the requirement of isotropic coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.