Scott's explicit finite sequence conditions

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

A realizing functional satisfies Scott's positive-weight condition (2).

theorem Scott1964.MeasurementStructures.LinearInequalities.WeightedSequenceCancellation.unweighted {L : Type u_1} [AddCommGroup L] [Module ℝ L] {X N : Set L} (h : WeightedSequenceCancellation X N) : UnweightedSequenceCancellation X N

Condition (2) immediately implies the unit-weight condition (4).

theorem Scott1964.MeasurementStructures.LinearInequalities.RelationRealizable.sequenceCancellation {L : Type u_1} [AddCommGroup L] [Module ℝ L] {Y : Set L} {R : L → L → Prop} (hreal : RelationRealizable Y R) : RelationSequenceCancellation Y R

A realizing relation satisfies Scott's paired equal-sums condition (6).