Physlib.Particles.StandardModel.HiggsBoson.EffectivePotential

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.StandardModel.HiggsBoson.Basic
public import Mathlib.RingTheory.MvPolynomial.Homogeneous

The effective potential of the Higgs field

We define a general effective potential for the Higgs field. For this we define two properties of the potential: invariance under the gauge group, and a maximum mass dimension.

Given these, we prove that the potential can be expressed as a polynomial in the norm of the Higgs field.

@[expose] public section

A general potential of the Higgs field.

abbrev EffectivePotential : Type := HiggsVec → ℝ

A. The invariance of the general potential under the gauge group

The proposition that the general potential is invariant under the global action of the gauge group.

def IsInvariant (V : EffectivePotential) : Prop :=
  ∀ (g : GaugeGroupI), ∀ (φ : HiggsVec), V (g • φ) = V φ

An invariant potential is equal on gauge orbits.

lemma eq_on_orbits {φ1 φ2 : HiggsVec} {V : EffectivePotential} (h : IsInvariant V)
    (hφ : φ1 ∈ MulAction.orbit GaugeGroupI  φ2) :
    V φ1 = V φ2 := byφ1:HiggsVecφ2:HiggsVecV:EffectivePotentialh:V.IsInvarianthφ:φ1 ∈ MulAction.orbit GaugeGroupI φ2⊢ V φ1 = V φ2
  obtain ⟨g, rfl⟩ := hφφ2:HiggsVecV:EffectivePotentialh:V.IsInvariantg:GaugeGroupI⊢ V ((fun m => m • φ2) g) = V φ2
  exact h g φ2All goals completed! 🐙

An invariant potential is equal on Higgs vectors with identical norms.

lemma eq_of_norm_eq {φ1 φ2 : HiggsVec} {V : EffectivePotential} (h : IsInvariant V)
    (hφ : ‖φ1‖ = ‖φ2‖) :
    V φ1 = V φ2 := h.eq_on_orbits <| (HiggsVec.mem_orbit_gaugeGroupI_iff φ2 φ1).mpr hφ

lemma factors_through_norm {V : EffectivePotential} (h : IsInvariant V) :
    ∃ (f : ℝ → ℝ), V = f ∘ norm := byV:EffectivePotentialh:V.IsInvariant⊢ ∃ f, V = f ∘ norm
  use fun a => V !2[a, 0]hV:EffectivePotentialh:V.IsInvariant⊢ V = (fun a => V !₂[↑a, 0]) ∘ norm
  ext φhV:EffectivePotentialh:V.IsInvariantφ:HiggsVec⊢ V φ = ((fun a => V !₂[↑a, 0]) ∘ norm) φ
  apply h.eq_of_norm_eqhV:EffectivePotentialh:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ = ‖!₂[↑‖φ‖, 0]‖
  conv_rhs => rw [PiLp.norm_eq_of_L2]V:EffectivePotentialh:V.IsInvariantφ:HiggsVec| √(∑ i, ‖!₂[↑‖φ‖, 0].ofLp i‖ ^ 2)
  simpAll goals completed! 🐙

B. Maximum mass dimension

The proposition that the potential V has a maximum mass dimension less then or equal to n - also implying it is a polynomial.

def HasMaxMassDimLE (V : EffectivePotential) (n : ℕ) : Prop :=
  ∃ p : MvPolynomial (Fin 4) ℝ, (∀ φ : HiggsVec, V φ = p.eval φ.toRealScalars) ∧
    p.totalDegree ≤ n

The polynomial associated to a potential V with a maximum mass dimension less than or equal to n.

def polynomial (V : EffectivePotential) {n : ℕ} (h : HasMaxMassDimLE V n) :
    MvPolynomial (Fin 4) ℝ := Classical.choose h

lemma polynomial_totalDegree {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n) :
    (polynomial V h).totalDegree ≤ n := (Classical.choose_spec h).2

lemma apply_eq_polynomial {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (φ : HiggsVec) : V φ = (polynomial V h).eval φ.toRealScalars := (Classical.choose_spec h).1 φ

C. Terms of a given mass dimension

The part of a potential at a given mass-dimension.

def termOfMassDim (V : EffectivePotential) {n : ℕ} (h : HasMaxMassDimLE V n) (m : ℕ) :
    HiggsVec → ℝ := fun φ => ((polynomial V h).homogeneousComponent m).eval φ.toRealScalars

              

lemma termOfMassDim_eq_zero_of_max_lt {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    {m : ℕ} (hm : n < m) (φ : HiggsVec) :
    termOfMassDim V h m φ = 0 := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhm:n < mφ:HiggsVec⊢ V.termOfMassDim h m φ = 0
  have h1 := polynomial_totalDegree hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhm:n < mφ:HiggsVech1:(V.polynomial h).totalDegree ≤ n⊢ V.termOfMassDim h m φ = 0
  simp only [termOfMassDim]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhm:n < mφ:HiggsVech1:(V.polynomial h).totalDegree ≤ n⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) = 0
  rw [MvPolynomial.homogeneousComponent_eq_zero _ _ (byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhm:n < mφ:HiggsVech1:(V.polynomial h).totalDegree ≤ n⊢ (V.polynomial h).totalDegree < mAll goals completed! 🐙 omegaAll goals completed! 🐙All goals completed! 🐙), map_zeroV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhm:n < mφ:HiggsVech1:(V.polynomial h).totalDegree ≤ n⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

lemma termOfMassDim_homogeneity {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n) (m : ℕ)
    (φ : HiggsVec) (t : ℝ) : termOfMassDim V h m (t • φ) = t ^ m * termOfMassDim V h m φ := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ V.termOfMassDim h m (t • φ) = t ^ m * V.termOfMassDim h m φ
  rw [termOfMassDim,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ (MvPolynomial.eval (HiggsVec.toRealScalars (t • φ))) ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) =
  t ^ m * V.termOfMassDim h m φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1) termOfMassDim,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ (MvPolynomial.eval (HiggsVec.toRealScalars (t • φ))) ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) =
  t ^ m * (MvPolynomial.eval (HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent m) (V.polynomial h))V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1) map_smul,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ (MvPolynomial.eval (t • HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) =
  t ^ m * (MvPolynomial.eval (HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent m) (V.polynomial h))V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1) MvPolynomial.eval_eq',V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m * (MvPolynomial.eval (HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent m) (V.polynomial h))V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1) MvPolynomial.eval_eq',V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
      MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i, HiggsVec.toRealScalars φ i ^ d iV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1)
    Finset.mul_sumV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1)]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ ∑ d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  ∑ i ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support,
    t ^ m *
      (MvPolynomial.coeff i ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
        ∏ i_1, HiggsVec.toRealScalars φ i_1 ^ i i_1)
  refine Finset.sum_congr rfl fun d hd => ?_V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).support⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)
  have hdeg : ∑ i, d i = m := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝ⊢ V.termOfMassDim h m (t • φ) = t ^ m * V.termOfMassDim h m φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)
    rw [MvPolynomial.support_homogeneousComponent,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ {c ∈ (V.polynomial h).support | Finsupp.degree c = m}⊢ ∑ i, d i = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ ∑ i, d i = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i) Finset.mem_filterV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ ∑ i, d i = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ ∑ i, d i = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)] at hdV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ ∑ i, d i = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)
    rw [← Finsupp.degree_eq_sumV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ Finsupp.degree d = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ Finsupp.degree d = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ (V.polynomial h).support ∧ Finsupp.degree d = m⊢ Finsupp.degree d = mV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)
    exact hd.2V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    ∏ i, (t • HiggsVec.toRealScalars φ) i ^ d i =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)
  simp only [Pi.smul_apply, smul_eq_mul, mul_pow, Finset.prod_mul_distrib,
    Finset.prod_pow_eq_pow_sum, hdeg]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕφ:HiggsVect:ℝd:Fin 4 →₀ ℕhd:d ∈ ((MvPolynomial.homogeneousComponent m) (V.polynomial h)).supporthdeg:∑ i, d i = m⊢ MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
    (t ^ m * ∏ x, HiggsVec.toRealScalars φ x ^ d x) =
  t ^ m *
    (MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) *
      ∏ i, HiggsVec.toRealScalars φ i ^ d i)
  ringAll goals completed! 🐙

lemma apply_eq_sum_termOfMassDim {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (φ : HiggsVec) :
    V φ = ∑ m ∈ Finset.range (n + 1), termOfMassDim V h m φ := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ V φ = ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ
  rw [apply_eq_polynomial h,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ)) (V.polynomial h) = ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ))
    (∑ i ∈ Finset.range ((V.polynomial h).totalDegree + 1), (MvPolynomial.homogeneousComponent i) (V.polynomial h)) =
  ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ ← MvPolynomial.sum_homogeneousComponent (polynomial V h)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ))
    (∑ i ∈ Finset.range ((V.polynomial h).totalDegree + 1), (MvPolynomial.homogeneousComponent i) (V.polynomial h)) =
  ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ))
    (∑ i ∈ Finset.range ((V.polynomial h).totalDegree + 1), (MvPolynomial.homogeneousComponent i) (V.polynomial h)) =
  ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ))
    (∑ i ∈ Finset.range ((V.polynomial h).totalDegree + 1), (MvPolynomial.homogeneousComponent i) (V.polynomial h)) =
  ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ
  simp only [map_sum]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ ∑ x ∈ Finset.range ((V.polynomial h).totalDegree + 1),
    (MvPolynomial.eval (HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent x) (V.polynomial h)) =
  ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ
  change  ∑ x ∈ Finset.range ((V.polynomial h).totalDegree + 1), termOfMassDim V h x φ = _V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ ∑ x ∈ Finset.range ((V.polynomial h).totalDegree + 1), V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ
  symmV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ =
  ∑ x ∈ Finset.range ((V.polynomial h).totalDegree + 1), V.termOfMassDim h x φ
  refine Finset.eventually_constant_sum ?_ ?_refine_1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ ∀ n_1 ≥ (V.polynomial h).totalDegree + 1, V.termOfMassDim h n_1 φ = 0refine_2V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (V.polynomial h).totalDegree + 1 ≤ n + 1
  ·refine_1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ ∀ n_1 ≥ (V.polynomial h).totalDegree + 1, V.termOfMassDim h n_1 φ = 0 intro m hmrefine_1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVecm:ℕhm:m ≥ (V.polynomial h).totalDegree + 1⊢ V.termOfMassDim h m φ = 0
    simp only [termOfMassDim]refine_1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVecm:ℕhm:m ≥ (V.polynomial h).totalDegree + 1⊢ (MvPolynomial.eval (HiggsVec.toRealScalars φ)) ((MvPolynomial.homogeneousComponent m) (V.polynomial h)) = 0
    rw [MvPolynomial.homogeneousComponent_eq_zero _ _ (byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVecm:ℕhm:m ≥ (V.polynomial h).totalDegree + 1⊢ (V.polynomial h).totalDegree < mAll goals completed! 🐙 omegaAll goals completed! 🐙All goals completed! 🐙), map_zerorefine_1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVecm:ℕhm:m ≥ (V.polynomial h).totalDegree + 1⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙
  ·refine_2V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVec⊢ (V.polynomial h).totalDegree + 1 ≤ n + 1 exact Nat.add_le_add_right (polynomial_totalDegree h) 1All goals completed! 🐙

lemma apply_smul_eq_sum_termOfMassDim {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (φ : HiggsVec) (t : ℝ) :
    V (t • φ) = ∑ m ∈ Finset.range (n + 1), t ^ m * termOfMassDim V h m φ := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVect:ℝ⊢ V (t • φ) = ∑ m ∈ Finset.range (n + 1), t ^ m * V.termOfMassDim h m φ
  rw [apply_eq_sum_termOfMassDim hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVect:ℝ⊢ ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m (t • φ) = ∑ m ∈ Finset.range (n + 1), t ^ m * V.termOfMassDim h m φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVect:ℝ⊢ ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m (t • φ) = ∑ m ∈ Finset.range (n + 1), t ^ m * V.termOfMassDim h m φ]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nφ:HiggsVect:ℝ⊢ ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m (t • φ) = ∑ m ∈ Finset.range (n + 1), t ^ m * V.termOfMassDim h m φ
  exact Finset.sum_congr rfl fun m _ => termOfMassDim_homogeneity h m φ tAll goals completed! 🐙

lemma termOfMassDim_isInvariant {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (m : ℕ) (hV : IsInvariant V) : IsInvariant (termOfMassDim V h m) := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariant⊢ IsInvariant (V.termOfMassDim h m)
  intro g φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantg:GaugeGroupIφ:HiggsVec⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
  have hV (t : ℝ) := hV g (t • φ)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
  have h1 (t : ℝ) : ∑  m ∈ Finset.range (n + 1), t ^ m * (termOfMassDim V h m (g • φ) -
      termOfMassDim V h m φ) = 0 := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariant⊢ IsInvariant (V.termOfMassDim h m)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
    simp [mul_sub, ← apply_smul_eq_sum_termOfMassDim]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)t:ℝ⊢ V (t • g • φ) - V (t • φ) = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
    rw [smul_comm,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)t:ℝ⊢ V (g • t • φ) - V (t • φ) = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ hV,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)t:ℝ⊢ V (t • φ) - V (t • φ) = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ sub_eq_zeroV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)t:ℝ⊢ V (t • φ) = V (t • φ)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
  by_cases hmn : m ≤ nposV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ n⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φnegV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:¬m ≤ n⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
  ·posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ n⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ have hp : (∑ k ∈ Finset.range (n + 1),
        Polynomial.C (termOfMassDim V h k (g • φ) - termOfMassDim V h k φ) * Polynomial.X ^ k)
          = 0 := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariant⊢ IsInvariant (V.termOfMassDim h m)posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
      apply Polynomial.funextV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ n⊢ ∀ (r : ℝ),
  Polynomial.eval r
      (∑ k ∈ Finset.range (n + 1),
        Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k) =
    Polynomial.eval r 0posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
      intro xV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nx:ℝ⊢ Polynomial.eval x
    (∑ k ∈ Finset.range (n + 1),
      Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k) =
  Polynomial.eval x 0posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
      simp only [Polynomial.eval_finsetSum, Polynomial.eval_mul, Polynomial.eval_C,
        Polynomial.eval_pow, Polynomial.eval_X, Polynomial.eval_zero]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nx:ℝ⊢ ∑ x_1 ∈ Finset.range (n + 1), (V.termOfMassDim h x_1 (g • φ) - V.termOfMassDim h x_1 φ) * x ^ x_1 = 0posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
      rw [← h1 xV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nx:ℝ⊢ ∑ x_1 ∈ Finset.range (n + 1), (V.termOfMassDim h x_1 (g • φ) - V.termOfMassDim h x_1 φ) * x ^ x_1 =
  ∑ m ∈ Finset.range (n + 1), x ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nx:ℝ⊢ ∑ x_1 ∈ Finset.range (n + 1), (V.termOfMassDim h x_1 (g • φ) - V.termOfMassDim h x_1 φ) * x ^ x_1 =
  ∑ m ∈ Finset.range (n + 1), x ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ)posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nx:ℝ⊢ ∑ x_1 ∈ Finset.range (n + 1), (V.termOfMassDim h x_1 (g • φ) - V.termOfMassDim h x_1 φ) * x ^ x_1 =
  ∑ m ∈ Finset.range (n + 1), x ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ)posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
      exact Finset.sum_congr rfl fun k _ => byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nx:ℝk:ℕx✝:k ∈ Finset.range (n + 1)⊢ (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * x ^ k =
  x ^ k * (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ)posV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ ringposV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φposV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
    have hcoeff := congrArg (fun p => p.coeff m) hpposV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:m ≤ nhp:∑ k ∈ Finset.range (n + 1), Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k = 0hcoeff:(∑ k ∈ Finset.range (n + 1),
        Polynomial.C (V.termOfMassDim h k (g • φ) - V.termOfMassDim h k φ) * Polynomial.X ^ k).coeff
    m =
  Polynomial.coeff 0 m⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ
    simpa only [Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul, Polynomial.coeff_X_pow,
      mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_range, Nat.lt_succ_iff, hmn,
      if_true, Polynomial.coeff_zero, sub_eq_zero] using hcoeffAll goals completed! 🐙
  ·negV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:¬m ≤ n⊢ V.termOfMassDim h m (g • φ) = V.termOfMassDim h m φ rw [termOfMassDim_eq_zero_of_max_lt h (not_le.mp hmn),negV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:¬m ≤ n⊢ 0 = V.termOfMassDim h m φAll goals completed! 🐙
      termOfMassDim_eq_zero_of_max_lt h (not_le.mp hmn)negV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV✝:V.IsInvariantg:GaugeGroupIφ:HiggsVechV:∀ (t : ℝ), V (g • t • φ) = V (t • φ)h1:∀ (t : ℝ), ∑ m ∈ Finset.range (n + 1), t ^ m * (V.termOfMassDim h m (g • φ) - V.termOfMassDim h m φ) = 0hmn:¬m ≤ n⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

lemma termOfMassDim_eq_mul_norm {V : EffectivePotential} {n : ℕ}
    (h : HasMaxMassDimLE V n) (m : ℕ) (hV : IsInvariant V) (φ : HiggsVec) :
    ∃ c, termOfMassDim V h m φ = c * ‖φ‖ ^ m := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ∃ c, V.termOfMassDim h m φ = c * ‖φ‖ ^ m
  use termOfMassDim V h m !2[1, 0]hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ V.termOfMassDim h m φ = V.termOfMassDim h m !₂[1, 0] * ‖φ‖ ^ m
  rw [(termOfMassDim_isInvariant h m hV).eq_of_norm_eq (φ2 := ‖φ‖ • !2[1, 0])
    (byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ = ‖‖φ‖ • !₂[1, 0]‖hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ ^ m * V.termOfMassDim h m !₂[1, 0] = V.termOfMassDim h m !₂[1, 0] * ‖φ‖ ^ m simp [PiLp.norm_eq_of_L2]All goals completed! 🐙hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ ^ m * V.termOfMassDim h m !₂[1, 0] = V.termOfMassDim h m !₂[1, 0] * ‖φ‖ ^ m), termOfMassDim_homogeneity h m !2[1, 0] ‖φ‖hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ ^ m * V.termOfMassDim h m !₂[1, 0] = V.termOfMassDim h m !₂[1, 0] * ‖φ‖ ^ mhV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ ^ m * V.termOfMassDim h m !₂[1, 0] = V.termOfMassDim h m !₂[1, 0] * ‖φ‖ ^ m]hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVec⊢ ‖φ‖ ^ m * V.termOfMassDim h m !₂[1, 0] = V.termOfMassDim h m !₂[1, 0] * ‖φ‖ ^ m
  ringAll goals completed! 🐙

lemma termOfMassDim_zero_of_odd {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n) (m : ℕ)
    (hV : IsInvariant V) (φ : HiggsVec) (hodd : Odd m)  :
    termOfMassDim V h m φ = 0 := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd m⊢ V.termOfMassDim h m φ = 0
  have h1 : termOfMassDim V h m φ = termOfMassDim V h m ((-1 : ℝ) • φ) :=
    (termOfMassDim_isInvariant h m hV).eq_of_norm_eq (byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd m⊢ ‖φ‖ = ‖-1 • φ‖V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = V.termOfMassDim h m (-1 • φ)⊢ V.termOfMassDim h m φ = 0 simpAll goals completed! 🐙V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = V.termOfMassDim h m (-1 • φ)⊢ V.termOfMassDim h m φ = 0)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = V.termOfMassDim h m (-1 • φ)⊢ V.termOfMassDim h m φ = 0
  rw [termOfMassDim_homogeneity h m φ (-1 : ℝ),V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = (-1) ^ m * V.termOfMassDim h m φ⊢ V.termOfMassDim h m φ = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = -1 * V.termOfMassDim h m φ⊢ V.termOfMassDim h m φ = 0 hodd.neg_one_powV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = -1 * V.termOfMassDim h m φ⊢ V.termOfMassDim h m φ = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = -1 * V.termOfMassDim h m φ⊢ V.termOfMassDim h m φ = 0] at h1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nm:ℕhV:V.IsInvariantφ:HiggsVechodd:Odd mh1:V.termOfMassDim h m φ = -1 * V.termOfMassDim h m φ⊢ V.termOfMassDim h m φ = 0
  linarithAll goals completed! 🐙

D. Potential in terms of the norm of the Higgs field



lemma apply_eq_sum_even_termOfMassDim {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (hV : IsInvariant V) (φ : HiggsVec) :
    V φ = ∑ m ∈ Finset.range (n / 2 + 1), termOfMassDim V h (2 * m) φ := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ V φ = ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
  rw [apply_eq_sum_termOfMassDim h,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ m ∈ Finset.range (n + 1), V.termOfMassDim h m φ = ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ ← Finset.sum_filter_add_sum_filter_not
    (Finset.range (n + 1)) EvenV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
  have hodd : ∑ m ∈ (Finset.range (n + 1)).filter (fun m => ¬ Even m),
      termOfMassDim V h m φ = 0 := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ V φ = ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    refine Finset.sum_eq_zero fun m hm => ?_V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVecm:ℕhm:m ∈ {m ∈ Finset.range (n + 1) | ¬Even m}⊢ V.termOfMassDim h m φ = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    simp only [Finset.mem_filter] at hmV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVecm:ℕhm:m ∈ Finset.range (n + 1) ∧ ¬Even m⊢ V.termOfMassDim h m φ = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    exact termOfMassDim_zero_of_odd h m hV φ (Nat.not_even_iff_odd.mp hm.2)V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ +
    ∑ x ∈ Finset.range (n + 1) with ¬Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
  rw [hodd,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ + 0 =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ add_zeroV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
  have hset : (Finset.range (n / 2 + 1)).image (fun k => 2 * k)
      = (Finset.range (n + 1)).filter Even := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ V φ = ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    ext aV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕ⊢ a ∈ Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) ↔ a ∈ Finset.filter Even (Finset.range (n + 1))V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    simp only [Finset.mem_image, Finset.mem_range, Finset.mem_filter, Nat.even_iff]V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕ⊢ (∃ a_1 < n / 2 + 1, 2 * a_1 = a) ↔ a < n + 1 ∧ a % 2 = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    constructormpV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕ⊢ (∃ a_1 < n / 2 + 1, 2 * a_1 = a) → a < n + 1 ∧ a % 2 = 0mprV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕ⊢ a < n + 1 ∧ a % 2 = 0 → ∃ a_2 < n / 2 + 1, 2 * a_2 = aV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    ·mpV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕ⊢ (∃ a_1 < n / 2 + 1, 2 * a_1 = a) → a < n + 1 ∧ a % 2 = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ rintro ⟨k, hk, rfl⟩mpV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0k:ℕhk:k < n / 2 + 1⊢ 2 * k < n + 1 ∧ 2 * k % 2 = 0V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
      omegaAll goals completed! 🐙V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
    ·mprV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕ⊢ a < n + 1 ∧ a % 2 = 0 → ∃ a_2 < n / 2 + 1, 2 * a_2 = aV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ rintro ⟨ha, hae⟩mprV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕha:a < n + 1hae:a % 2 = 0⊢ ∃ a_1 < n / 2 + 1, 2 * a_1 = aV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
      exact ⟨a / 2, byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕha:a < n + 1hae:a % 2 = 0⊢ a / 2 < n / 2 + 1V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ omegaAll goals completed! 🐙V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ, byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0a:ℕha:a < n + 1hae:a % 2 = 0⊢ 2 * (a / 2) = aV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ omegaAll goals completed! 🐙V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ⟩V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.range (n + 1) with Even x, V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ
  rw [← hset,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))⊢ ∑ x ∈ Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)), V.termOfMassDim h x φ =
  ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φAll goals completed! 🐙 Finset.sum_image fun x _ y _ hxy => byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVechodd:∑ m ∈ Finset.range (n + 1) with ¬Even m, V.termOfMassDim h m φ = 0hset:Finset.image (fun k => 2 * k) (Finset.range (n / 2 + 1)) = Finset.filter Even (Finset.range (n + 1))x:ℕx✝¹:x ∈ ↑(Finset.range (n / 2 + 1))y:ℕx✝:y ∈ ↑(Finset.range (n / 2 + 1))hxy:2 * x = 2 * y⊢ x = yAll goals completed! 🐙 omegaAll goals completed! 🐙All goals completed! 🐙]All goals completed! 🐙



lemma apply_eq_sum_even_termOfMassDim_fin {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (hV : IsInvariant V) (φ : HiggsVec) :
    V φ = ∑ m : Fin (n/2 + 1), termOfMassDim V h (2 * m) φ := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ V φ = ∑ m, V.termOfMassDim h (2 * ↑m) φ
  rw [apply_eq_sum_even_termOfMassDim h hV φ,V:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ m ∈ Finset.range (n / 2 + 1), V.termOfMassDim h (2 * m) φ = ∑ m, V.termOfMassDim h (2 * ↑m) φAll goals completed! 🐙 Finset.sum_rangeV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ i, V.termOfMassDim h (2 * ↑i) φ = ∑ m, V.termOfMassDim h (2 * ↑m) φAll goals completed! 🐙]All goals completed! 🐙

The potential is equal to the sum of norms to even powers.


lemma apply_eq_sum_norm_pow {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n)
    (hV : IsInvariant V) (φ : HiggsVec) :
    ∃ c : Fin (n/2 + 1) → ℝ, V φ = ∑ m, c m • ‖φ‖ ^ (2 * m.1) := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∃ c, V φ = ∑ m, c m • ‖φ‖ ^ (2 * ↑m)
  use fun m' => Classical.choose (termOfMassDim_eq_mul_norm h (2 * m'.1) hV φ)hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ V φ = ∑ m, (fun m' => Classical.choose ⋯) m • ‖φ‖ ^ (2 * ↑m)
  rw [apply_eq_sum_even_termOfMassDim_fin h hV φhV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ m, V.termOfMassDim h (2 * ↑m) φ = ∑ m, (fun m' => Classical.choose ⋯) m • ‖φ‖ ^ (2 * ↑m)hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ m, V.termOfMassDim h (2 * ↑m) φ = ∑ m, (fun m' => Classical.choose ⋯) m • ‖φ‖ ^ (2 * ↑m)]hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVec⊢ ∑ m, V.termOfMassDim h (2 * ↑m) φ = ∑ m, (fun m' => Classical.choose ⋯) m • ‖φ‖ ^ (2 * ↑m)
  refine Finset.sum_congr rfl fun m _ => ?_hV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nhV:V.IsInvariantφ:HiggsVecm:Fin (n / 2 + 1)x✝:m ∈ Finset.univ⊢ V.termOfMassDim h (2 * ↑m) φ = (fun m' => Classical.choose ⋯) m • ‖φ‖ ^ (2 * ↑m)
  simpa using Classical.choose_spec (termOfMassDim_eq_mul_norm h (2 * m.1) hV φ)All goals completed! 🐙