import PhysicsLogic.Paradigm.EquivalencePrinciples

set_option autoImplicit false
open PhysicsLogic.Paradigm.EquivalencePrinciples

variable {E F P R : Type}

example (ng : E -> Prop) (localAt : E -> P -> Prop)
    (falling : F -> P -> Prop) (uniform : F -> F -> P -> Prop)
    (result : E -> F -> P -> R) :
    LocalNongravitationalExperimentContext.mk ng localAt falling uniform result =
      ({ nongravitationalExperiment := ng, localAt := localAt,
         freelyFallingFrameAt := falling, relativelyUniformAt := uniform,
         experimentResult := result } : LocalNongravitationalExperimentContext E F P R) := rfl

variable (context : LocalNongravitationalExperimentContext E F P R)

example : context.LocalLorentzInvariance =
    (forall experiment place first second,
      context.nongravitationalExperiment experiment -> context.localAt experiment place ->
      context.freelyFallingFrameAt first place -> context.freelyFallingFrameAt second place ->
      context.relativelyUniformAt first second place ->
      context.experimentResult experiment first place = context.experimentResult experiment second place) := rfl

example : context.LocalPositionInvariance =
    (forall experiment firstPlace secondPlace frame,
      context.nongravitationalExperiment experiment ->
      context.localAt experiment firstPlace -> context.localAt experiment secondPlace ->
      context.freelyFallingFrameAt frame firstPlace -> context.freelyFallingFrameAt frame secondPlace ->
      context.experimentResult experiment frame firstPlace = context.experimentResult experiment frame secondPlace) := rfl

example : context.LocalLorentzComparisonScope =
    (exists experiment place first second,
      first ≠ second /\ context.nongravitationalExperiment experiment /\
      context.localAt experiment place /\ context.freelyFallingFrameAt first place /\
      context.freelyFallingFrameAt second place /\ context.relativelyUniformAt first second place) := rfl

example : context.LocalPositionComparisonScope =
    (exists experiment firstPlace secondPlace frame,
      firstPlace ≠ secondPlace /\ context.nongravitationalExperiment experiment /\
      context.localAt experiment firstPlace /\ context.localAt experiment secondPlace /\
      context.freelyFallingFrameAt frame firstPlace /\ context.freelyFallingFrameAt frame secondPlace) := rfl

example : context.NonvacuousLocalLorentzInvariance =
    (context.LocalLorentzInvariance /\ context.LocalLorentzComparisonScope) := rfl
example : context.NonvacuousLocalPositionInvariance =
    (context.LocalPositionInvariance /\ context.LocalPositionComparisonScope) := rfl