gauge_alignment_possible

proof body

Tactic-mode proof.

  58  use (lepton_gauge.B_B * Constants.E_coh * phi ^ lepton_gauge.r0)
  59  use (up_quark_gauge.B_B * Constants.E_coh * phi ^ up_quark_gauge.r0)
  60  use (down_quark_gauge.B_B * Constants.E_coh * phi ^ down_quark_gauge.r0)
  61  -- NOTE: We keep this proof explicit because `positivity` can be brittle
  62  -- for `Real.rpow` and `zpow` terms without unfolding.
  63  have h2pos : (0 : ℝ) < 2 := by norm_num
  64  have hphi_pos : (0 : ℝ) < phi := phi_pos
  65  have hE_pos : (0 : ℝ) < Constants.E_coh := Constants.E_coh_pos
  66  constructor
  67  · -- A_lepton > 0
  68    have hB : (0 : ℝ) < lepton_gauge.B_B := by
  69      simp [lepton_gauge, zpow_pos h2pos]
  70    have hpow : (0 : ℝ) < phi ^ lepton_gauge.r0 := Real.rpow_pos_of_pos hphi_pos _
  71    have : (0 : ℝ) < lepton_gauge.B_B * Constants.E_coh := mul_pos hB hE_pos
  72    exact mul_pos this hpow
  73  · constructor
  74    · -- A_up > 0
  75      have hB : (0 : ℝ) < up_quark_gauge.B_B := by
  76        simp [up_quark_gauge, zpow_pos h2pos]
  77      have hpow : (0 : ℝ) < phi ^ up_quark_gauge.r0 := Real.rpow_pos_of_pos hphi_pos _
  78      have : (0 : ℝ) < up_quark_gauge.B_B * Constants.E_coh := mul_pos hB hE_pos
  79      exact mul_pos this hpow
  80    · -- A_down > 0
  81      have hB : (0 : ℝ) < down_quark_gauge.B_B := by
  82        simp [down_quark_gauge, zpow_pos h2pos]
  83      have hpow : (0 : ℝ) < phi ^ down_quark_gauge.r0 := Real.rpow_pos_of_pos hphi_pos _
  84      have : (0 : ℝ) < down_quark_gauge.B_B * Constants.E_coh := mul_pos hB hE_pos
  85      exact mul_pos this hpow
  86
  87end SectorYardsticks
  88end Physics
  89end IndisputableMonolith