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

mixing_verified

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)

 236theorem mixing_verified : MixingCert where
 237  vcb_ratio := vcb_derived

proof body

Term-mode proof.

 238  vub_leakage := vub_derived
 239  theta13_match := pmns_theta13_match
 240  theta12_match := pmns_theta12_match
 241  theta23_match := pmns_theta23_match
 242
 243/-- **THEOREM: PMNS Mixing Angle Relation**
 244    The predicted mixing angles satisfy the Born rule probability ratios
 245    between the generations (with radiative corrections). -/

depends on (9)

Lean names referenced from this declaration's body.