pith. machine review for the scientific record. sign in
def definition def or abbrev

predictions

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)

 211def predictions : List String := [

proof body

Definition body.

 212  "λ ≈ (φ - 1)²/φ ≈ 0.236",
 213  "A might be φ-related",
 214  "CP phase η from 8-tick asymmetry",
 215  "Unitarity angles constrained by φ"
 216]
 217
 218/-! ## RS Derivation of ρ̄ and η̄ from Jarlskog Invariant
 219
 220The Wolfenstein parameters ρ̄, η̄ parametrize the unitarity triangle:
 221  ρ̄ + iη̄ = −V_ud V_ub* / (V_cd V_cb*)
 222
 223With δ_CKM = π/2 (proved in CPPhaseDerivation), both ρ̄ and η̄ are positive.
 224
 225The Jarlskog invariant J_CP = A²λ⁶η̄(1 − λ²/2)² ≈ A²λ⁶η̄.
 226With A = 9/11, λ ≈ 0.236, J_CP ≈ 3.05 × 10⁻⁵:
 227  η̄ ≈ J_CP / (A²λ⁶) ≈ 3.05e-5 / (0.669 × 1.47e-4) ≈ 0.31
 228  ρ̄ is constrained by unitarity: ρ̄² + η̄² ≤ 1.
 229-/
 230
 231/-- The Jarlskog CP invariant (PDG 2024 central value). -/

depends on (27)

Lean names referenced from this declaration's body.