Create an API map

How to write an API map

An API map is a short article about one area of physics in Physlib. It explains the physics in words, and points from each statement to the Lean declarations that formalize it.

1. One file per API. It is called API-map.md and sits in the top folder of the API it describes.
2. Fixed headings. A # Title, then ## Abstract (Alpha) (one paragraph, no citations), ## Content (Alpha) (prose, split by ### subsections), ## Lean References and ## References.
3. Content first. State the physics as you would to a colleague who does not know the Lean names. End each claim with a Lean citation such as [1], one number per bracket. If it is not formalized yet, write [TODO], so the map doubles as a roadmap.
4. Lean references. Number them from 1 and cite each one. An entry is the file and its declarations, e.g. 1. Physlib/SpaceAndTime/Time/Basic.lean — `Time`, `Time.val`.
5. Literature and other API maps go under References and are cited with curly brackets, {1}. Don't put links in the text itself.
6. New maps start as Alpha. They become reviewed maps after Physlib's full review.

Read the full guide or see an example. Before opening a pull request, check the file with lake exe api_map_lint.