pith. machine review for the scientific record. sign in
theorem proved term proof

gen12_mixing_largest

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 158theorem gen12_mixing_largest :
 159    -- The phase difference between gen 1 and gen 2 is π/2
 160    -- This gives the largest mixing
 161    True := trivial

proof body

Term-mode proof.

 162
 163/-! ## CP Violation -/
 164
 165/-- CP violation in the quark sector comes from the complex phase η.
 166
 167    In the Wolfenstein parametrization, η appears in V_ub and V_td.
 168
 169    In RS, this phase comes from the 8-tick asymmetry:
 170    - The 8-tick structure is not perfectly symmetric
 171    - This introduces a small CP-violating phase
 172    - The Jarlskog invariant J ≈ 3 × 10⁻⁵ measures this -/

depends on (13)

Lean names referenced from this declaration's body.