Q3Vertex
plain-language theorem explainer
The eight vertices of the 3-cube Q₃, labeled by binary triples 000–111. Anyone working the CKMExact derivation cites this as the discrete carrier for Gray-code edge flips and face-flux counts. It is a plain inductive enumeration with DecidableEq, Repr, and Fintype instances.
Claim. Let $Q_3$ be the 3-dimensional hypercube. Its vertex set is the finite type with eight elements $\{v_{000}, v_{001}, v_{010}, v_{011}, v_{100}, v_{101}, v_{110}, v_{111}\}$, one for each bit-string in $\{0,1\}^3$.
background
The module CKMExact derives the Wolfenstein parameter $A$ from first principles of $Q_3$ geometry. The headline result is $A_{\mathrm{corrected}} = 9/11 \approx 0.818$, within $0.6\sigma$ of the PDG value $0.826 \pm 0.013$, with zero sorry and zero axioms.
$Q_3$ is the Boolean 3-cube whose edges realize the Gray-code walk used throughout Recognition Science (the eight-tick octave of the forcing chain, T7). Vertices are bit-strings of length 3; an edge flips exactly one coordinate. The module counts flips per axis as $(4,2,2)$ and combines them with generation torsion ${\Delta\tau_{12}=11,\Delta\tau_{23}=6}$ and face-flux ratios to obtain the structural and corrected $A$ values.
This inductive type is the discrete carrier for those counts: every subsequent flip, flux, and torsion identity is stated over these eight points.
proof idea
No proof body: the declaration is an inductive type with eight nullary constructors and derived DecidableEq, Repr, and Fintype instances. Finiteness and decidable equality are obtained automatically from the inductive structure; the card equality is discharged downstream by decide.
why it matters
Supplies the vertex set on which q3_vertex_count proves there are exactly eight points, anchoring the Gray-code flip census (4,2,2) and the face-flux correction that multiplies structural $A = 6/11$ up to $A_{\mathrm{corrected}} = 9/11$.
That factor $9/11$ sits in the same $Q_3$-chirality family as the 44-connection appearing in $\alpha^{-1}$ and $\eta_B \approx \varphi^{-44}$. The construction is the discrete geometric substrate for the CKMExact five-line derivation and for the eight-tick octave (T7) used across the Standard Model sector of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.