pith. the verified trust layer for science. sign in
module module high

IndisputableMonolith.Constants.SolidAngleExclusivity

show as:
view Lean formalization →

The SolidAngleExclusivity module defines the surface area of the unit sphere in D dimensions and proves its value equals 4π exclusively for D=3. Researchers deriving the fine-structure constant from cubic ledger geometry cite it to fix the solid-angle factor in electromagnetic couplings. The argument uses the standard gamma-function formula for sphere area together with direct substitution and comparison lemmas for D=2, D=3 and other cases.

claimThe surface area of the unit sphere in $ℝ^D$ is $S_{D-1} = 2π^{D/2}/Γ(D/2)$. This quantity equals $4π$ if and only if $D=3$.

background

Recognition Science fixes constants from the geometry of the cubic ledger Q₃ and the J-cost functional. The upstream Constants module sets the RS-native time quantum τ₀ = 1 tick. The AlphaDerivation module obtains 4π from vertex deficits via the Gauss-Bonnet theorem on that lattice, quoting: “4π from Gauss-Bonnet: Structural derivation via vertex deficits of Q₃”

proof idea

This is a collection of definitions and lemmas rather than a single proof. The module states the general unit-sphere surface formula, then specializes via direct evaluation to D=3 (yielding 4π), D=2 (yielding 2π), and shows non-unit or non-4π values in other dimensions using gamma-function identities and explicit comparison.

why it matters in Recognition Science

The module supplies the dimensional uniqueness of the 4π solid angle that the AlphaDerivation module requires for its Gauss-Bonnet step. It thereby anchors the geometric seed for α⁻¹ to the T8-forced value D=3, ensuring the fine-structure derivation remains specific to three spatial dimensions.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)