per_face_solid_angle_eq
plain-language theorem explainer
The equality shows each of the six faces of the 3-cube subtends a solid angle of 2π/3 at the center. Workers deriving the fine-structure constant from the discrete cubic ledger cite this step in the geometric seed assembly. The tactic proof substitutes the face count of 6 and the total solid angle of 4π into the definition, then reduces algebraically with ring.
Claim. Each face of the three-dimensional cube subtends a solid angle of $2π/3$ at the center, where the total solid angle equals $4π$ and the face count is 6.
background
The Alpha Derivation module works inside the cubic ledger for D=3. Cube faces are given by the definition cube_faces d := 2*d, and faces_at_D3 proves this equals 6. The total solid angle around the cube center is fixed at 4π by solid_angle_Q3_eq, which invokes gauss_bonnet_Q3. Per-face solid angle is defined as that total divided by the face count.
proof idea
The tactic proof first obtains the face count hypothesis via exact_mod_cast from faces_at_D3. It then applies simp to unfold per_face_solid_angle and solid_angle_Q3_eq, followed by the ring tactic for algebraic closure.
why it matters
This theorem is invoked by face_solid_angle_sum to recover the total solid angle as 6 × (2π/3) = 4π. It supplies an intermediate equality in the geometric seed (4π·11) step of the alpha derivation from the cubic ledger, aligning with the D=3 and eight-tick octave landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.