docs(electromagnetism): add kinematics API map

Physlib/Electromagnetism/Kinematics/API-map.yaml

@@ -0,0 +1,98 @@
+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:
+  - J. D. Jackson, Classical Electrodynamics, 3rd ed., Sections 6.2-6.3 (vector and scalar potentials; 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)