Skip to content

docs(electromagnetism): add kinematics API map#1439

Merged
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
Robby955:api-map-electromagnetism
Jul 20, 2026
Merged

docs(electromagnetism): add kinematics API map#1439
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
Robby955:api-map-electromagnetism

Conversation

@Robby955

Copy link
Copy Markdown
Contributor

Motivation

Related to #1414. This adds an API map for the electromagnetic-potential API (the "API - Electromagnetic potential" issue). An API map records the implemented status and source location of each requirement, so the state of the API stays visible in-tree.

Changes

Adds Physlib/Electromagnetism/Kinematics/API-map.yaml.

The map records the electromagnetic-potential API: the ElectromagneticPotential structure with its additive-group and real-scalar-action and Lorentz-group-action API, its constructors (from a scalar potential, a vector potential, and a pair of non-relativistic potentials), the distributional counterpart DistElectromagneticPotential, and the derived electric field, magnetic field (as a vector and as an antisymmetric matrix), field-strength kinetic term, and Lagrangian, each in both the function and distributional settings. The one requirement that is not implemented, identifying the potential with a connection on a U(1)-gauge bundle, is marked not done with location N/A, since the library only remarks on it in documentation.

Testing

Ran the API-map linter:

python3 scripts/api_map_linter.py --repo .

The map passes: every declared source file and name resolves, and no completed entry is missing a location.

@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@github-actions github-actions Bot added the t-electromagnetism Electromagnetism label Jul 18, 2026
@Robby955
Robby955 marked this pull request as ready for review July 18, 2026 17:49

References:
- HEPLean/PhysLean issue "API - Electromagnetic potential"
- J. D. Jackson, Classical Electrodynamics, Chapter 6 (potentials and gauge transformations)

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Have we checked this reference? If so this looks good.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Checked against the third edition: potentials are 6.2 and gauge transformations 6.3.

Comment thread Physlib/Electromagnetism/Kinematics/API-map.yaml Outdated

@jstoobysmith jstoobysmith left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved - will merge shortly.

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Jul 20, 2026
@jstoobysmith
jstoobysmith merged commit 1706ae6 into leanprover-community:master Jul 20, 2026
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly t-electromagnetism Electromagnetism

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants