From 12345467043f6caf014ed718ad2f9a77dfc91217 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 14 Jul 2026 08:18:31 +0100 Subject: [PATCH 1/5] feat: Add API map for the SM --- Physlib/Particles/StandardModel/API-map.yaml | 55 ++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 Physlib/Particles/StandardModel/API-map.yaml diff --git a/Physlib/Particles/StandardModel/API-map.yaml b/Physlib/Particles/StandardModel/API-map.yaml new file mode 100644 index 000000000..00aa95a78 --- /dev/null +++ b/Physlib/Particles/StandardModel/API-map.yaml @@ -0,0 +1,55 @@ +version: v0.1 + +Title: Standard model + +Overview: | + The Standard Model is our current best theory of everything, containing all of the fermions that + we know to exist, the Higgs boson, and the gauge bosons that contribute to the forces that we have + in the world. This API covers the Standard Model, the fermions, the potentials, and everything + else that goes into it. + +ParentAPIs: + +References: [] + +Requirements: + + - description: "The definition of Quark doublets sitting in the (3, 2)_{1} (left-handed) representation of the SM gauge group." + done: true + location: "Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean (QuarkDoublet)" + + - description: "The definition of up-type singlets sitting in the (3, 1)_{4} (right-handed) representation of the SM gauge group." + done: false + location: N/A + + - description: "The definition of down-type singlets sitting in the (3, 1)_{-2} (right-handed) representation of the SM gauge group." + done: false + location: N/A + + - description: "The definition of lepton doublets sitting in the (1, 2)_{-3} (left-handed) representation of the SM gauge group." + done: false + location: N/A + + - description: "The definition of lepton singlets sitting in the (1, 1)_{-6} (right-handed) representation of the SM gauge group." + done: false + + + - description: "The definition of the type corresponding to the effective potential of the Standard model including the fermions and the Higgs boson, excluding derivatives." + done: false + location: N/A + + - description: "The action of the Lorentz group on the effective potential." + done: false + location: N/A + + - description: "The action of the SM gauge group on the effective potential." + done: false + location: N/A + + - description: "The definition of the mass dimension on the effective potential." + done: false + location: N/A + + - description: "The proof that up to mass dimension 4, the effective potential gives us the Yukawa sector of the Standard Model." + done: false + location: N/A From 5b8691ef3e1783e760e3fee1baac8afef65553da Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 14 Jul 2026 15:04:43 +0100 Subject: [PATCH 2/5] feat: Add selection rules --- Physlib/Particles/StandardModel/API-map.yaml | 82 ++++++++++++++++++-- 1 file changed, 75 insertions(+), 7 deletions(-) diff --git a/Physlib/Particles/StandardModel/API-map.yaml b/Physlib/Particles/StandardModel/API-map.yaml index 00aa95a78..8be50648b 100644 --- a/Physlib/Particles/StandardModel/API-map.yaml +++ b/Physlib/Particles/StandardModel/API-map.yaml @@ -14,27 +14,52 @@ References: [] Requirements: - - description: "The definition of Quark doublets sitting in the (3, 2)_{1} (left-handed) representation of the SM gauge group." + - description: | + The definition of Quark doublets sitting in the (3, 2)_{1} (left-handed) + representation of the SM gauge group. done: true location: "Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean (QuarkDoublet)" - - description: "The definition of up-type singlets sitting in the (3, 1)_{4} (right-handed) representation of the SM gauge group." + - description: | + The definition of up-type singlets sitting in the (3, 1)_{4} (right-handed) + representation of the SM gauge group. done: false location: N/A - - description: "The definition of down-type singlets sitting in the (3, 1)_{-2} (right-handed) representation of the SM gauge group." + - description: | + The definition of down-type singlets sitting in the (3, 1)_{-2} (right-handed) + representation of the SM gauge group. done: false location: N/A - - description: "The definition of lepton doublets sitting in the (1, 2)_{-3} (left-handed) representation of the SM gauge group." + - description: | + The definition of lepton doublets sitting in the (1, 2)_{-3} (left-handed) + representation of the SM gauge group. done: false location: N/A - - description: "The definition of lepton singlets sitting in the (1, 1)_{-6} (right-handed) representation of the SM gauge group." + - description: | + The definition of lepton singlets sitting in the (1, 1)_{-6} (right-handed) + representation of the SM gauge group." done: false + location: N/A + + - description: | + Define the Z_3 subgroup of the SM gauge group corresponding to + the center of SU(3). This is sometimes called the triality group. + done: false + location: N/A - - description: "The definition of the type corresponding to the effective potential of the Standard model including the fermions and the Higgs boson, excluding derivatives." + - description: | + Define the Z_2 subgroup of the SM gauge group corresponding to + the center of SU(2). + done: false + location: N/A + + - description: | + The definition of the type corresponding to the effective potential of the Standard model + including the fermions and the Higgs boson, excluding derivatives. done: false location: N/A @@ -50,6 +75,49 @@ Requirements: done: false location: N/A - - description: "The proof that up to mass dimension 4, the effective potential gives us the Yukawa sector of the Standard Model." + - description: | + Effective potential: Show that the effective potential + can be separated into the direct sum of submodules based on + multi-degree, such that each independent field and separately its dual + has associated with it its own degree. + done: false + location: N/A + + - description: | + Effective potential: Show that the multi-degree submodules are closed + under the action of the Lorentz group and the SM gauge group. + done: false + location: N/A + + - description: | + Effective potential: Show that each multi-degree submodule has + a fixed hyper-charge, write a computable function to evaluate it, and + consequently, show that only those submodules with hyper-charge 0 + can be used to construct an invariant potential. This can be thought + of as a selection rule. + done: false + location: N/A + + - description: | + Effective potential: Show that each multi-degree submodule has + a fixed triality, write a computable function to evaluate it, and + consequently, show that only those submodules with triality 0 + can be used to construct an invariant potential. This can be thought + of as a selection rule, which relates to the number of quarks in a term in the potential. + done: false + location: N/A + + - description: | + Effective potential: Show that each multi-degree submodule has + a fixed charge under the SU(2)-center, write a computable function to evaluate it, and + consequently, show that only those submodules with charge 0 under the SU(2)-center + can be used to construct an invariant potential. This can be thought + of as a selection rule, which relates to the number of doublets in a term in the potential. + done: false + location: N/A + + - description: | + The proof that up to mass dimension 4, the effective potential gives us the + Yukawa sector of the Standard Model. done: false location: N/A From e591a756094c0e767f01344be59c6747cecd09d3 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 15 Jul 2026 06:21:37 +0100 Subject: [PATCH 3/5] Update API-map.yaml --- Physlib/Particles/StandardModel/API-map.yaml | 50 +++++++++++++++++--- 1 file changed, 43 insertions(+), 7 deletions(-) diff --git a/Physlib/Particles/StandardModel/API-map.yaml b/Physlib/Particles/StandardModel/API-map.yaml index 8be50648b..c2b45ecc2 100644 --- a/Physlib/Particles/StandardModel/API-map.yaml +++ b/Physlib/Particles/StandardModel/API-map.yaml @@ -14,6 +14,22 @@ References: [] Requirements: +## Gauge group + + - description: | + Define the Z_3 subgroup of the SM gauge group corresponding to + the center of SU(3). This is sometimes called the triality group. + done: false + location: N/A + + - description: | + Define the Z_2 subgroup of the SM gauge group corresponding to + the center of SU(2). + done: false + location: N/A + +## Fermions + - description: | The definition of Quark doublets sitting in the (3, 2)_{1} (left-handed) representation of the SM gauge group. @@ -44,30 +60,50 @@ Requirements: done: false location: N/A +## Higgs boson + - description: | - Define the Z_3 subgroup of the SM gauge group corresponding to - the center of SU(3). This is sometimes called the triality group. + The definition of the Higgs boson sitting in the (1, 2)_{3} representation + of the SM gauge group. done: false location: N/A + - description: | + The trivial representation of the Lorentz group acting on the Higgs boson. + done: false + location: N/A - description: | - Define the Z_2 subgroup of the SM gauge group corresponding to - the center of SU(2). + The effective potential of the Higgs boson, defined as a symmetric algebra + over the dual of the Higgs boson and its conjugate. done: false location: N/A +## The effective potential + - description: | The definition of the type corresponding to the effective potential of the Standard model - including the fermions and the Higgs boson, excluding derivatives. + including the fermions and the Higgs boson, excluding derivatives. For fermions + they contribute via an exterior algebra, and for the Higgs boson they contribute + via the symmetric algebra. This should be called `EffectivePotentialExclDeriv`. done: false location: N/A - - description: "The action of the Lorentz group on the effective potential." + - description: | + The representation of the Lorentz group (really `SL(2, ℂ)` here) on the + effective potential. done: false location: N/A - - description: "The action of the SM gauge group on the effective potential." + - description: | + The representation of the Standard Model gauge group on the effective potential. + done: false + location: N/A + + - description: | + The definition of an SU(3)-multi-degree on terms in the effective potential. + This should be defined such that every independent representation of SU(3) + has its own degree. done: false location: N/A From 1eb4a9c14205ac560ada7307edddef770e343166 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 15 Jul 2026 06:26:06 +0100 Subject: [PATCH 4/5] feat: Add comment about hypercharge --- Physlib/Particles/StandardModel/API-map.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Physlib/Particles/StandardModel/API-map.yaml b/Physlib/Particles/StandardModel/API-map.yaml index c2b45ecc2..416d64bff 100644 --- a/Physlib/Particles/StandardModel/API-map.yaml +++ b/Physlib/Particles/StandardModel/API-map.yaml @@ -32,7 +32,8 @@ Requirements: - description: | The definition of Quark doublets sitting in the (3, 2)_{1} (left-handed) - representation of the SM gauge group. + representation of the SM gauge group. The representations used here have there hypercharge + scaled to be integers, so the hypercharge of the quark doublet is 1 instead of 1/6. done: true location: "Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean (QuarkDoublet)" From e171ffb4bf465238e113549387475dcaf66a459c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 15 Jul 2026 06:32:53 +0100 Subject: [PATCH 5/5] add: Potentially useful reference --- Physlib/Particles/StandardModel/API-map.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/Particles/StandardModel/API-map.yaml b/Physlib/Particles/StandardModel/API-map.yaml index 416d64bff..a795ff583 100644 --- a/Physlib/Particles/StandardModel/API-map.yaml +++ b/Physlib/Particles/StandardModel/API-map.yaml @@ -10,7 +10,7 @@ Overview: | ParentAPIs: -References: [] +References: ["https://arxiv.org/pdf/1008.4884"] Requirements: