Commit d80932bc authored by nipkow's avatar nipkow
Browse files

New entry No_FTL_observers

parent 1fdda5d6f2be
......@@ -3634,3 +3634,15 @@ abstract =
recursive fashion, following the Shannon decomposition of the argument
functions. The implementation mixes and adapts known techniques and is
built with efficiency in mind.
title = No Faster-Than-Light Observers
author = Mike Stannett <>, István Németi <>
date = 2016-04-28
topic = Mathematics/Physics
abstract =
We provide a formal proof within First Order Relativity Theory that no
observer can travel faster than the speed of light. Originally
reported in Stannett & Németi (2014) "Using Isabelle/HOL to verify
first-order relativity theory", Journal of Automated Reasoning 52(4),
pp. 361-378.
......@@ -33,5 +33,6 @@ Mathematics
Graph Theory
Category Theory
Author: Mike Stannett
Date: 22 October 2012
Updated 28 April 2016 to run under Isabelle2016.
theory Axioms
imports SpaceTime SomeFunc
record Body =
Ph :: "bool"
IOb :: "bool"
class WorldView = SpaceTime +
(* Worldview relation *)
W :: "Body \<Rightarrow> Body \<Rightarrow> 'a Point \<Rightarrow> bool" ("_ sees _ at _")
(* Worldview transformation *)
wvt :: "Body \<Rightarrow> Body \<Rightarrow> 'a Point \<Rightarrow> 'a Point"
AxWVT: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow> (W k b x \<longleftrightarrow> W m b (wvt m k x))"
AxWVTSym: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow> (y = wvt k m x \<longleftrightarrow> x = wvt m k y)"
(* ================ *)
class AxiomPreds = WorldView
fun sqrtTest :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
"sqrtTest x r = ((r \<ge> 0) \<and> (r*r = x))"
fun cTest :: "Body \<Rightarrow> 'a \<Rightarrow> bool" where
"cTest m v = ( (v > 0) \<and> ( \<forall>x y . (
(\<exists>p. (Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (v * v)*(time2 x y))
Quantities form a Euclidean field, ie positive quantities have
square roots. We introduce a function, sqrt, that determines them.
class AxEuclidean = AxiomPreds + Quantities +
AxEuclidean: "(x \<ge> \<Longrightarrow> (\<exists>r. sqrtTest x r)"
abbreviation sqrt :: "'a \<Rightarrow> 'a" where
"sqrt \<equiv> someFunc sqrtTest"
lemma lemSqrt:
assumes "x \<ge> 0"
and "r = sqrt x"
shows "r \<ge> 0 \<and> r*r = x"
proof -
have rootExists: "(\<exists>r. sqrtTest x r)" by (metis AxEuclidean assms(1))
hence "sqrtTest x (sqrt x)" by (metis lemSomeFunc)
thus ?thesis using assms(2) by simp
There is an inertial observer, according to whom, any light
signal moves with the same velocity in any direction
class AxLight = WorldView +
AxLight: "\<exists>m v.( IOb m \<and> (v > (0::'a)) \<and> ( \<forall>x y.(
(\<exists>p.(Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (v * v)*time2 x y)
For any inertial observer, the speed of light is the same in every
direction everywhere, and it is finite. Furthermore, it is possible
to send out a light signal in any direction.
class AxPh = WorldView + AxiomPreds +
AxPh: "IOb m \<Longrightarrow> (\<exists>v. cTest m v)"
abbreviation c :: "Body \<Rightarrow> 'a" where
"c \<equiv> someFunc cTest"
fun lightcone :: "Body \<Rightarrow> 'a Point \<Rightarrow> 'a Cone" where
"lightcone m v = mkCone v (c m)"
lemma lemCProps:
assumes "IOb m"
and "v = c m"
shows "(v > 0) \<and> (\<forall>x y.((\<exists>p. (Ph p \<and> W m p x \<and> W m p y))
\<longleftrightarrow> ( space2 x y = (c m * c m)*time2 x y )))"
proof -
have vExists: "(\<exists>v. cTest m v)" by (metis AxPh assms(1))
hence "cTest m (c m)" by (metis lemSomeFunc)
thus ?thesis using assms(2) by simp
lemma lemCCone:
assumes "IOb m"
and "onCone y (lightcone m x)"
shows "\<exists>p. (Ph p \<and> W m p x \<and> W m p y)"
proof -
have "(\<exists>p.(Ph p \<and> W m p x \<and> W m p y))
\<longleftrightarrow> ( space2 x y = (c m * c m)*time2 x y )"
by (smt assms(1) lemCProps)
hence ph_exists: "(space2 x y = (c m * c m)*time2 x y) \<longrightarrow> (\<exists>p.(Ph p \<and> W m p x \<and> W m p y))"
by metis
def lcmx \<equiv> "lightcone m x"
have lcmx_vertex: "vertex lcmx = x" by (simp add: lcmx_def)
have lcmx_slope: "slope lcmx = c m" by (simp add: lcmx_def)
have "onCone y lcmx \<longrightarrow> (space2 x y = (c m * c m)*time2 x y)"
by (metis lcmx_vertex lcmx_slope onCone.simps)
hence "space2 x y = (c m * c m)*time2 x y" by (metis lcmx_def assms(2))
thus ?thesis by (metis ph_exists)
lemma lemCPos:
assumes "IOb m"
shows "c m > 0"
by (metis assms(1) lemCProps)
lemma lemCPhoton:
assumes "IOb m"
shows "\<forall>x y. (\<exists>p. (Ph p \<and> W m p x \<and> W m p y)) \<longleftrightarrow> (space2 x y = (c m * c m)*(time2 x y))"
by (metis assms(1) lemCProps)
Inertial observers see the same events (meetings of bodies).
This also enables us to discuss the worldview transformation.
class AxEv = WorldView +
AxEv: "\<lbrakk> IOb m; IOb k\<rbrakk> \<Longrightarrow> (\<exists>y. (\<forall>b. (W m b x \<longleftrightarrow> W k b y)))"
Inertial observers can move with any speed slower than that of light
class AxThExp = WorldView + AxPh +
AxThExp: "IOb m \<Longrightarrow> (\<forall>x y .(
(\<exists>k.(IOb k \<and> W m k x \<and> W m k y)) \<longleftrightarrow> (space2 x y < (c m * c m) * time2 x y)
Every inertial observer is stationary according to himself
class AxSelf = WorldView +
AxSelf: "IOb m \<Longrightarrow> (W m m x) \<longrightarrow> (onAxisT x)"
All inertial observers agree that the speed of light is 1
class AxC = WorldView + AxPh +
AxC: "IOb m \<Longrightarrow> c m = 1"
Inertial observers agree as to the spatial distance between two
events if these two events are simultaneous for both of them.
class AxSym = WorldView +
AxSym: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow>
(W m e x \<and> W m f y \<and> W k e x'\<and> W k f y' \<and>
tval x = tval y \<and> tval x' = tval y' )
\<longrightarrow> (space2 x y = space2 x' y')"
All observers agree about lines
class AxLines = WorldView +
AxLines: "\<lbrakk> IOb m; IOb k; collinear x p q \<rbrakk> \<Longrightarrow>
collinear (wvt k m x) (wvt k m p) (wvt k m q)"
All observers agree about planes
class AxPlanes = WorldView +
AxPlanes: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow>
(coplanar e x y z \<longrightarrow> coplanar (wvt k m e) (wvt k m x) (wvt k m y) (wvt k m z))"
All observers agree about lightcones
class AxCones = WorldView + AxPh +
AxCones: "\<lbrakk> IOb m; IOb k \<rbrakk> \<Longrightarrow>
( onCone x (lightCone m v) \<longrightarrow> onCone (wvt k m x) (lightcone k (wvt k m v)))"
All inertial observers see time travelling in the same direction. That
is, if m thinks that k reached y after he reached x, then
k should also think that he reached y after he reached x.
class AxTime = WorldView +
AxTime: "\<lbrakk> IOb m; IOb k \<rbrakk>
\<Longrightarrow>( x \<lesssim> y \<longrightarrow> wvt k m x \<lesssim> wvt k m y )"
\ No newline at end of file
chapter AFP
session No_FTL_observers (AFP) = HOL +
options [timeout = 600]
Author: Mike Stannett
Date: 27 April 2016
theory SomeFunc
imports Main
fun someFunc :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b" where
"someFunc P x = (SOME y. (P x y))"
lemma lemSomeFunc:
assumes "\<exists>y . P x y"
and "f = someFunc P"
shows "P x (f x)"
proof -
have "f x = (SOME y. (P x y))"
using assms(2) by simp
thus ?thesis using assms(1)
by (simp add: someI_ex)
\ No newline at end of file
This diff is collapsed.
Author: Mike Stannett
Date: 22 October 2012
Updated 28 April 2016 to run under Isabelle2016.
theory SpecRel
imports Axioms
class SpecRel = WorldView + AxPh + AxEv + AxSelf + AxSym
The following proof assumes that the quantity field is Euclidean. It
may be possible to produce a proof without this constraint.
+ AxEuclidean
We also assume for now that lines, planes and lightcones are
preserved by the worldview transformation.
+ AxLines + AxPlanes + AxCones
(* *******************************************************************
* *
* No inertial observer can move faster than light. *
* *
** **************************************************************** *)
lemma lemZEG:
shows "z - e = g - e + (z - g)"
proof -
have "g - e + (z - g) = (g - e + z) - g" by (rule add_diff_eq)
also have "(g - e + z) - g = (-e + z)"
by (metis local.diff_add_cancel
thus ?thesis
by (simp add: calculation)
lemma noFTLObserver:
assumes iobm: "IOb m"
and iobk: "IOb k"
and mke: "m sees k at e"
and mkf: "m sees k at f"
and enotf: "e \<noteq> f"
shows "space2 e f \<le> (c m * c m) * time2 e f"
proof - (* by reductio *)
(* Step 1: Suppose k is going FTL from m's viewpoint. *)
assume converse: "space2 e f > (c m * c m) * time2 e f"
(* Step 2: Consider the m-lightcone at e *)
def eCone \<equiv> "mkCone e (c m)"
have e_on_econe: "onCone e eCone" by (simp add: eCone_def)
(* Step 3: There is a tangent plane for eCone containing both e and f,
defined using some point g on the tangent line *)
have e_is_vertex: "e = vertex eCone" by (simp add: eCone_def)
have cm_is_slope: "c m = slope eCone" by (simp add: eCone_def)
hence outside: "outsideCone f eCone"
by (metis (lifting) e_is_vertex cm_is_slope converse outsideCone.simps)
have "outsideCone f eCone
\<longrightarrow> (\<exists>x.(onCone x eCone \<and> x \<noteq> vertex eCone \<and> inPlane f (tangentPlane x eCone)))"
by (rule AxParallelConesE)
hence tplane_exists: "\<exists>x.(onCone x eCone \<and> x \<noteq> vertex eCone \<and> inPlane f (tangentPlane x eCone))"
by (metis outside)
then obtain g where g_props: "(onCone g eCone \<and> g \<noteq> vertex eCone \<and> inPlane f (tangentPlane g eCone))"
by auto
have g_on_eCone: "onCone g eCone" by (metis g_props)
have g_not_vertex: "g \<noteq> vertex eCone" by (metis g_props)
def tplane \<equiv> "tangentPlane g eCone"
have e_in_tplane: "inPlane e tplane" by (metis AxTangentVertex e_is_vertex tplane_def)
have f_in_tplane: "inPlane f tplane" by (metis g_props tplane_def)
have g_in_tplane: "inPlane g tplane" by (metis lemPlaneContainsBasePoint tplane_def AxTangentBase)
(* We'll need to show that e-f-g aren't collinear *)
have "(onCone g eCone) \<longrightarrow>
((inPlane f (tangentPlane g eCone) \<and> onCone f eCone)
\<longleftrightarrow> collinear (vertex eCone) g f)"
by (metis AxConeTangent)
hence axconetangent: "collinear e g f \<longrightarrow> onCone f eCone"
by (metis g_on_eCone e_is_vertex)
have "\<not>(onCone f eCone)" by (metis outside lemOutsideNotOnCone)
hence g_not_collinear: "\<not> (collinear e g f)"
by (metis axconetangent)
(* Step 4: k considers wvte and wvtf to be distinct points on the t-axis, and wvtg is off
k's t-axis. *)
def wvte \<equiv> "wvt k m e"
def wvtf \<equiv> "wvt k m f"
def wvtg \<equiv> "wvt k m g"
have "W k k wvte" by (metis wvte_def AxWVT mke iobm iobk)
hence wvte_onAxis: "onAxisT wvte" by (metis AxSelf iobk)
have "W k k wvtf" by (metis wvtf_def AxWVT mkf iobm iobk)
hence wvtf_onAxis: "onAxisT wvtf" by (metis AxSelf iobk)
have wvte_inv: "e = wvt m k wvte" by (metis AxWVTSym iobk iobm wvte_def)
have wvtf_inv: "f = wvt m k wvtf" by (metis AxWVTSym iobk iobm wvtf_def)
have wvtg_inv: "g = wvt m k wvtg" by (metis AxWVTSym iobk iobm wvtg_def)
have e_not_g: "e \<noteq> g" by (metis e_is_vertex g_not_vertex)
have f_not_g: "f \<noteq> g" by (metis outside lemOutsideNotOnCone g_on_eCone)
have wvt_e_not_f: "wvte \<noteq> wvtf" by (metis wvte_inv wvtf_inv enotf)
have wvt_f_not_g: "wvtf \<noteq> wvtg" by (metis wvtf_inv wvtg_inv f_not_g)
have wvt_g_not_e: "wvtg \<noteq> wvte" by (metis wvtg_inv wvte_inv e_not_g)
have if_g_onAxis: "onAxisT wvtg \<longrightarrow> collinear wvte wvtg wvtf"
by (metis lemAxisIsLine wvte_onAxis wvtf_onAxis wvt_e_not_f wvt_f_not_g wvt_g_not_e)
have "collinear wvte wvtg wvtf \<longrightarrow> collinear e g f"
by (metis AxLines iobm iobk wvte_inv wvtf_inv wvtg_inv)
hence "onAxisT wvtg \<longrightarrow> collinear e g f" by (metis if_g_onAxis)
hence wvtg_offAxis: "\<not> (onAxisT wvtg)" by (metis g_not_collinear)
(* Step 5: There is a point z with various contradictory properties. *)
have "\<forall>s.(\<exists>p.( collinear wvte wvtg p \<and> (space2 p wvtf = (s*s)*time2 p wvtf)))"
by (metis AxSlopedLineInVerticalPlane wvte_onAxis wvtf_onAxis wvtg_offAxis wvt_e_not_f)
hence exists_wvtz: "\<exists>p.( collinear wvte wvtg p \<and> (space2 p wvtf = (c k * c k)*time2 p wvtf))"
by metis
then obtain wvtz where
wvtz_props: "collinear wvte wvtg wvtz \<and> (space2 wvtz wvtf = (c k * c k)*time2 wvtz wvtf)" by auto
hence wvtf_speed: "space2 wvtz wvtf = (c k * c k)*time2 wvtz wvtf" by metis
def z \<equiv> "wvt m k wvtz"
def wvtzCone \<equiv> "lightcone k wvtz"
have wvtz_is_vertex: "wvtz = vertex wvtzCone" by (simp add: wvtzCone_def)
have ck_is_slope: "c k = slope wvtzCone" by (simp add: wvtzCone_def)
hence "space2 (vertex wvtzCone) wvtf = ((slope wvtzCone) *(slope wvtzCone))*time2 (vertex wvtzCone) wvtf"
by (metis wvtf_speed wvtz_is_vertex ck_is_slope)
hence "onCone wvtf wvtzCone" by (metis onCone.simps)
hence wvtf_on_wvtzCone: "onCone (wvt m k wvtf) (lightcone m z)"
by (metis iobm iobk AxCones wvtzCone_def z_def)
(* f is on the lightcone at z *)
def zCone \<equiv> "lightcone m z"
have z_is_vertex: "z = vertex zCone" by (simp add: zCone_def)
have cm_is_zSlope: "c m = slope zCone" by (simp add: zCone_def)
have f_on_zCone: "onCone f zCone" by (metis wvtf_inv wvtf_on_wvtzCone zCone_def)
(* whence z is on the lightcone at f *)
hence "space2 (vertex zCone) f = (slope zCone * slope zCone)*time2 (vertex zCone) f"
by (simp add: zCone_def)
hence "space2 z f = (c m * c m)*time2 z f" by (metis z_is_vertex cm_is_zSlope)
hence fz_speed: "space2 f z = (c m * c m)*time2 f z" by (metis lemSpace2Sym lemTime2Sym)
def fCone \<equiv> "lightcone m f"
have f_is_fVertex: "f = vertex fCone" by (simp add: fCone_def)
have cm_is_fSlope: "c m = slope fCone" by (simp add: fCone_def)
hence "space2 (vertex fCone) z = ((slope fCone) *(slope fCone))*time2 (vertex fCone) z"
by (metis fz_speed f_is_fVertex cm_is_fSlope)
hence z_on_fCone: "onCone z fCone" by (metis onCone.simps)
(* z is also on the lightcone at e, as well as in the tangent plane at g *)
have "collinear wvte wvtg wvtz" by (metis wvtz_props)
hence egz_collinear: "collinear e g z" by (metis wvte_inv wvtg_inv z_def AxLines iobm iobk)
hence z_geometry: "(inPlane z (tangentPlane g eCone) \<and> onCone z eCone)"
by (metis AxConeTangent e_is_vertex g_on_eCone)
have z_on_eCone: "onCone z eCone" by (metis z_geometry)
have z_in_tplane: "inPlane z tplane" by (metis z_geometry tplane_def)
hence z_not_f: "z \<noteq> f" by (metis z_on_eCone outside lemOutsideNotOnCone)
hence z_not_fVertex: "z \<noteq> vertex fCone" by (simp add: fCone_def z_not_f)
assume assm: "z = e"
have "space2 f e = (c m * c m)*time2 f e \<and> space2 f e = space2 e f \<and> time2 f e = time2 e f"
by (metis lemSpace2Sym lemTime2Sym fz_speed assm)
hence "space2 e f = (c m * c m)*time2 e f" by metis
hence "False" by (metis less_irrefl converse)
from this have z_not_e: "z \<noteq> e" by blast
(* but the lines e-z and f-z must be parallel *)
def lineA \<equiv> "lineJoining e z"
def lineB \<equiv> "lineJoining f z"
assume assm: "direction lineA = vecZero"
have lemnullline: "(direction lineA = vecZero \<and> inLine z lineA) \<longrightarrow> z = basepoint lineA"
by (metis lemNullLine)
have "inLine z lineA" by (metis lineA_def lemLineContainsEndpoint)
hence z_is_bp: "z = basepoint lineA" by (metis lemnullline assm)
have "basepoint lineA = e" by (simp add: lineA_def)
hence "False" by (metis z_is_bp z_not_e)
from this have ez_not_null: "direction lineA \<noteq> vecZero" by blast
assume assm: "direction lineB = vecZero"
have lemnullline: "(direction lineB = vecZero \<and> inLine z lineB) \<longrightarrow> z = basepoint lineB"
by (metis lemNullLine)
have "inLine z lineB" by (metis lineB_def lemLineContainsEndpoint)
hence z_is_bp: "z = basepoint lineB" by (metis lemnullline assm)
have "basepoint lineB = f" by (simp add: lineB_def)
hence "False" by (metis z_is_bp z_not_f)
from this have fz_not_null: "direction lineB \<noteq> vecZero" by blast
have "samePlane tplane (tangentPlane z fCone)
\<and> ((lineJoining e g) \<parallel> (lineJoining f z))"
by (metis AxParallelCones tplane_def
g_on_eCone g_not_vertex z_on_fCone z_not_fVertex z_in_tplane
e_is_vertex f_is_fVertex)
hence eg_par_fz: "(lineJoining e g) \<parallel> (lineJoining f z)" by metis
assume case1: "direction (lineJoining e g) = vecZero"
have "direction (lineJoining e g) = from e to g" by simp
hence "from e to g = vecZero" by (metis case1)
hence "e = g" by (simp)
hence "False" by (metis e_not_g)
from this have eg_not_null: "\<not>(direction (lineJoining e g) = vecZero)" by blast
then obtain a where a_props: "a \<noteq> 0 \<and> direction (lineJoining f z) = a**direction (lineJoining e g)"
by (metis fz_not_null eg_not_null eg_par_fz parallel.simps lineB_def)
hence f_to_z: "from f to z = a**(from e to g)" by simp
have a_nonzero: "a \<noteq> 0" by (metis a_props)
have eg_dir: "from e to g = direction (lineJoining e g)" by simp
have gz_dir: "from g to z = direction (lineJoining g z)" by simp
have egz: "z = g \<leadsto> (from g to z)" by (metis lemLineEndpoint)
hence "collinear e g (g \<leadsto> (from g to z))" by (metis egz_collinear)
then obtain b where e_to_g: "from e to g = (-b)**(from g to z)"
by (metis lemDirectionCollinear)
assume assm: "-b = 0"
have "from e to g = (-b)**(from g to z)" by (metis e_to_g)
hence "from e to g = vecZero" by (simp add: assm)
hence "direction (lineJoining e g) = vecZero" by (simp)
hence "False" by (metis eg_not_null lineA_def)
from this have b_nonzero: "-b \<noteq> 0" by blast
def binv \<equiv> "inverse (-b)"
def factor \<equiv> "1+binv"
have binv_nonzero: "binv \<noteq> 0" by (metis b_nonzero add.comm_neutral binv_def nonzero_imp_inverse_nonzero right_minus)
have "from e to g = (-b)**(from g to z)" by (metis e_to_g)
hence g_to_z: "(from g to z) = binv**(from e to g)"
by (metis b_nonzero lemScaleInverse binv_def)
have "from e to z = from e to g \<oplus> from g to z"
by (simp add: lemZEG)
hence "from e to z = (from e to g) \<oplus> binv**(from e to g)" by (metis g_to_z)
hence e_to_z: "from e to z = factor**(from e to g)" by (metis lemAddOverScale lemScale1 factor_def)
have ez_dir: "direction (lineJoining e z) = from e to z" by simp
have eg_dir: "direction (lineJoining e g) = from e to g" by simp
assume assm: "factor = 0"
have "from e to z = factor**(from e to g)" by (metis e_to_z)
hence "from e to z = vecZero" by (simp add: assm)
hence "direction (lineJoining e z) = vecZero" by (simp)
hence "False" by (metis ez_not_null lineA_def)
from this have factor_nonzero: "factor \<noteq> 0" by blast
have "direction (lineJoining e z) = factor**(direction (lineJoining e g))"
by (metis e_to_z ez_dir eg_dir)
hence "(lineJoining e g) \<parallel> (lineJoining e z)" by (metis parallel.simps factor_nonzero)
hence "(lineJoining e z) \<parallel> (lineJoining e g)" by (metis lemParallelSym)