  49  · rw [inv_lt_comm₀ phi_pos (by norm_num)]
  50    linarith
  51
  52structure PMNSCert where
  53  five_params : Fintype.card PMNSParameter = 5
  54  maximal_mix : Real.tan (Real.pi / 4) = 1
  55  solar_tangent_band : (0.617 : ℝ) < solarTangent ∧ solarTangent < 0.623
  56
  57noncomputable def pmnsCert : PMNSCert where
  58  five_params := pmnsParameterCount
  59  maximal_mix := maximal_mixing
  60  solar_tangent_band := solarTangent_band
  61
  62end IndisputableMonolith.Physics.PMNSMixingAnglesFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.