mixingFromCycles
plain-language theorem explainer
The definition packages CKM mixing angles as a record assembled from an RS bridge geometry and the golden ratio parameter. Flavor physicists deriving CKM elements from Recognition Science cycle structures would cite this when linking bridge projections to observed mixing. It is a direct record constructor that applies separate bridge-derived projections for each angle.
Claim. The CKM mixing angles are given by the triple where the up-strange element follows the golden projection of the RS bridge with parameter $phi$, the charm-bottom element follows the real edge-dual geometry of the bridge, and the up-bottom element follows the fine-structure coupling of the bridge.
background
The Bridge Derivation module extracts observable payloads from RSBridge geometry. Canonical mixing angles are defined as the set with vus from golden projection phi to the minus three with radiative correction, vcb from edge-dual geometry equal to one over twenty-four, and vub from fine-structure coupling alpha over two. The RSBridge carries a structural loopOrder integer whose default value is five.
proof idea
This is a one-line wrapper that constructs the CKM mixing angles record by applying the V_us projection to the bridge and phi, the real V_cb geometry to the bridge, and the V_ub projection to the bridge.
why it matters
This definition supplies the canonical CKM mixing angles inside the Recognition Science bridge framework and realizes the mixingAngles payload described in the module documentation. It connects directly to the phi fixed point and eight-tick octave from the forcing chain T5-T8. No downstream theorems are listed, so the result stands as a terminal packaging step for flavor observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.