ckm_cert_exists
plain-language theorem explainer
ckm_cert_exists establishes the existence of a CKMCert structure encoding the observed CKM hierarchy, unitarity bound, and torsion differences from the phi-geometry. Particle physicists deriving quark flavor mixing from Recognition Science would cite this result to link the generation torsion schedule {0, 11, 17} to PDG values. The proof is a direct term construction that bundles three prior theorems into the certificate structure.
Claim. There exists a structure CKMCert such that rs_V_ub < rs_V_cb ∧ rs_V_cb < rs_V_us, rs_V_us² + rs_V_cb² + rs_V_ub² < 1, and τ(1) − τ(0) = 11 ∧ τ(2) − τ(1) = 6.
background
The module derives the CKM matrix from torsion geometry on the Q₃ cube, where mixing arises from mismatch between up-type and down-type sectors. The Cabibbo angle follows from the ratio of torsion differences as sin(θ_C) ≈ φ^−11. CKMCert is the structure that packages the three required properties: the mass hierarchy ordering, the unitarity inequality, and the exact torsion schedule τ(1) − τ(0) = 11, τ(2) − τ(1) = 6. Upstream, torsion_differences is obtained by simp and omega on the definitions of tau, E_passive, W, and the cube edges; ckm_hierarchy and ckm_unitarity_structural both unfold the rs_V_* abbreviations and invoke cabibbo_parameter_pos to close the inequalities.
proof idea
The proof is a one-line term wrapper that constructs the CKMCert record by supplying the three theorems ckm_hierarchy, ckm_unitarity_structural, and torsion_differences as its fields.
why it matters
This theorem supplies the existence witness for the CKM certificate in the Q6 derivation, closing the structural part of the torsion-based mixing argument. It directly supports the RS claim that the observed hierarchy and unitarity follow from the fixed torsion schedule {0, 11, 17} on the phi-ladder. No downstream uses are recorded yet; the result remains internal to the Particles.CKMDerivation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.