auto-task(LorentzGroup): add API-map.yaml tracking the Lorentz Group API

[ShlokVaibhav]

Summary

Adds Physlib/Relativity/LorentzGroup/API-map.yaml tracking the Lorentz Group API. Uses GitHub issue #885 as a reference for intended scope; every entry is generated from and verified against the directory's Lean files.

No Lean source is touched — this is a single new .yaml file.

Verification

Links are pinned to the base commit (3dddd61) so line numbers stay accurate.

Field / Requirement	YAML says	Source of truth
Title / Overview	"Lorentz Group" — group of matrices preserving the Minkowski metric (Λ * dual Λ = 1)	module docstring + def: Basic.lean#L14-L16, #L44-L48; scope ("Lorentz tensors, fermions, EM potential") from issue #885 Need section
ParentAPIs	Physlib/Relativity/MinkowskiMatrix.lean	key import: Basic.lean#L8
References	Jaffe, Lorentz Transformations, Rotations, and Boosts	cited in docstring: Basic.lean#L18-L21

Requirements (each checked against the code, not the issue's checkboxes)

Requirement	done	Evidence
LorentzGroup defined as matrices with Λ * dual Λ = 1	✅	Basic.lean#L44-L48 (LorentzGroup)
Instance as a group	✅	Basic.lean#L129-L138 (lorentzGroupIsGroup)
Instance as a Lie group	❌	TODO: Basic.lean#L26
Inclusion of boosts	✅	Boosts/Basic.lean#L50-L52 (boost)
Inclusion of rotations	✅	Rotations.lean#L23 (Rotations)
Different membership conditions	✅	Basic.lean#L58-L119 (mem_iff_self_mul_dual, mem_iff_dual_mul_self, mem_iff_transpose, mem_iff_neg_mem, mem_iff_transpose_mul_minkowskiMatrix_mul_self)
Proper Lorentz transforms	✅	Proper.lean#L176 (IsProper)
Orthochronous Lorentz transforms	✅	Orthochronous/Basic.lean#L35 (IsOrthochronous)
Restricted Lorentz group	✅	Restricted/Basic.lean#L29 (restricted)
Topological properties of orthochronous group	❌	TODO: Orthochronous/Basic.lean#L20
Restricted = boost × rotation	❌	TODO: Restricted/Basic.lean#L19-L20

🤖 Generated with Claude Code

[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]

Approved. Will merge shortly.