cube_vertices
plain-language theorem explainer
The definition assigns to each natural number D the count 2^D as the vertices of the D-dimensional hypercube. Workers deriving PMNS mixing angles from 3-cube geometry cite this count when fixing the vertex number at eight for D equal to three. The implementation is the direct power-of-two formula with no reduction steps.
Claim. The number of vertices of the D-dimensional hypercube is given by $V(D) = 2^D$.
background
The module derives integer coefficients in PMNS mixing-angle predictions from the topology of the 3-cube voxel ledger. A 3-cube supplies eight vertices, twelve edges and six faces; these counts fix the radiative corrections 6α (atmospheric) and 10α (solar). The vertex count enters every downstream curvature and solid-angle statement. Upstream results supply the same power-of-two formula in AlphaDerivation and PlanckScaleMatching, where the 3-cube is identified with the eight-tick Gray cycle.
proof idea
The declaration is the direct definition of vertex count via the exponential formula. No lemmas are applied; the expression 2^D is taken as primitive and exported for use in Gauss-Bonnet and solid-angle calculations.
why it matters
This supplies the vertex count required by the discrete Gauss-Bonnet theorem on Q3 and by the solid-angle definition. It closes the counting step that produces the coefficients 6 and 10 in the atmospheric and solar PMNS corrections. The eight vertices for D=3 align with the eight-tick octave of the Recognition framework and with the D=3 spatial dimension forced at T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.