import PhysicsLogicConsumer.LightConePropagation

open PhysicsLogicConsumer.LightConePropagation

example : Event = (Real × Real) := rfl
example (p : Event) : interval p = p.1 ^ 2 - p.2 ^ 2 := rfl
example (b g : Real) (p : Event) :
    boost b g p = (g * (p.1 - b * p.2), g * (p.2 - b * p.1)) := rfl
example (s : Event → Event → Prop) (p q : Event) :
    (cone s).spacelike p q ↔ |q.1 - p.1| < |q.2 - p.2| := Iff.rfl
example (s : Event → Event → Prop) (p q : Event) :
    (cone s).causallyReachable p q ↔ |q.2 - p.2| ≤ q.1 - p.1 := Iff.rfl
example (s : Event → Event → Prop) : (cone s).signalPossible = s := rfl
example (p q : Event) : light p q ↔ 0 < q.1 - p.1 ∧ |q.2 - p.2| = q.1 - p.1 := Iff.rfl
example (p q : Event) : unrestrictedFuture.spacelike p q ↔ |q.1 - p.1| < |q.2 - p.2| := Iff.rfl
example (p q : Event) : unrestrictedFuture.causallyReachable p q ↔ p.1 < q.1 := Iff.rfl
example (p q : Event) : unrestrictedFuture.signalPossible p q ↔ p.1 < q.1 := Iff.rfl