CKMExactCert
plain-language theorem explainer
Certificate structure that packages the exact RS derivation of the Wolfenstein A parameter from Q₃ Gray-code face flux. A CKM phenomenologist matching first-principles predictions to PDG would cite it: structural A is 6/11, Berry-corrected A is 9/11, and the corrected value lies inside the PDG 1σ window. The structure is a pure Prop bundle; each field is discharged by a named equality or inequality theorem in the same module.
Claim. A certificate asserting: the structural Wolfenstein parameter equals $6/11$; the Berry-corrected value equals $9/11$; the Berry factor equals $3/2$ (square $9/4$); the corrected $A$ lies in $(0.813,0.839)$ and satisfies $|A-0.826|<0.008$; the structural gap to the PDG centre exceeds $0.27$ while the corrected residual is under $0.008$; axis-$0$ flip count times $\Delta\tau_{12}$ equals $44$; flip counts obey the Gray asymmetry $(4,2,2)$; $\lambda_{\mathrm{RS}}\in(0.234,0.238)$; and face fluxes on generations $1$–$2$ and $2$–$3$ equal $6$ and $4$.
background
The module derives the Wolfenstein $A$ of the CKM matrix from the geometry of the three-cube $Q_3$ and the eight-tick Gray-code cycle. Flip counts on the three axes are fixed by the path $000\to001\to011\to010\to110\to111\to101\to100\to000$, giving the chirality pattern $(4,2,2)$. Generation torsion differences are $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, so the bare structural ratio is $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$.
Face flux on the generation-$i$–$j$ face is the sum of flip counts on the two spanning axes. The Berry correction is the ratio of the $1\to2$ face flux to the $2\to3$ face flux, equal to $6/4=3/2$: $V_{us}$ sees the high-flux face while $V_{cb}$ sees the low-flux face. Multiplying yields $A_{\mathrm{corrected}}=(6/11)\times(3/2)=9/11$.
The same $Q_3$ chirality produces the integer $44=4\times11$, which also appears in the fine-structure formula and in $\eta_B\approx\varphi^{-44}$.
proof idea
The declaration is a structure whose fields are propositions, not a theorem with a tactic body. Instantiation (ckmExactCert) fills each field by a one-line application of the corresponding equality or inequality lemma already proved in the module: A_structural_eq, A_corrected_exact, berry_correction_eq, berry_sq_eq, the PDG-band inequalities, the flip-count identities (asymmetry and axis symmetry), the $44$ product, the $\lambda_{\mathrm{RS}}$ interval, and the two face-flux evaluations. No new reasoning occurs at the structure level; it only packages those facts into a single certificate type.
why it matters
This certificate is the single object that records the fully proved CKM $A$ derivation in the Standard Model sector of Recognition Science. Downstream, ckmExactCert constructs an inhabitant by wiring each field to its theorem. The result closes the five-line derivation in the module header: Gray flips $\to$ torsion ratio $\to$ face-flux Berry factor $\to A=9/11$, within $0.6\sigma$ of PDG $0.826\pm0.013$. The integer $44$ that appears as flipCount(axis$0$)$\times\Delta\tau{12}$ is the same $44$ that governs $\alpha^{-1}$ and $\eta_B\approx\varphi^{-44}$, tying CKM mixing to the eight-tick octave (T7) and the fine-structure band. Doc-comment status: zero sorry, zero axioms; every field is a proved theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.