auto-task(EffectivePotential): TODO to make Higgs potential polynomial basis-independent

[jstoobysmith]

Summary

This PR records a single TODO item in
Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean.

The TODO was human-written; Claude placed it in the appropriate file and
section of the library and verified that the build and linters remain green.

Original user input

change the Polynomial in Effective Potential for the Higgs field to be based
on the basis independent Module.Dual HiggsVec R, rather then on Fin 4.

What was added

A TODO command just after apply_eq_polynomial, inside section B. Maximum
mass dimension, next to the declarations it concerns (HasMaxMassDimLE and
polynomial):

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`."

Why this is the right home

HasMaxMassDimLE and polynomial currently express the effective potential as
an MvPolynomial (Fin 4) ℝ evaluated on HiggsVec.toRealScalars, i.e. tied to
an explicit coordinate choice. The TODO sits directly beside these definitions,
making the intended basis-independent reformulation discoverable to future
contributors. No TODO for this already existed.

Verification

• lake build succeeds with the TODO elaborating cleanly (no sorry, no new
  axioms, no new warnings).
• lake exe runPhyslibLinters passes.
• ./scripts/lint-style.sh passes.

---

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.

[morrison-daniel]

Actual TODO in the PR description looks good, but another case of a second TODO being added at the same time