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
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