faces_at_D3
plain-language theorem explainer
The declaration fixes the face count of the three-dimensional cubic cell at six. Researchers deriving the fine-structure constant from the Recognition Science ledger cite this to normalize the total solid angle to 4π. The proof is a one-line native decision that evaluates the definition of cube_faces at D=3.
Claim. For the spatial dimension $D=3$, the D-hypercube has $2D=6$ faces.
background
The Alpha Derivation module constructs the fine-structure constant from the geometry of the cubic ledger cell Q₃. D is defined as 3, the spatial dimension required by the forcing chain. The sibling definition cube_faces d computes 2*d, the standard count of faces on a D-hypercube.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic definition cube_faces D directly at D=3.
why it matters
This supplies the face count used by face_solid_angle_sum to obtain 6 × (2π/3) = 4π, closing the geometric seed for α⁻¹. It instantiates the D=3 requirement from the Recognition Science forcing chain. The same count appears in the sector-dependent torsion calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.