q3_vertex_count
plain-language theorem explainer
The 3-cube vertex type has exactly eight elements. Anyone counting Gray-code flips, face fluxes, or generation torsion on Q₃ cites this cardinality. The proof is a one-line `decide` on the derived `Fintype` instance for the eight named constructors.
Claim. The finite set of vertices of the 3-cube $Q_3$ has cardinality $8$.
background
The module derives the Wolfenstein CKM parameter $A$ from $Q_3$ geometry: Gray-code flip counts $(4,2,2)$, generation torsion gaps, and a face-flux correction that together give $A_{\mathrm{corrected}}=9/11$.
$Q_3$ is the 3-dimensional hypercube. Its vertices are the eight binary strings of length 3, encoded here as an inductive type with constructors v000 through v111 and a derived Fintype instance. Edges, Gray-code axes, and face fluxes are built on this vertex set.
The eight-tick octave (forcing step T7) already forces period $2^3$; the same $2^3$ appears as the vertex count of spatial $Q_3$ (T8 forces $D=3$).
proof idea
One-line computational proof: by decide. Lean enumerates the eight constructors of the inductive vertex type via its derived Fintype and DecidableEq instances and checks that the cardinality equals 8. No lemmas are invoked beyond the automatic finite-type infrastructure.
why it matters
This is the base count for every subsequent $Q_3$ statistic in the module: edge count, per-axis Gray flip counts $(4,2,2)$, total flips, and the face-flux ratios that correct structural $A=6/11$ to $9/11$. The module doc ties the same chirality $[4,2,2]\times$ torsion to the fine-structure $44$ and to $\eta_B\sim\varphi^{-44}$. Without $|V(Q_3)|=8$ the Gray-code and flux normalizations are undefined. Downstream siblings (q3_edge_count, flip_axis0/1/2, A_corrected_exact) rest on this cardinality; the page lists no further used_by edges yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.