sectorCost_zero_at_vacuum

formal source

  43/-- Per-sector J-cost on the sector's canonical-deviation ratio. -/
  44def sectorCost (r : ℝ) : ℝ := Cost.Jcost r
  45
  46theorem sectorCost_zero_at_vacuum : sectorCost 1 = 0 := Cost.Jcost_unit0
  47
  48theorem sectorCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  49    sectorCost r = sectorCost r⁻¹ := Cost.Jcost_symm hr
  50
  51theorem sectorCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ sectorCost r :=
  52  Cost.Jcost_nonneg hr
  53
  54theorem sectorCost_pos_off_vacuum {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  55    0 < sectorCost r := Cost.Jcost_pos_of_ne_one r hr hne
  56
  57/-- Total Lagrangian cost is the sum of per-sector costs (no
  58cross-sector mixing at tree level on the canonical sector). -/
  59def totalCost (r : SMLagrangianSector → ℝ) : ℝ :=
  60  sectorCost (r .gaugeKinetic) + sectorCost (r .fermionKinetic) +
  61    sectorCost (r .yukawa) + sectorCost (r .higgsPotential)
  62
  63/-- Total cost vanishes when every sector sits at unity. -/
  64theorem totalCost_zero_at_vacuum :
  65    totalCost (fun _ => 1) = 0 := by
  66  unfold totalCost
  67  simp [sectorCost_zero_at_vacuum]
  68
  69/-- Total cost is nonnegative when every sector is in the physical
  70domain `r > 0`. -/
  71theorem totalCost_nonneg (r : SMLagrangianSector → ℝ)
  72    (h : ∀ s, 0 < r s) : 0 ≤ totalCost r := by
  73  unfold totalCost
  74  have h1 := sectorCost_nonneg (h .gaugeKinetic)
  75  have h2 := sectorCost_nonneg (h .fermionKinetic)
  76  have h3 := sectorCost_nonneg (h .yukawa)