From a2820779a2063cff4a34d4196af16b34fbc21bae Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 29 Jun 2026 12:48:02 +0100 Subject: [PATCH 1/2] auto-task(Fermion.dirac): record TODO to add Dirac fermion representations and Color Co-authored-by: Claude --- Physlib.lean | 1 + .../BeyondTheStandardModel/Axion/Basic.lean | 28 +++++++++++++++++++ .../Tensors/ComplexTensor/Weyl/Basic.lean | 6 ++++ 3 files changed, 35 insertions(+) create mode 100644 Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index 9cde490af..84918d67e 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean new file mode 100644 index 000000000..5b2b65fcd --- /dev/null +++ b/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 diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean index 0a3c356a8..f5db6baae 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean +++ b/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 From 5e23ce13cc028299c10a9231305367e208b486b9 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 1 Jul 2026 08:43:49 +0100 Subject: [PATCH 2/2] feat: Fix axion addition --- Physlib.lean | 1 - .../BeyondTheStandardModel/Axion/Basic.lean | 28 ------------------- 2 files changed, 29 deletions(-) delete mode 100644 Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index 84918d67e..9cde490af 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -127,7 +127,6 @@ 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 diff --git a/Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean deleted file mode 100644 index 5b2b65fcd..000000000 --- a/Physlib/Particles/BeyondTheStandardModel/Axion/Basic.lean +++ /dev/null @@ -1,28 +0,0 @@ -/- -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