cube3_vertices
plain-language theorem explainer
The declaration establishes that the three-dimensional hypercube has exactly eight vertices. Physicists extracting integer coefficients for PMNS mixing predictions from cube topology would cite this base count when linking the eight-tick octave to the reactor weight. The proof reduces immediately to the recursive definition of hypercube vertices via a native decision procedure.
Claim. The number of vertices of the three-dimensional hypercube equals eight, where the vertex count in dimension $D$ is defined by $2^D$.
background
The PMNS radiative correction module extracts integer coefficients (6, 10, 3/2) for mixing angle predictions from the topology of the three-dimensional cube. The vertex count function is defined as $2^D$ in the AlphaDerivation and PlanckScaleMatching modules, with the explicit statement that a 3-cube has eight vertices corresponding to the eight ticks in the Gray cycle. This supplies the base enumeration used for the reactor weight derived from eight-tick octave closure.
proof idea
The proof is a one-line wrapper that applies native_decide directly to the definition of the vertex count function evaluated at dimension three.
why it matters
This result anchors the cube topology derivations that produce the atmospheric coefficient 6 (from faces) and solar coefficient 10 (from edges) in the PMNS module. It directly supports the framework's T8 requirement of three spatial dimensions and the eight-tick octave (period $2^3$) that yields the reactor mixing weight. The declaration closes a basic enumeration step without addressing open questions on higher-order corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.