per_face_solid_angle_eq
The solid angle subtended by each face of the three-dimensional cube at its center equals two pi over three steradians. Derivations of the fine-structure constant from the discrete cubic ledger cite this partition when summing face contributions to recover the total solid angle. The proof substitutes the established count of six faces together with the total solid angle of four pi and reduces the quotient by algebraic simplification.
claimThe solid angle subtended by each face of the three-dimensional cube at its center equals $2π/3$ steradians.
background
The Alpha Derivation module constructs the fine-structure constant from the geometry of the cubic ledger cell Q₃ in three dimensions. The number of faces is defined as twice the dimension, which equals six when the dimension is three. The total solid angle around the center is four pi steradians by the Gauss-Bonnet theorem applied to Q₃.
proof idea
The argument first recalls that the cube has six faces. It substitutes this count into the definition of per-face solid angle as total solid angle divided by six, where the total equals four pi, and reduces the expression with the ring tactic.
why it matters in Recognition Science
The equality is invoked by the theorem confirming that six times the per-face value recovers the total four pi. It supplies the geometric partition step in the module's derivation of four pi from Gauss-Bonnet, which seeds the alpha calculation together with the eleven passive edges. The result rests on the forced three-dimensionality of space in the Recognition Science framework.
scope and limits
- Does not apply to hypercubes of dimension other than three.
- Does not prove the total solid angle equals four pi.
- Does not extend to non-cubic polyhedra or curved spaces.
- Does not incorporate active edge transitions or tick dynamics.
Lean usage
rw [per_face_solid_angle_eq]formal statement (Lean)
139theorem per_face_solid_angle_eq :
140 per_face_solid_angle = 2 * Real.pi / 3 := by
proof body
Tactic-mode proof.
141 have h6 : (cube_faces D : ℝ) = 6 := by exact_mod_cast faces_at_D3
142 simp only [per_face_solid_angle, solid_angle_Q3_eq, h6]; ring
143
144/-- Face solid angles reconstruct the total: 6 × (2π/3) = 4π. -/