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

Physlib.lean

@@ -127,6 +127,7 @@ public import Physlib.Meta.TODO.Global
 public import Physlib.Meta.TransverseTactics
 public import Physlib.Optics.Basic
 public import Physlib.Optics.Polarization.Basic
+public import Physlib.Particles.BeyondTheStandardModel.Axion.Basic
 public import Physlib.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
 public import Physlib.Particles.BeyondTheStandardModel.PatiSalam.Basic
 public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Basic

Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Physlib.Meta.TODO.Basic
+/-!
+
+# The Axion
+
+The axion is a hypothetical pseudo-Nambu-Goldstone boson arising from a spontaneously broken
+Peccei-Quinn `U(1)` symmetry, introduced to solve the strong CP problem.
+
+This file is a placeholder for results about the axion.
+
+-/
+
+@[expose] public section
+
+namespace Axion
+
+TODO "Define the axion effective potential generated by QCD instantons, of the schematic form
+  `V(a) = Λ⁴ (1 - cos(a / fₐ))` for an axion field `a`, decay constant `fₐ`, and
+  non-perturbative scale `Λ`, and show that it is minimised at `a = 0` (CP conservation)."
+
+end Axion

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

@@ -34,6 +34,12 @@ TODO "Rename the Weyl fermion representations `leftHandedRep`, `dualLeftHandedRe
   respectively, so that each representation lives in the namespace of the module it
   acts on, and update all references accordingly."
 
+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."
+
 /-- The vector space ℂ^2 carrying the fundamental representation of SL(2,C).
   In index notation corresponds to a Weyl fermion with indices ψ^a. -/
 def leftHandedRep : Representation ℂ SL(2,ℂ) LeftHandedWeyl where