vacuum_zero_potential

formal source

  39def higgsPotential (r : ℝ) : ℝ := Jcost r
  40
  41/-- The vacuum has zero potential. -/
  42theorem vacuum_zero_potential : higgsPotential 1 = 0 := Jcost_unit0
  43
  44/-- The potential is symmetric about the vacuum. -/
  45theorem higgs_symmetric {r : ℝ} (hr : 0 < r) :
  46    higgsPotential r = higgsPotential r⁻¹ := Jcost_symm hr
  47
  48/-- The potential is non-negative (all field values above vacuum). -/
  49theorem higgs_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ higgsPotential r :=
  50  Jcost_nonneg hr
  51
  52/-- The vacuum is the unique minimum. -/
  53theorem higgs_unique_minimum {r : ℝ} (hr : 0 < r) :
  54    higgsPotential r = 0 ↔ r = 1 := by
  55  unfold higgsPotential
  56  constructor
  57  · intro h
  58    by_contra hne
  59    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one r hr hne))
  60  · rintro rfl; exact Jcost_unit0
  61
  62structure HiggsPotentialCert where
  63  vacuum_zero : higgsPotential 1 = 0
  64  symmetric : ∀ {r : ℝ}, 0 < r → higgsPotential r = higgsPotential r⁻¹
  65  nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ higgsPotential r
  66  unique_min : ∀ {r : ℝ}, 0 < r → (higgsPotential r = 0 ↔ r = 1)
  67
  68/-- Higgs potential from recognition vacuum certificate. -/
  69def higgsPotentialCert : HiggsPotentialCert where
  70  vacuum_zero := vacuum_zero_potential
  71  symmetric := higgs_symmetric
  72  nonneg := higgs_nonneg