docs(fermions): add Weyl and Dirac fermion API maps

[Robby955]

This adds an API-map.yaml for the Weyl fermion API and one for the Dirac fermion API, addressing #906 and #907. It is a step of the first task in #1414, moving API specifications out of GitHub issues and into map files. Both issues are still the unfilled API template, so what is missing there is the specification rather than the code; these maps write down what each API already contains, where each result lives, and what is still to be built. Following the discussion in #1414, requirements with no implementation yet are carried in the map as not done rather than left out.

Nothing outside the two new files changes, and no Lean source is touched.

Files added

Physlib/Relativity/Fermions/Weyl/API-map.yaml — 14 requirements marked done, 4 still to build.

Covers the four spinor types and their module structures over ℂ, the bases indexed by Fin 2 and the expansion of an element in them, the SL(2, ℂ) representations together with their matrices in those bases, the invariant contractions between each type and its dual and their values on basis elements, the epsilon metrics and how the raw metric commutes past SL(2, ℂ), the units realizing the duality and their contraction identities, the identification of the left-handed Weyl representation with the dual left-handed Weyl representation, and the identification of pairwise tensor products with 2 × 2 matrices together with their equivariance.

Recorded as not yet done: the right-handed dual equivalence, which exists in Duals.lean only as informal_definition RightHandedWeyl.dualEquiv and informal_lemma RightHandedWeyl.dualEquiv_equivariant; the identification of the right-handed representation with the conjugate of the left-handed one; the Weyl equation; and the Majorana condition. The dual requirement that is marked done is stated for the left-handed case only, which is the half that is formalized.

One departure from the issue worth flagging: #906 lists #886, the Lorentz tensor API, as its parent. I have given the parent as the Lorentz group instead, because the dependency runs the other way around: Physlib/Relativity/Tensors/ComplexTensor/Basic.lean imports Physlib.Relativity.Fermions.Weyl.Metric, so the tensor API builds on this one rather than the reverse.

Physlib/Relativity/Fermions/Dirac/API-map.yaml — 9 requirements marked done, 7 still to build.

Covers the Dirac structure and its module structure over ℂ, the decomposition into a left-handed Weyl fermion and a dual right-handed one, the chiral basis indexed by Fin 4 and its relation to the Weyl bases, the SL(2, ℂ) representation and its equivalence with the product of the two Weyl representations, and, from Physlib/Relativity/CliffordAlgebra.lean, the gamma matrices, the Dirac algebra they generate, and the surjection onto it from the Clifford algebra of the Minkowski form.

Recorded as not yet done: the injectivity half of the Clifford isomorphism, which the source already flags as outstanding; the gamma action on Dirac; the chiral projectors; the Dirac adjoint; the Dirac bilinears; the Dirac equation; and charge conjugation with the Majorana condition.

One thing worth flagging for a reviewer: the gamma matrices are written in the Dirac representation while Dirac is presented in the chiral basis, so the gamma action on Dirac needs the change of basis between the two to be settled first. The Overview and that requirement both say so rather than leaving it implicit.

The Dirac map cites declarations in CliffordAlgebra.lean, which #1206 is currently refactoring. I checked the diff there: every name cited survives that PR, so these locations hold either way.

Reviewer map

Read Weyl/API-map.yaml first, since the Dirac map lists it as a parent API. In each file the Overview and the done requirements describe existing code; the trailing done: false entries are the roadmap and claim no locations.

python scripts/api_map_linter.py --repo . passes on both, and ./scripts/lint-style.sh is clean.

[github-actions]

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.

[jstoobysmith]

@Robby955 Let me know when you want me to look at this, won't look at it now as marked as draft :).

[jstoobysmith]

Approved - looks great.