auto-task(Fermion.dirac): record TODO to add Dirac fermion representations and Color

[jstoobysmith]

Summary

Records a single TODO in the Weyl fermion representations file noting that the
Dirac and dual-Dirac fermion representations should be added and incorporated into
complexLorentzTensor.

The TODO item is human written; Claude placed it in the right file and section
of the library, reworded it to fit Physlib conventions, and verified the build and
linters.

Original user input

• What TODO item would you like to add to the Physlib repository? This could be a new lemma, definition, or other task such as a refactoring.
  Add Fermion.dirac and Fermion.dualDirac to Physlib, include them within complexLorentzTensor.
• What is your name (for the copyright header), if needed?
  Joseph Tooby-Smith

TODO added

In Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean:

TODO "Define the Dirac and dual-Dirac fermion representations `Fermion.dirac` and
  `Fermion.dualDirac` (built from the left- and right-handed Weyl representations
  `leftHandedRep`/`rightHandedRep` and their duals), and incorporate them into
  `complexLorentzTensor` by adding the corresponding `complexLorentzTensor.Color`
  constructors."

Why this location

Weyl/Basic.lean defines the Fermion namespace Weyl representations
(leftHandedRep, dualLeftHandedRep, rightHandedRep, dualRightHandedRep), so
it is the most specific home for the proposed Fermion.dirac/Fermion.dualDirac
representations. The TODO sits next to those definitions, alongside an existing
TODO about the same representations. The file already transitively imports
Physlib.Meta.TODO.Basic, so no new import was needed.

Verification

• lake build succeeds (no sorry, no new axioms, no new warnings).
• lake exe runPhyslibLinters — passed.
• ./scripts/lint-style.sh — passed.

---

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]

Only concern is the seemingly extra file added.