Registry · Theorem V.T165 tau-effective formalized

V.T165 — Mass Eigenvalue Ratio Formula

Delta_m^2_31/Delta_m^2_21 = (lambda3^2-lambda1^2)/(lambda2^2-lambda1^2) where lambda1=a=iota^p (sigma-odd), lambda2=(a+c-sqrt((a-c)^2+8b^2))/2 (lighter sigma-even), lambda3=(a+c+sqrt((a-c)^2+8b^2))/2 (heavier sigma-even). Scale-invariant under (p,q,r)->(p+n,q+n,r+n). Best integer shape (p,p+1,p-1) gives ratio 39.45 (21% from PDG). Sprint 3 achieves 32.82 (0.75% from PDG 32.58).

Book V Part 3 Ch. 24

Dependency Graph

Depends on (1)

Depended on by (10)

Lean Formalization

Module: TauLib.BookIV.Electroweak.NeutrinoMode

Symbol: three_distinct_eigenvalues