cert
plain-language theorem explainer
Packages the hard-falsifiable CKM-sector claims into one certificate object: geometric origin of V_cb from the 3-cube edge count, PDG matches for V_cb, V_ub, V_us, and tight interval bounds on α and φ^{-3}. Anyone auditing the CKM verification layer cites this as the single entry point. Construction is pure field assembly: each field is an already-proved theorem from CKMGeometry.
Claim. The CKM certificate is the record whose fields assert: $V_{cb}^{\mathrm{geom}}=1/(2\cdot\#\mathrm{edges}(I^3))$, $|V_{cb}^{\mathrm{pred}}-V_{cb}^{\mathrm{exp}}|<V_{cb}^{\mathrm{err}}$, $0.00729<\alpha<0.00731$, $0.2360<\varphi^{-3}<0.2361$, and the corresponding absolute-error matches for $V_{ub}$ and $V_{us}$.
background
The module mirrors the neutrino-sector certificate pattern: it gathers experimentally checkable CKM claims into one Lean object rather than leaving them scattered. The structure Cert records geometric origin of $V_{cb}$, PDG matches for the three mixing magnitudes, and the numerical bounds on $\alpha$ and $\varphi^{-3}$ that the Cabibbo-angle formulas need.
Upstream, $V_{cb}$ is forced by cube topology: $V_{cb}^{\mathrm{geom}}=1/(2\cdot 12)=1/24$, proved by simplifying the edge-dual ratio on the 3-cube. The match theorem states $|1/24-0.04182|<0.00085$. Alpha bounds come from the RS interval certificate $\alpha^{-1}\in(137.030,137.039)$, inverted to $0.00729<\alpha<0.00731$. The $\varphi^{-3}$ bounds ($\approx 0.236068$) are the antitonic images of the tight golden-ratio interval, used in $V_{us}^{\mathrm{pred}}=\varphi^{-3}-(3/2)\alpha$.
proof idea
One-line structure construction. Each field of Cert is filled by the corresponding theorem from CKMGeometry: V_cb_from_cube_edges for geometric origin, V_cb_match / V_ub_match / V_us_match for the absolute-error inequalities, and the four interval theorems alpha_lower_bound, alpha_upper_bound, phi_inv3_lower_bound, phi_inv3_upper_bound. No new reasoning occurs here; the definition is a pure packaging of already-closed proofs.
why it matters
Gives the Verification layer a single hard-falsifiable handle on the CKM sector, parallel to the neutrino certificate. Downstream consumers (none yet wired in-tree) can demand the whole record rather than individual lemmas. Framework landmarks in play: $\varphi$ from the T6 self-similar fixed point, the eight-tick / cube geometry that forces $D=3$ (T7–T8) and thereby $#\mathrm{edges}(I^3)=12$, and the RS $\alpha$ band $(137.030,137.039)$ that pins the fine-structure window used in the Cabibbo correction. Closes the packaging step for CKM; the underlying geometry and numerics are already proved, not axiomatized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.