cube_vertices
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the value of the dimension d.
- Does not calculate edge or face counts of the hypercube.
- Does not apply to non-integer dimensions or continuous spaces.
- Does not include physical scaling factors or units.
formal statement (Lean)
51def cube_vertices (d : ℕ) : ℕ := 2^d
proof body
Definition body.
52
53/-- Number of edges in the D-hypercube: D · 2^(D-1). -/