auto-task(TwoHiggsDoublet.potential): TODO for a general 2HDM effective potential

[jstoobysmith]

Summary

Records a single TODO item requesting a general effective potential for the
two Higgs doublet model, mirroring the existing
StandardModel.HiggsField.EffectivePotential framework for the Standard Model
Higgs field.

The Higgs boson directory already has both a specific parameterized potential
(HiggsBoson/Potential.lean) and a general gauge-invariant effective-potential
framework (HiggsBoson/EffectivePotential.lean). The 2HDM currently only has the
specific parameterized potential, so the analogous general construction is a
natural gap to flag.

Original request

What TODO item would you like to add to the Physlib repository?
The effective potential of the two Higgs doublet model, mirroring that of the
Higgs potential.

Name (for copyright header): Joseph Tooby-Smith

What was done

The TODO text is human-written; Claude placed it in the right file and section
of the library and confirmed the project still builds.

It was added to
Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean, in section
D. The full potential, immediately after potential_eq_gramVector — the most
specific existing home, alongside the concrete potential it generalises and the
gauge-invariant gramVector it would be expressed in. The exact command added:

TODO "Define a general effective potential for the two Higgs doublet model, mirroring
  `StandardModel.HiggsField.EffectivePotential`: characterise the potentials `TwoHiggsDoublet → ℝ`
  that are invariant under the gauge group `StandardModel.GaugeGroupI` and have a bounded maximum
  mass dimension, and express such potentials in terms of the gauge-invariant `gramVector`. The
  `potential` defined here should arise as the special case of maximum mass dimension four."

No public import Physlib.Meta.TODO.Basic was needed — the TODO command
already elaborates via a transitive import. No other declarations were touched.

lake build completes successfully with no errors, warnings, sorrys, or new
axioms.

🤖 Generated with Claude Code

---

Human review

• Does the TODO item look correctly placed in the library and an accurate reflection of the input? Yes

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.