Representation and Physical Values

Exact root statement

∀ {System : Type uSystem} {PhysicalState : Type uPhysicalState} {MathematicalState : Type uMathematicalState}
  {PhysicalQuantity : Type uPhysicalQuantity} {MathematicalQuantity : Type uMathematicalQuantity}
  {PhysicalValue : Type uPhysicalValue} {MathematicalValue : Type uMathematicalValue} {Regime : Type uRegime}
  (context :
    PhysicsLogic.Philosophy.MathematicsAndNature.QuantityRepresentationContext System PhysicalState MathematicalState
      PhysicalQuantity MathematicalQuantity PhysicalValue MathematicalValue Regime)
  (mathematicalQuantity : MathematicalQuantity) (physicalQuantity : PhysicalQuantity) (system : System)
  (regime : Regime),
  context.FaithfullyRepresentsAt mathematicalQuantity physicalQuantity system regime ↔
    (∃ mathematicalState physicalState mathematicalValue physicalValue,
        context.mathematicalStateAdmissibleAt mathematicalState regime ∧
          context.mathematicalQuantityAdmissibleAt mathematicalQuantity regime ∧
            context.representsStateAt mathematicalState physicalState system regime ∧
              context.representsQuantityAt mathematicalQuantity physicalQuantity system regime ∧
                context.assignsValueAt mathematicalQuantity mathematicalState mathematicalValue regime ∧
                  context.representsValueAt mathematicalValue physicalValue mathematicalQuantity physicalQuantity
                    regime) ∧
      ∀ (mathematicalState : MathematicalState) (physicalState : PhysicalState) (mathematicalValue : MathematicalValue)
        (physicalValue : PhysicalValue),
        context.mathematicalStateAdmissibleAt mathematicalState regime →
          context.mathematicalQuantityAdmissibleAt mathematicalQuantity regime →
            context.representsStateAt mathematicalState physicalState system regime →
              context.representsQuantityAt mathematicalQuantity physicalQuantity system regime →
                context.assignsValueAt mathematicalQuantity mathematicalState mathematicalValue regime →
                  context.representsValueAt mathematicalValue physicalValue mathematicalQuantity physicalQuantity
                      regime →
                    context.physicallyHasValueAt physicalQuantity physicalState system physicalValue regime