mixing_verified
plain-language theorem explainer
The mixing_verified declaration assembles geometric derivations of CKM and PMNS matrix elements into one certificate. Flavor physicists would cite it to confirm that the predicted ratios and angles satisfy the stated numerical tolerances. The proof is a direct term construction that instantiates each field of the certificate using the corresponding derived lemmas.
Claim. The CKM and PMNS mixing parameters satisfy $V_{cb} = 1/24$, $V_{ub} = α/2$, and the squared sines of the PMNS angles obey $|sin²θ_{12} - 0.307| < 0.01$, $|sin²θ_{13} - 0.022| < 0.002$, $|sin²θ_{23} - 0.546| < 0.01$.
background
In the Recognition Science setting the cubic ledger fixes generation couplings by overlap of 8-tick windows. The MixingCert structure packages the resulting predictions for the mixing-matrix entries, replacing numerical fits with topological relations derived from edge-dual coupling and fine-structure leakage. Unitarity follows from 8-tick closure. Upstream results include the Born-rule probability definition from QuantumLedger and the individual match theorems pmns_theta12_match, pmns_theta13_match, pmns_theta23_match, vcb_derived and vub_derived that supply the concrete values.
proof idea
The proof is a term-mode construction of the MixingCert structure. It directly assigns the vcb_ratio field to the result of vcb_derived, the vub_leakage field to vub_derived, and each PMNS angle field to the corresponding pmns_theta*_match theorem.
why it matters
This declaration supplies the top-level certificate for the mixing-matrix geometry in Phase 7.2. It bundles the topological derivations that replace numerical matches with exact relations from cubic symmetry and the phi-ladder. The construction relies on the eight-tick octave and D = 3 spatial dimensions to enforce unitarity through ledger closure. No downstream uses are recorded, leaving open its integration into a full S-matrix unitarity argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.