vertices_at_D3
plain-language theorem explainer
The result fixes the vertex count of the three-dimensional hypercube at exactly eight. Workers deriving the fine-structure constant from cubic ledger geometry cite it when converting vertex deficits into total curvature. The proof is a one-line native evaluation of the hypercube vertex function at the forced dimension three.
Claim. Let $D=3$ be the spatial dimension. The number of vertices of the $D$-hypercube is $2^D=8$.
background
The module derives the fine-structure constant from the geometry of the cubic ledger $Q_3$. The fundamental cell is the three-dimensional hypercube whose vertices, edges and faces are counted by the functions cube_vertices, cube_edges and cube_faces. The doc-comment states that during one atomic tick a recognition event traverses one edge while the remaining eleven edges couple to the vacuum geometry. The definition cube_vertices(d) := 2^d is imported from sibling modules and from PlanckScaleMatching, where it is described as the vertex count of the $D$-hypercube equal to eight ticks in the Gray cycle.
proof idea
The proof is a one-line wrapper that applies native_decide to the defining equation cube_vertices D = 2^D at the concrete value D=3 supplied by the module constant.
why it matters
This count supplies the factor eight that appears in the discrete Gauss-Bonnet theorem gauss_bonnet_Q3, where eight vertex deficits of π/2 sum to 4π. The same eight enters the Ramanujan π-certificate as the tick count that governs convergence rate and the octave period in the electron-mass definitions. It therefore closes the T8 step that forces D=3 and the eight-tick octave inside the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.