cube_vertices
plain-language theorem explainer
The definition states that the number of vertices in a d-dimensional hypercube equals 2^d. Researchers deriving the fine-structure constant from cubic ledger geometry cite this count when summing vertex deficits or solid angles on the 3-cube. It is implemented as a direct power-of-two expression with no lemmas or tactics required.
Claim. The number of vertices of the $d$-dimensional hypercube is $2^d$.
background
The Alpha Derivation module constructs the fine-structure constant from the geometry of the cubic ledger Q_3. The spatial dimension D is fixed at 3 by the linking requirement in the forcing chain. Cube vertices are counted as 2 to the power of the dimension, yielding eight points for the three-cube that correspond to the eight ticks in the Gray cycle.
proof idea
The declaration is a direct definition equating the vertex count to the exponential 2^d. No tactics or lemmas are applied beyond the built-in power operation.
why it matters
This vertex count is invoked by the discrete Gauss-Bonnet theorem on Q_3 to establish that the total curvature of the boundary equals 4π via eight vertex deficits of π/2 each. It also supports the solid angle definition and octave offset calculations in mass baseline derivations. The result aligns with the eight-tick octave forced at T7 and the D=3 requirement at T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.