unitSphereSurface_D2
plain-language theorem explainer
The declaration shows that the surface measure of the unit circle equals 2π. Researchers deriving the fine-structure constant from isotropic coupling cite this base case to isolate the D=3 result. The tactic proof unfolds the general surface-area formula and simplifies via the gamma function at one together with real-power rules.
Claim. The surface area of the unit circle satisfies $S_1 = 2π$, where the general formula is $S_{D-1} = 2π^{D/2}/Γ(D/2)$.
background
The module establishes why the factor 4π appears in the α derivation α^{-1} = 4π·11 - f_gap - δ_κ. It requires isotropic coupling, normalization to the passive-edge count, and D=3 dimensionality. The supporting definition is unitSphereSurface(D) := 2 * π^{D/2} / Γ(D/2), which recovers the circumference 2π when D=2 and the solid angle 4π when D=3.
proof idea
The proof unfolds unitSphereSurface, introduces the normalization (2/2)=1 by norm_num, and applies simp using Real.Gamma_one together with Real.rpow_one.
why it matters
This base case supports the module's uniqueness argument that only the D=3 solid angle supplies the required 4π factor. It contrasts with the sibling unitSphereSurface_D3 and feeds the broader claim that isotropic measure is forced by the Recognition Composition Law and the eight-tick octave. The result touches the alpha-band interval (137.030, 137.039) but leaves open the explicit gap term f_gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.