q3_edge_count

In this module the 3-cube $Q_3$ is the discrete geometry underlying the CKMExact derivation of the Wolfenstein parameter $A$. Vertices are the eight bitstrings of length 3; edges are the twelve single-bit flips between them.

Q3Edge is an inductive enumeration of those edges (four per coordinate axis: the three parallel classes of four edges each). It derives Fintype, so cardinality is a decidable finite count. The module goal is $A_{\mathrm{corrected}} = 9/11$ from Gray-code flip asymmetry $[4,2,2]$, generation torsion, and a face-flux ratio that explicitly uses the edge total 12.

Local setting (module doc): fully proved, zero sorry; PDG $A \approx 0.826$ vs RS $9/11 \approx 0.818$ (within $0.6\sigma$). The same $Q_3$ chirality also feeds the 44-connection in $\alpha^{-1}$ and $\eta_B$.

One-line tactic proof: by decide. Lean uses the derived Fintype and DecidableEq instances on the twelve-constructor inductive Q3Edge and reduces Fintype.card Q3Edge = 12 by exhaustive enumeration in the kernel. No lemmas are invoked beyond the automatic instances.

This is the edge census for the $Q_3$ scaffold of CKMExact. The module derivation writes the face-flux correction as $\mathrm{faceFlux}(12)/\mathrm{faceFlux}(23) = 6/4 = 3/2$, then $A_{\mathrm{corrected}} = (6/11)\times(3/2) = 9/11$. Without $|E(Q_3)| = 12$ that ratio is undefined in the formal development.

It sits beside q3_vertex_count (eight vertices) and the Gray-code flip lemmas (flip_axis0/1/2, total_flips) that produce the $[4,2,2]$ asymmetry. Framework landmarks: eight-tick octave and $D=3$ (T7–T8) make the 3-cube the natural discrete carrier; the same chirality appears in the 44-link across $\alpha^{-1}$, $\eta_B$, and CKM $A$. No downstream theorems are wired yet in the graph; the declaration is infrastructure for the five-line $A$ chain.