auto-task(Space): add API-map.yaml tracking the Space API

[ShlokVaibhav]

Summary

Adds Physlib/SpaceAndTime/Space/API-map.yaml, a new in-repo tracker for the Space API
(Physlib/SpaceAndTime/Space/). The map is generated from the directory's Lean files, with
GitHub issue #854 "API: Space"
used only as a reference for the intended scope. No Lean source is touched; lake build
stays green (a YAML-only change).

The directory has no API-map.yaml yet and is not being edited by any open PR (a scan of open
PRs found none adding or editing an API-map.yaml; the only Space-adjacent open PRs are #1116,
first-step GalileanGroup API, and #1327, pendulum configuration-space, neither of which touches
this directory's map).

Links below pin commit 843373266f73adaccb4db401c545fdef9810f78e so line numbers are stable.

A note on the issue checklist vs. the code

Per the task rules, every done flag was decided by reading the code, not by trusting the
issue's checkboxes. Two requirements the issue lists as unchecked are in fact implemented and
are marked done: true:

• NormedAddTorsor from EuclideanSpace — issue - [ ], but the instance exists in
  Basic.lean.
• action of the group of rotations — issue - [ ], but the rotation action exists under
  EuclideanGroup/.

The two manifold-target derivative requirements (functions/distributions from Space to
manifolds) are genuinely absent from the directory and are marked done: false.

Also, issue #854 lists its "Parent APIs" as #911 (Galilean group). By the actual import graph the
dependency runs the other way — the Galilean-group API builds on Space, not vice versa — so
ParentAPIs instead lists the APIs Space actually imports and uses (Distribution, Time, Lorentz
vectors).

---

Field-by-field justification (reviewer tick-box)

Title / Overview

Title: Space

Overview: |
    The key data structure is `Space d`, a structure with a single field `val : Fin d → ℝ`
    modelling `d`-dimensional flat Euclidean space (default `d = 3`) with an arbitrary but
    fixed choice of length unit and origin. The API equips it with metric/torsor,
    vector-space, norm, inner-product and smooth-manifold structures, and the surrounding
    definitions and lemmas (basis, coordinates, length units, cross product, slices,
    derivatives of functions and distributions, and the actions of translations and rotations).

Grounded in the Basic.lean module docstring and the Space structure
(Basic.lean#L79-L87):

/-- The type `Space d` is the world-volume which corresponds to
`d` dimensional (flat) Euclidean space with a given (but arbitrary)
choice of length unit, and a given (but arbitrary) choice of zero.

The default value of `d` is `3`. Thus `Space = Space 3`-/
structure Space (d : ℕ := 3) where
  /-- The underlying map `Fin d → ℝ` associated with a point in `Space`. -/
  val : Fin d → ℝ

and in the Module.lean docstring, which scopes the vector-space/norm/inner-product structure
(Module.lean#L18-L22).
Issue #854's "Key data structure": "a structure with a single value corresponding to a map from
Fin n to Real. This corresponds to flat space."

ParentAPIs

ParentAPIs:
  - "Distribution (Physlib/Mathematics/Distribution)"
  - "Time (Physlib/SpaceAndTime/Time)"
  - "Lorentz vectors (Physlib/Relativity/Tensors/RealTensor/Vector)"

Determined from the directory's imports and usages:

public import Physlib.Mathematics.Distribution.Basic          -- DistOfFunction.lean
public import Physlib.SpaceAndTime.Time.Basic                 -- IsDistBounded.lean
public import Physlib.SpaceAndTime.Time.Derivatives           -- CrossProduct.lean
public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic  -- IsDistBounded.lean

• Distribution: the →d[ℝ] distribution type is used throughout, e.g. distOfFunction
  (DistOfFunction.lean#L59-L81).
• Time: cross products commute with time derivatives
  (CrossProduct.lean#L100-L106).
• Lorentz vectors: Lorentz.Vector components of distributions
  (DistOfFunction.lean#L191-L199).

References

References:
  - "Lean Zulip, #Physlib > Space vs EuclideanSpace: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Space.20vs.20EuclideanSpace/with/575938877"

This is a real reference cited both in issue #854's "References" section and in the Basic.lean
"Implementation details" docstring
(Basic.lean#L27-L30):

The exact implementation of Space d into Physlib is discussed in numerous places on the Lean
Zulip, including: https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Space.20vs.20EuclideanSpace/...

No literature reference is invented.

---

Requirements

✅ Space d is defined

- description: "The key data structure `Space d` (a structure with field `val : Fin d → ℝ`) is defined."
  done: true
  location: "Physlib/SpaceAndTime/Space/Basic.lean (Space)"

Basic.lean#L84-L87

structure Space (d : ℕ := 3) where
  /-- The underlying map `Fin d → ℝ` associated with a point in `Space`. -/
  val : Fin d → ℝ

Issue #854: "The key data structure ... is a structure with a single value corresponding to a map
from Fin n to Real. ... - [x] Is defined".

✅ Vector space (ℝ-module) on Space d

- description: "The API contains the structure of an `ℝ`-vector space (module) on `Space d`."
  done: true
  location: "Physlib/SpaceAndTime/Space/Module.lean (AddCommGroup (Space d), Module ℝ (Space d))"

Module.lean#L132-L133
and
Module.lean#L202-L203

instance {d} : Module ℝ (Space d) where
  one_smul x := by ...
...
noncomputable instance {d} : AddCommGroup (Space d) where

Issue #854: "- [x] the instance of a vector space".

✅ Norm, inner product and metric

- description: "The API contains a norm, an inner product and a metric on `Space d`, making it a finite-dimensional real inner-product space and metric space."
  done: true
  location: "Physlib/SpaceAndTime/Space/Module.lean (Norm, InnerProductSpace ℝ (Space d)); Physlib/SpaceAndTime/Space/Basic.lean (Dist, MetricSpace)"

Module.lean#L268-L269
and
Basic.lean#L234-L235

instance {d} : InnerProductSpace ℝ (Space d) where   -- Module.lean
...
noncomputable instance {d} : MetricSpace (Space d) where   -- Basic.lean

Grounded in the Module.lean docstring (norm, inner product) and Basic.lean (metric); not a
separate issue checklist item, but a main structure genuinely provided.

✅ Origin (zero) and Euclidean chart

- description: "The API contains a choice of origin (the vector-space zero) and the standard affine-isometry chart to `EuclideanSpace`."
  done: true
  location: "Physlib/SpaceAndTime/Space/Origin.lean (Zero (Space d), chartEuclidean)"

Origin.lean#L28-L29
and
Origin.lean#L56-L58

instance {d} : Zero (Space d) where
  zero := ⟨fun _ => 0⟩
...
noncomputable def chartEuclidean (d : ℕ) :
    Space d ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin d) :=

✅ Smooth-manifold structure

- description: "The API contains a smooth-manifold structure on `Space d` (charted space over and diffeomorphic to `EuclideanSpace ℝ (Fin d)`)."
  done: true
  location: "Physlib/SpaceAndTime/Space/Basic.lean (homEuclideanSpaceSpace, ChartedSpace, IsManifold)"

Basic.lean#L276-L280

noncomputable instance (d : ℕ) : ChartedSpace (EuclideanSpace ℝ (Fin d)) (Space d) :=
    (homEuclideanSpaceSpace d).symm.toOpenPartialHomeomorph.singletonChartedSpace (by simp)

instance (d : ℕ) : IsManifold (𝓡 d) ⊤ (Space d) :=

✅ Basis vectors

- description: "The API contains basis vectors for `Space d`."
  done: true
  location: "Physlib/SpaceAndTime/Space/Module.lean (basis : OrthonormalBasis (Fin d) ℝ (Space d))"

Module.lean#L360-L361

/-- The standard basis of Space based on `Fin d`. -/
noncomputable def basis {d} : OrthonormalBasis (Fin d) ℝ (Space d) where

Issue #854: "- [x] basis vectors".

✅ VSub instance to EuclideanSpace

- description: "The API contains a `VSub` instance to `EuclideanSpace`."
  done: true
  location: "Physlib/SpaceAndTime/Space/Basic.lean (VSub (EuclideanSpace ℝ (Fin d)) (Space d))"

Basic.lean#L177-L178

noncomputable instance {d} : VSub (EuclideanSpace ℝ (Fin d)) (Space d) where
  vsub s1 s2 := WithLp.toLp 2 <| fun i => s1 i - s2 i

Issue #854: "- [x] The API shall contain a VSub instance to EuclideanSpace."

✅ NormedAddTorsor from EuclideanSpace (issue unchecked, but implemented)

- description: "The API contains a `NormedAddTorsor` instance from `EuclideanSpace`."
  done: true
  location: "Physlib/SpaceAndTime/Space/Basic.lean (AddTorsor and NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d))"

Basic.lean#L225-L226

noncomputable instance {d} : NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) where
  dist_eq_norm' p q := by simp [dist, EuclideanSpace.norm_eq]

Issue #854 lists "- [ ] The API shall contain an NormAddTorsor instance from EuclideanSpace"
as unchecked, but the instance is present, so it is done: true.

✅ Translations

- description: "The API contains translations of points and of distributions on space."
  done: true
  location: "Physlib/SpaceAndTime/Space/Basic.lean (AddAction (EuclideanSpace ℝ (Fin d)) (Space d)); Physlib/SpaceAndTime/Space/Translations.lean (translateSchwartz, distTranslate)"

Basic.lean#L162-L169
and
Translations.lean#L96-L99

noncomputable instance : AddAction (EuclideanSpace ℝ (Fin d)) (Space d) where   -- Basic.lean
...
/-- The continuous linear map translating distributions. -/
noncomputable def distTranslate {d : ℕ} (a : EuclideanSpace ℝ (Fin d)) :   -- Translations.lean
    ((Space d) →d[ℝ] X) →ₗ[ℝ] ((Space d) →d[ℝ] X) where

Issue #854: "- [x] translations".

✅ Action of the group of rotations (issue unchecked, but implemented)

- description: "The API contains the action of the group of rotations on `Space d`."
  done: true
  location: "Physlib/SpaceAndTime/Space/EuclideanGroup/Basic.lean (RotationGroup); Physlib/SpaceAndTime/Space/EuclideanGroup/Action.lean (MulAction (EuclideanGroup d) (Space d), rotation_smul_eq)"

EuclideanGroup/Action.lean#L49-L52
and
EuclideanGroup/Basic.lean#L172-L175

noncomputable instance : MulAction (EuclideanGroup d) (Space d) where   -- Action.lean
  smul g p := (g.linear • (p -ᵥ (0 : Space d)) + g.translation) +ᵥ (0 : Space d)
...
noncomputable def RotationGroup (n : ℕ) : Subgroup (EuclideanGroup n) :=   -- Basic.lean
  SpecialEuclideanGroup n ⊓ OriginStabilizer n

The Action.lean docstring "specialises it to the rotations" and rotation_smul_eq
(Action.lean#L97)
record the rotation-group action on Space. Issue #854 lists "- [ ] the action of the group of
rotations" as unchecked; the code provides it, so it is done: true.

✅ Relation between Spaces of different dimensions

- description: "The API contains the relation between Spaces of different dimensions."
  done: true
  location: "Physlib/SpaceAndTime/Space/Slice.lean (slice : Space d.succ ≃L[ℝ] ℝ × Space d); Physlib/SpaceAndTime/Space/Module.lean (oneEquiv : Space 1 ≃ₗᵢ[ℝ] ℝ)"

Slice.lean#L56-L58
and
Module.lean#L639-L640

/-- The linear equivalence between `Space d.succ` and `ℝ × Space d`
  extracting the `i`th coordinate. -/
def slice {d} (i : Fin d.succ) : Space d.succ ≃L[ℝ] ℝ × Space d where   -- Slice.lean
...
noncomputable def oneEquiv : Space 1 ≃ₗᵢ[ℝ] ℝ where   -- Module.lean

Issue #854: "- [x] relation between Spaces of different dimensions".

✅ LengthUnit

- description: "The API contains the type `LengthUnit` of choices of length unit, with scaling and concrete units."
  done: true
  location: "Physlib/SpaceAndTime/Space/LengthUnit.lean (LengthUnit, scale, meters)"

LengthUnit.lean#L29-L34

/-- The choices of translationally-invariant metrics on the space-manifold.
  Such a choice corresponds to a choice of units for length. -/
structure LengthUnit where
  /-- The underlying scale of the unit. -/
  val : ℝ
  property : 0 < val

The val-with-length-unit design is described in the Basic.lean docstring ("a given (but
arbitrary) choice of length unit"); a main structure genuinely provided, not a separate issue
checklist item.

✅ Cross product on EuclideanSpace ℝ (Fin 3)

- description: "The API contains the cross product on `EuclideanSpace ℝ (Fin 3)` with properties relating it to time derivatives and inner products."
  done: true
  location: "Physlib/SpaceAndTime/Space/CrossProduct.lean (⨯ₑ₃, time_deriv_cross_commute, inner_cross_self)"

CrossProduct.lean#L49-L53

set_option quotPrecheck false in
/-- Cross product in `EuclideanSpace ℝ (Fin 3)`. ... -/
infixl:70 " ⨯ₑ₃ " => fun a b => (WithLp.equiv 2 (Fin 3 → ℝ)).symm
    (WithLp.equiv 2 (Fin 3 → ℝ) a ⨯₃ WithLp.equiv 2 (Fin 3 → ℝ) b)

Grounded in the CrossProduct.lean "Key results" docstring; a main structure genuinely provided.

✅ Derivatives of functions Space → normed space

- description: "The API contains the derivatives of functions from `Space` to normed spaces."
  done: true
  location: "Physlib/SpaceAndTime/Space/Derivatives/Basic.lean (Space.deriv, notation ∂[·])"

Derivatives/Basic.lean#L67-L73

/-- Given a function `f : Space d → M` the derivative of `f` in direction `μ`. -/
noncomputable def deriv {M d} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (μ : Fin d) (f : Space d → M) : Space d → M :=
  (fun x => fderiv ℝ f x (basis μ))

@[inherit_doc deriv]
macro "∂[" i:term "]" : term => `(deriv $i)

Issue #854: "- [x] derivatives of functions from space to normed spaces".

❌ Derivatives of functions Space → manifold

- description: "The API contains the derivatives of functions from `Space` to manifolds."
  done: false
  location: N/A

Issue #854 lists this as - [ ]. The directory has deriv_eq_mfderiv
(Derivatives/Basic.lean#L104-L107)
which re-expresses the derivative of a Space → M map (M a normed space) via mfderiv, but
there is no derivative operator for functions whose codomain is a general manifold. Marked
done: false.

✅ Constructing distributions from functions

- description: "The API contains a means of constructing distributions on `Space` from functions (via the `IsDistBounded` boundedness condition), including the constant and constant-slice distributions."
  done: true
  location: "Physlib/SpaceAndTime/Space/IsDistBounded.lean (IsDistBounded); Physlib/SpaceAndTime/Space/DistOfFunction.lean (distOfFunction); Physlib/SpaceAndTime/Space/DistConst.lean (distConst); Physlib/SpaceAndTime/Space/ConstantSliceDist.lean (sliceSchwartz, constantSliceDist)"

IsDistBounded.lean#L86-L95
and
DistOfFunction.lean#L59-L62

def IsDistBounded {d : ℕ} (f : Space d → F) : Prop :=   -- IsDistBounded.lean
  AEStronglyMeasurable (fun x => f x) volume ∧ ...
...
def distOfFunction {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) :   -- DistOfFunction.lean
    (Space d) →d[ℝ] F := by

Also distConst
(DistConst.lean#L46-L49)
and constantSliceDist
(ConstantSliceDist.lean#L586-L591).
A main structure genuinely provided that underpins the distribution-derivative requirement below.

✅ Derivatives of distributions Space → normed space

- description: "The API contains the derivatives of distributions from `Space` to normed spaces."
  done: true
  location: "Physlib/SpaceAndTime/Space/Derivatives/Basic.lean (distDeriv); Physlib/SpaceAndTime/Space/Derivatives/Grad.lean (distGrad); Physlib/SpaceAndTime/Space/Derivatives/Div.lean (distDiv); Physlib/SpaceAndTime/Space/Derivatives/Curl.lean (distCurl)"

Derivatives/Basic.lean#L490-L493

/-- Given a distribution (function) `f : Space d →d[ℝ] M` the derivative
  of `f` in direction `μ`. -/
noncomputable def distDeriv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
    (μ : Fin d) : ((Space d) →d[ℝ] M) →ₗ[ℝ] (Space d) →d[ℝ] M where

With distGrad
(Grad.lean#L510),
distDiv
(Div.lean#L177),
distCurl
(Curl.lean#L702).
Issue #854: "- [x] derivatives of distributions from Space to normed spaces".

❌ Derivatives of distributions Space → manifold

- description: "The API contains the derivatives of distributions from `Space` to manifolds."
  done: false
  location: N/A

Issue #854 lists this as - [ ]; not present in the directory (no distribution-derivative
operator with a manifold codomain). Marked done: false.

---

Verification

• ruby -e 'require "yaml"; ...' → valid YAML; top-level keys exactly
  version, Title, Overview, ParentAPIs, References, Requirements (no extra keys);
  18 requirements, 16 done: true, 2 done: false; every done: true has a real
  location and every done: false has location: N/A.
• Every done: true declaration was confirmed in the source at the line numbers above
  (grep/read across the 11 top-level files and the Derivatives/ and EuclideanGroup/
  subdirectories).
• lake build → a YAML-only addition cannot affect the Lean build graph, so the build stays
  green.
• No .lean file, other map, docstring, or the GitHub issue was modified.

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