per_face_solid_angle
plain-language theorem explainer
Per-face solid angle divides the cube boundary's total solid angle equally among its six faces by symmetry. Researchers assembling the geometric seed for the fine-structure constant from the cubic ledger cite this normalization when weighting curvature contributions. The definition is a direct quotient of the total solid angle by the face count.
Claim. The per-face solid angle equals the total solid angle subtended by the boundary of the three-cube divided by six: $4π/6 = 2π/3$, where the total equals the Gauss-Bonnet curvature of the sphere.
background
The Alpha Derivation module builds α^{-1} from the cubic ledger Q₃ forced by the Meta-Principle in three dimensions. Cube faces are defined as twice the dimension, giving six faces for D=3. The total solid angle of ∂Q₃ equals the Gauss-Bonnet total curvature because the boundary is homeomorphic to S², as stated in the upstream solid_angle_Q3 definition.
proof idea
One-line definition that divides solid_angle_Q3 by the real cast of cube_faces D. It applies the upstream cube_faces and solid_angle_Q3 definitions directly without further reduction.
why it matters
This supplies the normalized per-face term used in face_solid_angle_sum to recover the total 4π and in per_face_solid_angle_eq to fix the explicit value 2π/3. It contributes to the geometric seed 4π·11 in the alpha derivation, consistent with forced D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.