From fd5a49a1602de5393d9f121566a81ace149a9d74 Mon Sep 17 00:00:00 2001
From: Robert Sneiderman <robbysneiderman@gmail.com>
Date: Thu, 16 Jul 2026 11:24:07 -0500
Subject: [PATCH] docs(classical-field): add gauge theory API map

---
 .../GaugeTheory/API-map.yaml                  | 91 +++++++++++++++++++
 1 file changed, 91 insertions(+)
 create mode 100644 Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml

diff --git a/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml b/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml
new file mode 100644
index 000000000..d883f9678
--- /dev/null
+++ b/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml
@@ -0,0 +1,91 @@
+version: v0.1
+
+Title: "Gauge theory"
+
+Overview: |
+  A general gauge-theory API would be built around a structure (gauge) group `G`,
+  a gauge field (connection) valued in the Lie algebra of `G`, its curvature
+  (field strength), the gauge-covariant derivative on matter fields, and the action
+  of gauge transformations under which the curvature transforms covariantly (and the
+  action is invariant).
+
+  This is a tracking map for issue #859. In the current library there is no
+  general/non-abelian gauge-theory framework. What exists are two disjoint concrete
+  pieces: (1) the abelian U(1) case, realised as gauge transformations of the
+  electromagnetic potential `A^μ ↦ A^μ + ∂^μ χ` together with gauge invariance of the
+  field strength `F^{μν}` (Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean),
+  and (2) the concrete Standard Model gauge group `SU(3) × SU(2) × U(1)` as a group
+  object with its central discrete subgroup, but with no connection, curvature, or
+  covariant-derivative theory attached to it. The general-theory requirements below are
+  therefore unimplemented and marked not done with location N/A.
+
+ParentAPIs:
+  - Electromagnetic potential (Physlib/Electromagnetism/Kinematics/EMPotential.lean)
+  - Field strength (Physlib/Electromagnetism/Kinematics/FieldStrength.lean)
+  - Standard Model gauge group (Physlib/Particles/StandardModel/Basic.lean)
+
+References:
+  - "https://en.wikipedia.org/wiki/Mathematical_descriptions_of_the_electromagnetic_field#Gauge_freedom"
+  - "https://en.wikipedia.org/wiki/Gauge_theory"
+
+Requirements:
+
+  - description: "A gauge (structure) group: the concrete Standard Model group SU(3) x SU(2) x U(1) with its projections and central discrete subgroup"
+    done: true
+    location: Physlib/Particles/StandardModel/Basic.lean (GaugeGroupI, GaugeGroupI.toSU3, GaugeGroupI.toSU2, GaugeGroupI.toU1, gaugeGroupℤ₆SubGroup)
+
+  - description: "The gauge field (connection) in the abelian U(1) case: the electromagnetic potential A^μ as a spacetime-valued Lorentz vector"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/EMPotential.lean (ElectromagneticPotential)
+
+  - description: "Curvature (field strength) of the abelian gauge field, F^{μν} built from the potential"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/FieldStrength.lean (toFieldStrength)
+
+  - description: "Gauge transformation of the gauge potential in the abelian U(1) case: the pure-gauge potential and the shift A^μ ↦ A^μ + ∂^μ χ"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (ofGradient, gaugeTransform, gaugeTransform_apply)
+
+  - description: "Gauge invariance of the field strength under abelian U(1) gauge transformations"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (toFieldStrength_gaugeTransform, fieldStrengthMatrix_gaugeTransform)
+
+  - description: "Pure-gauge (flat) configurations have vanishing curvature, and the bare gradient does not (necessity of the metric contraction)"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (toFieldStrength_ofGradient, fieldStrengthMatrix_bareGradient_inl_inr, toFieldStrength_bareGradient_ne_zero)
+
+  - description: "Group structure of gauge transformations: identity shift and composition of successive shifts"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (gaugeTransform_zero, gaugeTransform_gaugeTransform, ofGradient_add, ofGradient_zero)
+
+  - description: "Compatibility of gauge transformations with the Lorentz group action (equivariance)"
+    done: true
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (ofGradient_equivariant, gaugeTransform_equivariant)
+
+  - description: "A general abstract gauge group G (an arbitrary Lie group as structure group), not tied to the Standard Model"
+    done: false
+    location: "N/A"
+
+  - description: "A gauge field (connection) for a general/non-abelian structure group, valued in the Lie algebra of G"
+    done: false
+    location: "N/A"
+
+  - description: "The gauge-covariant derivative D = d + A acting on matter fields, and its transformation law"
+    done: false
+    location: "N/A"
+
+  - description: "Non-abelian field strength (Yang-Mills curvature) F = dA + A wedge A and its covariant transformation"
+    done: false
+    location: "N/A"
+
+  - description: "The Yang-Mills action and its Euler-Lagrange (field) equations"
+    done: false
+    location: "N/A"
+
+  - description: "Parallel transport, Wilson lines/loops, and holonomy of the connection"
+    done: false
+    location: "N/A"
+
+  - description: "A principal-bundle / fibre-bundle formulation of gauge fields as connections"
+    done: false
+    location: "N/A"