cube_faces
plain-language theorem explainer
The definition states that the number of faces of a d-dimensional hypercube equals 2d. Researchers assembling the geometric seed for the fine-structure constant from the cubic ledger cite this when counting contributions from the 3-cube Q3. It is a direct algebraic definition with no lemmas or case analysis.
Claim. The number of faces of the $d$-dimensional hypercube is $F(d) = 2d$.
background
The Alpha Derivation module starts from the Recognition Science forcing chain that fixes spatial dimension at D=3 and takes the fundamental unit cell to be the 3-cube Q3. During each atomic tick one edge is traversed while the remaining edges supply the vacuum coupling. The module lists the cube geometry explicitly: vertices 2^D, edges D·2^(D-1), faces 2D. This definition supplies the face count used for the seam denominator 6×17=102 and the curvature fraction 103/102π^5.
proof idea
This is a direct definition returning twice the input dimension. No lemmas are applied; the body is the algebraic identity 2*d.
why it matters
The definition supplies the face count that feeds alpha_ingredients_from_D3_cube, faces_at_D3, face_solid_angle_sum, and seam_denominator. Those results assemble the geometric seed 4π·11 and the curvature term from voxel seam topology, completing the constructive derivation of α^{-1} from the cubic ledger. It instantiates the D=3 geometry required by the eight-tick octave and the passive-edge counting in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.