CKMCert
plain-language theorem explainer
CKMCert is a structure that bundles the hierarchy of RS-derived CKM mixing parameters, their approximate unitarity bound, and the exact torsion differences from the generation schedule. Flavor physicists deriving quark mixing from phi-geometry would cite it to anchor the Cabibbo angle to the torsion mismatch on the Q3 cube. The declaration is a pure structure definition with no proof body or lemmas, serving only to record the three predicates for later existence results.
Claim. A CKM certificate asserts the hierarchy $r_{V_{ub}} < r_{V_{cb}} < r_{V_{us}}$, the bound $r_{V_{us}}^2 + r_{V_{cb}}^2 + r_{V_{ub}}^2 < 1$, and the torsion relations $tau(1) - tau(0) = 11$ together with $tau(2) - tau(1) = 6$, where $r_{V_{us}}$ is the base Cabibbo parameter, $r_{V_{cb}}$ its square, and $r_{V_{ub}}$ its cube.
background
In the CKM derivation module the RS approach obtains mixing from torsion mismatch between up- and down-type sectors on the Q3 cube. The torsion function tau, imported from the Anchor module, is defined by tau(0) = 0, tau(1) = 11, tau(2) = 17. The RS mixing parameters are defined locally as powers of the Cabibbo parameter: rs_V_us equals the base value, rs_V_cb its square, and rs_V_ub its cube, consistent with the phi-ladder scaling noted in the module documentation.
proof idea
CKMCert is a structure definition whose three fields directly encode the required predicates. No tactics, lemmas, or reductions are applied; the declaration simply introduces a record type whose inhabitants are triples of proofs for the hierarchy, unitarity bound, and torsion equalities.
why it matters
CKMCert supplies the type inhabited by the downstream theorem ckm_cert_exists, which constructs an explicit certificate from the hierarchy lemma, unitarity structural result, and torsion differences. It closes the structural step that links the torsion schedule {0, 11, 17} to the observed CKM hierarchy, realizing the RS prediction for the Cabibbo angle within the T7 eight-tick octave and the phi-geometry framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.