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

Physlib/Relativity/LorentzGroup/API-map.yaml

@@ -0,0 +1,61 @@
+version: v0.1
+
+Title: "Lorentz Group"
+
+Overview: |
+  The Lorentz group is the group of matrices preserving the Minkowski metric,
+  defined as matrices satisfying Λ * dual Λ = 1. It is the key symmetry group
+  of Minkowski spacetime, used throughout the library to define Lorentz tensors,
+  fermions, and the electromagnetic potential.
+
+ParentAPIs:
+  - Physlib/Relativity/MinkowskiMatrix.lean
+
+References:
+  - "Lorentz Transformations, Rotations, and Boosts, Jaffe. https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf"
+
+Requirements:
+
+  - description: LorentzGroup is defined as the set of matrices satisfying Λ * dual Λ = 1
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Basic.lean (LorentzGroup)
+
+  - description: Instance as a group
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Basic.lean (lorentzGroupIsGroup)
+
+  - description: Instance as a Lie group
+    done: false
+    location: N/A
+
+  - description: Inclusion of boosts
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Boosts/Basic.lean (boost)
+
+  - description: Inclusion of rotations
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Rotations.lean (Rotations)
+
+  - description: Different membership conditions
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Basic.lean (mem_iff_self_mul_dual, mem_iff_dual_mul_self, mem_iff_transpose, mem_iff_neg_mem, mem_iff_transpose_mul_minkowskiMatrix_mul_self)
+
+  - description: Definition of proper Lorentz transforms
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Proper.lean (IsProper)
+
+  - description: Definition of orthochronous Lorentz transforms
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Orthochronous/Basic.lean (IsOrthochronous)
+
+  - description: Definition of the restricted Lorentz group
+    done: true
+    location: Physlib/Relativity/LorentzGroup/Restricted/Basic.lean (restricted)
+
+  - description: Prove topological properties of the Orthochronous Lorentz Group
+    done: false
+    location: N/A
+
+  - description: Prove that every member of the restricted Lorentz group is a combination of a boost and a rotation
+    done: false
+    location: N/A