solid_angle_Q3_eq
plain-language theorem explainer
Recognition Science derives the total solid angle subtended by the boundary of the three-dimensional cube Q3 as exactly 4π from the sum of its eight vertex angular deficits. Researchers constructing the geometric seed for the fine-structure constant from the cubic ledger would cite this equality. The proof is a one-line term application of the discrete Gauss-Bonnet theorem on Q3.
Claim. The total solid angle subtended by the boundary of the three-dimensional cube equals $4π$.
background
The Alpha Derivation module starts from the Meta-Principle forcing a discrete cubic ledger on Z³ with D=3. The cube Q3 has eight vertices, twelve edges and six faces; one edge is active per recognition tick while the remaining eleven are passive field channels. The solid angle is defined as the product of vertex count and the angular deficit at each vertex, which the upstream Gauss-Bonnet theorem identifies with total curvature of the sphere. The module doc states: 'Discrete Gauss-Bonnet on Q₃: total curvature of ∂Q₃ (sum of vertex deficits over all 8 vertices) equals 4π. 8 × (π/2) = 4π = 2π · χ(S²).'
proof idea
The declaration is a one-line term-mode wrapper that directly invokes the gauss_bonnet_Q3 theorem. That upstream result first casts the vertex count to eight via vertices_at_D3 and then substitutes the vertex_deficit_eq identity before simplifying by ring.
why it matters
This equality supplies the factor 4π required by the downstream geometric_seed_eq theorem, which multiplies it by the eleven passive edges to produce the seed 4π·11 for α. It also feeds per_face_solid_angle_eq. The step closes the Gauss-Bonnet portion of the first-principles derivation of α^{-1} from cubic geometry, consistent with the D=3 forcing and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.