import PhysicsLogic.Philosophy.MathematicsAndNature

open PhysicsLogic.Philosophy.MathematicsAndNature
variable {S P M Q F V W R : Type}

example : ∀ (c : QuantityRepresentationContext S P M Q F V W R)
    (f : F) (q : Q) (s : S) (r : R), c.FaithfullyRepresentsAt f q s r ↔
    (∃ m p w v,
      c.mathematicalStateAdmissibleAt m r ∧ c.mathematicalQuantityAdmissibleAt f r ∧
      c.representsStateAt m p s r ∧ c.representsQuantityAt f q s r ∧
      c.assignsValueAt f m w r ∧ c.representsValueAt w v f q r) ∧
    (∀ m p w v,
      c.mathematicalStateAdmissibleAt m r → c.mathematicalQuantityAdmissibleAt f r →
      c.representsStateAt m p s r → c.representsQuantityAt f q s r →
      c.assignsValueAt f m w r → c.representsValueAt w v f q r →
      c.physicallyHasValueAt q p s v r) :=
  faithful_representation_iff_nonempty_sound_assignments

#print axioms faithful_representation_iff_nonempty_sound_assignments

example : ∀ (c : QuantityRepresentationContext S P M Q F V W R)
    (f : F) (q : Q) (s : S) (r : R), c.AssignmentSoundAt f q s r ↔
    ∀ m p w v,
      c.mathematicalStateAdmissibleAt m r → c.mathematicalQuantityAdmissibleAt f r →
      c.representsStateAt m p s r → c.representsQuantityAt f q s r →
      c.assignsValueAt f m w r → c.representsValueAt w v f q r →
      c.physicallyHasValueAt q p s v r := assignment_soundness_iff_explicit_assignments

example : ∀ (c : QuantityRepresentationContext S P M Q F V W R)
    (m : M) (p : P) (f : F) (q : Q) (w : W) (v : V) (s : S) (r : R),
    c.EstablishedRepresentedValueAt m p f q w v s r ↔
      c.mathematicalStateAdmissibleAt m r ∧ c.mathematicalQuantityAdmissibleAt f r ∧
      c.representsStateAt m p s r ∧ c.representsQuantityAt f q s r ∧
      c.assignsValueAt f m w r ∧ c.representsValueAt w v f q r ∧
      c.physicallyHasValueAt q p s v r := established_value_iff_explicit_assignment_and_physical_value