### Abstract

We have previously verified, in the first order theory SpecRel of Special Relativity, that inertial observers cannot travel faster than light. We now prove the corresponding result for GenRel, the first-order theory of General Relativity. Specifically, we prove that whenever an observer m encounters another observer k (so that m and k are both present at some spacetime location x), k will necessarily be observed by m to be traveling at less than light speed.

### License

BSD License

### Topics

- Mathematics/Physics

### Related publications

- https://isa-afp.org/entries/No_FTL_observers.html

### Session No_FTL_observers_Gen_Rel

- Sorts
- Points
- WorldView
- Functions
- WorldLine
- Translations
- AxSelfMinus
- TangentLines
- Cones
- AxLightMinus
- Proposition1
- AxEField
- Norms
- AxTriangleInequality
- Sublemma3
- Vectors
- CauchySchwarz
- Matrices
- LinearMaps
- Affine
- Sublemma4
- MainLemma
- AxDiff
- TangentLineLemma
- Proposition2
- AxEventMinus
- Proposition3
- ObserverConeLemma
- Quadratics
- Classification
- ReverseCauchySchwarz
- KeyLemma
- Cardinalities
- AffineConeLemma
- NoFTLGR

## Cite

×

No_FTL_observers_Gen_Rel-AFP

    @article{No_FTL_observers_Gen_Rel-AFP,
      author  = {Mike Stannett and Edward Higgins and Hajnal Andreka and Judit Madarasz and István Németi and Gergely Szekely},
      title   = {No Faster-Than-Light Observers (GenRel)},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/No_FTL_observers_Gen_Rel.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Mar 27, 2023 : Isabelle2022