Registry · Theorem IV.T167 tau-effective formalized

IV.T167 — Jarlskog Invariant J from τ-Parameters

Jarlskog invariant J = A²·λ_C^6·η̄ from τ-parameters: J_τ = A_τ²·λ_τ^6·η̄_PDG = 3.060×10^-5 at -6479 ppm from PDG 3.08×10^-5. Inverted: η̄_from_J = J_PDG/(A_τ²·λ_τ^6) = 0.350269 at +6522 ppm from PDG 0.348. Shows self-consistency of τ-CKM parameters at 0.65% level.

Book IV Part 5 Ch. 36

Dependency Graph

Depends on (3)

Depended on by (8)

Lean Formalization

Module: TauLib.BookIV.Particles.ThreeGenerations

Symbol: Tau.BookIV.Particles.jarlskog_invariant_tau