solidAngle
plain-language theorem explainer
The solid angle in three dimensions is defined as exactly 4π. Researchers deriving the fine-structure constant in Recognition Science cite this to fix the geometric seed factor. The definition is a direct constant assignment that matches the surface area of the unit sphere in D=3.
Claim. The solid angle in three spatial dimensions is defined by the constant assignment $4π$.
background
In Recognition Science the solid angle is the total surface measure of the unit sphere in ℝ³, required by isotropic coupling and normalization to the passive edge count. The module states that this value is forced by D=3 (from the eight-tick octave and T8) together with the general sphere-area formula $S_{D-1}=2π^{D/2}/Γ(D/2)$, which evaluates to 4π when D=3. The definition therefore supplies the geometric seed factor that appears in the α^{-1} expression.
proof idea
The declaration is a direct noncomputable definition that assigns the literal value 4 * Real.pi. No lemmas are invoked and no tactics are executed beyond the constant binding itself.
why it matters
This definition supplies the 4π factor used by the downstream theorem geometric_seed_eq_solidAngle_times_11, which states geometric_seed = solidAngle * 11 and thereby anchors the α derivation. It realizes the isotropic-measure requirement and the D=3 constraint stated in the module doc-comment. The companion theorem solidAngle_is_sphere_area equates the same quantity to unitSphereSurface 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.