Cert
plain-language theorem explainer
Certificate record bundling the hard-falsifiable CKM-sector claims: geometric origin of V_cb from the 3-cube edge count, PDG absolute-error matches for V_cb, V_ub, and V_us, plus tight decimal bounds on α and φ^{-3}. Cited by anyone checking the RS CKM sector against experiment. Structure definition only; no proof body, instances discharge the field propositions.
Claim. A CKM certificate is a record asserting: (i) the geometric CKM entry equals $V_{cb}^{\mathrm{geom}} = 1/(2\, e_3)$ with $e_3$ the edge count of the 3-cube; (ii) $|V_{cb}^{\mathrm{pred}}-V_{cb}^{\mathrm{exp}}|<\varepsilon_{cb}$, and likewise for $V_{ub}$ and $V_{us}$ within their stated errors; (iii) $0.00729 < \alpha < 0.00731$; (iv) $0.2360 < \varphi^{-3} < 0.2361$.
background
This module mirrors the neutrino-sector certificate: it packages experimentally checkable CKM claims as one Lean object. In RS, CKM geometry is tied to hypercube topology. The edge count of the $D$-cube is $e_D = D\cdot 2^{D-1}$ (so $e_3 = 12$), and the geometric $V_{cb}$ seed is written $1/(2 e_3)$.
The fine-structure constant $\alpha$ is the RS-native $1/\alpha_{\mathrm{inv}}$ in the constants layer, and also appears as a CODATA anchor in cosmology modules. The factor $\varphi^{-3}$ (the dream fraction in the RS primer) is bounded here because it enters the Cabibbo sector. Predicted entries $V_{}^{\mathrm{pred}}$ are compared to PDG values $V_{}^{\mathrm{exp}}$ inside fixed absolute tolerances.
proof idea
Definitional structure, not a proved theorem: there is no proof body. Each field is a proposition (equality for the geometric $V_{cb}$ origin; strict inequalities for the $\alpha$ and $\varphi^{-3}$ windows; absolute-error inequalities for the three PDG matches). An instance is built by supplying separate proofs or numeric certificates for those fields; consumers then project the fields they need.
why it matters
Gives the verification layer a single hard-falsifiable CKM bundle, parallel to the neutrino-sector certificate. The geometric $V_{cb}$ field ties the mixing entry to $D=3$ cube topology (forcing-chain landmark T8) via the edge-count formula. The $\varphi^{-3}$ bounds lock the dream-fraction input used for Cabibbo-scale matches; the $\alpha$ window is the local decimal form of the RS fine-structure constraint.
Downstream, certificate-shaped objects feed the completion-conservativity API (certificate-covered predicates, absence of uncertified display artifacts, and the conservativity headline). The same certificate pattern appears beside the result that $\mathbb{R}$ is not forced from distinction: countable native certificates never faithfully cover the reals. Open experimental pressure sits on the three PDG match fields and the two numeric windows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.