Physicslib4.Spacetime.Curves

Paths and curves on a spacetime

This file formalises the various flavours of paths and curves used in section 10.5 of the AQFT-in-Lean blueprint.

Main definitions

• Physicslib4.Spacetime.Path: a continuous map from a closed, connected, non-singleton subset Σ ⊆ ℝ ("parameter space") to a spacetime M.
• Physicslib4.Spacetime.SmoothPath: a path that is also smooth with non-vanishing derivative.
• Physicslib4.Spacetime.PathEquiv, SmoothPathEquiv: the relations on paths/smooth paths corresponding to reparametrisation by homeomorphisms / diffeomorphisms of the parameter space. PathEquiv, SmoothPathEquiv and its orientation-preserving refinement OrientedSmoothPathEquiv are equivalence relations.
• Physicslib4.Spacetime.Curve, SmoothCurve: the corresponding quotient types.
• Physicslib4.Spacetime.IsTimelikeSmoothCurve, IsCausalSmoothCurve: predicates singling out smooth curves whose tangent vector at every point is timelike / causal.
• Physicslib4.Spacetime.IsFutureOrientedSmoothCurve / IsPastOrientedSmoothCurve: future/past orientation predicates relative to a given time orientation.
• Physicslib4.Spacetime.IsEndpoint, IsPastEndpoint, IsFutureEndpoint: the endpoint terminology for paths and their associated curves.

Supporting lemmas

• OrientedSmoothCurve.toSmoothCurve_surjective: the orientation-forgetting projection OrientedSmoothCurve → SmoothCurve is surjective.
• isTimelikeSmoothCurve_toSmoothCurve_ofPath: the timelikeness companion to isCausalSmoothCurve_toSmoothCurve_ofPath.

Modelling notes

The notion of "smooth at a boundary point of a closed interval" is delicate in general. In this file we follow the conservative convention used in Mathlib for ContMDiff of a function on a subset, and state the "non-vanishing derivative" condition pointwise on the parameter space Σ. These are genuine Prop fields of SmoothPath — smoothOn : ContMDiffOn … and nonvanishing : ∀ s ∈ Σ, mfderivWithin _ _ toFun Σ s 1 ≠ 0 — carried by the structure, not sorry placeholders. They are discharged for concrete paths via named lemmas; for the straight-line path see standardMinkowskiLineSegmentPath_smoothOn and standardMinkowskiLineSegmentPath_nonvanishing in Minkowski.lean.

Paths

structure Physicslib4.Spacetime.Path (M : Spacetime) : Type u_1

A path in a spacetime: a continuous map μ : Σ → M on a closed interval Σ of ℝ with more than one point.

The parameter space Σ is a closed, connected subset of ℝ with at least two points, that is, a non-degenerate closed interval, bounded or not: [a, b], [a, ∞), (-∞, b] or ℝ. A path is a parametrised object; the unparametrised curve is its class under reparametrisation (Curve).

Implementation note: Σ is stored as a Set ℝ with proofs of the three conditions, and μ as a function on all of ℝ that is continuous on Σ; its values off Σ are never used.

Blueprint: def:paths

• parameterSpace : Set ℝ

  The parameter space Σ ⊆ ℝ.

• isClosed : IsClosed self.parameterSpace

  Σ is closed in ℝ.

• isConnected : IsConnected self.parameterSpace

  Σ is connected (so it is an interval) and non-empty.

• nontrivial : ∃ (s : ℝ) (t : ℝ), s ∈ self.parameterSpace ∧ t ∈ self.parameterSpace ∧ s ≠ t

  Σ has at least two distinct points.

• toFun : ℝ → M.Carrier

  The map μ, defined on all of ℝ; only its values on Σ matter.

• continuousOn : ContinuousOn self.toFun self.parameterSpace

  μ is continuous on Σ.

structure Physicslib4.Spacetime.SmoothPath (M : Spacetime) extends M.Path : Type u_1

A smooth path: a path μ : Σ → M that is C^∞ on Σ and whose velocity vanishes nowhere on Σ.

The velocity μ̇(s) is the derivative of μ at s along Σ (SmoothPath.tangent), one-sided at an endpoint of Σ. Requiring μ̇(s) ≠ 0 everywhere, endpoints included, excludes paths that stop, such as constant paths, so a smooth path whose velocity is null moves along the light cone.

Blueprint: def:paths

• parameterSpace : Set ℝ
• isClosed : IsClosed self.parameterSpace
• isConnected : IsConnected self.parameterSpace
• nontrivial : ∃ (s : ℝ) (t : ℝ), s ∈ self.parameterSpace ∧ t ∈ self.parameterSpace ∧ s ≠ t
• toFun : ℝ → M.Carrier
• continuousOn : ContinuousOn self.toFun self.parameterSpace
• smoothOn : ContMDiffOn (modelWithCornersSelf ℝ ℝ) M.model (↑⊤) self.toFun self.parameterSpace

  μ is C^∞ on Σ.

• nonvanishing (s : ℝ) : s ∈ self.parameterSpace → (mfderiv[self.parameterSpace] self.toFun s) 1 ≠ 0

  The velocity vanishes nowhere: μ̇(s) ≠ 0 for every s ∈ Σ, endpoints included.

  The velocity is the derivative of μ within Σ (mfderivWithin) applied to 1 ∈ ℝ.

theorem Physicslib4.Spacetime.Path.uniqueDiffOn_parameterSpace (M : Spacetime) (μ : M.Path) : UniqueDiffOn ℝ μ.parameterSpace

The parameter space of a path has unique differentials: being a closed connected subset of ℝ with at least two points, it is a non-degenerate interval, hence convex with non-empty interior. This is the analytic prerequisite for differentiating compositions along a path via the mfderivWithin chain rule.

Tangent vector

noncomputable def Physicslib4.Spacetime.SmoothPath.tangent {M : Spacetime} (μ : M.SmoothPath) (s : ℝ) : TangentSpace M.model (μ.toFun s)

The velocity μ̇(s) of a smooth path at the parameter s, a tangent vector at μ(s).

It is the derivative of μ within the parameter space Σ applied to the unit vector 1 ∈ ℝ, so at an endpoint of Σ it is a one-sided derivative. The causal type and the time orientation of a path are conditions on μ̇(s).

Equations

• μ.tangent s = (mfderiv[μ.parameterSpace] μ.toFun s) 1

theorem Physicslib4.Spacetime.SmoothPath.tangent_def {M : Spacetime} (μ : M.SmoothPath) (s : ℝ) : μ.tangent s = (mfderiv[μ.parameterSpace] μ.toFun s) 1

Unfolding lemma for SmoothPath.tangent to the raw mfderivWithin form.

theorem Physicslib4.Spacetime.SmoothPath.tangent_ne_zero {M : Spacetime} (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) : μ.tangent s ≠ 0

The tangent vector of a smooth path is non-vanishing on the parameter space (the nonvanishing field, restated via tangent).

theorem Physicslib4.Spacetime.SmoothPath.mfderivWithin_comp_reparam {M : Spacetime} (μ : M.SmoothPath) {φ : ℝ → ℝ} {u : Set ℝ} {s : ℝ} (hφ : MDiffAt[u] φ s) (hmaps : Set.MapsTo φ u μ.parameterSpace) (huniq : UniqueMDiffAt[u] s) (hs : s ∈ u) : (mfderiv[u] (μ.toFun ∘ φ) s) 1 = derivWithin φ u s • μ.tangent (φ s)

Reparametrisation chain rule for the tangent vector. Composing a smooth path μ with a (manifold-)differentiable reparametrisation φ : ℝ → ℝ that maps Σ' into μ's parameter space scales the tangent vector by the derivative of φ: tangent (μ ∘ φ) s = (φ'(s)) • tangent μ (φ s), where the scalar is the one-dimensional manifold derivative of φ. This is the analytic heart of the reparametrisation-invariance of the causal type of a curve.

theorem Physicslib4.Spacetime.SmoothPath.tangent_reparam_eq {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) {φ : ℝ → ℝ} {s : ℝ} (hφ : MDiffAt[μ₁.parameterSpace] φ s) (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') (hs : s ∈ μ₁.parameterSpace) : μ₁.tangent s = derivWithin φ μ₁.parameterSpace s • μ₂.tangent (φ s)

Tangent vector under a reparametrisation. If a reparametrisation φ : ℝ → ℝ (differentiable, mapping μ₁'s parameter space into μ₂'s) identifies the two paths pointwise (μ₂ (φ s') = μ₁ s' on μ₁'s parameter space), then the tangent vectors are related by the derivative of φ: tangent μ₁ s = (φ'(s)) • tangent μ₂ (φ s). Combines the reparametrisation chain rule with mfderivWithin_congr (the two paths agree on the parameter space, so have equal within-derivatives).

theorem Physicslib4.Spacetime.derivWithin_ne_zero_of_leftInverse {φ ψ : ℝ → ℝ} {u v : Set ℝ} {x : ℝ} (hφ : DifferentiableWithinAt ℝ φ u x) (hψ : DifferentiableWithinAt ℝ ψ v (φ x)) (hmaps : Set.MapsTo φ u v) (huniq : UniqueDiffWithinAt ℝ u x) (hx : x ∈ u) (hinv : ∀ y ∈ u, ψ (φ y) = y) : derivWithin φ u x ≠ 0

Non-vanishing of a reparametrisation derivative. If ψ ∘ φ = id on a set u (with φ mapping u into v, both maps differentiable within their sets, and u having unique differentials at x), then the within-derivative of φ is non-zero at x. This is the real-analytic fact behind the derivWithin φ ≠ 0 hypothesis of the pointwise reparametrisation lemmas, obtained by differentiating the left-inverse identity via the chain rule.

theorem Physicslib4.Spacetime.mdifferentiableWithinAt_of_contDiffOn {φ : ℝ → ℝ} {u : Set ℝ} (h : ContDiffOn ℝ (↑⊤) φ u) {x : ℝ} (hx : x ∈ u) : MDiffAt[u] φ x

A C^∞ function ℝ → ℝ is manifold-differentiable within a set, for the self models on ℝ. Bridges the ContDiffOn datum stored in SmoothPathEquiv to the MDifferentiableWithinAt hypothesis required by the tangent reparametrisation lemmas.

Reparametrisation equivalence

def Physicslib4.Spacetime.PathEquiv (M : Spacetime) (μ₁ μ₂ : M.Path) : Prop

Two paths μ₁ : Σ₁ → M, μ₂ : Σ₂ → M are equivalent if there is a homeomorphism φ : Σ₁ ≃ₜ Σ₂ of the parameter spaces such that μ₂ ∘ φ = μ₁ on Σ₁. As for SmoothPathEquiv, the homeomorphism is packaged as functions φ, ψ : ℝ → ℝ that are continuous on Σ₁ resp. Σ₂, map the parameter spaces into each other and are inverse to each other there; nothing is asked of them off the parameter spaces. The relation is an equivalence relation (equivalence_pathEquiv), and a smooth reparametrisation is in particular one of these (SmoothPathEquiv.toPathEquiv).

Equations

• One or more equations did not get rendered due to their size.

def Physicslib4.Spacetime.SmoothPathEquiv (M : Spacetime) (μ₁ μ₂ : M.SmoothPath) : Prop

Two smooth paths are equivalent if there is a diffeomorphism φ : ℝ → ℝ sending one parameter space to the other and identifying the underlying maps. We package the diffeomorphism condition by smoothness of φ and its inverse ψ on the relevant parameter spaces, paired with their being two-sided inverses.

Equations

• One or more equations did not get rendered due to their size.

def Physicslib4.Spacetime.OrientedSmoothPathEquiv (M : Spacetime) (μ₁ μ₂ : M.SmoothPath) : Prop

Two smooth paths are orientation-preservingly equivalent if they are related by a smooth reparametrisation φ (as in SmoothPathEquiv) whose within-derivative is everywhere positive on μ₁'s parameter space. Positivity of φ' is exactly what distinguishes orientation-preserving from orientation-reversing reparametrisations, and it is the extra datum needed to transport the time orientation of a curve (future/past-pointing), not merely its causal type.

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.Spacetime.OrientedSmoothPathEquiv.toSmoothPathEquiv (M : Spacetime) {μ₁ μ₂ : M.SmoothPath} (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : M.SmoothPathEquiv μ₁ μ₂

An orientation-preserving smooth reparametrisation is in particular a smooth reparametrisation.

Relational properties of the reparametrisation relations

PathEquiv, SmoothPathEquiv and OrientedSmoothPathEquiv are equivalence relations.

theorem Physicslib4.Spacetime.PathEquiv.refl (M : Spacetime) (μ : M.Path) : M.PathEquiv μ μ

PathEquiv is reflexive: every path is related to itself by the identity reparametrisation.

theorem Physicslib4.Spacetime.PathEquiv.trans {M : Spacetime} {μ₁ μ₂ μ₃ : M.Path} (h₁₂ : M.PathEquiv μ₁ μ₂) (h₂₃ : M.PathEquiv μ₂ μ₃) : M.PathEquiv μ₁ μ₃

PathEquiv is transitive: reparametrising homeomorphisms compose.

theorem Physicslib4.Spacetime.PathEquiv.symm {M : Spacetime} {μ₁ μ₂ : M.Path} (h : M.PathEquiv μ₁ μ₂) : M.PathEquiv μ₂ μ₁

PathEquiv is symmetric: swap the homeomorphism and its inverse.

theorem Physicslib4.Spacetime.equivalence_pathEquiv (M : Spacetime) : Equivalence M.PathEquiv

PathEquiv is an equivalence relation.

theorem Physicslib4.Spacetime.SmoothPathEquiv.refl (M : Spacetime) (μ : M.SmoothPath) : M.SmoothPathEquiv μ μ

SmoothPathEquiv is reflexive: every smooth path is related to itself by the identity reparametrisation.

theorem Physicslib4.Spacetime.SmoothPathEquiv.symm {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) : M.SmoothPathEquiv μ₂ μ₁

SmoothPathEquiv is symmetric: swap the diffeomorphism φ and its inverse ψ.

theorem Physicslib4.Spacetime.SmoothPathEquiv.trans {M : Spacetime} {μ₁ μ₂ μ₃ : M.SmoothPath} (h₁₂ : M.SmoothPathEquiv μ₁ μ₂) (h₂₃ : M.SmoothPathEquiv μ₂ μ₃) : M.SmoothPathEquiv μ₁ μ₃

SmoothPathEquiv is transitive: reparametrising diffeomorphisms compose.

theorem Physicslib4.Spacetime.equivalence_smoothPathEquiv (M : Spacetime) : Equivalence M.SmoothPathEquiv

SmoothPathEquiv is an equivalence relation.

theorem Physicslib4.Spacetime.SmoothPathEquiv.toPathEquiv {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) : M.PathEquiv μ₁.toPath μ₂.toPath

A smooth reparametrisation is in particular a reparametrisation of the underlying paths.

theorem Physicslib4.Spacetime.OrientedSmoothPathEquiv.refl (M : Spacetime) (μ : M.SmoothPath) : M.OrientedSmoothPathEquiv μ μ

OrientedSmoothPathEquiv is reflexive: the identity reparametrisation has derivative 1 > 0.

theorem Physicslib4.Spacetime.OrientedSmoothPathEquiv.symm {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : M.OrientedSmoothPathEquiv μ₂ μ₁

OrientedSmoothPathEquiv is symmetric: swap φ and its inverse ψ. The inverse has positive derivative because, by the chain rule applied to φ ∘ ψ = id, φ'(ψ t) · ψ'(t) = 1 with φ'(ψ t) > 0.

theorem Physicslib4.Spacetime.OrientedSmoothPathEquiv.trans {M : Spacetime} {μ₁ μ₂ μ₃ : M.SmoothPath} (h₁₂ : M.OrientedSmoothPathEquiv μ₁ μ₂) (h₂₃ : M.OrientedSmoothPathEquiv μ₂ μ₃) : M.OrientedSmoothPathEquiv μ₁ μ₃

OrientedSmoothPathEquiv is transitive: orientation-preserving reparametrisations compose, the derivative of the composite being the (positive) product of the derivatives by the chain rule.

theorem Physicslib4.Spacetime.equivalence_orientedSmoothPathEquiv (M : Spacetime) : Equivalence M.OrientedSmoothPathEquiv

OrientedSmoothPathEquiv is an equivalence relation.

Curves

def Physicslib4.Spacetime.Curve (M : Spacetime) : Type

A curve in a spacetime: a path up to reparametrisation by homeomorphisms of the parameter space.

Two paths μ₁ : Σ₁ → M and μ₂ : Σ₂ → M define the same curve when μ₂ ∘ φ = μ₁ for some homeomorphism φ : Σ₁ → Σ₂ (PathEquiv). Informally, a curve remembers the points of a path and the order in which they are traversed, up to reversal, but not the speed.

Implementation note: the type is the quotient Quot by PathEquiv. Since PathEquiv is an equivalence relation (equivalence_pathEquiv), the classes are exactly the fibres of Curve.ofPath (Quot.eqvGen_exact with Equivalence.eqvGen_iff).

Blueprint: def:curves

Equations

• M.Curve = Quot M.PathEquiv

def Physicslib4.Spacetime.SmoothCurve (M : Spacetime) : Type

A smooth curve in a spacetime: a smooth path up to reparametrisation by diffeomorphisms of the parameter space.

The reparametrisations (SmoothPathEquiv) may reverse the direction of the parameter, so a smooth curve has a causal type (timelike, causal) but no time orientation; the finer quotient by orientation-preserving reparametrisations is OrientedSmoothCurve.

Implementation note: the type is the quotient Quot by SmoothPathEquiv, an equivalence relation (equivalence_smoothPathEquiv), so the classes are exactly the fibres of SmoothCurve.ofPath.

Blueprint: def:curves

Equations

• M.SmoothCurve = Quot M.SmoothPathEquiv

def Physicslib4.Spacetime.SmoothCurve.ofPath (M : Spacetime) (μ : M.SmoothPath) : M.SmoothCurve

Constructor: every smooth path determines a smooth curve.

Equations

• Physicslib4.Spacetime.SmoothCurve.ofPath M μ = Quot.mk M.SmoothPathEquiv μ

def Physicslib4.Spacetime.Curve.ofPath (M : Spacetime) (μ : M.Path) : M.Curve

Constructor: every path determines a curve.

Equations

• Physicslib4.Spacetime.Curve.ofPath M μ = Quot.mk M.PathEquiv μ

Timelike and causal smooth curves

def Physicslib4.Spacetime.SmoothPath.IsTimelikeAt (M : Spacetime) (μ : M.SmoothPath) (s : ℝ) : Prop

A smooth path μ : Σ → M is timelike at parameter s ∈ Σ if its tangent vector at s (the image under mfderivWithin of 1 : ℝ) is a timelike tangent vector at the spacetime point μ s.

Equations

• Physicslib4.Spacetime.SmoothPath.IsTimelikeAt M μ s = M.IsTimelike (μ.tangent s)

theorem Physicslib4.Spacetime.SmoothPath.isTimelikeAt_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) {φ : ℝ → ℝ} {s : ℝ} (hφ : MDiffAt[μ₁.parameterSpace] φ s) (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') (hs : s ∈ μ₁.parameterSpace) (hφ' : derivWithin φ μ₁.parameterSpace s ≠ 0) : IsTimelikeAt M μ₁ s ↔ IsTimelikeAt M μ₂ (φ s)

Pointwise reparametrisation-invariance of timelikeness. Under a reparametrisation identifying μ₁ with μ₂ (as in tangent_reparam_eq) with non-vanishing derivative φ'(s) ≠ 0, μ₁ is timelike at s iff μ₂ is timelike at φ s. Combines the reparametrisation chain rule with the scaling invariance isTimelike_smul_iff.

theorem Physicslib4.Spacetime.SmoothPath.causalAt_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) {φ : ℝ → ℝ} {s : ℝ} (hφ : MDiffAt[μ₁.parameterSpace] φ s) (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') (hs : s ∈ μ₁.parameterSpace) (hφ' : derivWithin φ μ₁.parameterSpace s ≠ 0) : M.IsTimelike (μ₁.tangent s) ∨ M.IsNull (μ₁.tangent s) ↔ M.IsTimelike (μ₂.tangent (φ s)) ∨ M.IsNull (μ₂.tangent (φ s))

Pointwise reparametrisation-invariance of the causal (timelike-or-null) condition. The direct analogue of isTimelikeAt_reparam for the disjunction timelike ∨ null, via the reparametrisation chain rule together with the scaling invariances isTimelike_smul_iff and isNull_smul_iff.

theorem Physicslib4.Spacetime.SmoothPath.isFuturePointing_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) (t : M.TimeOrientation) {φ : ℝ → ℝ} {s : ℝ} (hφ : MDiffAt[μ₁.parameterSpace] φ s) (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') (hs : s ∈ μ₁.parameterSpace) (hφ' : 0 < derivWithin φ μ₁.parameterSpace s) : M.IsFuturePointing t (μ₁.tangent s) ↔ M.IsFuturePointing t (μ₂.tangent (φ s))

Pointwise reparametrisation-invariance of future-pointing. Under an orientation-preserving reparametrisation identifying μ₁ with μ₂ (positive derivative 0 < φ'(s)), μ₁'s tangent is future-pointing at s iff μ₂'s is at φ s. Combines the reparametrisation chain rule with the positive-scaling invariance isFuturePointing_smul_iff.

theorem Physicslib4.Spacetime.SmoothPath.isPastPointing_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) (t : M.TimeOrientation) {φ : ℝ → ℝ} {s : ℝ} (hφ : MDiffAt[μ₁.parameterSpace] φ s) (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') (hs : s ∈ μ₁.parameterSpace) (hφ' : 0 < derivWithin φ μ₁.parameterSpace s) : M.IsPastPointing t (μ₁.tangent s) ↔ M.IsPastPointing t (μ₂.tangent (φ s))

Pointwise reparametrisation-invariance of past-pointing. The dual of isFuturePointing_reparam, via isPastPointing_smul_iff.

def Physicslib4.Spacetime.SmoothPath.IsTimelike (M : Spacetime) (μ : M.SmoothPath) : Prop

A smooth path is timelike when its velocity μ̇(s) is timelike for every s in the parameter space.

Equations

• Physicslib4.Spacetime.SmoothPath.IsTimelike M μ = ∀ s ∈ μ.parameterSpace, M.IsTimelike (μ.tangent s)

def Physicslib4.Spacetime.SmoothPath.IsCausal (M : Spacetime) (μ : M.SmoothPath) : Prop

A smooth path is causal when its velocity μ̇(s) is timelike or null for every s in the parameter space.

The type may change along the path: a causal path can be timelike on one stretch and null on another. Since μ̇(s) ≠ 0, a null velocity is a non-zero light-like vector.

Equations

• Physicslib4.Spacetime.SmoothPath.IsCausal M μ = ∀ s ∈ μ.parameterSpace, M.IsTimelike (μ.tangent s) ∨ M.IsNull (μ.tangent s)

theorem Physicslib4.Spacetime.SmoothPath.isTimelike_iff_of_smoothPathEquiv {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) : IsTimelike M μ₁ ↔ IsTimelike M μ₂

Reparametrisation-invariance of timelikeness. Two smooth paths related by a smooth reparametrisation (SmoothPathEquiv) are timelike together: one is timelike iff the other is. The forward direction uses the inverse diffeomorphism ψ for surjectivity onto μ₂'s parameter space; both directions rest on the pointwise isTimelikeAt_reparam (via the chain rule and scaling invariance), with the reparametrisation derivative non-vanishing by derivWithin_ne_zero_of_leftInverse.

theorem Physicslib4.Spacetime.SmoothPath.isCausal_iff_of_smoothPathEquiv {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) : IsCausal M μ₁ ↔ IsCausal M μ₂

Reparametrisation-invariance of the causal condition. Two smooth paths related by a smooth reparametrisation (SmoothPathEquiv) are causal together. Same structure as isTimelike_iff_of_smoothPathEquiv, using the pointwise causalAt_reparam.

def Physicslib4.Spacetime.IsTimelikeSmoothCurve (M : Spacetime) (c : M.SmoothCurve) : Prop

A smooth curve is timelike when it has a timelike representative path.

Every representative is then timelike (isTimelikeSmoothCurve_ofPath_iff): a reparametrisation φ multiplies the velocity by φ' ≠ 0, and g(cv, cv) = c² g(v, v) has the sign of g(v, v).

Blueprint: def:timelike-and-causal-smooth-curves

Equations

• M.IsTimelikeSmoothCurve c = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.SmoothCurve.ofPath M μ ∧ Physicslib4.Spacetime.SmoothPath.IsTimelike M μ

def Physicslib4.Spacetime.IsCausalSmoothCurve (M : Spacetime) (c : M.SmoothCurve) : Prop

A smooth curve is causal when it has a causal representative path.

As for IsTimelikeSmoothCurve, every representative is then causal (isCausalSmoothCurve_ofPath_iff).

Blueprint: def:timelike-and-causal-smooth-curves

Equations

• M.IsCausalSmoothCurve c = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.SmoothCurve.ofPath M μ ∧ Physicslib4.Spacetime.SmoothPath.IsCausal M μ

Future and past oriented smooth curves

def Physicslib4.Spacetime.SmoothPath.IsFutureOriented (M : Spacetime) (μ : M.SmoothPath) (t : M.TimeOrientation) : Prop

A smooth path is future-oriented for a time orientation t when its velocity μ̇(s) is future-pointing for every s in the parameter space.

A future-oriented path is causal (future-pointing vectors are timelike or null) and runs toward the future as the parameter increases.

Equations

• Physicslib4.Spacetime.SmoothPath.IsFutureOriented M μ t = ∀ s ∈ μ.parameterSpace, M.IsFuturePointing t (μ.tangent s)

def Physicslib4.Spacetime.SmoothPath.IsPastOriented (M : Spacetime) (μ : M.SmoothPath) (t : M.TimeOrientation) : Prop

A smooth path is past-oriented for a time orientation t when its velocity μ̇(s) is past-pointing for every s in the parameter space.

Equations

• Physicslib4.Spacetime.SmoothPath.IsPastOriented M μ t = ∀ s ∈ μ.parameterSpace, M.IsPastPointing t (μ.tangent s)

def Physicslib4.Spacetime.IsFutureOrientedSmoothCurve (M : Spacetime) (t : M.TimeOrientation) (c : M.SmoothCurve) : Prop

A smooth curve is future-oriented for a time orientation t when it has a future-oriented representative path.

A smooth curve does not fix the direction of its parameter, so the reversed representative of a future-oriented curve is past-oriented, and the curve is then both future- and past-oriented in this sense. The time orientation of a curve is well defined only on OrientedSmoothCurve (IsFutureOrientedCurve).

Blueprint: def:future-and-past-oriented-smooth-curves

Equations

• M.IsFutureOrientedSmoothCurve t c = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.SmoothCurve.ofPath M μ ∧ Physicslib4.Spacetime.SmoothPath.IsFutureOriented M μ t

def Physicslib4.Spacetime.IsPastOrientedSmoothCurve (M : Spacetime) (t : M.TimeOrientation) (c : M.SmoothCurve) : Prop

A smooth curve is past-oriented for a time orientation t when it has a past-oriented representative path.

See IsFutureOrientedSmoothCurve for why this does not exclude being future-oriented.

Blueprint: def:future-and-past-oriented-smooth-curves

Equations

• M.IsPastOrientedSmoothCurve t c = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.SmoothCurve.ofPath M μ ∧ Physicslib4.Spacetime.SmoothPath.IsPastOriented M μ t

theorem Physicslib4.Spacetime.SmoothPath.isFutureOriented_iff_of_orientedSmoothPathEquiv {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (t : M.TimeOrientation) (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : IsFutureOriented M μ₁ t ↔ IsFutureOriented M μ₂ t

Reparametrisation-invariance of future-orientedness. Two smooth paths related by an orientation-preserving smooth reparametrisation (OrientedSmoothPathEquiv) are future-oriented together: one is future-oriented iff the other is. The forward direction uses the inverse diffeomorphism ψ for surjectivity; both directions rest on the pointwise isFuturePointing_reparam, with the reparametrisation derivative positive by hypothesis.

theorem Physicslib4.Spacetime.SmoothPath.isPastOriented_iff_of_orientedSmoothPathEquiv {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (t : M.TimeOrientation) (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : IsPastOriented M μ₁ t ↔ IsPastOriented M μ₂ t

Reparametrisation-invariance of past-orientedness. The dual of isFutureOriented_iff_of_orientedSmoothPathEquiv, via isPastPointing_reparam.

Well-definedness of the causal type on smooth curves

Timelikeness and causality are invariant under any smooth reparametrisation, so they descend to genuine predicates on SmoothCurve (the quotient by SmoothPathEquiv): a curve is timelike/causal iff any chosen representative is. The transfer along the quotient uses the equivalence closure of SmoothPathEquiv (via Quot.eqvGen_exact) together with the per-reparametrisation iffs.

theorem Physicslib4.Spacetime.SmoothPath.isTimelike_iff_of_eqvGen {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : Relation.EqvGen M.SmoothPathEquiv μ₁ μ₂) : IsTimelike M μ₁ ↔ IsTimelike M μ₂

Timelikeness is invariant along the equivalence closure of SmoothPathEquiv.

theorem Physicslib4.Spacetime.isTimelikeSmoothCurve_ofPath_iff {M : Spacetime} (μ : M.SmoothPath) : M.IsTimelikeSmoothCurve (SmoothCurve.ofPath M μ) ↔ SmoothPath.IsTimelike M μ

Well-definedness of timelikeness on smooth curves. A smooth curve is timelike (has a timelike representative) iff the chosen representative μ is timelike; the value does not depend on the representative.

theorem Physicslib4.Spacetime.SmoothPath.isCausal_iff_of_eqvGen {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : Relation.EqvGen M.SmoothPathEquiv μ₁ μ₂) : IsCausal M μ₁ ↔ IsCausal M μ₂

Causality is invariant along the equivalence closure of SmoothPathEquiv.

theorem Physicslib4.Spacetime.isCausalSmoothCurve_ofPath_iff {M : Spacetime} (μ : M.SmoothPath) : M.IsCausalSmoothCurve (SmoothCurve.ofPath M μ) ↔ SmoothPath.IsCausal M μ

Well-definedness of causality on smooth curves.

Oriented smooth curves and well-definedness of orientation

The time orientation of a curve (future- vs past-pointing) is not invariant under orientation-reversing reparametrisations, so it does not descend to SmoothCurve. It does descend to the finer quotient by OrientedSmoothPathEquiv, which is the correct home for future/past-oriented curves.

def Physicslib4.Spacetime.OrientedSmoothCurve (M : Spacetime) : Type

An oriented smooth curve: a smooth path up to orientation-preserving reparametrisation.

The reparametrisations (OrientedSmoothPathEquiv) have positive derivative, φ' > 0, so they multiply the velocity by a positive number and preserve future- and past-pointing vectors. Being future-oriented or past-oriented is therefore a property of the oriented curve (isFutureOrientedCurve_ofPath_iff), which SmoothCurve cannot provide. Forgetting the orientation gives OrientedSmoothCurve.toSmoothCurve.

Implementation note: the type is the quotient Quot by OrientedSmoothPathEquiv, an equivalence relation (equivalence_orientedSmoothPathEquiv), so the classes are exactly the fibres of OrientedSmoothCurve.ofPath.

Blueprint: def:oriented-smooth-curve

Equations

• M.OrientedSmoothCurve = Quot M.OrientedSmoothPathEquiv

def Physicslib4.Spacetime.OrientedSmoothCurve.ofPath (M : Spacetime) (μ : M.SmoothPath) : M.OrientedSmoothCurve

Every smooth path determines an oriented smooth curve.

Equations

• Physicslib4.Spacetime.OrientedSmoothCurve.ofPath M μ = Quot.mk M.OrientedSmoothPathEquiv μ

def Physicslib4.Spacetime.IsFutureOrientedCurve (M : Spacetime) (t : M.TimeOrientation) (c : M.OrientedSmoothCurve) : Prop

An oriented smooth curve is future-oriented (relative to a time orientation t) if it admits a future-oriented representative smooth path.

Equations

• M.IsFutureOrientedCurve t c = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.OrientedSmoothCurve.ofPath M μ ∧ Physicslib4.Spacetime.SmoothPath.IsFutureOriented M μ t

def Physicslib4.Spacetime.IsPastOrientedCurve (M : Spacetime) (t : M.TimeOrientation) (c : M.OrientedSmoothCurve) : Prop

An oriented smooth curve is past-oriented (relative to a time orientation t) if it admits a past-oriented representative smooth path.

Equations

• M.IsPastOrientedCurve t c = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.OrientedSmoothCurve.ofPath M μ ∧ Physicslib4.Spacetime.SmoothPath.IsPastOriented M μ t

theorem Physicslib4.Spacetime.SmoothPath.isFutureOriented_iff_of_eqvGen {M : Spacetime} (t : M.TimeOrientation) {μ₁ μ₂ : M.SmoothPath} (h : Relation.EqvGen M.OrientedSmoothPathEquiv μ₁ μ₂) : IsFutureOriented M μ₁ t ↔ IsFutureOriented M μ₂ t

Future-orientedness is invariant along the equivalence closure of OrientedSmoothPathEquiv.

theorem Physicslib4.Spacetime.isFutureOrientedCurve_ofPath_iff {M : Spacetime} (t : M.TimeOrientation) (μ : M.SmoothPath) : M.IsFutureOrientedCurve t (OrientedSmoothCurve.ofPath M μ) ↔ SmoothPath.IsFutureOriented M μ t

Well-definedness of future-orientedness on oriented smooth curves.

theorem Physicslib4.Spacetime.SmoothPath.isPastOriented_iff_of_eqvGen {M : Spacetime} (t : M.TimeOrientation) {μ₁ μ₂ : M.SmoothPath} (h : Relation.EqvGen M.OrientedSmoothPathEquiv μ₁ μ₂) : IsPastOriented M μ₁ t ↔ IsPastOriented M μ₂ t

Past-orientedness is invariant along the equivalence closure of OrientedSmoothPathEquiv.

theorem Physicslib4.Spacetime.isPastOrientedCurve_ofPath_iff {M : Spacetime} (t : M.TimeOrientation) (μ : M.SmoothPath) : M.IsPastOrientedCurve t (OrientedSmoothCurve.ofPath M μ) ↔ SmoothPath.IsPastOriented M μ t

Well-definedness of past-orientedness on oriented smooth curves.

Projection to the coarser quotient

Every orientation-preserving reparametrisation is a smooth reparametrisation, so there is a canonical projection OrientedSmoothCurve → SmoothCurve forgetting the orientation. It sends ofPath μ to ofPath μ, hence is compatible with the (orientation-independent) timelike and causal predicates.

def Physicslib4.Spacetime.OrientedSmoothCurve.toSmoothCurve (M : Spacetime) (c : M.OrientedSmoothCurve) : M.SmoothCurve

The canonical projection from oriented smooth curves to smooth curves, forgetting the orientation. Well-defined because OrientedSmoothPathEquiv refines SmoothPathEquiv.

Equations

• Physicslib4.Spacetime.OrientedSmoothCurve.toSmoothCurve M c = Quot.lift (fun (μ : M.SmoothPath) => Physicslib4.Spacetime.SmoothCurve.ofPath M μ) ⋯ c

@[simp]

theorem Physicslib4.Spacetime.OrientedSmoothCurve.toSmoothCurve_ofPath (M : Spacetime) (μ : M.SmoothPath) : toSmoothCurve M (ofPath M μ) = SmoothCurve.ofPath M μ

theorem Physicslib4.Spacetime.OrientedSmoothCurve.toSmoothCurve_surjective (M : Spacetime) : Function.Surjective (toSmoothCurve M)

The projection is surjective: every smooth curve underlies an oriented one.

theorem Physicslib4.Spacetime.isTimelikeSmoothCurve_toSmoothCurve_ofPath (M : Spacetime) (μ : M.SmoothPath) : M.IsTimelikeSmoothCurve (OrientedSmoothCurve.toSmoothCurve M (OrientedSmoothCurve.ofPath M μ)) ↔ SmoothPath.IsTimelike M μ

Compatibility with timelikeness. The smooth curve underlying an oriented smooth curve ofPath μ is timelike iff μ is — the timelike predicate factors through the projection.

theorem Physicslib4.Spacetime.isCausalSmoothCurve_toSmoothCurve_ofPath (M : Spacetime) (μ : M.SmoothPath) : M.IsCausalSmoothCurve (OrientedSmoothCurve.toSmoothCurve M (OrientedSmoothCurve.ofPath M μ)) ↔ SmoothPath.IsCausal M μ

Compatibility with causality.

theorem Physicslib4.Spacetime.IsFutureOrientedCurve.isCausal_toSmoothCurve (M : Spacetime) {t : M.TimeOrientation} {c : M.OrientedSmoothCurve} (h : M.IsFutureOrientedCurve t c) : M.IsCausalSmoothCurve (OrientedSmoothCurve.toSmoothCurve M c)

A future-oriented oriented smooth curve projects to a causal smooth curve (future-pointing tangents are timelike or null).

theorem Physicslib4.Spacetime.IsPastOrientedCurve.isCausal_toSmoothCurve (M : Spacetime) {t : M.TimeOrientation} {c : M.OrientedSmoothCurve} (h : M.IsPastOrientedCurve t c) : M.IsCausalSmoothCurve (OrientedSmoothCurve.toSmoothCurve M c)

A past-oriented oriented smooth curve projects to a causal smooth curve.

Endpoints

def Physicslib4.Spacetime.IsEndpoint (M : Spacetime) (μ : M.Path) (p : M.Carrier) : Prop

A point p is an endpoint of a path μ : Σ → M when p = μ(s) for some s in the boundary ∂Σ of the parameter space in ℝ.

Endpoints do not depend on the parametrisation (IsEndpoint.of_pathEquiv), but which endpoint is the past one and which the future one does; see IsPastEndpoint and IsFutureEndpoint.

Blueprint: def:endpoints

Equations

• M.IsEndpoint μ p = ∃ s ∈ frontier μ.parameterSpace, μ.toFun s = p

def Physicslib4.Spacetime.IsPastEndpoint (M : Spacetime) (μ : M.Path) (p : M.Carrier) : Prop

A point p is a past endpoint of a path μ : Σ → M when p = μ(s) for the least element s of Σ.

The condition asks for an s ∈ Σ with s ≤ s' for every s' ∈ Σ, so Σ must be bounded below. A path with both a past and a future endpoint therefore has Σ = [a, b] with a < b (parameterSpace_eq_Icc_of_endpoints). No smoothness or causal condition is involved; trips apply the notion to their future-oriented segments, so the past endpoint is where the segment starts.

Implementation note: the definition quantifies over Σ rather than over its boundary ∂Σ, because Σ need not have two boundary points (for example Σ = [0, ∞) or Σ = ℝ), and then "the lesser boundary point" would not be defined.

Blueprint: def:endpoints

Equations

• M.IsPastEndpoint μ p = ∃ s ∈ μ.parameterSpace, μ.toFun s = p ∧ ∀ s' ∈ μ.parameterSpace, s ≤ s'

def Physicslib4.Spacetime.IsFutureEndpoint (M : Spacetime) (μ : M.Path) (p : M.Carrier) : Prop

A point q is a future endpoint of a path μ : Σ → M when q = μ(s) for the greatest element s of Σ.

This is the dual of IsPastEndpoint: it forces Σ to be bounded above.

Blueprint: def:endpoints

Equations

• M.IsFutureEndpoint μ p = ∃ s ∈ μ.parameterSpace, μ.toFun s = p ∧ ∀ s' ∈ μ.parameterSpace, s' ≤ s

Extremal parameters and the shape of the parameter space

These two results are what justify quantifying over the parameter space rather than over its frontier in IsPastEndpoint and IsFutureEndpoint: a genuine minimum or maximum automatically lies in the frontier, and having both forces the parameter space to be a compact interval.

theorem Physicslib4.Spacetime.mem_frontier_of_isMin (M : Spacetime) (μ : M.Path) {s : ℝ} (hs : s ∈ μ.parameterSpace) (hmin : ∀ s' ∈ μ.parameterSpace, s ≤ s') : s ∈ frontier μ.parameterSpace

A minimal parameter lies in the frontier (lmm:extremal-parameter-mem-frontier). If s is a minimum of the parameter space then it cannot be interior: an interior point has a whole interval around it inside the parameter space, which would contain smaller elements.

theorem Physicslib4.Spacetime.mem_frontier_of_isMax (M : Spacetime) (μ : M.Path) {s : ℝ} (hs : s ∈ μ.parameterSpace) (hmax : ∀ s' ∈ μ.parameterSpace, s' ≤ s) : s ∈ frontier μ.parameterSpace

A maximal parameter lies in the frontier (lmm:extremal-parameter-mem-frontier), the mirror of mem_frontier_of_isMin.

theorem Physicslib4.Spacetime.isEndpoint_of_isPastEndpoint (M : Spacetime) (μ : M.Path) {p : M.Carrier} (h : M.IsPastEndpoint μ p) : M.IsEndpoint μ p

A past endpoint is in particular an endpoint (lmm:extremal-parameter-mem-frontier, consequence).

theorem Physicslib4.Spacetime.isEndpoint_of_isFutureEndpoint (M : Spacetime) (μ : M.Path) {p : M.Carrier} (h : M.IsFutureEndpoint μ p) : M.IsEndpoint μ p

A future endpoint is in particular an endpoint (lmm:extremal-parameter-mem-frontier, consequence).

theorem Physicslib4.Spacetime.parameterSpace_eq_Icc_of_endpoints (M : Spacetime) (μ : M.Path) {p q : M.Carrier} (hp : M.IsPastEndpoint μ p) (hq : M.IsFutureEndpoint μ q) : ∃ (a : ℝ) (b : ℝ), a < b ∧ μ.parameterSpace = Set.Icc a b

Two endpoints force a compact parameter interval (lmm:endpoint-parameter-space-eq-Icc).

The past-endpoint witness is a minimum and the future-endpoint witness a maximum, so the parameter space is bounded on both sides; being also nonempty, connected and closed, it is the closed interval between them. It is non-degenerate because a path has more than one parameter.

Endpoints of curves

An endpoint of a path is also called an endpoint of its associated curve. This is well defined because a reparametrisation carries the frontier of one parameter space onto the frontier of the other. Past and future endpoints are not defined on unoriented curves: an orientation-reversing reparametrisation exchanges them.

def Physicslib4.Spacetime.IsCurveEndpoint (M : Spacetime) (c : M.Curve) (p : M.Carrier) : Prop

A point p is an endpoint of a curve c if it is an endpoint of a path representing c. By isCurveEndpoint_ofPath_iff this does not depend on the representative.

Equations

• M.IsCurveEndpoint c p = ∃ (μ : M.Path), c = Physicslib4.Spacetime.Curve.ofPath M μ ∧ M.IsEndpoint μ p

def Physicslib4.Spacetime.IsSmoothCurveEndpoint (M : Spacetime) (c : M.SmoothCurve) (p : M.Carrier) : Prop

A point p is an endpoint of a smooth curve c if it is an endpoint of a smooth path representing c. By isSmoothCurveEndpoint_ofPath_iff this does not depend on the representative.

Equations

• M.IsSmoothCurveEndpoint c p = ∃ (μ : M.SmoothPath), c = Physicslib4.Spacetime.SmoothCurve.ofPath M μ ∧ M.IsEndpoint μ.toPath p

theorem Physicslib4.Spacetime.IsEndpoint.of_pathEquiv {M : Spacetime} {μ₁ μ₂ : M.Path} (h : M.PathEquiv μ₁ μ₂) {p : M.Carrier} (hp : M.IsEndpoint μ₁ p) : M.IsEndpoint μ₂ p

Endpoints are invariant under reparametrisation of paths.

theorem Physicslib4.Spacetime.IsEndpoint.of_smoothPathEquiv {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) {p : M.Carrier} (hp : M.IsEndpoint μ₁.toPath p) : M.IsEndpoint μ₂.toPath p

Endpoints are invariant under smooth reparametrisation of smooth paths.

theorem Physicslib4.Spacetime.isCurveEndpoint_ofPath_iff {M : Spacetime} (μ : M.Path) {p : M.Carrier} : M.IsCurveEndpoint (Curve.ofPath M μ) p ↔ M.IsEndpoint μ p

Well-definedness of endpoints of curves.

theorem Physicslib4.Spacetime.isSmoothCurveEndpoint_ofPath_iff {M : Spacetime} (μ : M.SmoothPath) {p : M.Carrier} : M.IsSmoothCurveEndpoint (SmoothCurve.ofPath M μ) p ↔ M.IsEndpoint μ.toPath p

Well-definedness of endpoints of smooth curves.