From df1f425d311f0a47cfdc2a9a0946775f7337db48 Mon Sep 17 00:00:00 2001 From: Robert Sneiderman Date: Thu, 16 Jul 2026 11:24:07 -0500 Subject: [PATCH 1/2] docs(electromagnetism): add kinematics API map --- .../Electromagnetism/Kinematics/API-map.yaml | 99 +++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 Physlib/Electromagnetism/Kinematics/API-map.yaml diff --git a/Physlib/Electromagnetism/Kinematics/API-map.yaml b/Physlib/Electromagnetism/Kinematics/API-map.yaml new file mode 100644 index 000000000..4dadf9a6e --- /dev/null +++ b/Physlib/Electromagnetism/Kinematics/API-map.yaml @@ -0,0 +1,99 @@ +version: v0.1 + +Title: Electromagnetic Potential + +Overview: | + The electromagnetic potential is the primitive kinematic object of the electromagnetism + API. It is packaged as a structure `ElectromagneticPotential d` wrapping a map from + `SpaceTime d` to contravariant Lorentz vectors `A^μ`, carrying an additive-group and + scalar-action structure, a Lorentz-group action, and differentiability/smoothness API. + Constructors build a potential from a scalar potential, a vector potential, or a pair of + non-relativistic potentials, and a further constructor recovers it from electric and + magnetic fields (Poincare gauge). + + A distributional counterpart, `DistElectromagneticPotential d`, is defined as a + distribution valued in Lorentz vectors, with parallel constructors from scalar and vector + potentials. + + From a potential the API derives the electric field, the magnetic field (as a vector and + as an antisymmetric matrix), the kinetic (field-strength) term, and the electromagnetic + Lagrangian, in both the function and the distributional settings. The identification of + the potential with a connection on a U(1)-gauge bundle is only remarked in documentation + and is not formalised. + +ParentAPIs: + - SpaceTime (Physlib/SpaceAndTime/SpaceTime) + - LorentzGroup (Physlib/Relativity/LorentzGroup) + +References: + - HEPLean/PhysLean issue "API - Electromagnetic potential" + - J. D. Jackson, Classical Electrodynamics, Chapter 6 (potentials and gauge transformations) + +Requirements: + + - description: > + The electromagnetic potential is defined as a data structure wrapping a map from + spacetime to contravariant Lorentz vectors, with extensionality, a function-like + coercion, and additive-group and real-scalar-action structure. + done: true + location: > + Physlib/Electromagnetism/Kinematics/EMPotential.lean + (ElectromagneticPotential, eq_of_val_eq, add_val, neg_val, sub_val, smul_val) + + - description: > + A distributional version of the electromagnetic potential is defined, as a distribution + on spacetime valued in Lorentz vectors, with constructors from distributional scalar and + vector potentials. + done: true + location: > + Physlib/Electromagnetism/Distributional/Basic.lean + (DistElectromagneticPotential, ofScalarPotential, ofVectorPotential) + + - description: > + Constructors build an electromagnetic potential from a scalar potential, from a vector + potential, and from a pair of non-relativistic potentials, together with their static + variants and the identity relating the combined constructor to the sum of the two. + done: true + location: > + Physlib/Electromagnetism/Kinematics/EMPotential.lean + (ofScalarPotential, ofVectorPotential, ofPotentials, ofStaticScalarPotential, ofStaticVectorPotential, ofStaticPotentials, ofPotentials_eq_add) + + - description: > + The API shall contain the definition of the EM potential from a connection on a + U(1)-gauge bundle. This relationship is only noted in the module documentation; no such + construction is formalised. + done: false + location: N/A + + - description: > + The electric field is defined from the electromagnetic potential, in both the function + setting and the distributional setting. + done: true + location: > + Physlib/Electromagnetism/Kinematics/ElectricField.lean (electricField); + Physlib/Electromagnetism/Distributional/ElectricField.lean (electricField) + + - description: > + The magnetic field is defined from the electromagnetic potential, as a vector field in the + function setting and as an antisymmetric matrix field in both the function and distributional + settings. + done: true + location: > + Physlib/Electromagnetism/Kinematics/MagneticField.lean (magneticField, magneticFieldMatrix); + Physlib/Electromagnetism/Distributional/MagneticField.lean (magneticFieldMatrix) + + - description: > + The kinetic (field-strength) term is defined from the electromagnetic potential, with a + gradient, in both the function and distributional settings. + done: true + location: > + Physlib/Electromagnetism/Dynamics/KineticTerm.lean (kineticTerm, gradKineticTerm); + Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean (gradKineticTerm) + + - description: > + The Lagrangian is defined from the electromagnetic potential, together with the free + current coupling term and their gradients. + done: true + location: > + Physlib/Electromagnetism/Dynamics/Lagrangian.lean (lagrangian, freeCurrentPotential, gradLagrangian, gradFreeCurrentPotential); + Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean (gradLagrangian, gradFreeCurrentPotential) From d435fada9d5d84765c6717b6a842d326caa4637a Mon Sep 17 00:00:00 2001 From: Robert Sneiderman Date: Sun, 19 Jul 2026 12:42:30 -0500 Subject: [PATCH 2/2] docs(electromagnetism): drop issue reference, cite Jackson sections --- Physlib/Electromagnetism/Kinematics/API-map.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Physlib/Electromagnetism/Kinematics/API-map.yaml b/Physlib/Electromagnetism/Kinematics/API-map.yaml index 4dadf9a6e..d491564be 100644 --- a/Physlib/Electromagnetism/Kinematics/API-map.yaml +++ b/Physlib/Electromagnetism/Kinematics/API-map.yaml @@ -26,8 +26,7 @@ ParentAPIs: - LorentzGroup (Physlib/Relativity/LorentzGroup) References: - - HEPLean/PhysLean issue "API - Electromagnetic potential" - - J. D. Jackson, Classical Electrodynamics, Chapter 6 (potentials and gauge transformations) + - J. D. Jackson, Classical Electrodynamics, 3rd ed., Sections 6.2-6.3 (vector and scalar potentials; gauge transformations) Requirements: