mixing_verified
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the mixing angles without external bounds on phi and alpha.
- Does not obtain the CP-violating phases of the CKM matrix.
- Does not address neutrino mass hierarchies or absolute scales.
- Does not prove unitarity of the full PMNS matrix beyond the listed angle matches.
formal statement (Lean)
236theorem mixing_verified : MixingCert where
237 vcb_ratio := vcb_derived
proof body
Term-mode proof.
238 vub_leakage := vub_derived
239 theta13_match := pmns_theta13_match
240 theta12_match := pmns_theta12_match
241 theta23_match := pmns_theta23_match
242
243/-- **THEOREM: PMNS Mixing Angle Relation**
244 The predicted mixing angles satisfy the Born rule probability ratios
245 between the generations (with radiative corrections). -/