Theory NoFTLGR

(*
   NoFTLGR.thy
   Author: Mike Stannett
   m.stannett@sheffield.ac.uk
   File created: Aug 2020
   Proof completed: Jan 2023
   Refactored: Feb 2023
*)

section ‹ NoFTLGR ›

text ‹This theory completes the proof of NoFTLGR.›

theory NoFTLGR
  imports ObserverConeLemma AffineConeLemma
begin

class NoFTLGR = ObserverConeLemma + AffineConeLemma
begin


(* ********************************************************************** *)
(* ********************************************************************** *)
(* *********               PROOF OF NoFTLGR                    ********** *)
(* ********************************************************************** *)
(* ********************************************************************** *)

text ‹The theorem says: if observer m encounters observer k (so that they
are both present at the same spacetime point x), then k is moving at sub-light
speed relative to m. In other words, no observer ever encounters another 
observer who appears to be moving at or above lightspeed.›


theorem lemNoFTLGR:
  assumes ass1: "x ∈ wline m m ∩ wline m k"
and       ass2: "tl l m k x"
and       ass3: "v ∈ lineVelocity l"
and       ass4: "∃ p . (p ≠ x) ∧ (p ∈ l)"
shows     "(lineSlopeFinite l) ∧ (sNorm2 v < 1)"
proof -

  define s where s: "s = (wline k k)"

  (* statement labels refer to conditions in lemPresentation *)
  have "axEventMinus m k x" using AxEventMinus by force 
  hence "(∃ q . ∀ b . ( (m sees b at x) ⟷ (k sees b at q)))"
    using ass1 by blast
  then obtain y where y: "∀ b . ( (m sees b at x) ⟷ (k sees b at y))" by auto
  hence mkxy: "wvtFunc m k x y" using ass1 by auto

  have "axDiff m k x" using AxDiff by simp
  hence "∃ A . (affineApprox A (wvtFunc m k) x )" using mkxy by fast
  then obtain A where A: "affineApprox A (wvtFunc m k) x" by auto

  hence affA: "affine A" by auto
  have lineL: "isLine l" using ass2 by auto

  define l' where l': "l' = applyToSet (asFunc A) l"

  hence lineL': "isLine l'" 
    using lineL affA lemAffineOfLineIsLine[of "l" "A" "l'"]
    by auto

  have tgtl': "tangentLine l' s y"
  proof -
    define g1 where g1: "g1 ≡ x ∈ wline m k"
    define g2 where g2: "g2 ≡ tangentLine l (wline m k) x"
    define g3 where g3: "g3 ≡ affineApprox A (wvtFunc m k) x"
    define g4 where g4: "g4 ≡ wvtFunc m k x y"
    define g5 where g5: "g5 ≡ applyAffineToLine A l l'" 
    define g6 where g6: "g6 ≡ tangentLine l' (wline k k) y"

    have "x ∈ wline m k
             ⟶ tangentLine l (wline m k) x
             ⟶ affineApprox A (wvtFunc m k) x
             ⟶ wvtFunc m k x y
             ⟶ applyAffineToLine A l l'
             ⟶ tangentLine l' (wline k k) y"
    using lemPresentation[of "x" "m" "k" "l" "k" "A" "y" "l'"] 
    by blast

    hence pres: "g1 ⟶ g2 ⟶ g3 ⟶ g4 ⟶ g5 ⟶ g6" 
      using g1 g2 g3 g4 g5 g6 by fastforce

    have 1: g1 using ass1 g1 by auto
    have 2: g2 using ass2 g2 by fast
    have 3: g3 using A g3 by fast
    have 4: g4 using mkxy g4 by fast
    have 5: g5 using 1 lineL l' affA lemAffineOfLineIsLine[of "l" "A" "l'"] g5 
      by auto
  
    hence g6   using 1 2 3 4 5 pres by meson
    thus ?thesis using s g6 by auto
  qed

  have ykk: "y ∈ wline k k" using ass1 y by auto

  (* l' = timeAxis *)
  have c2: "l' = timeAxis"
  proof -
    have "tl l' k k y" using tgtl' l' s by auto
    thus ?thesis
      using lemSelfTangentIsTimeAxis[of "y" "k" "l'"] by auto
  qed

  (* y is on the timeAxis *)
  have yOnAxis: "onLine y timeAxis"
    using lemTimeAxisIsLine ykk AxSelfMinus by blast

  (* y is on l' *)
  hence yOnl': "onLine y l'" using c2 by auto

  (* have cone k y is regular *)
  have "∀ p . cone k y p ⟷ regularCone y p" 
    using ykk lemProposition1[of "y" "k"] by auto
  hence ycone: "coneSet k y = regularConeSet y" by auto

  (* Page 34: bottom - "Also cone m x is regular" *)
  have xcone: "coneSet m x = regularConeSet x"
  proof -
    have "x ∈ wline m m" using ass1 by auto
    hence "∀ p . cone m x p ⟷ regularCone x p" 
      using lemProposition1[of "x" "m"] by auto
    thus ?thesis by auto
  qed
    
  (* Page 34: get a new affine map A~kmy *)
  have assm1': "y ∈ wline k k ∩ wline k m"
    using ass1 y by auto
  have "axEventMinus k m y" using AxEventMinus by force 
  hence "(∃ q . ∀ b . ( (k sees b at y) ⟷ (m sees b at q)))"
    using assm1' by blast
  then obtain z where z: "∀ b . ( (k sees b at y) ⟷ (m sees b at z))" by auto
  hence kmyz: "wvtFunc k m y z" using assm1' by auto

  have "axDiff k m y" using AxDiff by simp
  hence "∃ A . (affineApprox A (wvtFunc k m) y )" using kmyz by fast
  then obtain Akmy where Akmy: "affineApprox Akmy (wvtFunc k m) y" by auto

  hence affA': "affine Akmy" by auto
  have  invA': "invertible Akmy" using Akmy by auto

  then obtain Amkx where 
    Amkx: "(affine Amkx) ∧ (∀ p q . Akmy p = q ⟷ Amkx q = p)"    
    using lemInverseAffine[of "Akmy"] affA' by blast


  (* Page 35 *)
  have "wvtFunc m k x y" using mkxy by auto
  hence kmyx: "wvtFunc k m y x" by auto
  hence xisz: "x = z" using kmyz lemWVTImpliesFunction by blast

  moreover have "z = Akmy y" 
    using lemAffineEqualAtBase[of "wvtFunc k m" "Akmy" "y"] Akmy kmyz
    by blast      
  ultimately have xA'y: "x = Akmy y" by auto

  (* 35a: Akmy[cone k y] = cone m x *)
  hence p35a: "applyToSet (asFunc Akmy) (coneSet k y) ⊆ coneSet m x"
    using Akmy lemProposition2[of "k" "m" "Akmy" "y"]
    by simp

  (* Express using regular cones and extend to equality *)
  have p35aRegular: "applyToSet (asFunc Akmy) (regularConeSet y) = regularConeSet x"
  proof -
    have "applyToSet (asFunc Akmy) (regularConeSet y) ⊆ coneSet m x"
      using ycone p35a by auto
    hence l2r: "applyToSet (asFunc Akmy) (regularConeSet y) ⊆ regularConeSet x"
      using xcone by auto

    have r2l: "regularConeSet x ⊆ applyToSet (asFunc Akmy) (regularConeSet y)"
    proof -
      { assume converse: "¬(regularConeSet x ⊆ applyToSet (asFunc Akmy) (regularConeSet y))"
        then obtain z where 
          z: "z ∈ regularConeSet x ∧ ¬(z ∈ applyToSet (asFunc Akmy) (regularConeSet y))"
          by blast
        define z' where z': "z' = Amkx z"

        have z'NotOnCone:"¬(z' ∈ regularConeSet y)" 
        proof -
          { assume conv: "z' ∈ regularConeSet y"
            have "Akmy z' = z" using Amkx z' by auto
            hence "(asFunc Akmy) z' z" by auto
            hence "∃ z' ∈ regularConeSet y . (asFunc Akmy) z' z" using conv by blast
            hence "z ∈ applyToSet (asFunc Akmy) (regularConeSet y)" by auto
            hence "False" using z by blast
          }
          thus ?thesis by blast
        qed

        hence "¬ (regularCone y z')" by auto
        then obtain l where
          l: "(onLine z' l) ∧ (¬ (y ∈ l)) ∧ (card (l ∩ (regularConeSet y)) = 2)"
          using lemConeLemma2[of "z'" "y"] by blast
        then obtain p q where
          pq: "(p ≠ q) ∧ p ∈ (l ∩ (regularConeSet y)) ∧ q ∈ (l ∩ (regularConeSet y))" 
          using lemElementsOfSet2[of "l ∩ (regularConeSet y)"] by blast

        have lineL: "isLine l" using l by auto

        define p' where p': "p' = Akmy p"
        define q' where q': "q' = Akmy q"
        have p'inv: "Amkx p' = p" using Amkx p' by auto
        have q'inv: "Amkx q' = q" using Amkx q' by auto

        have pOnCone: "p ∈ regularConeSet y" using pq by blast
        moreover have "(asFunc Akmy) p p'" using p' by auto
        ultimately have "∃ p ∈ regularConeSet y . (asFunc Akmy) p p'" by blast
        hence "p' ∈ applyToSet (asFunc Akmy) (regularConeSet y)" by auto
        hence Ap: "p' ∈ regularConeSet x" using l2r by blast
            
        have qOnCone: "q ∈ regularConeSet y" using pq by blast
        moreover have "(asFunc Akmy) q q'" using q' by auto
        ultimately have "∃ q ∈ regularConeSet y . (asFunc Akmy) q q'" by blast
        hence "q' ∈ applyToSet (asFunc Akmy) (regularConeSet y)" by auto
        hence Aq: "q' ∈ regularConeSet x" using l2r by blast

        have p'q': "p' ≠ q'" 
        proof -
          { assume "p' = q'"
            hence "Akmy p' = Akmy q'" by auto
            hence "p = q" by (metis p' q' Amkx)
            hence "False" using pq by simp
          }
          thus ?thesis by auto
        qed

        have p'z: "p' ≠ z" 
        proof -
          { assume "p' = z"
            hence "p = z'" using p'inv z' by auto
            hence "False" using pOnCone z'NotOnCone by auto
          }
          thus ?thesis by auto
        qed
        
        have q'z: "q' ≠ z" 
        proof -
          { assume "q' = z"
            hence "q = z'" using q'inv z' by auto
            hence "False" using qOnCone z'NotOnCone by auto
          }
          thus ?thesis by auto
        qed

        define l' where l': "l' = applyToSet (asFunc Akmy) l"
        have "affine Akmy" using Akmy by auto
        hence All': "applyAffineToLine Akmy l l'" 
          using l' lineL lemAffineOfLineIsLine[of "l" "Akmy" "l'"]
          by blast 

        have lineL': "isLine l'" using All' by auto


        define S where S: "S = l' ∩ regularConeSet x"

        have xNotInL': "¬ (x ∈ l')"
        proof -
          { assume "x ∈ l'" 
            hence "∃ y1 ∈ l . (asFunc Akmy) y1 x" using l' by auto
            then obtain y1 where y1: "(y1 ∈ l) ∧ (Akmy y1 = x)" by auto 
            hence "Akmy y1 =  Akmy y" using xA'y by auto
            hence "y1 = y" using invA' by auto
            hence "y ∈ l" using y1 by auto
            hence "False" using l by auto
          }
          thus ?thesis by auto
        qed

        have p'InMeet: "p' ∈ S"
        proof -
          have "p ∈ l ∧ (asFunc Akmy) p p'" using p' pq by auto
          hence "∃ p ∈ l . (asFunc Akmy) p p'" by auto
          hence "p' ∈ l'" using l' by auto
          thus ?thesis using Ap S by blast
        qed

        have q'InMeet: "q' ∈ S"
        proof -
          have "q ∈ l ∧ (asFunc Akmy) q q'" using q' pq by auto
          hence "∃ q ∈ l . (asFunc Akmy) q q'" by auto
          hence "q' ∈ l'" using l' by auto
          thus ?thesis using Aq S by blast
        qed

        have zInMeet: "z ∈ S"
        proof -
          have "Akmy z' = z" using z' Amkx by blast
          moreover have "z' ∈ l" using l by auto
          ultimately have "z' ∈ l ∧ (asFunc Akmy) z' z" by auto  
          hence "∃ z' ∈ l . (asFunc Akmy) z' z" by auto  
          hence "z ∈ l'" using l' by auto
          thus ?thesis using z S by blast
        qed

        have "finite S ∧ card S ≤ 2"          
          using xNotInL' lineL' S lemConeLemma1[of "x" "l'" "S"]
          by auto

        moreover have "S ≠ {}" using zInMeet by auto

        ultimately have "card S = 1 ∨ card S = 2"
          using card_0_eq by fastforce

          
        moreover have "card S ≠ 2"
        proof -
          { assume "card S = 2"
            hence "p' = z ∨ q' = z" 
              using p'q' p'InMeet q'InMeet zInMeet
                    lemThirdElementOfSet2[of "p'" "q'" "S" "z"] 
              by auto
            hence "False" using p'z q'z by auto
          }
          thus ?thesis by auto
        qed

        moreover have "card S ≠ 1" 
          using p'InMeet q'InMeet p'q' card_1_singletonE by force

              
        ultimately have "False" by blast
      }
      thus ?thesis by blast
    qed
    thus ?thesis using l2r by blast
  qed


  (* 35b: Akmy[tAxis] = l *)
  have lprops: "l = applyToSet (asFunc Akmy) timeAxis"
  proof - 
    define t' where t': "t' = applyToSet (asFunc Akmy) timeAxis"
                                                      
    define p1 where p1: "p1 = (y ∈ wline k k)"
    define p2 where p2: "p2 = tangentLine timeAxis (wline k k) y"
    define p3 where p3: "p3 = affineApprox Akmy (wvtFunc k m) y"
    define p4 where p4: "p4 = wvtFunc k m y x"
    define p5 where p5: "p5 = applyAffineToLine Akmy timeAxis t'"
  
    define tgt where tgt: "tgt = tangentLine t' (wline m k) x"
  
    have pre1: "p1" using p1 ykk by auto
    have pre2: "p2" 
    proof -
      have "tangentLine l' (wline k k) y" using tgtl' s by auto
      hence "tangentLine timeAxis (wline k k) y" using c2 by meson
      thus ?thesis using p2 by blast
    qed
    have pre3: "p3" using p3 Akmy by auto
    have pre4: "p4" using p4 kmyx by auto
    have pre5: "p5" 
      using p5 affA' lemTimeAxisIsLine t' Akmy
            lemAffineOfLineIsLine[of "timeAxis" "Akmy" "t'"]
      by blast
  
    (* t' = l *)
    have "p1 ⟶ p2 ⟶ p3 ⟶ p4 ⟶ p5 ⟶ tgt"
      using p1 p2 p3 p4 p5 tgt
           lemPresentation[of "y" "k" "k" "timeAxis" "m" "Akmy" "x" "t'"]
      by fast
    hence "tl t' m k x" using tgt pre1 pre2 pre3 pre4 pre5 by auto
    moreover have "tl l m k x" using ass2 by auto
    moreover have "affineApprox A (wvtFunc m k) x" using A by auto
    moreover have "wvtFunc m k x y" using mkxy by auto
    moreover have "x ∈ wline m k" using ass1 by auto
    ultimately have "t' = l" 
      using lemTangentLineUnique[of "x" "m" "k" "t'" "l" "A" "y"]
      by fast
    thus ?thesis using t' by blast
  qed

  (* p35c: Pick any py ∈ tAxis. Show that py is inside cone k y *)
  { fix py assume py: "onTimeAxis py ∧ py ≠ y"

    have pyInsideCone: "insideRegularCone y py"
    proof -
      have pyOnAxis: "onLine py timeAxis" using py lemTimeAxisIsLine by blast

      hence pyprops: "timeAxis = lineJoining y py" 
        using py yOnAxis lemLineAndPoints[of "y" "py" "timeAxis"] by auto

      define d where d: "d = (y ⊖ py)"
      hence "∃ py y . (py ≠ y) ∧ (onLine py timeAxis) 
                                ∧ (onLine y timeAxis) ∧ (d = (y ⊖ py))"
        using py pyOnAxis yOnAxis by blast
      hence ddrtn: "d ∈ drtn timeAxis" by simp

      have scomp0: "sComponent d = sOrigin" using d py yOnAxis by auto

      have sf: "slopeFinite py y" using py yOnAxis by force
      hence "sloper py y = ((-1) ⊗ ((1 / (tval py - tval y)) ⊗ d))" 
        using d by auto
      hence "velocityJoining py y = sOrigin" using scomp0 by simp
      hence "velocityJoining origin d = sOrigin" using d by auto

      hence "(d ∈ drtn timeAxis) ∧ (sOrigin = velocityJoining origin d)" 
        using ddrtn by auto
      hence "∃ d . (d ∈ drtn timeAxis) ∧ (sOrigin = velocityJoining origin d)" 
        by blast
      hence "(sOrigin ∈ lineVelocity timeAxis)" by auto

      hence "(sOrigin ∈ lineVelocity timeAxis) ∧ (sNorm2 sOrigin < 1)"
        by auto
      hence "∃ v . (v ∈ lineVelocity timeAxis) ∧ (sNorm2 v < 1)"
        by blast
      thus ?thesis using pyprops sf by auto
    qed
    
    (* Therefore: px is insideRegularCone x  *)
    define px where px: "px = Akmy py"

    have "insideRegularCone x px"
    proof - 
      have "insideRegularCone y py" using pyInsideCone by blast
      moreover have "affInvertible Akmy" using affA' invA' by blast
      moreover have "x = Akmy y" by (simp add: xA'y)
      moreover have "px = Akmy py" by (simp add: px)
      moreover have "regularConeSet x = applyToSet (asFunc Akmy) (regularConeSet y)"
        using p35aRegular by simp
      ultimately show ?thesis 
        using lemInsideRegularConeUnderAffInvertible[of "Akmy" "y" "py"]
        by auto
    qed

    moreover have "x ≠ px"
    proof -
      { assume xispx:"x = px"
        hence "False" using xispx invA' px xA'y py by auto
      }
      thus ?thesis by auto
    qed

    ultimately have "insideRegularCone x (Akmy py) ∧ x ≠ (Akmy py)" 
      using px by blast 
  }
  hence result: "∀py . (onTimeAxis py ∧ py ≠ y) 
                         ⟶ insideRegularCone x (Akmy py) ∧ x ≠ (Akmy py)"
    by blast

  (* AND FINALLY: SHOW The two parts of ?thesis to end the proof *)
  {
    obtain p where p: "(p ≠ x) ∧ (p ∈ l)" using assms(4) by blast

    have "l = applyToSet (asFunc Akmy) timeAxis" using lprops by simp
    hence "p ∈ { p . ∃ py ∈ timeAxis . (asFunc Akmy) py p }" using p by auto
    then obtain py where py: "py ∈ timeAxis ∧ (asFunc Akmy) py p" by blast

    hence "onTimeAxis py" by blast
    moreover have "py ≠ y"
    proof -
      { assume "py = y"
        hence "False" using py p by (simp add: xA'y)
      }
      thus ?thesis by auto
    qed
    ultimately have "onTimeAxis py ∧ py ≠ y" by blast

    hence inside: "insideRegularCone x p ∧ x ≠ p" using result py by auto
    have onl: "onLine x l ∧ onLine p l" using ass2 using p by blast
    have pnotx: "p ≠ x" using inside by auto
    hence xnotp: "x ≠ p" by simp

    hence lj: "l = lineJoining x p" 
      using lemLineAndPoints[of "x" "p" "l"] xnotp onl by auto

    (* TARGET: Part 1 *)
    hence "lineSlopeFinite l" using onl inside by blast

    (* TARGET: Part 2 *)
    moreover have "(sNorm2 v < 1)"
    proof -
      have "(∃ v ∈ lineVelocity l . sNorm2 v < 1)" using lj inside by auto
      then obtain u where u: "u ∈ lineVelocity l ∧ sNorm2 u < 1" by blast
      hence "u = v" 
        using lemFiniteLineVelocityUnique[of "u" "l" "v"] ass3 calculation 
        by presburger
      thus ?thesis using u by auto
    qed

    ultimately have "(lineSlopeFinite l) ∧ (sNorm2 v < 1)" by auto
  }
  thus ?thesis by auto
qed
    

end (* of class NoFTLGR *)

end (* of theory NoFTLGR *)