import PhysicsLogicConsumer.LightConePropagation

open PhysicsLogicConsumer.LightConePropagation
open PhysicsLogicConsumer.LightConePropagation.Redescription
open PhysicsLogic.Philosophy.Covariance

example : Event = (Real × Real) := rfl
example (event : Event) : interval event = event.1 ^ 2 - event.2 ^ 2 := rfl
example (beta gamma : Real) (event : Event) : boost beta gamma event =
    (gamma * (event.1 - beta * event.2), gamma * (event.2 - beta * event.1)) := rfl
example (chart : Bool) (coordinate : Event) :
    (Description.mk chart coordinate).chart = chart ∧
      (Description.mk chart coordinate).coordinate = coordinate := ⟨rfl, rfl⟩
example (chart : Bool) (event : Event) : coordinates chart event =
    (if chart then ((5 / 4) * (event.1 - (3 / 5) * event.2),
      (5 / 4) * (event.2 - (3 / 5) * event.1)) else event) := rfl
example (description : Description) : decodedEvent description =
    (if description.chart then
      ((5 / 4) * (description.coordinate.1 - (-3 / 5) * description.coordinate.2),
        (5 / 4) * (description.coordinate.2 - (-3 / 5) * description.coordinate.1))
      else description.coordinate) := rfl
example (targetChart : Bool) : comparison targetChart = ({
    admissibleReexpression := fun _ => True
    reexpresses := fun _ first second => first.chart = false ∧ second.chart = targetChart ∧
      second.coordinate = ((5 / 4) * (first.coordinate.1 - (3 / 5) * first.coordinate.2),
        (5 / 4) * (first.coordinate.2 - (3 / 5) * first.coordinate.1))
  } : RedescriptionContext Description Unit) := rfl
example (targetChart : Bool) : intervalCovariance targetChart = ({
    toRedescriptionContext := comparison targetChart
    lawSatisfied := fun squaredInterval description =>
      description.coordinate.1 ^ 2 - description.coordinate.2 ^ 2 = squaredInterval
  } : LawCovarianceContext Description Unit Real) := rfl
example (targetChart : Bool) : eventInterpretation targetChart = ({
    toRedescriptionContext := comparison targetChart
    represents := fun description event => description.coordinate =
      (if description.chart then
        ((5 / 4) * (event.1 - (3 / 5) * event.2),
          (5 / 4) * (event.2 - (3 / 5) * event.1)) else event)
  } : PhysicalRedescriptionContext Description Unit Event) := rfl