face_solid_angle_sum
plain-language theorem explainer
The identity shows that the six faces of the three-dimensional cube, each subtending a solid angle of 2π/3 at the center, sum exactly to the full 4π steradians. Researchers deriving the fine-structure constant from the discrete cubic ledger would cite this step when assembling the geometric seed factor. The proof is a short tactic sequence that substitutes the face count of six and the per-face solid angle equality, then finishes with ring simplification.
Claim. For spatial dimension $D=3$, the cube has six faces and each subtends solid angle $2π/3$ at the center, yielding $6 × (2π/3) = 4π$.
background
Recognition Science fixes the spatial dimension at three. The module constructs α inverse from the geometry of the cubic ledger Q₃ during one atomic tick. Cube faces are given by the definition cube_faces D = 2D, which equals six when D=3. Each face subtends equal solid angle 4π/6 = 2π/3 by cubic symmetry, as stated in the definition per_face_solid_angle.
proof idea
The tactic proof first obtains (cube_faces D : ℝ) = 6 via exact_mod_cast from faces_at_D3. It then rewrites using per_face_solid_angle_eq and closes with the ring tactic.
why it matters
This supplies the total solid angle 4π that multiplies the eleven passive edges to form the geometric seed 4π·11 in the alpha derivation. It completes the Gauss-Bonnet reconstruction for the cubic cell listed among the module's main results. The step rests on D=3 from the forcing chain and the active-versus-passive edge split during each tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.