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

[jstoobysmith]

Summary

Adds Physlib/SpaceAndTime/Time/API-map.yaml, a new in-repo tracker for the Time API
(Physlib/SpaceAndTime/Time/). The map is generated from the directory's Lean files, with
GitHub issue #855 "API: Time"
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 (the only open
API-map PR is #1266, for StatisticalMechanics/CanonicalEnsemble).

Links below pin commit 61f0412 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
(manifoldDeriv and the translation action) and are marked done: true. One requirement the
issue lists as checked (distribution derivatives) is not present in this directory and is
marked done: false.

---

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

Title / Overview

Title: Time

Overview: |
    The key data structure is `Time`, the usual one-dimensional notion of time used in
    non-relativistic physics: a real value with an arbitrary but fixed choice of units,
    origin (time zero), and orientation, equipped with the structure of a 1d real
    inner-product space. The directory additionally provides the metric-free time
    manifolds `TimeMan` (topological time) and `TimeTransMan` (time with a transitive
    translation action of `ℝ`), the type `TimeUnit` of choices of time unit, and time
    derivatives of functions from `Time` into normed spaces and manifolds.

Grounded in the Basic.lean module docstring:
Basic.lean#L13-L32

In this module we define the type Time, corresponding to time in a given (but arbitrary)
set of units, with a given (but arbitrary) choice of origin (time zero), and a choice of
orientation (i.e. a positive time direction). … With this notion of Time, becomes a 1d
vector space over ℝ with an inner product.

and on issue #855's "Key data structure": "The key data structure is Time consisting of a
real value. … It is the usual notion of Time used by physicists."

ParentAPIs

ParentAPIs:
  - Space (Physlib/SpaceAndTime/Space)
  - Lorentz vectors (Physlib/Relativity/Tensors/RealTensor/Vector)

Determined from the imports/usages in Derivatives.lean
(Derivatives.lean#L8-L10):

public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
public import Physlib.SpaceAndTime.Space.Module
public import Physlib.SpaceAndTime.Time.Basic

Both are actually used: Space d
(Derivatives.lean#L188-L192)
and Lorentz.Vector d
(Derivatives.lean#L227-L237).

References

References: []

The ## iv. References sections of the module docstrings are empty
(Basic.lean#L62-L64),
and issue #855 cites no literature — so no reference is invented.

---

Requirements

✅ Time is defined

- description: >
    The key input data structure `Time` … is defined.
  done: true
  location: Physlib/SpaceAndTime/Time/Basic.lean (Time)

Basic.lean#L74-L79

/-- The type `Time` represents the time in a given (but arbitrary) set of units, and
  with a given (but arbitrary) choice of origin. -/
@[ext]
structure Time where
  /-- The underlying real number associated with a point in time. -/
  val : ℝ

Issue #855: "The key data structure is Time … - [x] is defined".

✅ Vector space (ℝ-module) on Time

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

Basic.lean#L266-L275

instance : AddCommGroup Time where
  add_comm := by intros; ext; simp [add_comm]

instance : Module ℝ Time where
  one_smul t := by ext; simp
  ...

Issue #855: "- [x] The API shall contain an instance of a vector space on Time."

✅ Ordering on Time

- description: The API contains an ordering (orientation) on `Time`.
  done: true
  location: Physlib/SpaceAndTime/Time/Basic.lean (LE Time, PartialOrder Time)

Basic.lean#L178-L188

/-- The choice of an orientation on `Time`. -/
instance : LE Time where
  le t1 t2 := t1.val ≤ t2.val
...
instance : PartialOrder Time where

Issue #855: "- [x] The API shall contain an ordering on Time".

✅ Norm on Time

- description: The API contains a norm on `Time`, making it a normed real vector space.
  done: true
  location: >
    Physlib/SpaceAndTime/Time/Basic.lean (Norm Time, NormedAddCommGroup Time,
    NormedSpace ℝ Time)

Basic.lean#L283-L320

instance : Norm Time where
  norm t := ‖t.val‖
...
instance : NormedAddCommGroup Time where
...
instance : NormedSpace ℝ Time where

Issue #855: "- [x] The API shall contain a norm on Time."

✅ Inner product on Time

- description: >
    The API contains an inner product on `Time`, making it a one-dimensional real
    inner-product space.
  done: true
  location: Physlib/SpaceAndTime/Time/Basic.lean (Inner ℝ Time, InnerProductSpace ℝ Time)

Basic.lean#L330-L341

instance : Inner ℝ Time where
  inner t1 t2 := t1.val * t2.val
...
noncomputable instance : InnerProductSpace ℝ Time where

(Not in the issue checklist, but stated in the Basic.lean overview — "a 1d vector space over ℝ with an inner product" — and genuinely provided.)

✅ Derivative of functions Time → normed space

- description: The API contains the derivative of functions from `Time` to a normed space.
  done: true
  location: Physlib/SpaceAndTime/Time/Derivatives.lean (Time.deriv, notation ∂ₜ)

Derivatives.lean#L58-L67

/-- Given a function `f : Time → M` the derivative of `f`. -/
noncomputable def deriv [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    (f : Time → M) : Time → M :=
  (fun t => fderiv ℝ f t 1)

@[inherit_doc deriv]
scoped notation "∂ₜ" => deriv

Issue #855: "- [x] The API shall contain the derivatives of functions from Time to a normed space."

✅ Derivative of functions Time → manifold (issue unchecked, but implemented)

- description: The API contains the derivative of functions from `Time` to a manifold.
  done: true
  location: Physlib/SpaceAndTime/Time/Derivatives.lean (Time.manifoldDeriv)

Derivatives.lean#L76-L81

/-- The time derivative of a function from `Time` to a manifold, as a tangent vector at
the value of the function. -/
noncomputable def manifoldDeriv {E H N : Type} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [TopologicalSpace N]
    [ChartedSpace H N] (f : Time → N) : (t : Time) → TangentSpace I (f t) :=
  fun t => mfderiv 𝓘(ℝ, Time) I f t ((1 : Time) : TangentSpace 𝓘(ℝ, Time) t)

Issue #855 lists this as - [ ] (unchecked), but the code provides it, so it is done: true.

✅ Translation group action (issue unchecked, but implemented)

- description: >
    The API contains an action of the (additive) translation group `ℝ` on time,
    realised as a transitive `AddAction ℝ` on the time manifold `TimeTransMan`.
  done: true
  location: >
    Physlib/SpaceAndTime/Time/TimeTransMan.lean (TimeTransMan, VAdd ℝ TimeTransMan,
    AddAction ℝ TimeTransMan)

TimeTransMan.lean#L170-L185

instance : VAdd ℝ TimeTransMan where
  vadd p t := { val := p + t.val }
...
instance : AddAction ℝ TimeTransMan where

The type's docstring describes it as "the time manifold with a transitive action of ℝ"
(TimeTransMan.lean#L13-L16).
Issue #855 lists "- [ ] action of the translation group on Time" as unchecked; the directory
provides exactly this action (on the metric/origin-free TimeTransMan), so it is done: true.

✅ Topological time manifold TimeMan

- description: >
    The API contains the topological time manifold `TimeMan` …
  done: true
  location: Physlib/SpaceAndTime/Time/TimeMan.lean (TimeMan, valDiffeomorphism)

TimeMan.lean#L33-L38
and
TimeMan.lean#L135-L142

structure TimeMan where
  /-- The choice of a map from `TimeMan` to `ℝ`. -/
  val : ℝ
...
noncomputable def valDiffeomorphism : TimeMan ≃ₘ^ω⟮𝓘(ℝ, ℝ), 𝓘(ℝ, ℝ)⟯ ℝ where

✅ TimeUnit (choices of time unit)

- description: >
    The API contains the type `TimeUnit` … together with concrete units such as seconds.
  done: true
  location: Physlib/SpaceAndTime/Time/TimeUnit.lean (TimeUnit, scale, seconds)

TimeUnit.lean#L34-L39
and
TimeUnit.lean#L144-L145

structure TimeUnit : Type where
  /-- The underlying scale of the unit. -/
  val : ℝ
  property : 0 < val
...
/-- The definition of a time unit of seconds. -/
def seconds : TimeUnit := ⟨1, by norm_num⟩

✅ toTime homeomorphism TimeTransMan ≃ₜ Time and operations

- description: >
    The API contains, for a choice of origin and time unit, the homeomorphism `toTime`
    between `TimeTransMan` and `Time`, with the supporting signed-difference, add-time
    and negation operations.
  done: true
  location: Physlib/SpaceAndTime/Time/TimeTransMan.lean (toTime, diff, addTime, neg)

TimeTransMan.lean#L342-L344

/-- With a choice of zero `zero : TimeTransMan` and a choice of units `x : TimeUnit`,
  `toTime` is the homeomorphism between the type `TimeTransMan` and `Time`. -/
noncomputable def toTime (zero : TimeTransMan) (x : TimeUnit) : TimeTransMan ≃ₜ Time where

Supporting ops: diff
(L221),
addTime
(L299),
neg
(L328).

❌ Derivatives of distributions Time → normed space (issue checked, but absent here)

- description: The API shall contain the derivatives of distributions from `Time` to normed spaces.
  done: false
  location: N/A

Issue #855 lists this as - [x], but grep -ri "distrib\|Schwartz\|tempered" Physlib/SpaceAndTime/Time/
returns nothing — distribution derivatives are not provided in this directory (they live under
Physlib/SpaceAndTime/TimeAndSpace/ and Physlib/Mathematics/Distribution/). Marked done: false
to reflect what this directory contains.

❌ Derivatives of distributions Time → manifold

- description: The API shall contain the derivatives of distributions from `Time` to manifolds.
  done: false
  location: N/A

Issue #855 lists this as - [ ]; not present in this directory.

---

Verification

• python3 -c "import yaml; yaml.safe_load(open(...))" → valid YAML; top-level keys exactly
  version, Title, Overview, ParentAPIs, References, Requirements; 11 done: true, 2 done: false.
• Every done: true declaration confirmed in the source (line numbers above); Time.manifoldDeriv
  and TimeTransMan.toTime additionally confirmed via lean_verify (standard axioms only).
• lake build → Build completed successfully (9107 jobs); only pre-existing deprecation
  warnings unrelated to this change. (YAML-only addition cannot affect the Lean build graph.)
• 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.