sectorCost_nonneg

formal source

  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)
  77  have h4 := sectorCost_nonneg (h .higgsPotential)
  78  linarith
  79
  80/-- Sector count = 4 (matches the canonical SM Lagrangian decomposition). -/
  81theorem sector_count : Fintype.card SMLagrangianSector = 4 := by decide