mixingAngle
plain-language theorem explainer
mixingAngle defines the quark generation mixing angle as the sine of half the phase difference between two generations. Researchers deriving CKM parameters from Recognition Science phase structures would cite this when assembling the full mixing matrix from 8-tick relations. The definition is a direct one-line expression applying the sine function to the normalized phase difference.
Claim. For phases $phi_1, phi_2 in mathbb{R}$, the mixing angle is $sin left( frac{phi_2 - phi_1}{2} right)$.
background
The StandardModel.CKMMatrix module constructs the CKM matrix from phi-quantized mixing angles tied to the eight-tick phase structure. The mixing angle between generations is expressed directly via their phase difference, consistent with the module's core insight that CKM elements emerge from RS phase relations. Upstream dependencies include collision-free properties from OptionAEmpiricalProgram.is and algebraic tautologies from SimplicialLedger.EdgeLengthFromPsi.is that ensure phase differences remain well-defined within the ledger framework.
proof idea
This is a one-line definition that applies the real sine function to the difference of the input phases divided by two.
why it matters
This definition supplies the mixing angle component used in the EWObservable inductive type within ElectroweakUnificationFromRS. It advances the paper proposition on CKM Matrix from Golden Ratio Geometry by providing the explicit angle formula tied to the T7 eight-tick octave in the forcing chain. It touches the open question of full numerical matching to observed CKM magnitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.