Q3Edge
plain-language theorem explainer
Enumerates the twelve edges of the 3-cube as a finite inductive type, with constructors labeled by binary endpoint pairs. Used wherever Q₃ geometry counts edges for Gray-code flip tallies and face-flux ratios that correct the Wolfenstein A parameter. Existence is by construction; Fintype and DecidableEq are derived automatically.
Claim. The type of edges of the 3-cube $Q_3$ is the finite set of twelve undirected edges joining vertices that differ in exactly one bit: four edges parallel to each coordinate axis, for axes $0,1,2$.
background
The module derives the Wolfenstein CKM parameter $A$ from pure $Q_3$ geometry. The 3-cube has eight vertices (binary strings of length 3) and twelve edges. A Gray-code Hamiltonian cycle on those vertices flips one bit per step; the flip counts per axis are the chirality signature $[4,2,2]$.
This inductive type is the edge set of that cube. Sibling Q3Vertex supplies the eight vertices. Downstream counting theorems (q3_edge_count, flip tallies, face fluxes) treat the edge set as a Fintype so that cardinalities and axis projections are decidable by decide.
Local setting (module doc): $A_{\mathrm{corrected}}=9/11$ arises as structural torsion $6/11$ times a face-flux ratio $3/2$, both read off $Q_3$ combinatorics. The same $[4,2,2]$ chirality appears in the fine-structure and baryon-asymmetry "44" identities.
proof idea
Definitional: twelve constructors, one per cube edge, grouped by the three axis directions (four edges each). DecidableEq, Repr, and Fintype are derived, so cardinality proofs reduce to decide with no manual casework.
why it matters
Supplies the edge carrier for q3_edge_count (Fintype.card = 12) and, indirectly, for Gray-code flip counts and face-flux ratios that produce $A_{\mathrm{corrected}}=9/11$. That value sits inside the PDG band $0.826\pm 0.013$ (RS prediction within $0.6\sigma$).
In the Recognition chain the same $Q_3$ geometry underlies the eight-tick octave (T7) and $D=3$ (T8). The module ties the edge combinatorics to the shared "44" factor appearing in $\alpha^{-1}$, $\eta_B\approx\varphi^{-44}$, and the CKM $A$ correction, all governed by $[4,2,2]$ Gray chirality times generation torsion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.