import PhysicsLogicConsumer.FrequencyReference

open PhysicsLogic.Philosophy.Measurement
open PhysicsLogicConsumer.FrequencyReference

example : frequencyRecords =
    (RecordAccessContext.mk
      (fun p : Real × Real => 0 < p.1 ∧ 0 < p.2)
      (fun (access : Bool) (p : Real × Real) =>
        if access then (p.1 / p.2, p.2) else (p.1 / p.2, 0))
      Prod.fst) := rfl

example (error : Real) : boundedReferenceRecords error =
    (RecordAccessContext.mk
      (fun p : Real × Real => (0 < p.1 ∧ 0 < p.2) ∧ |p.2 - 1| ≤ error)
      (fun (access : Bool) (p : Real × Real) =>
        if access then (p.1 / p.2, p.2) else (p.1 / p.2, 0))
      Prod.fst) := rfl