pmnsParameterCount

formal source

  29  | theta12 | theta23 | theta13 | deltaCP | majoranaPhases
  30  deriving DecidableEq, Repr, BEq, Fintype
  31
  32theorem pmnsParameterCount : Fintype.card PMNSParameter = 5 := by decide
  33
  34/-- Maximal mixing angle: tan(π/4) = 1. -/
  35theorem maximal_mixing : Real.tan (Real.pi / 4) = 1 := by
  36  simp [Real.tan_pi_div_four]
  37
  38/-- Solar mixing tangent ≈ 1/φ ∈ (0.617, 0.622). -/
  39noncomputable def solarTangent : ℝ := phi⁻¹
  40
  41theorem solarTangent_band :
  42    (0.617 : ℝ) < solarTangent ∧ solarTangent < 0.623 := by
  43  unfold solarTangent
  44  have h1 := phi_gt_onePointSixOne
  45  have h2 := phi_lt_onePointSixTwo
  46  constructor
  47  · rw [lt_inv_comm₀ (by norm_num) phi_pos]
  48    linarith
  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