CkmMixingAngles
plain-language theorem explainer
CkmMixingAngles is a record type that packages the three CKM mixing-angle magnitudes v_us, v_cb, v_ub as real numbers. Bridge-derivation authors cite it when assembling the dimensionless observable set that must match Recognition Science targets. The declaration is a bare structure definition with no proof obligations or computational body.
Claim. Define the record type for CKM mixing angles with fields $v_{us}, v_{cb}, v_{ub} : ℝ$.
background
The ObservablePayloads module supplies strongly typed records that replace raw List ℝ fields for dimensionless mass ratios and mixing angles. LeptonMassRatios is the sibling structure holding the lepton-sector ratios mu_over_e, tau_over_e, tau_over_mu. CkmMixingAngles follows the same pattern for the CKM sector. The local setting is the canonical semantics section of the module, which assigns explicit field meanings to each payload.
proof idea
This is a structure definition that directly introduces the record type. No lemmas or tactics are applied; the declaration serves only as a type constructor for the three real-valued mixing angles.
why it matters
CkmMixingAngles supplies the mixingAngles field inside DimlessPack and the mixingAngles0 target inside UniversalDimless. It is constructed by the downstream definition mixingFromCycles, which populates the record from an RSBridge and the parameter phi. The structure therefore closes the observable-payload layer that lets Recognition Science predictions be compared against the forced constants arising from the T0-T8 chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.