pith. machine review for the scientific record. sign in
def definition def or abbrev high

cube_faces

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  57def cube_faces (d : ℕ) : ℕ := 2 * d

proof body

Definition body.

  58
  59/-- For D=3: vertices = 8 -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.