Documentation

LeanPool.ScottMeasurement.LinearInequalities.OrderedGroup

Ordered groups after Scott's Theorem 1.4 #

The first result makes precise Scott's observation that every finite part of a linearly ordered abelian group has a real-valued model. Pair-sums are put into the finite system, so the model preserves every addition equation visible inside that finite part.

The second group of results records the standard lexicographic obstruction: each finite subsystem is real-valued, but the whole ordered monoid is not.

source
theorem Scott1964.MeasurementStructures.LinearInequalities.finite_local_real_embedding {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (S : Set G) (hS : S.Finite) :
∃ (f : ↑S → ℝ), (∀ (x y : ↑S), x ≤ y ↔ f x ≤ f y) ∧ ∀ (x y z : ↑S), ↑x + ↑y = ↑z → f x + f y = f z

Every finite subset of a linearly ordered abelian group admits a local real embedding. It reflects the ambient order and preserves every equation x + y = z all three of whose terms belong to the finite set.

source
@[reducible, inline]
abbrev Scott1964.MeasurementStructures.LinearInequalities.LexIntPair :
Type

The ordered abelian group used to obstruct a global real representation.

Equations
Instances For
    source
    def Scott1964.MeasurementStructures.LinearInequalities.lexGenerators :
    Set LexIntPair

    The two positive coordinate generators of the lexicographic example.

    Equations
    Instances For
      source
      def Scott1964.MeasurementStructures.LinearInequalities.lexPreference (x y : LexIntPair) :
      Prop

      Comparison oriented as preference, with the first coordinate taking priority.

      Equations
      Instances For
        source
        theorem Scott1964.MeasurementStructures.LinearInequalities.lexPreference_strictlyMonotonic :
        StrictlyMonotonic (additiveClosure lexGenerators) lexPreference
        source
        theorem Scott1964.MeasurementStructures.LinearInequalities.no_global_real_additive_lex_realization :
        ¬∃ (f : LexIntPair →+ ℝ), ∀ (x y : LexIntPair), lexPreference x y ↔ f y ≤ f x

        No additive real-valued functional realizes lexicographic comparison on the whole lexicographically ordered group ℤ × ℤ. The obstruction already uses the positive additive closure of the two nonzero generators: (0,1) > 0, while every natural multiple (0,n) remains below (1,0).