mixing_verified

formal source

 233  theta12_match : abs (sin2_theta12_pred - 0.307) < 0.01
 234  theta23_match : abs (sin2_theta23_pred - 0.546) < 0.01
 235
 236theorem mixing_verified : MixingCert where
 237  vcb_ratio := vcb_derived
 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). -/
 246theorem pmns_theta12_born_forced :
 247    sin2_theta12_pred = solar_weight - solar_radiative_correction := by
 248  unfold sin2_theta12_pred
 249  rfl
 250
 251theorem pmns_theta23_born_forced :
 252    sin2_theta23_pred = atmospheric_weight + atmospheric_radiative_correction := by
 253  unfold sin2_theta23_pred
 254  rfl
 255
 256theorem pmns_theta13_born_forced :
 257    sin2_theta13_pred = reactor_weight := by
 258  unfold sin2_theta13_pred
 259  rfl
 260
 261/-! ## CP Violation and Jarlskog Invariant -/
 262
 263/-- **THEOREM: CP Phase from Eight-Tick Cycle**
 264    The CP-violating phase δ arises from the fundamental phase increment of the
 265    8-tick cycle. Each tick contributes π/4 to the global phase.
 266    The maximum CP violation occurs at δ = π/2 (two ticks shift).