Skip to content

docs(Electromagnetism): document the three-dimensional Maxwell equations module - #1484

Merged
gloges merged 3 commits into
leanprover-community:masterfrom
sankalpsthakur:agent/maxwell-equations-module-docs
Aug 4, 2026
Merged

docs(Electromagnetism): document the three-dimensional Maxwell equations module#1484
gloges merged 3 commits into
leanprover-community:masterfrom
sankalpsthakur:agent/maxwell-equations-module-docs

Conversation

@sankalpsthakur

Copy link
Copy Markdown
Contributor

Documents the three-dimensional Maxwell equations module: lists the four results it proves (gaussLawElectric, gaussLawMagnetic, ampereLaw, faradayLaw), explains how they relate to the covariant IsExtrema formulation (the two inhomogeneous equations come from the extremality condition, the two homogeneous ones follow directly from the potential definitions), and notes the current scope (pointwise differential form in free space; integral formulations, boundary conditions, and material media are out of scope).

Documentation only — no declarations, proofs, or signatures changed.

AI/LLM disclosure

AI coding tools were used to help draft this documentation. I reviewed the complete change for accuracy before submitting.

Co-authored-by: OpenAI GPT-5.6 Pro <noreply@openai.com>
@github-actions

github-actions Bot commented Aug 2, 2026

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 Aug 2, 2026
@gloges gloges self-assigned this Aug 3, 2026

@gloges gloges left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Looks good - I've left one minor suggested rephrasing for referring to Gauss's law.

Comment thread Physlib/Electromagnetism/ThreeDimension/MaxwellEquations.lean Outdated
@gloges gloges added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 3, 2026
@gloges

gloges commented Aug 3, 2026

Copy link
Copy Markdown
Collaborator

@sankalpsthakur the linters are failing because the changed lines are now too long - 100 char max! When ready you can comment with "-awaiting-author" to remove the tag (this helps reviewers keep track of the PR's status).

@sankalpsthakur

Copy link
Copy Markdown
Contributor Author

-awaiting-author

Changed lines wrapped to the 100-char limit and the Gauss's-law wording is in; all four linter jobs are green. Thanks @gloges!

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Aug 4, 2026

@gloges gloges left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Great - thanks again!

@gloges gloges added the ready-to-merge This PR is approved and will be merged shortly label Aug 4, 2026
@gloges
gloges merged commit c55cc33 into leanprover-community:master Aug 4, 2026
6 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