import PhysicsLogic.Framework.LinearRelativeStateMeasurement

open PhysicsLogic.Framework.CoherentRecordMeasurement

variable {Outcome : Type} [Fintype Outcome] [DecidableEq Outcome]

example : ∀ (process : Process Outcome) (first second : Outcome -> Complex)
    (alpha beta : Complex) (pair : Outcome × Outcome),
    process.measurement (fun outcome => alpha * first outcome + beta * second outcome) pair =
      alpha * process.measurement first pair + beta * process.measurement second pair :=
  Process.measurement_preserves_superpositions

example : ∀ process : Process Outcome,
    process.MeasurementCalibration ↔ ∀ amplitude : Outcome -> Complex,
      ∀ pair : Outcome × Outcome,
        process.measurement amplitude pair =
          if pair.1 = pair.2 then amplitude pair.1 else 0 :=
  Process.measurement_calibration_iff_amplitude_transport

example : ∀ (process : Process Outcome) (_ : process.MeasurementCalibration)
    (recorded value : Outcome),
    process.toCorrelationAccessContext.RecordDeterminesValueAt false (Sum.inr recorded) value ↔
      process.inputAmplitude recorded ≠ 0 ∧ value = recorded :=
  Process.pointer_record_determination_iff_supported_value

example : ∀ (process : Process Outcome) (_ : process.MeasurementCalibration) (value : Outcome),
    process.toCorrelationAccessContext.RecordDeterminesValueAt true (Sum.inl true) value ↔
      process.inputAmplitude value ≠ 0 ∧
        ∀ alternative, process.inputAmplitude alternative ≠ 0 -> alternative = value :=
  Process.correlation_record_determination_iff_single_support

#print axioms Process.measurement_preserves_superpositions
#print axioms Process.measurement_calibration_iff_amplitude_transport
#print axioms Process.pointer_record_determination_iff_supported_value
#print axioms Process.correlation_record_determination_iff_single_support