From dd9490495dd2a8ea89ff214e0e9b4aa5c06be078 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 29 Jun 2026 15:01:17 +0100 Subject: [PATCH 1/2] auto-task(TwoHiggsDoublet): add TODO to define the Module instance Co-authored-by: Claude --- Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean index e7a1bdb23..02398ac8f 100644 --- a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean @@ -52,6 +52,10 @@ lemma ext_of_fst_snd {H1 H2 : TwoHiggsDoublet} cases H1 cases H2 congr + +TODO "Define the `Module ℂ TwoHiggsDoublet` instance (with its underlying `AddCommGroup`), + making the configuration space `TwoHiggsDoublet` a complex vector space via the componentwise + structure on the two `HiggsVec` doublets `Φ1` and `Φ2`." /-! ## B. Gauge group actions From 9712aaaf537ef9e03dcb3edca0dfc10c385111d4 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 29 Jun 2026 15:06:22 +0100 Subject: [PATCH 2/2] auto-task(EffectivePotential): TODO to make Higgs potential polynomial basis-independent Co-authored-by: Claude --- .../StandardModel/HiggsBoson/EffectivePotential.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean b/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean index c102110c3..789c1dd25 100644 --- a/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean +++ b/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean @@ -95,6 +95,11 @@ lemma polynomial_totalDegree {V : EffectivePotential} {n : ℕ} (h : HasMaxMassD lemma apply_eq_polynomial {V : EffectivePotential} {n : ℕ} (h : HasMaxMassDimLE V n) (φ : HiggsVec) : V φ = (polynomial V h).eval φ.toRealScalars := (Classical.choose_spec h).1 φ +TODO "Reformulate `HasMaxMassDimLE` (and `polynomial`) to use the basis-independent polynomial + ring `MvPolynomial (Module.Dual ℝ HiggsVec) ℝ` rather than `MvPolynomial (Fin 4) ℝ`, so that the + effective potential is expressed without reference to the explicit coordinate map + `HiggsVec.toRealScalars`." + /-! ## C. Terms of a given mass dimension