PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.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.BeyondTheStandardModel.TwoHDM.GramMatrix
public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.Module
public import Mathlib.RingTheory.MvPolynomial.Tower

The effective potential of the two Higgs doublet model

i. Overview

An effective potential of the two Higgs doublet model is a real-valued function V : TwoHiggsDoublet → ℝ of the field configuration. This file introduces the two physical properties of such a potential used when expressing it through the gauge-invariant bilinears:

IsInvariant V — invariance under the global gauge group, and

HasMaxMassDimLE V n — being a polynomial in the field components of mass dimension ≤ n.

ii. Key results

EffectivePotential — the type of effective potentials.

IsInvariant — gauge invariance of a potential.

HasMaxMassDimLE — being a bounded-degree polynomial in the field components.

HasMaxMassDimLE.exists_comp_linear_poly — a polynomial potential, restricted along any real-linear parametrisation of configurations, is a polynomial in the parameters.

iii. Table of contents

A. The effective potential and its gauge invariance

B. Maximum mass dimension

@[expose] public section

A general potential of the Higgs field.

abbrev EffectivePotential : Type := TwoHiggsDoublet → ℝ

A. The effective potential and its gauge invariance

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

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

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 (Module.Dual ℝ TwoHiggsDoublet) ℝ, (∀ φ : TwoHiggsDoublet, V φ = p.eval
   (fun i => i φ) ) ∧ p.totalDegree ≤ n

A polynomial potential, restricted along any real-linear parametrisation L of field configurations, is a genuine polynomial in the parameters. This is the bookkeeping that lets the potential be evaluated on the field components of a gauge slice.


lemma HasMaxMassDimLE.exists_comp_linear_poly {V : EffectivePotential} {n : ℕ}
    (h : HasMaxMassDimLE V n) {ι : Type*} [Fintype ι] [DecidableEq ι]
    (L : (ι → ℝ) →ₗ[ℝ] TwoHiggsDoublet) :
    ∃ P : MvPolynomial ι ℝ, ∀ a : ι → ℝ, V (L a) = P.eval a := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoublet⊢ ∃ P, ∀ (a : ι → ℝ), V (L a) = (MvPolynomial.eval a) P
  obtain ⟨p, hp, -⟩ := hV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) p⊢ ∃ P, ∀ (a : ι → ℝ), V (L a) = (MvPolynomial.eval a) P
  refine ⟨MvPolynomial.aeval
    (fun i => ∑ k : ι, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p, fun a => ?_⟩V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝ⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
  have key : (fun i : Module.Dual ℝ TwoHiggsDoublet => i (L a))
      = fun i => MvPolynomial.eval a
        (∑ k : ι, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoublet⊢ ∃ P, ∀ (a : ι → ℝ), V (L a) = (MvPolynomial.eval a) PV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    funext iV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoublet⊢ i (L a) = (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    have ha : a = ∑ k : ι, a k • (Pi.single k 1 : ι → ℝ) := byV:EffectivePotentialn:ℕh:V.HasMaxMassDimLE nι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoublet⊢ ∃ P, ∀ (a : ι → ℝ), V (L a) = (MvPolynomial.eval a) PV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
      funext jV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletj:ι⊢ a j = (∑ k, a k • Pi.single k 1) jV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
      simp [Finset.sum_apply, Pi.single_apply, Finset.sum_ite_eq]V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    rw [map_sumV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = ∑ x, (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single x 1))) * MvPolynomial.X x)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = ∑ x, (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single x 1))) * MvPolynomial.X x)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)]V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ i (L a) = ∑ x, (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single x 1))) * MvPolynomial.X x)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    conv_lhs => rw [ha, map_sum, map_sum]V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1| ∑ x, i (L (a x • Pi.single x 1))V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    apply Finset.sum_congr rflV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1⊢ ∀ x ∈ Finset.univ,
  i (L (a x • Pi.single x 1)) = (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single x 1))) * MvPolynomial.X x)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    intro k _V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ i (L (a k • Pi.single k 1)) = (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
    rw [map_smul,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ i (a k • L (Pi.single k 1)) = (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p) map_smul,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ a k • i (L (Pi.single k 1)) = (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p) MvPolynomial.eval_mul,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ a k • i (L (Pi.single k 1)) =
  (MvPolynomial.eval a) (MvPolynomial.C (i (L (Pi.single k 1)))) * (MvPolynomial.eval a) (MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p) MvPolynomial.eval_C,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ a k • i (L (Pi.single k 1)) = i (L (Pi.single k 1)) * (MvPolynomial.eval a) (MvPolynomial.X k)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p) MvPolynomial.eval_X,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ a k • i (L (Pi.single k 1)) = i (L (Pi.single k 1)) * a kV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
      smul_eq_mul,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ a k * i (L (Pi.single k 1)) = i (L (Pi.single k 1)) * a kV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p) mul_commV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝi:Module.Dual ℝ TwoHiggsDoubletha:a = ∑ k, a k • Pi.single k 1k:ιa✝:k ∈ Finset.univ⊢ i (L (Pi.single k 1)) * a k = i (L (Pi.single k 1)) * a kV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)]V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ V (L a) =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)
  rw [hp,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => i (L a)) p =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    p key,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval a) ((MvPolynomial.aeval fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    p MvPolynomial.aeval_def,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval a)
    (MvPolynomial.eval₂ (algebraMap ℝ (MvPolynomial ι ℝ))
      (fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    p MvPolynomial.algebraMap_eq,V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval a)
    (MvPolynomial.eval₂ MvPolynomial.C (fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k) p)V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    p ← MvPolynomial.eval_assocV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    pV:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    p]V:EffectivePotentialn:ℕι:Type u_1inst✝¹:Fintype ιinst✝:DecidableEq ιL:(ι → ℝ) →ₗ[ℝ] TwoHiggsDoubletp:MvPolynomial (Module.Dual ℝ TwoHiggsDoublet) ℝhp:∀ (φ : TwoHiggsDoublet), V φ = (MvPolynomial.eval fun i => i φ) pa:ι → ℝkey:(fun i => i (L a)) = fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)⊢ (MvPolynomial.eval fun i => (MvPolynomial.eval a) (∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k)) p =
  (MvPolynomial.eval (⇑(MvPolynomial.eval a) ∘ fun i => ∑ k, MvPolynomial.C (i (L (Pi.single k 1))) * MvPolynomial.X k))
    p
  rflAll goals completed! 🐙