Paths and curves on a spacetime

This file formalises the various flavours of paths and curves used in section 10.2 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 equivalence relations on paths/smooth paths corresponding to reparametrisation by homeomorphisms / diffeomorphisms of the parameter space.
• 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.

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 M is a continuous map μ : Σ → M.Carrier whose domain Σ, called the parameter space, is a closed, connected subset of ℝ containing more than one point.

Following the blueprint we store Σ as a Set ℝ along with proofs that it is closed, connected and not a singleton (i.e. contains more than one point).

• parameterSpace : Set ℝ

  The parameter space, a subset of ℝ.

• isClosed : IsClosed self.parameterSpace

  The parameter space is closed in ℝ.

• isConnected : IsConnected self.parameterSpace

  The parameter space is connected.

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

  The parameter space contains at least two distinct points.

• toFun : ℝ → M.Carrier

  The underlying continuous map Σ → M.Carrier.

• continuousOn : ContinuousOn self.toFun self.parameterSpace

  Continuity of the underlying map on the parameter space.

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

A smooth path in a spacetime M is a path μ : Σ → M which is smooth and has a non-vanishing derivative along Σ.

The smoothness condition is ContMDiffOn on the parameter space, relative to the identity model with corners on ℝ and the spacetime's model. The non-vanishing-derivative condition states that the manifold derivative mfderiv of μ, applied to the basis vector 1 : ℝ, is non-zero at every point of Σ.

• 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

  Smoothness of the underlying map on the parameter space.

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

  The tangent vector along the path is non-vanishing on the parameter space: the manifold derivative of toFun applied to 1 : ℝ is non-zero at each interior point of the parameter space.

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 tangent vector of a smooth path μ at parameter s: the manifold derivative of μ along its parameter space, applied to the basis vector 1 : ℝ. This is the object all the causal predicates below are phrased in terms of.

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 ℝ mapping Σ₁ bijectively onto Σ₂ such that μ₂ ∘ φ = μ₁ on Σ₁. We package the homeomorphism on the parameter spaces via its underlying function on ℝ together with the relevant restriction conditions.

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.

Curves

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

A curve in a spacetime is an equivalence class of paths under parameter reparametrisation by homeomorphisms. We package this as a Quot over the (possibly non-equivalence) relation PathEquiv; the actual equivalence-class structure is left implicit.

Equations

• M.Curve = Quot M.PathEquiv

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

A smooth curve in a spacetime is an equivalence class of smooth paths under parameter reparametrisation by diffeomorphisms.

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 if its tangent vector is timelike at every point of 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 if its tangent vector is either timelike or null at every point of the parameter space.

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 timelike smooth curve is a smooth curve all of whose representative smooth paths are timelike. Since the timelike condition is invariant under reparametrisation by an orientation-preserving diffeomorphism but not orientation-reversing ones — and since the underlying tangent vector condition g(v,v) < 0 is invariant under non-zero scaling — we state the predicate by existential quantification over a representative.

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 causal smooth curve is a smooth curve all of whose representative smooth paths are causal.

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 with respect to a time orientation t if its tangent vector is future-pointing at every parameter point.

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 with respect to a time orientation t if its tangent vector is past-pointing at every parameter point.

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 future-oriented smooth curve is a smooth curve admitting a future-oriented representative smooth path (relative to a fixed time orientation t).

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 past-oriented smooth curve is a smooth curve admitting a past-oriented representative smooth path (relative to a fixed time orientation t).

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: an equivalence class of smooth paths under orientation-preserving reparametrisation. Finer than SmoothCurve (which also allows orientation-reversing reparametrisations), it is the natural domain on which the time orientation of a curve is well-defined.

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 of a spacetime M is an endpoint of a path μ : Σ → M if it lies in the image of the topological frontier of Σ (i.e. its boundary ∂Σ in ℝ) under μ.

Equations

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

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

For a smooth path μ whose associated smooth curve is timelike and future-oriented, a past endpoint is the image under μ of the lesser of the two boundary components of ∂Σ.

We capture this as: there exists a value s ∈ Σ such that every other s' ∈ Σ satisfies s ≤ s', and μ s = p. Quantifying over the parameter space (rather than its frontier ∂Σ) ensures the witness is a genuine minimum of Σ, which on a closed connected Σ ⊆ ℝ forces Σ to be bounded below; together with IsFutureEndpoint this excludes half-lines and pins Σ down to a compact closed interval [a, b].

Equations

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

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

For a smooth path μ whose associated smooth curve is timelike and future-oriented, a future endpoint is the image under μ of the greater of the two boundary components of ∂Σ. Quantifying over the parameter space (rather than ∂Σ) ensures the witness is a genuine maximum, forcing boundedness above; see IsPastEndpoint for the dual.

Equations

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