Scott 1964, Theorems 1.1–1.4

Finite convex-separation forms of the general method in §1.

theorem Scott1964.MeasurementStructures.LinearInequalities.WeightedSequenceCancellation.fintype {L : Type u_1} [AddCommGroup L] [Module ℝ L] {X N : Set L} (h : WeightedSequenceCancellation X N) {I : Type u_2} [Fintype I] [Nonempty I] (x : I → L) (c : I → ℝ) (hx : ∀ (i : I), x i ∈ X) (hN : ∀ (i : I), x i ∈ N) (hc : ∀ (i : I), 0 < c i) (hsum : ∑ i : I, c i • x i = 0) (i : I) : -x i ∈ N

The sequence formulation may be used with any nonempty finite index type.

theorem Scott1964.MeasurementStructures.LinearInequalities.weightedCancellation_of_sequence {L : Type u_1} [AddCommGroup L] [Module ℝ L] {X N : Set L} (hsym : Symmetric X) (hseq : WeightedSequenceCancellation X N) : WeightedCancellation X N

Scott's positive-weight sequence condition is equivalent to the geometric cancellation condition.

theorem Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_4_forward {L : Type u_1} [AddCommGroup L] [Module ℝ L] {Y : Set L} {R : L → L → Prop} (hreal : RelationRealizable Y R) : ∃ (Rplus : L → L → Prop), ExtendsOn Y (additiveClosure Y) R Rplus ∧ StrictlyMonotonic (additiveClosure Y) Rplus

A realizing functional supplies Scott's strictly monotonic extension to the additive closure. This is the forward half of Theorem 1.4.

theorem Scott1964.MeasurementStructures.LinearInequalities.StrictlyMonotonic.relationSequenceCancellation {L : Type u_1} [AddCommGroup L] {Y : Set L} {R Rplus : L → L → Prop} (hext : ExtendsOn Y (additiveClosure Y) R Rplus) (hmono : StrictlyMonotonic (additiveClosure Y) Rplus) : RelationSequenceCancellation Y R

A strictly monotonic extension implies Scott's literal condition (6).

theorem Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_1 {L : Type u_1} [NormedAddCommGroup L] [NormedSpace ℝ L] [FiniteDimensional ℝ L] {X N : Set L} (hX : X.Finite) (hsym : Symmetric X) : Realizable X N ↔ SignComplete X N ∧ WeightedSequenceCancellation X N

Scott (1964), Theorem 1.1.

theorem Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_2 {S : Type u_2} [Finite S] {X N : Set (S → ℝ)} (hX : X.Finite) (hrat : IsRationalSet X) (hsym : Symmetric X) : Realizable X N ↔ SignComplete X N ∧ UnweightedSequenceCancellation X N

Scott (1964), Theorem 1.2, for rational coordinate vectors.

Rationality is used to replace a positive real dependence by a positive rational dependence, clear denominators, and reduce to repeated unweighted summands.

theorem Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_3_geometric {L : Type u_1} [NormedAddCommGroup L] [NormedSpace ℝ L] [FiniteDimensional ℝ L] {Y : Set L} {R : L → L → Prop} (hY : Y.Finite) : RelationRealizable Y R ↔ RelationComplete Y R ∧ RelationCancellation Y R

Geometric intermediate form used in the proof of Theorem 1.3.

theorem Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_3 {S : Type u_2} [Finite S] {Y : Set (S → ℝ)} {R : (S → ℝ) → (S → ℝ) → Prop} (hY : Y.Finite) (hYrat : IsRationalSet Y) : RelationRealizable Y R ↔ RelationComplete Y R ∧ RelationSequenceCancellation Y R

Scott (1964), Theorem 1.3, with the literal paired equal-sums cancellation condition (6).

theorem Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_4 {S : Type u_2} [Finite S] {Y : Set (S → ℝ)} {R : (S → ℝ) → (S → ℝ) → Prop} (hY : Y.Finite) (hYrat : IsRationalSet Y) : RelationRealizable Y R ↔ ∃ (Rplus : (S → ℝ) → (S → ℝ) → Prop), ExtendsOn Y (additiveClosure Y) R Rplus ∧ StrictlyMonotonic (additiveClosure Y) Rplus

Scott (1964), Theorem 1.4: realizability is equivalent to extendability to a strictly monotonic relation on the additive closure.