diff --git a/LeanPool/ScottMeasurement.lean b/LeanPool/ScottMeasurement.lean
new file mode 100644
index 0000000000..a1e400293d
--- /dev/null
+++ b/LeanPool/ScottMeasurement.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Basic
+
+/-!
+# Scott's measurement representation theorems
+
+Source: url:https://github.com/catskillsresearch/scott1964
+Authors: Lars Warren Ericson
+Status: verified
+Main declarations: `Scott1964.MeasurementStructures.theorem_4_1_vector`
+Tags: measurement-theory, utility-representation, qualitative-probability
+MSC: 91B16, 91B06, 60A05, 52A20
+-/
+
+/-!
+# Scott’s measurement structures and linear inequalities
+
+Ported from catskillsresearch/scott1964 at
+591e8a6a5d7d1ebf4cc761b4a1cb749b6480dfeb (Apache-2.0).
+Lars Warren Ericson directed and reviewed the AI-generated Lean development.
+
+The third-party source paper is cited, not redistributed. Its copyright remains
+with its publisher. The infinite probability equivalence is a modern reconstruction
+under an explicit generalized Kelley condition, not a published theorem of Scott.
+-/
diff --git a/LeanPool/ScottMeasurement/Basic.lean b/LeanPool/ScottMeasurement/Basic.lean
new file mode 100644
index 0000000000..745e0d6872
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Basic.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.FinHead
+public import LeanPool.ScottMeasurement.LinearInequalities.Definitions
+public import LeanPool.ScottMeasurement.LinearInequalities.Separation
+public import LeanPool.ScottMeasurement.LinearInequalities.Rationalization
+public import LeanPool.ScottMeasurement.LinearInequalities.Sequences
+public import LeanPool.ScottMeasurement.LinearInequalities.ScottTheorems
+public import LeanPool.ScottMeasurement.LinearInequalities.OrderedGroup
+public import LeanPool.ScottMeasurement.Preference.Direct
+public import LeanPool.ScottMeasurement.Preference.Cycle
+public import LeanPool.ScottMeasurement.Preference.Intransitive
+public import LeanPool.ScottMeasurement.Differences.Pair
+public import LeanPool.ScottMeasurement.Differences.Ordered
+public import LeanPool.ScottMeasurement.Probability.Basic
+public import LeanPool.ScottMeasurement.Probability.Atoms
+public import LeanPool.ScottMeasurement.Probability.Finite
+public import LeanPool.ScottMeasurement.Probability.KPSCounterexample
+public import LeanPool.ScottMeasurement.Probability.Infinite.EventSpace
+public import LeanPool.ScottMeasurement.Probability.Infinite.HahnBanach
+public import LeanPool.ScottMeasurement.Probability.Infinite.Kelley
+public import LeanPool.ScottMeasurement.Probability.Infinite.Reconstructed
+
+/-!
+# Scott 1964 — Measurement Structures and Linear Inequalities
+
+Primary source: Dana S. Scott, *Measurement Structures and Linear
+Inequalities*, Journal of Mathematical Psychology 1 (1964), 233–247.
+Working transcription in the pinned upstream repository:
+`sources/ScottMeasurement1964_vision.md`.
+
+The paper applies the general solvability criterion for finite systems of
+linear inequalities (Theorems 1.1–1.4) to three measurement problems:
+intransitive indifference (Theorem 2.1), ordered differences (Theorems 3.1
+and 3.2), and subjective probability (Theorem 4.1).
+
+This module re-exports the complete development used by upstream
+`Solution.lean` (not included here): Scott's eight published theorems, the finite KPS
+counterexample, and the separately labelled modern reconstruction of the
+infinite probability theorem.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Differences/Ordered.lean b/LeanPool/ScottMeasurement/Differences/Ordered.lean
new file mode 100644
index 0000000000..8cecafd588
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Differences/Ordered.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Differences.Pair
+
+/-!
+# Ordered differences
+
+Scott's reduction of the one-utility problem to Theorem 3.1 is entirely
+algebraic.  The key point is that reversal lets the two utilities be combined.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+/-- Representation of comparisons of utility differences. -/
+def RealizableDifference {A : Type u} (D : A → A → A → A → Prop) : Prop :=
+  ∃ f : A → ℝ, ∀ x y z w, D x y z w ↔ f x - f y ≥ f z - f w
+
+/-- Scott 1964, condition `(1_D)`. -/
+def DiffTotal {A : Type u} (D : A → A → A → A → Prop) : Prop :=
+  ∀ x y z w, D x y z w ∨ D z w x y
+
+/-- Scott 1964, condition `(2_D)`. -/
+def DiffPermutation {A : Type u} (D : A → A → A → A → Prop) : Prop :=
+  ∀ (n : ℕ) (x y : Fin (n + 1) → A) (π σ : Equiv.Perm (Fin (n + 1))),
+    (∀ i, i ≠ finHead n → D (x i) (y i) (x (π i)) (y (σ i))) →
+      D (x (π (finHead n))) (y (σ (finHead n))) (x (finHead n)) (y (finHead n))
+
+/-- Scott 1964, condition `(3_D)`. -/
+def DiffReversal {A : Type u} (D : A → A → A → A → Prop) : Prop :=
+  ∀ x y z w, D x y z w → D w z y x
+
+theorem RealizableDifference.utilityPair {A : Type u}
+    {D : A → A → A → A → Prop} (hD : RealizableDifference D) :
+    RealizableUtilityPair D := by
+  rcases hD with ⟨f, hf⟩
+  refine ⟨f, fun y ↦ -f y, ?_⟩
+  intro x y z w
+  rw [hf]
+  constructor <;> intro h <;> dsimp at h ⊢ <;> linarith
+
+theorem RealizableDifference.reversal {A : Type u}
+    {D : A → A → A → A → Prop} (hD : RealizableDifference D) :
+    DiffReversal D := by
+  rcases hD with ⟨f, hf⟩
+  intro x y z w h
+  rw [hf] at h ⊢
+  linarith
+
+theorem RealizableDifference.necessary {A : Type u}
+    {D : A → A → A → A → Prop} (hD : RealizableDifference D) :
+    DiffTotal D ∧ DiffPermutation D ∧ DiffReversal D := by
+  have hp := hD.utilityPair.necessary
+  exact ⟨hp.1, hp.2, hD.reversal⟩
+
+/-- The combining-utilities argument in the proof of Theorem 3.2. -/
+theorem difference_of_pair_and_reversal {A : Type u}
+    {D : A → A → A → A → Prop} (hp : RealizableUtilityPair D)
+    (hr : DiffReversal D) : RealizableDifference D := by
+  rcases hp with ⟨g, q, hrep⟩
+  refine ⟨fun x ↦ g x - q x, ?_⟩
+  intro x y z w
+  constructor
+  · intro h
+    have h₁ := (hrep x y z w).1 h
+    have h₂ := (hrep w z y x).1 (hr x y z w h)
+    dsimp
+    linarith
+  · intro hdiff
+    by_contra hn
+    have hstrict : g x + q y < g z + q w :=
+      lt_of_not_ge (fun h ↦ hn ((hrep x y z w).2 h))
+    have hreverse : D z w x y := (hrep z w x y).2 (le_of_lt hstrict)
+    have h₂ := (hrep y x w z).1 (hr z w x y hreverse)
+    dsimp at hdiff
+    linarith
+
+/-- The exact logical reduction used for Theorem 3.2. -/
+theorem realizableDifference_iff_pair_reversal {A : Type u}
+    (D : A → A → A → A → Prop) :
+    RealizableDifference D ↔ RealizableUtilityPair D ∧ DiffReversal D := by
+  exact ⟨fun h ↦ ⟨h.utilityPair, h.reversal⟩,
+    fun h ↦ difference_of_pair_and_reversal h.1 h.2⟩
+
+/-- Once Theorem 3.1 is available, its sufficiency immediately yields Scott's
+Theorem 3.2 through the preceding combining lemma. -/
+theorem difference_sufficient_of_pair_sufficient {A : Type u}
+    (pairSufficient :
+      ∀ V : A → A → A → A → Prop,
+        PairTotal V ∧ PairPermutation V → RealizableUtilityPair V)
+    {D : A → A → A → A → Prop}
+    (hD : DiffTotal D ∧ DiffPermutation D ∧ DiffReversal D) :
+    RealizableDifference D :=
+  difference_of_pair_and_reversal (pairSufficient D ⟨hD.1, hD.2.1⟩) hD.2.2
+
+/-- **Scott 1964, Theorem 3.2 (ordered differences).**
+The result also holds when the alternative type is empty. -/
+theorem theorem_3_2 {A : Type u} [Finite A]
+    (D : A → A → A → A → Prop) :
+    RealizableDifference D ↔ DiffTotal D ∧ DiffPermutation D ∧ DiffReversal D := by
+  let := Fintype.ofFinite A
+  constructor
+  · exact RealizableDifference.necessary
+  · rintro ⟨htotal, hperm, hreversal⟩
+    exact difference_of_pair_and_reversal
+      ((theorem_3_1 D).2 ⟨htotal, hperm⟩) hreversal
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Differences/Pair.lean b/LeanPool/ScottMeasurement/Differences/Pair.lean
new file mode 100644
index 0000000000..a010ba51bb
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Differences/Pair.lean
@@ -0,0 +1,282 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.FinHead
+public import LeanPool.ScottMeasurement.LinearInequalities.ScottTheorems
+
+/-!
+# Additive utility for pairs
+
+This is Scott 1964, Theorem 3.1.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+open scoped BigOperators
+
+open Classical in
+/-- The incidence vector of a pair, with one coordinate in each summand. -/
+noncomputable def pairVector {A : Type u} {A' : Type v} (x : A) (x' : A') :
+    Sum A A' → ℝ :=
+  Pi.single (Sum.inl x) 1 + Pi.single (Sum.inr x') 1
+
+theorem pairVector_injective {A : Type u} {A' : Type v} :
+    Function.Injective (Function.uncurry (@pairVector A A')) := by
+  classical
+  rintro ⟨x, x'⟩ ⟨y, y'⟩ h
+  have hx : x = y := by
+    simpa [pairVector, Pi.single_apply] using congrFun h (Sum.inl x)
+  have hx' : x' = y' := by
+    simpa [pairVector, Pi.single_apply] using congrFun h (Sum.inr x')
+  exact Prod.ext hx hx'
+
+/-- Equality of sums of incidence vectors gives the two independent
+permutations of coordinates used in condition `(2_V)`. -/
+theorem pairVector_sum_eq_permutations {A : Type u} {A' : Type v}
+    {ι : Type*} [Fintype ι] (x y : ι → A) (x' y' : ι → A')
+    (h : ∑ i, pairVector (x i) (x' i) =
+      ∑ i, pairVector (y i) (y' i)) :
+    ∃ π σ : Equiv.Perm ι,
+      (∀ i, y i = x (π i)) ∧ (∀ i, y' i = x' (σ i)) := by
+  classical
+  have hleft (a : A) :
+      Fintype.card {i // y i = a} = Fintype.card {i // x i = a} := by
+    have ha := congrFun h (Sum.inl a)
+    simp only [Fintype.sum_apply, pairVector, Pi.add_apply, Pi.single_apply,
+      Sum.inl.injEq, Sum.inl_ne_inr, ↓reduceIte, add_zero] at ha
+    have hy :
+        Fintype.card {i // y i = a} =
+          (Finset.univ.filter fun i ↦ y i = a).card := by
+      rw [← Fintype.card_coe]
+      exact Fintype.card_congr
+        (Equiv.subtypeEquivRight fun i ↦ by simp)
+    have hx :
+        Fintype.card {i // x i = a} =
+          (Finset.univ.filter fun i ↦ x i = a).card := by
+      rw [← Fintype.card_coe]
+      exact Fintype.card_congr
+        (Equiv.subtypeEquivRight fun i ↦ by simp)
+    rw [hy, hx]
+    rw [Finset.card_filter, Finset.card_filter]
+    exact_mod_cast (by simpa [eq_comm] using ha.symm)
+  have hright (a : A') :
+      Fintype.card {i // y' i = a} = Fintype.card {i // x' i = a} := by
+    have ha := congrFun h (Sum.inr a)
+    simp only [Fintype.sum_apply, pairVector, Pi.add_apply, Pi.single_apply,
+      Sum.inr.injEq, Sum.inr_ne_inl, ↓reduceIte, zero_add] at ha
+    have hy :
+        Fintype.card {i // y' i = a} =
+          (Finset.univ.filter fun i ↦ y' i = a).card := by
+      rw [← Fintype.card_coe]
+      exact Fintype.card_congr
+        (Equiv.subtypeEquivRight fun i ↦ by simp)
+    have hx :
+        Fintype.card {i // x' i = a} =
+          (Finset.univ.filter fun i ↦ x' i = a).card := by
+      rw [← Fintype.card_coe]
+      exact Fintype.card_congr
+        (Equiv.subtypeEquivRight fun i ↦ by simp)
+    rw [hy, hx]
+    rw [Finset.card_filter, Finset.card_filter]
+    exact_mod_cast (by simpa [eq_comm] using ha.symm)
+  let π : Equiv.Perm ι :=
+    Equiv.ofFiberEquiv fun a ↦ Fintype.equivOfCardEq (hleft a)
+  let σ : Equiv.Perm ι :=
+    Equiv.ofFiberEquiv fun a ↦ Fintype.equivOfCardEq (hright a)
+  refine ⟨π, σ, ?_, ?_⟩
+  · intro i
+    change y i = x ((Equiv.ofFiberEquiv
+      (fun a ↦ Fintype.equivOfCardEq (hleft a))) i)
+    exact ((Fintype.equivOfCardEq (hleft (y i)))
+      ((Equiv.sigmaFiberEquiv y).symm i).2).2.symm
+  · intro i
+    change y' i = x' ((Equiv.ofFiberEquiv
+      (fun a ↦ Fintype.equivOfCardEq (hright a))) i)
+    exact ((Fintype.equivOfCardEq (hright (y' i)))
+      ((Equiv.sigmaFiberEquiv y').symm i).2).2.symm
+
+/-- A relation on pairs is represented by the sum of two utility functions. -/
+def RealizableUtilityPair {A : Type u} {A' : Type v}
+    (V : A → A' → A → A' → Prop) : Prop :=
+  ∃ f : A → ℝ, ∃ f' : A' → ℝ,
+    ∀ x x' y y', V x x' y y' ↔ f x + f' x' ≥ f y + f' y'
+
+/-- Scott 1964, condition `(1_V)`. -/
+def PairTotal {A : Type u} {A' : Type v}
+    (V : A → A' → A → A' → Prop) : Prop :=
+  ∀ x x' y y', V x x' y y' ∨ V y y' x x'
+
+/-- Scott 1964, condition `(2_V)`, indexed at length `n + 1` so that the
+distinguished index `0` always exists. -/
+def PairPermutation {A : Type u} {A' : Type v}
+    (V : A → A' → A → A' → Prop) : Prop :=
+  ∀ (n : ℕ) (x : Fin (n + 1) → A) (x' : Fin (n + 1) → A')
+    (π σ : Equiv.Perm (Fin (n + 1))),
+    (∀ i, i ≠ finHead n → V (x i) (x' i) (x (π i)) (x' (σ i))) →
+      V (x (π (finHead n))) (x' (σ (finHead n))) (x (finHead n)) (x' (finHead n))
+
+/-- Scott's observation following `(2_V)`: the permutation condition already
+implies transitivity. -/
+theorem PairPermutation.transitive {A : Type u} {A' : Type v}
+    {V : A → A' → A → A' → Prop} (hV : PairPermutation V) :
+    ∀ p q r : A × A',
+      V p.1 p.2 q.1 q.2 → V q.1 q.2 r.1 r.2 → V p.1 p.2 r.1 r.2 := by
+  rintro ⟨x, x'⟩ ⟨y, y'⟩ ⟨z, z'⟩ hxy hyz
+  let p : Equiv.Perm (Fin 3) :=
+    Equiv.ofBijective ![1, 2, 0] (by decide +kernel)
+  apply hV 2 ![z, x, y] ![z', x', y'] p p
+  intro i hi
+  have hi0 : i ≠ 0 := by simpa [finHead_eq_zero] using hi
+  fin_cases i
+  · contradiction
+  · simpa [p] using hxy
+  · simpa [p] using hyz
+
+theorem RealizableUtilityPair.total {A : Type u} {A' : Type v}
+    {V : A → A' → A → A' → Prop} (hV : RealizableUtilityPair V) :
+    PairTotal V := by
+  rcases hV with ⟨f, f', hrep⟩
+  intro x x' y y'
+  rcases le_total (f y + f' y') (f x + f' x') with h | h
+  · exact Or.inl ((hrep x x' y y').2 h)
+  · exact Or.inr ((hrep y y' x x').2 h)
+
+theorem RealizableUtilityPair.permutation {A : Type u} {A' : Type v}
+    {V : A → A' → A → A' → Prop} (hV : RealizableUtilityPair V) :
+    PairPermutation V := by
+  rcases hV with ⟨f, f', hrep⟩
+  intro n x x' π σ h
+  let s : Fin (n + 1) → ℝ := fun i ↦ f (x i) + f' (x' i)
+  let t : Fin (n + 1) → ℝ := fun i ↦ f (x (π i)) + f' (x' (σ i))
+  have hπ : ∑ i, f (x (π i)) = ∑ i, f (x i) :=
+    Fintype.sum_equiv π _ _ (fun _ ↦ rfl)
+  have hσ : ∑ i, f' (x' (σ i)) = ∑ i, f' (x' i) :=
+    Fintype.sum_equiv σ _ _ (fun _ ↦ rfl)
+  have hsum : ∑ i, s i = ∑ i, t i := by
+    simp only [s, t, Finset.sum_add_distrib]
+    rw [hπ, hσ]
+  have hrest :
+      ∑ i ∈ (Finset.univ.erase (finHead n)), t i ≤
+        ∑ i ∈ (Finset.univ.erase (finHead n)), s i := by
+    apply Finset.sum_le_sum
+    intro i hi
+    have hi0 : i ≠ finHead n := by
+      simpa using (Finset.mem_erase.mp hi).1
+    exact (hrep _ _ _ _).1 (h i hi0)
+  apply (hrep _ _ _ _).2
+  have hzero : finHead n ∈ Finset.univ := Finset.mem_univ _
+  have hs := Finset.sum_erase_add _ s hzero
+  have ht := Finset.sum_erase_add _ t hzero
+  dsimp only [s, t] at *
+  linarith
+
+theorem RealizableUtilityPair.necessary {A : Type u} {A' : Type v}
+    {V : A → A' → A → A' → Prop} (hV : RealizableUtilityPair V) :
+    PairTotal V ∧ PairPermutation V :=
+  ⟨hV.total, hV.permutation⟩
+
+/-- **Scott 1964, Theorem 3.1 (additive utility for pairs).**
+The result also holds when either coordinate type is empty. -/
+theorem theorem_3_1 {A : Type u} {A' : Type v}
+    [Finite A] [Finite A']
+    (V : A → A' → A → A' → Prop) :
+    RealizableUtilityPair V ↔ PairTotal V ∧ PairPermutation V := by
+  let := Fintype.ofFinite A
+  let := Fintype.ofFinite A'
+  constructor
+  · exact RealizableUtilityPair.necessary
+  · rintro ⟨htotal, hperm⟩
+    classical
+    let Y : Set (Sum A A' → ℝ) :=
+      Set.range (Function.uncurry (@pairVector A A'))
+    let R : (Sum A A' → ℝ) → (Sum A A' → ℝ) → Prop :=
+      fun z w ↦ ∀ x x' y y',
+        z = pairVector x x' → w = pairVector y y' → V x x' y y'
+    have hR_pair (x : A) (x' : A') (y : A) (y' : A') :
+        R (pairVector x x') (pairVector y y') ↔ V x x' y y' := by
+      constructor
+      · intro h
+        exact h x x' y y' rfl rfl
+      · intro h a a' b b' ha hb
+        have hxa : (x, x') = (a, a') :=
+          pairVector_injective ha
+        have hyb : (y, y') = (b, b') :=
+          pairVector_injective hb
+        have hxa₁ : x = a := congrArg Prod.fst hxa
+        have hxa₂ : x' = a' := congrArg Prod.snd hxa
+        have hyb₁ : y = b := congrArg Prod.fst hyb
+        have hyb₂ : y' = b' := congrArg Prod.snd hyb
+        simpa [← hxa₁, ← hxa₂, ← hyb₁, ← hyb₂] using h
+    have hYfinite : Y.Finite := Set.finite_range _
+    have hYrat : LinearInequalities.IsRationalSet Y := by
+      rintro z ⟨⟨x, x'⟩, rfl⟩ s
+      rcases s with a | a'
+      · by_cases ha : a = x
+        · exact ⟨1, by simp [pairVector, ha]⟩
+        · exact ⟨0, by simp [pairVector, ha]⟩
+      · by_cases ha : a' = x'
+        · exact ⟨1, by simp [pairVector, ha]⟩
+        · exact ⟨0, by simp [pairVector, ha]⟩
+    have hcomplete : LinearInequalities.RelationComplete Y R := by
+      rintro z ⟨⟨x, x'⟩, rfl⟩ w ⟨⟨y, y'⟩, rfl⟩
+      change R (pairVector x x') (pairVector y y') ∨
+        R (pairVector y y') (pairVector x x')
+      rw [hR_pair, hR_pair]
+      exact htotal x x' y y'
+    have hcancel : LinearInequalities.RelationSequenceCancellation Y R := by
+      intro n z w hz hw hR hsum
+      choose p hp using hz
+      choose q hq using hw
+      let x : Fin (n + 1) → A := fun i ↦ (p i).1
+      let x' : Fin (n + 1) → A' := fun i ↦ (p i).2
+      let y : Fin (n + 1) → A := fun i ↦ (q i).1
+      let y' : Fin (n + 1) → A' := fun i ↦ (q i).2
+      have hx (i) : z i = pairVector (x i) (x' i) := by
+        have hi := hp i
+        change pairVector (p i).1 (p i).2 = z i at hi
+        simpa [x, x'] using hi.symm
+      have hy (i) : w i = pairVector (y i) (y' i) := by
+        have hi := hq i
+        change pairVector (q i).1 (q i).2 = w i at hi
+        simpa [y, y'] using hi.symm
+      have hsum' :
+          ∑ i, pairVector (x i) (x' i) =
+            ∑ i, pairVector (y i) (y' i) := by
+        simpa only [hx, hy] using hsum
+      obtain ⟨π, σ, hπ, hσ⟩ :=
+        pairVector_sum_eq_permutations x y x' y' hsum'
+      intro i
+      let τ : Equiv.Perm (Fin (n + 1)) := Equiv.swap (finHead n) i
+      let π' : Equiv.Perm (Fin (n + 1)) := τ.trans (π.trans τ)
+      let σ' : Equiv.Perm (Fin (n + 1)) := τ.trans (σ.trans τ)
+      have hconcl := hperm n (fun j ↦ x (τ j)) (fun j ↦ x' (τ j)) π' σ' (by
+        intro j hj
+        have hτj : τ j ≠ i := by
+          intro heq
+          have : j = finHead n := τ.injective (by simpa [τ] using heq)
+          exact hj this
+        have hvR := hR (τ j)
+        rw [hx (τ j), hy (τ j), hR_pair] at hvR
+        have hv := hvR
+        simpa [π', σ', τ, hπ (τ j), hσ (τ j)] using hv)
+      rw [hy i, hx i, hR_pair]
+      simpa [π', σ', τ, hπ i, hσ i] using hconcl
+    obtain ⟨φ, hφ⟩ :=
+      (LinearInequalities.scott_theorem_1_3 hYfinite hYrat).2
+        ⟨hcomplete, hcancel⟩
+    refine ⟨fun x ↦ φ (Pi.single (Sum.inl x) 1),
+      fun x' ↦ φ (Pi.single (Sum.inr x') 1), ?_⟩
+    intro x x' y y'
+    have hxy := hφ (pairVector x x') ⟨(x, x'), rfl⟩
+      (pairVector y y') ⟨(y, y'), rfl⟩
+    rw [hR_pair] at hxy
+    simpa only [pairVector, map_add] using hxy
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/FinHead.lean b/LeanPool/ScottMeasurement/FinHead.lean
new file mode 100644
index 0000000000..5aebc4d9c0
--- /dev/null
+++ b/LeanPool/ScottMeasurement/FinHead.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Data.Fin.Basic
+
+/-!
+# Stable `Fin (n + 1)` head index
+
+Compared Scott permutation/cancellation conditions mention the distinguished
+index `0 : Fin (n + 1)`.  Elaborating that literal attaches a generated
+`._proof_N` to whichever declaration first needs `OfNat`.  Palomar compares
+those generated constants, so Challenge and Solution must share a named
+proof of `0 < n + 1` instead.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+theorem fin_succ_pos (n : ℕ) : 0 < n + 1 :=
+  Nat.succ_pos n
+
+/-- The distinguished index in a nonempty Scott sequence of length `n + 1`. -/
+def finHead (n : ℕ) : Fin (n + 1) :=
+  ⟨0, fin_succ_pos n⟩
+
+theorem finHead_eq_zero (n : ℕ) : finHead n = 0 :=
+  Fin.ext rfl
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Imports.lean b/LeanPool/ScottMeasurement/Imports.lean
new file mode 100644
index 0000000000..ebf867ddd6
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Imports.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.ScottMeasurement
+public import LeanPool.ScottMeasurement.Basic
+public import LeanPool.ScottMeasurement.Differences.Ordered
+public import LeanPool.ScottMeasurement.Differences.Pair
+public import LeanPool.ScottMeasurement.FinHead
+public import LeanPool.ScottMeasurement.LinearInequalities.Definitions
+public import LeanPool.ScottMeasurement.LinearInequalities.OrderedGroup
+public import LeanPool.ScottMeasurement.LinearInequalities.Rationalization
+public import LeanPool.ScottMeasurement.LinearInequalities.ScottTheorems
+public import LeanPool.ScottMeasurement.LinearInequalities.Separation
+public import LeanPool.ScottMeasurement.LinearInequalities.Sequences
+public import LeanPool.ScottMeasurement.Preference.Cycle
+public import LeanPool.ScottMeasurement.Preference.Direct
+public import LeanPool.ScottMeasurement.Preference.Intransitive
+public import LeanPool.ScottMeasurement.Probability.Atoms
+public import LeanPool.ScottMeasurement.Probability.Basic
+public import LeanPool.ScottMeasurement.Probability.Finite
+public import LeanPool.ScottMeasurement.Probability.Infinite.EventSpace
+public import LeanPool.ScottMeasurement.Probability.Infinite.HahnBanach
+public import LeanPool.ScottMeasurement.Probability.Infinite.Kelley
+public import LeanPool.ScottMeasurement.Probability.Infinite.Reconstructed
+public import LeanPool.ScottMeasurement.Probability.KPSCounterexample
diff --git a/LeanPool/ScottMeasurement/LinearInequalities/Definitions.lean b/LeanPool/ScottMeasurement/LinearInequalities/Definitions.lean
new file mode 100644
index 0000000000..bc8e4dfe4d
--- /dev/null
+++ b/LeanPool/ScottMeasurement/LinearInequalities/Definitions.lean
@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Basic.Real.Basic
+public import Mathlib.Analysis.Convex.Hull
+
+/-!
+# Scott's finite systems of linear inequalities
+
+Definitions corresponding to §1 of Scott (1964), pp. 233–237.
+-/
+
+@[expose] public section
+
+open Set
+
+namespace Scott1964.MeasurementStructures.LinearInequalities
+
+variable {L : Type*} [AddCommGroup L] [Module ℝ L]
+
+/-- A set is symmetric when it is closed under negation. -/
+def Symmetric (X : Set L) : Prop := ∀ ⦃x⦄, x ∈ X → -x ∈ X
+
+/-- `N` is realized on `X` by a real linear functional. -/
+def Realizable (X N : Set L) : Prop :=
+  ∃ φ : Module.Dual ℝ L, ∀ x ∈ X, x ∈ N ↔ 0 ≤ φ x
+
+/-- Scott's notation `x ≻ 0`: positive, but its negative is not positive. -/
+def strictPositive (X N : Set L) : Set L :=
+  {x | x ∈ X ∧ x ∈ N ∧ -x ∉ N}
+
+/-- Vectors declared both nonnegative and nonpositive. -/
+def indifferent (X N : Set L) : Set L :=
+  {x | x ∈ X ∧ x ∈ N ∧ -x ∈ N}
+
+/-- Condition (1): every vector has one of the two weak signs. -/
+def SignComplete (X N : Set L) : Prop :=
+  ∀ ⦃x⦄, x ∈ X → x ∈ N ∨ -x ∈ N
+
+/-- Geometric form of Scott's condition (2).
+
+No convex combination of strictly positive vectors belongs to the linear
+span of vectors carrying both weak signs. For finite symmetric systems this
+is equivalent to Scott's positive-coefficient cancellation condition.
+-/
+def WeightedCancellation (X N : Set L) : Prop :=
+  Disjoint (convexHull ℝ (strictPositive X N))
+    (Submodule.span ℝ (indifferent X N) : Set L)
+
+/-- Scott's literal positive-weight finite-sequence condition (2).
+Sequences are indexed by `Fin (n + 1)`, making nonemptiness explicit. -/
+def WeightedSequenceCancellation (X N : Set L) : Prop :=
+  ∀ (n : ℕ) (x : Fin (n + 1) → L) (c : Fin (n + 1) → ℝ),
+    (∀ i, x i ∈ X) → (∀ i, x i ∈ N) → (∀ i, 0 < c i) →
+    ∑ i, c i • x i = 0 → ∀ i, -x i ∈ N
+
+/-- Scott's literal unweighted finite-sequence condition (4). -/
+def UnweightedSequenceCancellation (X N : Set L) : Prop :=
+  ∀ (n : ℕ) (x : Fin (n + 1) → L),
+    (∀ i, x i ∈ X) → (∀ i, x i ∈ N) →
+    ∑ i, x i = 0 → ∀ i, -x i ∈ N
+
+/-- Positive natural-multiplicity version, intermediate between rational
+weights and literal repetition. -/
+def NatWeightedSequenceCancellation (X N : Set L) : Prop :=
+  ∀ (n : ℕ) (x : Fin (n + 1) → L) (k : Fin (n + 1) → ℕ),
+    (∀ i, x i ∈ X) → (∀ i, x i ∈ N) → (∀ i, 0 < k i) →
+    ∑ i, k i • x i = 0 → ∀ i, -x i ∈ N
+
+/-- A vector in `S → ℝ` has rational coordinates. -/
+def IsRationalVector {S : Type*} (x : S → ℝ) : Prop :=
+  ∀ s, ∃ q : ℚ, x s = q
+
+/-- A set consists of rational vectors. -/
+def IsRationalSet {S : Type*} (X : Set (S → ℝ)) : Prop :=
+  ∀ ⦃x⦄, x ∈ X → IsRationalVector x
+
+/-- Realizability of a relation by comparison of functional values. -/
+def RelationRealizable (Y : Set L) (R : L → L → Prop) : Prop :=
+  ∃ φ : Module.Dual ℝ L, ∀ x ∈ Y, ∀ y ∈ Y, R x y ↔ φ y ≤ φ x
+
+/-- Condition (5): completeness on `Y`. -/
+def RelationComplete (Y : Set L) (R : L → L → Prop) : Prop :=
+  ∀ ⦃x⦄, x ∈ Y → ∀ ⦃y⦄, y ∈ Y → R x y ∨ R y x
+
+/-- Strictly positive differences associated to a relation. -/
+def strictDifferences (Y : Set L) (R : L → L → Prop) : Set L :=
+  {z | ∃ x ∈ Y, ∃ y ∈ Y, R x y ∧ ¬R y x ∧ z = x - y}
+
+/-- Indifferent differences associated to a relation. -/
+def indifferentDifferences (Y : Set L) (R : L → L → Prop) : Set L :=
+  {z | ∃ x ∈ Y, ∃ y ∈ Y, R x y ∧ R y x ∧ z = x - y}
+
+/-- Geometric form of Scott's equal-sums cancellation condition (6). -/
+def RelationCancellation (Y : Set L) (R : L → L → Prop) : Prop :=
+  Disjoint (convexHull ℝ (strictDifferences Y R))
+    (Submodule.span ℝ (indifferentDifferences Y R) : Set L)
+
+/-- Scott's literal paired equal-sums condition (6). -/
+def RelationSequenceCancellation (Y : Set L) (R : L → L → Prop) : Prop :=
+  ∀ (n : ℕ) (x y : Fin (n + 1) → L),
+    (∀ i, x i ∈ Y) → (∀ i, y i ∈ Y) → (∀ i, R (x i) (y i)) →
+    ∑ i, x i = ∑ i, y i → ∀ i, R (y i) (x i)
+
+/-- The additive closure `Y⁺` (including the empty sum). -/
+def additiveClosure (Y : Set L) : Set L :=
+  AddSubmonoid.closure Y
+
+/-- Scott's three axioms (i)–(iii) for a strictly monotonic relation. -/
+structure StrictlyMonotonic (Z : Set L) (R : L → L → Prop) : Prop where
+  complete : ∀ ⦃x⦄, x ∈ Z → ∀ ⦃y⦄, y ∈ Z → R x y ∨ R y x
+  add : ∀ ⦃x₀ y₀ x₁ y₁⦄, x₀ ∈ Z → y₀ ∈ Z → x₁ ∈ Z → y₁ ∈ Z →
+    R x₀ y₀ → R x₁ y₁ → R (x₀ + x₁) (y₀ + y₁)
+  cancel : ∀ ⦃x₀ y₀ x₁ y₁⦄, x₀ ∈ Z → y₀ ∈ Z → x₁ ∈ Z → y₁ ∈ Z →
+    x₀ + x₁ = y₀ + y₁ → R x₁ y₁ → R y₀ x₀
+
+/-- `Rplus` extends `R` from `Y` to `Z`. -/
+def ExtendsOn (Y Z : Set L) (R Rplus : L → L → Prop) : Prop :=
+  Y ⊆ Z ∧ ∀ ⦃x⦄, x ∈ Y → ∀ ⦃y⦄, y ∈ Y → (Rplus x y ↔ R x y)
+
+end Scott1964.MeasurementStructures.LinearInequalities
diff --git a/LeanPool/ScottMeasurement/LinearInequalities/OrderedGroup.lean b/LeanPool/ScottMeasurement/LinearInequalities/OrderedGroup.lean
new file mode 100644
index 0000000000..e3ea85e4f5
--- /dev/null
+++ b/LeanPool/ScottMeasurement/LinearInequalities/OrderedGroup.lean
@@ -0,0 +1,327 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.LinearInequalities.ScottTheorems
+public import Mathlib.Algebra.Order.Monoid.Lex
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+open Set
+
+namespace Scott1964.MeasurementStructures.LinearInequalities
+
+section Local
+
+variable {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
+
+private def localBasis {S : Set G} (x : S) : S → ℝ :=
+  Pi.single x 1
+
+private def localPair {S : Set G} (p : S × S) : S → ℝ :=
+  localBasis p.1 + localBasis p.2
+
+private def localTests (S : Set G) : Set (S → ℝ) :=
+  Set.range localBasis ∪ Set.range localPair
+
+private def natCoordinates {S : Set G} (n : S → ℕ) : S → ℝ :=
+  fun i ↦ n i
+
+private def coordinateValue {S : Set G} [Fintype S] (n : S → ℕ) : G :=
+  ∑ i, n i • (i : G)
+
+omit [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] in
+private theorem natCoordinates_injective {S : Set G} :
+    Function.Injective (natCoordinates (S := S)) := by
+  intro m n h
+  funext i
+  exact Nat.cast_injective (congrFun h i)
+
+omit [AddCommGroup G] [IsOrderedAddMonoid G] in
+private theorem localBasis_coordinates {S : Set G} (x : S) :
+    localBasis x = natCoordinates (Pi.single x 1) := by
+  funext i
+  classical
+  by_cases h : i = x
+  · subst i
+    simp [localBasis, natCoordinates]
+  · simp [localBasis, natCoordinates, h]
+
+omit [AddCommGroup G] [IsOrderedAddMonoid G] in
+private theorem localPair_coordinates {S : Set G} (p : S × S) :
+    localPair p =
+      natCoordinates (Pi.single p.1 1 + Pi.single p.2 1) := by
+  rw [localPair, localBasis_coordinates, localBasis_coordinates]
+  funext i
+  simp [natCoordinates]
+
+omit [IsOrderedAddMonoid G] in
+private theorem coordinateValue_single {S : Set G} [Fintype S] (x : S) :
+    coordinateValue (Pi.single x 1) = x := by
+  classical
+  rw [coordinateValue, Finset.sum_eq_single x]
+  · simp
+  · intro b _ hbx
+    simp [hbx]
+  · simp
+
+omit [LinearOrder G] [IsOrderedAddMonoid G] in
+private theorem coordinateValue_add {S : Set G} [Fintype S] (m n : S → ℕ) :
+    coordinateValue (m + n) = coordinateValue m + coordinateValue n := by
+  classical
+  simp only [coordinateValue, Pi.add_apply, add_nsmul, Finset.sum_add_distrib]
+
+omit [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] in
+private theorem natCoordinates_add {S : Set G} (m n : S → ℕ) :
+    natCoordinates m + natCoordinates n = natCoordinates (m + n) := by
+  funext i
+  simp [natCoordinates]
+
+private def coordinateRelation {S : Set G} [Fintype S]
+    (v w : S → ℝ) : Prop :=
+  ∃ m n : S → ℕ,
+    natCoordinates m = v ∧ natCoordinates n = w ∧
+      coordinateValue n ≤ coordinateValue m
+
+omit [IsOrderedAddMonoid G] in
+private theorem coordinateRelation_encode_iff {S : Set G} [Fintype S]
+    (m n : S → ℕ) :
+    coordinateRelation (natCoordinates m) (natCoordinates n) ↔
+      coordinateValue n ≤ coordinateValue m := by
+  constructor
+  · rintro ⟨m', n', hm, hn, hle⟩
+    have hmm : m' = m := natCoordinates_injective hm
+    have hnn : n' = n := natCoordinates_injective hn
+    simpa [hmm, hnn] using hle
+  · intro hle
+    exact ⟨m, n, rfl, rfl, hle⟩
+
+omit [AddCommGroup G] [IsOrderedAddMonoid G] in
+private theorem localTests_finite {S : Set G} [Finite S] :
+    (localTests S).Finite := by
+  let := Fintype.ofFinite S
+  exact (Set.finite_range localBasis).union (Set.finite_range localPair)
+
+omit [AddCommGroup G] [IsOrderedAddMonoid G] in
+private theorem localTests_rational {S : Set G} :
+    IsRationalSet (localTests S) := by
+  rintro v (⟨x, rfl⟩ | ⟨p, rfl⟩) i
+  · classical
+    by_cases h : i = x
+    · subst i
+      exact ⟨1, by simp [localBasis]⟩
+    · exact ⟨0, by simp [localBasis, h]⟩
+  · classical
+    by_cases h₁ : i = p.1 <;> by_cases h₂ : i = p.2
+    · subst i
+      have : p.1 = p.2 := h₂
+      exact ⟨2, by simp [localPair, localBasis, this]; norm_num⟩
+    · subst i
+      exact ⟨1, by simp [localPair, localBasis, h₂]⟩
+    · subst i
+      exact ⟨1, by simp [localPair, localBasis, h₁]⟩
+    · exact ⟨0, by simp [localPair, localBasis, h₁, h₂]⟩
+
+omit [AddCommGroup G] [IsOrderedAddMonoid G] in
+private theorem localTests_closure_coordinates {S : Set G} {v : S → ℝ}
+    (hv : v ∈ additiveClosure (localTests S)) :
+    ∃ n : S → ℕ, natCoordinates n = v := by
+  induction hv using AddSubmonoid.closure_induction with
+  | mem v hv =>
+      rcases hv with ⟨x, rfl⟩ | ⟨p, rfl⟩
+      · exact ⟨Pi.single x 1, localBasis_coordinates x |>.symm⟩
+      · exact ⟨Pi.single p.1 1 + Pi.single p.2 1,
+          localPair_coordinates p |>.symm⟩
+  | zero => exact ⟨fun _ ↦ 0, by funext i; norm_num [natCoordinates]⟩
+  | add v w hv hw ihv ihw =>
+      obtain ⟨m, rfl⟩ := ihv
+      obtain ⟨n, rfl⟩ := ihw
+      exact ⟨m + n, natCoordinates_add m n |>.symm⟩
+
+private theorem coordinateRelation_strictlyMonotonic {S : Set G} [Fintype S] :
+    StrictlyMonotonic (additiveClosure (localTests S))
+      (coordinateRelation (S := S)) := by
+  refine ⟨?_, ?_, ?_⟩
+  · intro v hv w hw
+    obtain ⟨m, rfl⟩ := localTests_closure_coordinates hv
+    obtain ⟨n, rfl⟩ := localTests_closure_coordinates hw
+    exact (le_total (coordinateValue n) (coordinateValue m)).imp
+      (coordinateRelation_encode_iff m n |>.mpr)
+      (coordinateRelation_encode_iff n m |>.mpr)
+  · intro v₀ w₀ v₁ w₁ hv₀ hw₀ hv₁ hw₁ h₀ h₁
+    obtain ⟨m₀, n₀, rfl, rfl, h₀⟩ := h₀
+    obtain ⟨m₁, n₁, hm₁, hn₁, h₁⟩ := h₁
+    subst v₁
+    subst w₁
+    rw [natCoordinates_add m₀ m₁, natCoordinates_add n₀ n₁,
+      coordinateRelation_encode_iff, coordinateValue_add, coordinateValue_add]
+    exact add_le_add h₀ h₁
+  · intro v₀ w₀ v₁ w₁ hv₀ hw₀ hv₁ hw₁ heq h₁
+    obtain ⟨m₀, rfl⟩ := localTests_closure_coordinates hv₀
+    obtain ⟨n₀, rfl⟩ := localTests_closure_coordinates hw₀
+    obtain ⟨m₁, rfl⟩ := localTests_closure_coordinates hv₁
+    obtain ⟨n₁, rfl⟩ := localTests_closure_coordinates hw₁
+    have hmn : m₀ + m₁ = n₀ + n₁ := by
+      apply natCoordinates_injective
+      rw [← natCoordinates_add, ← natCoordinates_add]
+      exact heq
+    have hvalue :
+        coordinateValue m₀ + coordinateValue m₁ =
+          coordinateValue n₀ + coordinateValue n₁ := by
+      rw [← coordinateValue_add, ← coordinateValue_add, hmn]
+    have htail : coordinateValue n₁ ≤ coordinateValue m₁ :=
+      (coordinateRelation_encode_iff m₁ n₁).mp h₁
+    apply (coordinateRelation_encode_iff n₀ m₀).mpr
+    apply (add_le_add_iff_right (coordinateValue m₁)).mp
+    rw [hvalue]
+    simpa [add_comm] using add_le_add_left htail (coordinateValue n₀)
+
+/-- 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. -/
+theorem finite_local_real_embedding (S : Set G) (hS : S.Finite) :
+    ∃ f : S → ℝ,
+      (∀ x y : S, x ≤ y ↔ f x ≤ f y) ∧
+      (∀ x y z : S, (x : G) + y = z → f x + f y = f z) := by
+  let : Fintype S := hS.fintype
+  have hext :
+      ∃ Rplus : (S → ℝ) → (S → ℝ) → Prop,
+        ExtendsOn (localTests S) (additiveClosure (localTests S))
+          (coordinateRelation (S := S)) Rplus ∧
+        StrictlyMonotonic (additiveClosure (localTests S)) Rplus :=
+    ⟨coordinateRelation, ⟨AddSubmonoid.subset_closure, fun _ _ _ _ ↦ Iff.rfl⟩,
+      coordinateRelation_strictlyMonotonic⟩
+  obtain ⟨φ, hφ⟩ :=
+    (scott_theorem_1_4 (localTests_finite (S := S))
+      (localTests_rational (S := S))).mpr hext
+  refine ⟨fun x ↦ φ (localBasis x), ?_, ?_⟩
+  · intro x y
+    have hx : localBasis x ∈ localTests S := Or.inl ⟨x, rfl⟩
+    have hy : localBasis y ∈ localTests S := Or.inl ⟨y, rfl⟩
+    rw [← hφ (localBasis y) hy (localBasis x) hx]
+    rw [localBasis_coordinates, localBasis_coordinates,
+      coordinateRelation_encode_iff, coordinateValue_single,
+      coordinateValue_single]
+    rfl
+  · intro x y z hxy
+    have hp : localPair (x, y) ∈ localTests S := Or.inr ⟨(x, y), rfl⟩
+    have hz : localBasis z ∈ localTests S := Or.inl ⟨z, rfl⟩
+    have hpz : coordinateRelation (localPair (x, y)) (localBasis z) := by
+      rw [localPair_coordinates, localBasis_coordinates,
+        coordinateRelation_encode_iff, coordinateValue_add,
+        coordinateValue_single, coordinateValue_single, coordinateValue_single,
+        hxy]
+    have hzp : coordinateRelation (localBasis z) (localPair (x, y)) := by
+      rw [localPair_coordinates, localBasis_coordinates,
+        coordinateRelation_encode_iff, coordinateValue_add,
+        coordinateValue_single, coordinateValue_single, coordinateValue_single,
+        hxy]
+    have hle := (hφ (localPair (x, y)) hp (localBasis z) hz).mp hpz
+    have hge := (hφ (localBasis z) hz (localPair (x, y)) hp).mp hzp
+    simpa [localPair, map_add] using le_antisymm hge hle
+
+end Local
+
+section Lexicographic
+
+/-- The ordered abelian group used to obstruct a global real representation. -/
+abbrev LexIntPair := ℤ ×ₗ ℤ
+
+/-- The two positive coordinate generators of the lexicographic example. -/
+def lexGenerators : Set LexIntPair :=
+  {toLex (1, 0), toLex (0, 1)}
+
+/-- Comparison oriented as preference, with the first coordinate taking priority. -/
+def lexPreference (x y : LexIntPair) : Prop :=
+  (ofLex y).1 < (ofLex x).1 ∨
+    (ofLex y).1 = (ofLex x).1 ∧ (ofLex y).2 ≤ (ofLex x).2
+
+theorem lexPreference_strictlyMonotonic :
+    StrictlyMonotonic (additiveClosure lexGenerators) lexPreference := by
+  refine ⟨?_, ?_, ?_⟩
+  · intro x hx y hy
+    rcases x with ⟨x₁, x₂⟩
+    rcases y with ⟨y₁, y₂⟩
+    simp only [lexPreference, ofLex]
+    omega
+  · intro x₀ y₀ x₁ y₁ _ _ _ _ h₀ h₁
+    rcases x₀ with ⟨x₀₁, x₀₂⟩
+    rcases y₀ with ⟨y₀₁, y₀₂⟩
+    rcases x₁ with ⟨x₁₁, x₁₂⟩
+    rcases y₁ with ⟨y₁₁, y₁₂⟩
+    change y₀₁ < x₀₁ ∨ y₀₁ = x₀₁ ∧ y₀₂ ≤ x₀₂ at h₀
+    change y₁₁ < x₁₁ ∨ y₁₁ = x₁₁ ∧ y₁₂ ≤ x₁₂ at h₁
+    change y₀₁ + y₁₁ < x₀₁ + x₁₁ ∨
+      y₀₁ + y₁₁ = x₀₁ + x₁₁ ∧ y₀₂ + y₁₂ ≤ x₀₂ + x₁₂
+    omega
+  · intro x₀ y₀ x₁ y₁ _ _ _ _ heq h₁
+    rcases x₀ with ⟨x₀₁, x₀₂⟩
+    rcases y₀ with ⟨y₀₁, y₀₂⟩
+    rcases x₁ with ⟨x₁₁, x₁₂⟩
+    rcases y₁ with ⟨y₁₁, y₁₂⟩
+    change y₁₁ < x₁₁ ∨ y₁₁ = x₁₁ ∧ y₁₂ ≤ x₁₂ at h₁
+    change x₀₁ < y₀₁ ∨ x₀₁ = y₀₁ ∧ x₀₂ ≤ y₀₂
+    change (x₀₁ + x₁₁, x₀₂ + x₁₂) =
+      (y₀₁ + y₁₁, y₀₂ + y₁₂) at heq
+    have hfirst := congrArg Prod.fst heq
+    have hsecond := congrArg Prod.snd heq
+    simp only at hfirst hsecond
+    omega
+
+/-- 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)`. -/
+theorem no_global_real_additive_lex_realization :
+    ¬ ∃ f : LexIntPair →+ ℝ,
+      ∀ x y, lexPreference x y ↔ f y ≤ f x := by
+  rintro ⟨f, hf⟩
+  let e₁ : LexIntPair := toLex (1, 0)
+  let e₂ : LexIntPair := toLex (0, 1)
+  have he₂pos : 0 < f e₂ := by
+    have hstrict : lexPreference e₂ 0 ∧ ¬lexPreference 0 e₂ := by
+      constructor
+      · right
+        norm_num [lexPreference, e₂]
+      · intro h
+        rcases h with h | h <;> norm_num [lexPreference, e₂] at h
+    have hnonneg := (hf e₂ 0).mp hstrict.1
+    have hne : f e₂ ≠ 0 := by
+      intro hzero
+      apply hstrict.2
+      apply (hf 0 e₂).mpr
+      simp [hzero]
+    have hnonneg' : 0 ≤ f e₂ := by simpa using hnonneg
+    exact lt_of_le_of_ne hnonneg' (Ne.symm hne)
+  obtain ⟨n, hn⟩ := exists_nat_gt (f e₁ / f e₂)
+  have hlex : lexPreference e₁ (n • e₂) := by
+    left
+    change (0 : ℤ) < 1
+    norm_num
+  have hbound := (hf e₁ (n • e₂)).mp hlex
+  simp only [map_nsmul] at hbound
+  have hlarge : f e₁ < n * f e₂ := by
+    have := (mul_lt_mul_of_pos_right hn he₂pos)
+    field_simp at this
+    simpa [mul_comm] using this
+  exact (not_lt_of_ge hbound) (by simpa [nsmul_eq_mul] using hlarge)
+
+end Lexicographic
+
+end Scott1964.MeasurementStructures.LinearInequalities
diff --git a/LeanPool/ScottMeasurement/LinearInequalities/Rationalization.lean b/LeanPool/ScottMeasurement/LinearInequalities/Rationalization.lean
new file mode 100644
index 0000000000..d9f6e9e3cc
--- /dev/null
+++ b/LeanPool/ScottMeasurement/LinearInequalities/Rationalization.lean
@@ -0,0 +1,250 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.LinearInequalities.Definitions
+public import Mathlib.Algebra.Algebra.Rat
+public import Mathlib.LinearAlgebra.TensorProduct.Pi
+public import Mathlib.RingTheory.Flat.Basic
+public import Mathlib.LinearAlgebra.Basis.VectorSpace
+public import Mathlib.Topology.Algebra.Ring.Real
+public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
+public import Mathlib.Topology.Algebra.Order.Archimedean
+
+/-!
+# Rational vectors
+
+Elementary closure facts used in Scott's reduction from relations to
+inequalities on the rational difference set `Y - Y`.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures.LinearInequalities
+
+variable {S : Type*}
+
+open scoped TensorProduct
+
+theorem isRationalVector_zero : IsRationalVector (0 : S → ℝ) := by
+  intro s
+  exact ⟨0, by simp⟩
+
+theorem IsRationalVector.neg {x : S → ℝ} (hx : IsRationalVector x) :
+    IsRationalVector (-x) := by
+  intro s
+  obtain ⟨q, hq⟩ := hx s
+  exact ⟨-q, by simp [hq]⟩
+
+theorem IsRationalVector.sub {x y : S → ℝ}
+    (hx : IsRationalVector x) (hy : IsRationalVector y) :
+    IsRationalVector (x - y) := by
+  intro s
+  obtain ⟨q, hq⟩ := hx s
+  obtain ⟨r, hr⟩ := hy s
+  exact ⟨q - r, by simp [hq, hr]⟩
+
+theorem rational_difference_set {Y : Set (S → ℝ)} (hY : IsRationalSet Y) :
+    IsRationalSet {z | ∃ x ∈ Y, ∃ y ∈ Y, z = x - y} := by
+  rintro z ⟨x, hx, y, hy, rfl⟩
+  exact (hY hx).sub (hY hy)
+
+section PositiveKernel
+
+variable {I : Type*} [Fintype I]
+  [Finite S]
+
+/-- A strictly positive real relation between finitely many rational vectors
+can be replaced by a strictly positive rational relation.
+
+This is the scalar-extension step in Scott's proof of Theorem 1.2.  Exactness
+of tensoring the rational kernel with `ℝ` writes the given real relation as a
+finite real linear combination of rational kernel vectors.  Density of a
+finite product of copies of `ℚ` then preserves all strict coordinate
+inequalities. -/
+theorem exists_pos_rational_relation (x : I → S → ℝ)
+    (hx : ∀ i, IsRationalVector (x i)) (c : I → ℝ)
+    (hc : ∀ i, 0 < c i) (hsum : ∑ i, c i • x i = 0) :
+    ∃ q : I → ℚ, (∀ i, 0 < q i) ∧ ∑ i, (q i : ℝ) • x i = 0 := by
+  let := Fintype.ofFinite S
+  classical
+  choose a ha using fun i s ↦ hx i s
+  let f : (I → ℚ) →ₗ[ℚ] (S → ℚ) :=
+    { toFun := fun d s ↦ ∑ i, d i * a i s
+      map_add' := by
+        intro d e
+        ext s
+        simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
+      map_smul' := by
+        intro r d
+        ext s
+        simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, mul_assoc, Finset.mul_sum] }
+  let eI := TensorProduct.piScalarRight ℚ ℝ ℝ I
+  let eS := TensorProduct.piScalarRight ℚ ℝ ℝ S
+  have hc_repr : eI.symm c = ∑ i, c i ⊗ₜ[ℚ] Pi.single i 1 := by
+    apply eI.injective
+    ext i
+    simp [eI, Pi.single_apply]
+  have hbase : f.baseChange ℝ (eI.symm c) = 0 := by
+    rw [hc_repr]
+    apply eS.injective
+    ext s
+    have hs := congrFun hsum s
+    simpa [eS, f, Pi.single_apply, ha, Algebra.smul_def, smul_eq_mul, mul_comm] using hs
+  have hexact :=
+    Module.Flat.lTensor_exact ℝ (LinearMap.exact_subtype_ker_map f)
+  rw [← LinearMap.baseChange_eq_ltensor] at hexact
+  obtain ⟨t, ht⟩ := (hexact (eI.symm c)).mp hbase
+  obtain ⟨k, r, v, rfl⟩ := TensorProduct.exists_sum_tmul_eq t
+  let U : Set (Fin k → ℝ) :=
+    {d | ∀ i, 0 < ∑ j, d j * ((v j : I → ℚ) i : ℝ)}
+  have hrU : r ∈ U := by
+    intro i
+    have htc := congrArg eI ht
+    have hi := congrFun htc i
+    have hi' : ∑ j, r j * ((v j : I → ℚ) i : ℝ) = c i := by
+      simpa [eI, Algebra.smul_def, smul_eq_mul, mul_comm] using hi
+    rw [hi']
+    exact hc i
+  have hUopen : IsOpen U := by
+    rw [show U = ⋂ i, {d | (0 : ℝ) < ∑ j, d j * ((v j : I → ℚ) i : ℝ)} by
+      ext d
+      simp [U]]
+    apply isOpen_iInter_of_finite
+    intro i
+    apply isOpen_lt continuous_const
+    fun_prop
+  have hdense : DenseRange (Pi.map fun _ : Fin k ↦ ((↑) : ℚ → ℝ)) :=
+    DenseRange.piMap fun _ ↦ Rat.denseRange_cast
+  obtain ⟨q, hqU⟩ := hdense.exists_mem_open hUopen ⟨r, hrU⟩
+  let w : I → ℚ := fun i ↦ ∑ j, q j * (v j : I → ℚ) i
+  refine ⟨w, ?_, ?_⟩
+  · intro i
+    have hi : (0 : ℝ) < ∑ j, (q j : ℝ) * ((v j : I → ℚ) i : ℝ) := by
+      simpa using hqU i
+    have hcast : (w i : ℝ) = ∑ j, (q j : ℝ) * ((v j : I → ℚ) i : ℝ) := by
+      simp [w]
+    rw [← hcast] at hi
+    exact_mod_cast hi
+  · have hv : ∀ j, f (v j : I → ℚ) = 0 :=
+      fun j ↦ LinearMap.mem_ker.mp (v j).property
+    ext s
+    have hwzero : ∑ i, w i * a i s = 0 := by
+      simp_rw [w, Finset.sum_mul]
+      rw [Finset.sum_comm, Finset.sum_eq_zero]
+      intro j hj
+      have hfj := congrFun (hv j) s
+      change (∑ i, (v j : I → ℚ) i * a i s) = 0 at hfj
+      calc
+        ∑ i, q j * (v j : I → ℚ) i * a i s =
+            q j * ∑ i, (v j : I → ℚ) i * a i s := by
+              rw [Finset.mul_sum]
+              apply Finset.sum_congr rfl
+              intro i hi
+              ring
+        _ = 0 := by rw [hfj, mul_zero]
+    have hwzeroR := congrArg ((↑) : ℚ → ℝ) hwzero
+    simpa only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Pi.zero_apply,
+      Rat.cast_sum, Rat.cast_mul, Rat.cast_zero, ha] using hwzeroR
+
+end PositiveKernel
+
+section Repetition
+
+variable {L : Type*} [AddCommGroup L]
+
+/-- Clearing to positive natural coefficients can be discharged by literal
+repetition of each vector. -/
+theorem UnweightedSequenceCancellation.natWeighted {X N : Set L}
+    (h : UnweightedSequenceCancellation X N) :
+    NatWeightedSequenceCancellation X N := by
+  intro n x k hx hN hk hsum
+  let I := Σ i : Fin (n + 1), Fin (k i)
+  let i0 : I := ⟨0, ⟨0, hk 0⟩⟩
+  have hI : 0 < Fintype.card I := Fintype.card_pos_iff.mpr ⟨i0⟩
+  let m := Fintype.card I - 1
+  have hcard : Fintype.card I = m + 1 := by
+    dsimp [m]
+    omega
+  let e : Fin (m + 1) ≃ I :=
+    Fintype.equivOfCardEq (by simpa using hcard.symm)
+  let z : Fin (m + 1) → L := fun j ↦ x (e j).1
+  have hzsum : ∑ j, z j = 0 := by
+    rw [← hsum]
+    change ∑ j, x (e j).1 = ∑ i, k i • x i
+    calc
+      ∑ j, x (e j).1 = ∑ a : I, x a.1 := e.sum_comp (fun a ↦ x a.1)
+      _ = ∑ i, ∑ _j : Fin (k i), x i := Fintype.sum_sigma (fun a : I ↦ x a.1)
+      _ = ∑ i, k i • x i := by simp
+  have hz := h m z (fun j ↦ hx (e j).1) (fun j ↦ hN (e j).1) hzsum
+  intro i
+  let a : I := ⟨i, ⟨0, hk i⟩⟩
+  simpa [z, a] using hz (e.symm a)
+
+end Repetition
+
+section RationalRepetition
+
+variable {S : Type*} [Finite S]
+
+/-- On rational coordinate vectors, Scott's unit-weight cancellation
+condition implies his arbitrary positive-real-weight condition. -/
+theorem UnweightedSequenceCancellation.rationalWeighted
+    {X N : Set (S → ℝ)} (h : UnweightedSequenceCancellation X N)
+    (hX : IsRationalSet X) : WeightedSequenceCancellation X N := by
+  let := Fintype.ofFinite S
+  intro n x c hx hN hc hsum
+  classical
+  obtain ⟨q, hq, hqsum⟩ :=
+    exists_pos_rational_relation x (fun i ↦ hX (hx i)) c hc hsum
+  let D : ℕ := ∏ i, (q i).den
+  have hden : ∀ i, (q i).den ∣ D := by
+    intro i
+    exact Finset.dvd_prod_of_mem (fun j ↦ (q j).den) (Finset.mem_univ i)
+  choose d hd using hden
+  let k : Fin (n + 1) → ℕ := fun i ↦ (q i).num.natAbs * d i
+  have hnum : ∀ i, 0 < (q i).num := fun i ↦ Rat.num_pos.mpr (hq i)
+  have hk : ∀ i, 0 < k i := by
+    intro i
+    have hD : 0 < D := Finset.prod_pos fun i _ ↦ (q i).den_pos
+    have hdpos : 0 < d i := by
+      have := hd i
+      nlinarith [(q i).den_pos]
+    exact Nat.mul_pos (Int.natAbs_pos.mpr (hnum i).ne') hdpos
+  have hkq : ∀ i, (k i : ℚ) = (D : ℚ) * q i := by
+    intro i
+    have hnumcast : ((q i).num.natAbs : ℤ) = (q i).num :=
+      Int.natAbs_of_nonneg (hnum i).le
+    rw [← (q i).num_div_den]
+    have hnumq : (0 : ℚ) < (q i).num := by exact_mod_cast hnum i
+    norm_num [k, hd i, hnumcast, abs_of_pos hnumq]
+    field_simp
+  have hksum : ∑ i, k i • x i = 0 := by
+    calc
+      ∑ i, k i • x i = ∑ i, (k i : ℝ) • x i := by
+        apply Finset.sum_congr rfl
+        intro i hi
+        exact (Nat.cast_smul_eq_nsmul ℝ (k i) (x i)).symm
+      _ = ∑ i, ((D : ℚ) * q i : ℚ) • x i := by
+        apply Finset.sum_congr rfl
+        intro i hi
+        rw [← hkq i]
+        rfl
+      _ = (D : ℝ) • ∑ i, (q i : ℝ) • x i := by
+        ext s
+        simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+        rw [Finset.mul_sum]
+        apply Finset.sum_congr rfl
+        intro i hi
+        simp [Algebra.smul_def]
+        ring
+      _ = 0 := by rw [hqsum, smul_zero]
+  exact h.natWeighted n x k hx hN hk hksum
+
+end RationalRepetition
+
+end Scott1964.MeasurementStructures.LinearInequalities
diff --git a/LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean b/LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean
new file mode 100644
index 0000000000..f0b08be2f2
--- /dev/null
+++ b/LeanPool/ScottMeasurement/LinearInequalities/ScottTheorems.lean
@@ -0,0 +1,421 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.LinearInequalities.Separation
+public import LeanPool.ScottMeasurement.LinearInequalities.Rationalization
+public import LeanPool.ScottMeasurement.LinearInequalities.Sequences
+
+/-!
+# Scott 1964, Theorems 1.1–1.4
+
+Finite convex-separation forms of the general method in §1.
+-/
+
+@[expose] public section
+
+open Set
+
+namespace Scott1964.MeasurementStructures.LinearInequalities
+
+section Algebraic
+
+variable {L : Type*} [AddCommGroup L] [Module ℝ L]
+
+/-- The sequence formulation may be used with any nonempty finite index type. -/
+theorem WeightedSequenceCancellation.fintype {X N : Set L}
+    (h : WeightedSequenceCancellation X N) {I : Type*} [Fintype I] [Nonempty I]
+    (x : I → L) (c : I → ℝ) (hx : ∀ i, x i ∈ X)
+    (hN : ∀ i, x i ∈ N) (hc : ∀ i, 0 < c i)
+    (hsum : ∑ i, c i • x i = 0) : ∀ i, -x i ∈ N := by
+  let n := Fintype.card I - 1
+  have hcard : Fintype.card I = n + 1 := by
+    dsimp [n]
+    have := Fintype.card_pos (α := I)
+    omega
+  let e : Fin (n + 1) ≃ I :=
+    Fintype.equivOfCardEq (by simpa using hcard.symm)
+  have he := h n (x ∘ e) (c ∘ e) (fun i ↦ hx (e i))
+    (fun i ↦ hN (e i)) (fun i ↦ hc (e i))
+    (by
+      rw [← hsum]
+      exact e.sum_comp (fun i ↦ c i • x i))
+  intro i
+  simpa using he (e.symm i)
+
+/-- Scott's positive-weight sequence condition is
+equivalent to the geometric cancellation condition. -/
+theorem weightedCancellation_of_sequence {X N : Set L}
+    (hsym : Symmetric X)
+    (hseq : WeightedSequenceCancellation X N) :
+    WeightedCancellation X N := by
+  rw [WeightedCancellation, Set.disjoint_left]
+  intro z hzconv hzspan
+  obtain ⟨ι, instι, w, a, hw, hwone, ha, hwa⟩ :=
+    mem_convexHull_iff_exists_fintype.mp hzconv
+  obtain ⟨d, t, ht, hdsupp, hdt⟩ :=
+    Submodule.mem_span_iff_exists_finset_subset.mp hzspan
+  let I₁ := {i : ι // w i ≠ 0}
+  let I₂ := {y : ↥t // d y ≠ 0}
+  let I := I₁ ⊕ I₂
+  let v : I → L
+    | Sum.inl i => a i
+    | Sum.inr y => if 0 < d y.1.1 then -y.1.1 else y.1.1
+  let c : I → ℝ
+    | Sum.inl i => w i
+    | Sum.inr y => |d y.1.1|
+  have hI : Nonempty I := by
+    have hwne : ∃ i, w i ≠ 0 := by
+      by_contra h
+      push Not at h
+      simp [h] at hwone
+    exact ⟨Sum.inl ⟨hwne.choose, hwne.choose_spec⟩⟩
+  let : Nonempty I := hI
+  have hvX : ∀ i, v i ∈ X := by
+    rintro (i | y)
+    · exact (ha i).1
+    · rcases ht y.1.2 with ⟨hyX, hyN, hnyN⟩
+      dsimp [v]
+      split_ifs
+      · exact hsym hyX
+      · exact hyX
+  have hvN : ∀ i, v i ∈ N := by
+    rintro (i | y)
+    · exact (ha i).2.1
+    · rcases ht y.1.2 with ⟨hyX, hyN, hnyN⟩
+      dsimp [v]
+      split_ifs
+      · exact hnyN
+      · exact hyN
+  have hc : ∀ i, 0 < c i := by
+    rintro (i | y)
+    · exact lt_of_le_of_ne (hw i) i.property.symm
+    · exact abs_pos.mpr y.property
+  have hsum : ∑ i, c i • v i = 0 := by
+    rw [Fintype.sum_sum_type]
+    have hleft : ∑ i : I₁, c (.inl i) • v (.inl i) = z := by
+      rw [← hwa]
+      rw [show (∑ i : I₁, c (.inl i) • v (.inl i)) =
+          (∑ i ∈ Finset.univ.filter (fun i ↦ w i ≠ 0), w i • a i) by
+        simpa [I₁, c, v] using
+          (Finset.sum_subtype (Finset.univ.filter fun i ↦ w i ≠ 0)
+            (by simp) (fun i ↦ w i • a i)).symm]
+      exact Finset.sum_filter_of_ne fun i hi hterm hwi ↦
+        hterm (by simp [hwi])
+    have hright : ∑ y : I₂, c (.inr y) • v (.inr y) = -z := by
+      rw [← hdt]
+      have hsub :
+          ∑ y : I₂, c (.inr y) • v (.inr y) =
+            -∑ y ∈ t, d y • y := by
+        rw [← Finset.sum_neg_distrib]
+        rw [show (∑ y : I₂, c (.inr y) • v (.inr y)) =
+            (∑ y : {y : ↥t // d y.1 ≠ 0}, -(d y.1.1 • y.1.1)) by
+          apply Finset.sum_congr rfl
+          intro y hy
+          dsimp [I₂, c, v]
+          split_ifs with hdy
+          · rw [abs_of_pos hdy, smul_neg]
+          · have hdyneg : d y.1.1 < 0 := lt_of_le_of_ne (le_of_not_gt hdy) y.2
+            rw [abs_of_neg hdyneg, neg_smul]]
+        calc
+          ∑ y : {y : ↥t // d y.1 ≠ 0}, -(d y.1.1 • y.1.1) =
+              ∑ y ∈ Finset.univ.filter (fun y : ↥t ↦ d y.1 ≠ 0),
+                -(d y.1 • y.1) := by
+                  exact (Finset.sum_subtype
+                    (Finset.univ.filter fun y : ↥t ↦ d y.1 ≠ 0)
+                    (by simp) (fun y : ↥t ↦ -(d y.1 • y.1))).symm
+          _ = ∑ y : ↥t, -(d y.1 • y.1) := by
+                exact Finset.sum_filter_of_ne fun y hy hterm hdy ↦
+                  hterm (by simp [hdy])
+          _ = ∑ y ∈ t, -(d y • y) := by
+                change (t.attach.sum fun y ↦ -(d y.1 • y.1)) = _
+                exact Finset.sum_attach t (fun y ↦ -(d y • y))
+      exact hsub
+    rw [hleft, hright]
+    exact add_neg_cancel z
+  have hall := hseq.fintype v c hvX hvN hc hsum
+  obtain ⟨i, hi⟩ : ∃ i, w i ≠ 0 := by
+    by_contra h
+    push Not at h
+    simp [h] at hwone
+  have hnot := (ha i).2.2
+  exact hnot (by
+    simpa [v] using hall (Sum.inl (show I₁ from ⟨i, hi⟩)))
+
+/-- A realizing functional supplies Scott's strictly monotonic extension to
+the additive closure. This is the forward half of Theorem 1.4. -/
+theorem scott_theorem_1_4_forward {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 := by
+  obtain ⟨φ, hφ⟩ := hreal
+  let Rplus : L → L → Prop := fun x y ↦ φ y ≤ φ x
+  refine ⟨Rplus, ⟨AddSubmonoid.subset_closure, ?_⟩, ?_⟩
+  · intro x hx y hy
+    exact (hφ x hx y hy).symm
+  · refine ⟨?_, ?_, ?_⟩
+    · intro x hx y hy
+      exact le_total (φ y) (φ x)
+    · intro x₀ y₀ x₁ y₁ hx₀ hy₀ hx₁ hy₁ h₀ h₁
+      dsimp [Rplus] at h₀ h₁ ⊢
+      simp only [map_add]
+      linarith
+    · intro x₀ y₀ x₁ y₁ hx₀ hy₀ hx₁ hy₁ heq h₁
+      dsimp [Rplus] at h₁ ⊢
+      have hsum : φ x₀ + φ x₁ = φ y₀ + φ y₁ := by
+        simpa only [map_add] using congrArg φ heq
+      linarith
+
+end Algebraic
+
+section Additive
+
+variable {L : Type*} [AddCommGroup L]
+
+/-- A strictly monotonic extension implies Scott's literal condition (6). -/
+theorem StrictlyMonotonic.relationSequenceCancellation
+    {Y : Set L} {R Rplus : L → L → Prop}
+    (hext : ExtendsOn Y (additiveClosure Y) R Rplus)
+    (hmono : StrictlyMonotonic (additiveClosure Y) Rplus) :
+    RelationSequenceCancellation Y R := by
+  intro n x y hx hy hR hsum
+  have hsumRel :
+      ∀ s : Finset (Fin (n + 1)),
+        Rplus (∑ i ∈ s, x i) (∑ i ∈ s, y i) := by
+    intro s
+    classical
+    induction s using Finset.induction_on with
+    | empty =>
+        simpa using (hmono.complete
+          (show (0 : L) ∈ additiveClosure Y from AddSubmonoid.zero_mem _)
+          (show (0 : L) ∈ additiveClosure Y from AddSubmonoid.zero_mem _)).elim id id
+    | @insert i s hi ih =>
+        rw [Finset.sum_insert hi, Finset.sum_insert hi]
+        apply hmono.add (hext.1 (hx i)) (hext.1 (hy i))
+          (AddSubmonoid.sum_mem _ fun j hj ↦ hext.1 (hx j))
+          (AddSubmonoid.sum_mem _ fun j hj ↦ hext.1 (hy j))
+          ((hext.2 (hx i) (hy i)).mpr (hR i)) ih
+  intro j
+  let t : Finset (Fin (n + 1)) := Finset.univ.erase j
+  have htail := hsumRel t
+  apply (hext.2 (hy j) (hx j)).mp
+  apply hmono.cancel (hext.1 (hx j)) (hext.1 (hy j))
+    (AddSubmonoid.sum_mem _ fun i hi ↦ hext.1 (hx i))
+    (AddSubmonoid.sum_mem _ fun i hi ↦ hext.1 (hy i))
+    ?_ htail
+  have hxsplit : x j + ∑ i ∈ t, x i = ∑ i, x i := by
+    rw [add_comm, ← Finset.sum_erase_add _ _ (Finset.mem_univ j)]
+  have hysplit : y j + ∑ i ∈ t, y i = ∑ i, y i := by
+    rw [add_comm, ← Finset.sum_erase_add _ _ (Finset.mem_univ j)]
+  rw [hxsplit, hysplit, hsum]
+
+end Additive
+
+variable {L : Type*} [NormedAddCommGroup L] [NormedSpace ℝ L]
+  [FiniteDimensional ℝ L]
+
+/-- Scott (1964), Theorem 1.1. -/
+theorem scott_theorem_1_1 {X N : Set L} (hX : X.Finite) (hsym : Symmetric X) :
+    Realizable X N ↔ SignComplete X N ∧ WeightedSequenceCancellation X N := by
+  constructor
+  · rintro ⟨φ, hφ⟩
+    refine ⟨?_, ?_⟩
+    · intro x hx
+      by_cases h : 0 ≤ φ x
+      · exact Or.inl ((hφ x hx).mpr h)
+      · right
+        have hnx := hsym hx
+        apply (hφ (-x) hnx).mpr
+        simpa using le_of_not_ge h
+    · exact Realizable.weightedSequenceCancellation ⟨φ, hφ⟩ hsym
+  · rintro ⟨htotal, hseq⟩
+    have hcancel := weightedCancellation_of_sequence hsym hseq
+    obtain ⟨φ, hstrict, hneutral⟩ :=
+      (finite_strict_separation
+        (hX.subset fun _ hx ↦ hx.1)).mp hcancel
+    refine ⟨φ, fun x hx ↦ ?_⟩
+    constructor
+    · intro hN
+      by_cases hnN : -x ∈ N
+      · exact le_of_eq (hneutral x ⟨hx, hN, hnN⟩).symm
+      · exact (hstrict x ⟨hx, hN, hnN⟩).le
+    · intro hφ
+      rcases htotal hx with hN | hnN
+      · exact hN
+      · by_contra hxN
+        have hneg := hstrict (-x) ⟨hsym hx, hnN, by simpa using hxN⟩
+        simp only [map_neg] at hneg
+        linarith
+
+/-- 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 scott_theorem_1_2 {S : Type*} [Finite S] {X N : Set (S → ℝ)}
+    (hX : X.Finite) (hrat : IsRationalSet X) (hsym : Symmetric X) :
+    Realizable X N ↔ SignComplete X N ∧ UnweightedSequenceCancellation X N := by
+  let := Fintype.ofFinite S
+  constructor
+  · intro hreal
+    have h := (scott_theorem_1_1 hX hsym).mp hreal
+    exact ⟨h.1, h.2.unweighted⟩
+  · rintro ⟨hcomplete, hunweighted⟩
+    apply (scott_theorem_1_1 hX hsym).mpr
+    exact ⟨hcomplete, hunweighted.rationalWeighted hrat⟩
+
+/-- Geometric intermediate form used in the proof of Theorem 1.3. -/
+theorem scott_theorem_1_3_geometric {Y : Set L} {R : L → L → Prop} (hY : Y.Finite) :
+    RelationRealizable Y R ↔ RelationComplete Y R ∧ RelationCancellation Y R := by
+  constructor
+  · rintro ⟨φ, hφ⟩
+    refine ⟨?_, ?_⟩
+    · intro x hx y hy
+      exact le_total (φ y) (φ x) |>.imp (fun h ↦ (hφ x hx y hy).mpr h)
+        (fun h ↦ (hφ y hy x hx).mpr h)
+    · have hstrictFinite : (strictDifferences Y R).Finite := by
+        apply ((hY.prod hY).image fun p : L × L ↦ p.1 - p.2).subset
+        rintro z ⟨x, hx, y, hy, -, -, rfl⟩
+        exact ⟨⟨x, y⟩, ⟨hx, hy⟩, rfl⟩
+      apply (finite_strict_separation hstrictFinite).mpr
+      refine ⟨φ, ?_, ?_⟩
+      · rintro z ⟨x, hx, y, hy, hxy, hyx, rfl⟩
+        have hle := (hφ x hx y hy).mp hxy
+        have hnle : ¬φ x ≤ φ y := by
+          intro h
+          exact hyx ((hφ y hy x hx).mpr h)
+        simp only [map_sub]
+        linarith
+      · rintro z ⟨x, hx, y, hy, hxy, hyx, rfl⟩
+        have h₁ := (hφ x hx y hy).mp hxy
+        have h₂ := (hφ y hy x hx).mp hyx
+        simp only [map_sub]
+        linarith
+  · rintro ⟨hcomplete, hcancel⟩
+    have hstrictFinite : (strictDifferences Y R).Finite := by
+      apply ((hY.prod hY).image fun p : L × L ↦ p.1 - p.2).subset
+      rintro z ⟨x, hx, y, hy, -, -, rfl⟩
+      exact ⟨⟨x, y⟩, ⟨hx, hy⟩, rfl⟩
+    obtain ⟨φ, hstrict, hneutral⟩ :=
+      (finite_strict_separation hstrictFinite).mp hcancel
+    refine ⟨φ, fun x hx y hy ↦ ?_⟩
+    constructor
+    · intro hxy
+      by_cases hyx : R y x
+      · have hz := hneutral (x - y) ⟨x, hx, y, hy, hxy, hyx, rfl⟩
+        have heq : φ x = φ y := by
+          simp only [map_sub] at hz
+          linarith
+        exact heq.ge
+      · have hz := hstrict (x - y) ⟨x, hx, y, hy, hxy, hyx, rfl⟩
+        simpa [map_sub, sub_pos] using hz.le
+    · intro hle
+      rcases hcomplete hx hy with hxy | hyx
+      · exact hxy
+      · by_contra hnxy
+        have hz := hstrict (y - x) ⟨y, hy, x, hx, hyx, hnxy, rfl⟩
+        simp only [map_sub, sub_pos] at hz
+        linarith
+
+/-- Scott (1964), Theorem 1.3, with the literal paired equal-sums
+cancellation condition (6). -/
+theorem scott_theorem_1_3 {S : Type*} [Finite S]
+    {Y : Set (S → ℝ)} {R : (S → ℝ) → (S → ℝ) → Prop}
+    (hY : Y.Finite) (hYrat : IsRationalSet Y) :
+    RelationRealizable Y R ↔
+      RelationComplete Y R ∧ RelationSequenceCancellation Y R := by
+  let := Fintype.ofFinite S
+  constructor
+  · intro hreal
+    obtain ⟨φ, hφ⟩ := hreal
+    refine ⟨?_, RelationRealizable.sequenceCancellation ⟨φ, hφ⟩⟩
+    intro x hx y hy
+    exact le_total (φ y) (φ x) |>.imp
+      (fun h ↦ (hφ x hx y hy).mpr h) (fun h ↦ (hφ y hy x hx).mpr h)
+  · rintro ⟨hcomplete, hcancel⟩
+    let X : Set (S → ℝ) := {z | ∃ x ∈ Y, ∃ y ∈ Y, z = x - y}
+    let N : Set (S → ℝ) := {z | ∃ x ∈ Y, ∃ y ∈ Y, R x y ∧ z = x - y}
+    have hXfinite : X.Finite := by
+      apply ((hY.prod hY).image fun p : (S → ℝ) × (S → ℝ) ↦ p.1 - p.2).subset
+      rintro z ⟨x, hx, y, hy, rfl⟩
+      exact ⟨(x, y), ⟨hx, hy⟩, rfl⟩
+    have hXrat : IsRationalSet X := rational_difference_set hYrat
+    have hXsym : Symmetric X := by
+      rintro z ⟨x, hx, y, hy, rfl⟩
+      exact ⟨y, hy, x, hx, by simp [sub_eq_add_neg]⟩
+    have hsign : SignComplete X N := by
+      rintro z ⟨x, hx, y, hy, rfl⟩
+      rcases hcomplete hx hy with hxy | hyx
+      · left
+        exact ⟨x, hx, y, hy, hxy, rfl⟩
+      · right
+        exact ⟨y, hy, x, hx, hyx, by simp [sub_eq_add_neg]⟩
+    have hunweighted : UnweightedSequenceCancellation X N := by
+      intro n z hzX hzN hsum
+      choose x hx y hy hR hxy using hzN
+      have hsumeq : ∑ i, x i = ∑ i, y i := by
+        have hzero : ∑ i, x i - ∑ i, y i = 0 := by
+          rw [← Finset.sum_sub_distrib]
+          simpa only [hxy] using hsum
+        exact sub_eq_zero.mp hzero
+      have hrev := hcancel n x y hx hy hR hsumeq
+      intro i
+      exact ⟨y i, hy i, x i, hx i, hrev i, by
+        rw [hxy i]
+        simp [sub_eq_add_neg]⟩
+    obtain ⟨φ, hφ⟩ :=
+      (scott_theorem_1_2 hXfinite hXrat hXsym).mpr ⟨hsign, hunweighted⟩
+    refine ⟨φ, fun x hx y hy ↦ ?_⟩
+    constructor
+    · intro hxy
+      have hN : x - y ∈ N := ⟨x, hx, y, hy, hxy, rfl⟩
+      have hnonneg := (hφ (x - y) ⟨x, hx, y, hy, rfl⟩).mp hN
+      simpa [map_sub, sub_nonneg] using hnonneg
+    · intro hle
+      have hnonneg : 0 ≤ φ (x - y) := by simpa [map_sub, sub_nonneg] using hle
+      obtain ⟨x', hx', y', hy', hx'y', heq⟩ :=
+        (hφ (x - y) ⟨x, hx, y, hy, rfl⟩).mpr hnonneg
+      by_contra hnxy
+      have hyx := (hcomplete hx hy).resolve_left hnxy
+      let xs : Fin 2 → S → ℝ := ![x', y]
+      let ys : Fin 2 → S → ℝ := ![y', x]
+      have hsum2 : ∑ i, xs i = ∑ i, ys i := by
+        rw [Fin.sum_univ_two, Fin.sum_univ_two]
+        dsimp [xs, ys]
+        ext s
+        have hs := congrFun heq s
+        dsimp at hs ⊢
+        linarith
+      have hback := hcancel 1 xs ys (by simp [xs, hx', hy])
+        (by simp [ys, hy', hx]) (by
+          intro i
+          fin_cases i <;> simp [xs, ys, hx'y', hyx]) hsum2
+      exact hnxy (by simpa [xs, ys] using hback (1 : Fin 2))
+
+/-- Scott (1964), Theorem 1.4: realizability is equivalent to extendability
+to a strictly monotonic relation on the additive closure. -/
+theorem scott_theorem_1_4 {S : Type*} [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 := by
+  let := Fintype.ofFinite S
+  constructor
+  · intro h
+    exact scott_theorem_1_4_forward h
+  · rintro ⟨Rplus, hext, hmono⟩
+    apply (scott_theorem_1_3 hY hYrat).mpr
+    refine ⟨?_, hmono.relationSequenceCancellation hext⟩
+    intro x hx y hy
+    exact (hmono.complete (hext.1 hx) (hext.1 hy)).imp
+      (fun h ↦ hext.2 hx hy |>.mp h) (fun h ↦ hext.2 hy hx |>.mp h)
+
+end Scott1964.MeasurementStructures.LinearInequalities
diff --git a/LeanPool/ScottMeasurement/LinearInequalities/Separation.lean b/LeanPool/ScottMeasurement/LinearInequalities/Separation.lean
new file mode 100644
index 0000000000..0606b75d16
--- /dev/null
+++ b/LeanPool/ScottMeasurement/LinearInequalities/Separation.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.LinearInequalities.Definitions
+public import Mathlib.Analysis.LocallyConvex.Separation
+public import Mathlib.Analysis.LocallyConvex.WithSeminorms
+
+/-!
+# Finite convex separation
+
+The separation lemma used in Scott's proof of Theorem 1.1.
+-/
+
+@[expose] public section
+
+open Set
+
+namespace Scott1964.MeasurementStructures.LinearInequalities
+
+variable {L : Type*} [NormedAddCommGroup L] [NormedSpace ℝ L]
+  [FiniteDimensional ℝ L]
+
+/-- A finite set `A` can be made strictly positive while `B` is made zero
+exactly when its convex hull misses the span of `B`. -/
+theorem finite_strict_separation {A B : Set L} (hA : A.Finite) :
+    Disjoint (convexHull ℝ A) (Submodule.span ℝ B : Set L) ↔
+      ∃ φ : Module.Dual ℝ L, (∀ x ∈ A, 0 < φ x) ∧ ∀ x ∈ B, φ x = 0 := by
+  constructor
+  · intro hdisj
+    let M : Submodule ℝ L := Submodule.span ℝ B
+    have hMclosed : IsClosed (M : Set L) := M.closed_of_finiteDimensional
+    obtain ⟨f, u, v, hfA, huv, hfM⟩ :=
+      geometric_hahn_banach_compact_closed (convex_convexHull ℝ A)
+        (hA.isCompact_convexHull ℝ) M.convex hMclosed hdisj
+    have hf_zero : ∀ m ∈ M, f m = 0 := by
+      intro m hm
+      by_contra hne
+      have hscaled := hfM (((v - 1) / f m) • m) (M.smul_mem _ hm)
+      have hmap : f (((v - 1) / f m) • m) = v - 1 := by
+        rw [map_smul, smul_eq_mul]
+        field_simp
+      rw [hmap] at hscaled
+      linarith
+    let φ : Module.Dual ℝ L := -(f : L →L[ℝ] ℝ).toLinearMap
+    refine ⟨φ, ?_, ?_⟩
+    · intro x hx
+      have hxHull : x ∈ convexHull ℝ A := subset_convexHull ℝ A hx
+      have hv : v < 0 := by simpa using hfM 0 M.zero_mem
+      have hfx : f x < 0 := (hfA x hxHull).trans (huv.trans hv)
+      simpa [φ] using neg_pos.mpr hfx
+    · intro x hx
+      have hxM : x ∈ M := Submodule.subset_span hx
+      simp [φ, hf_zero x hxM]
+  · rintro ⟨φ, hφA, hφB⟩
+    rw [Set.disjoint_left]
+    intro z hzA hzB
+    have hzpos : 0 < φ z := by
+      exact convexHull_min (fun x hx ↦ hφA x hx)
+        (convex_halfSpace_gt φ.isLinear 0) hzA
+    have hzM : φ z = 0 := by
+      have hle : Submodule.span ℝ B ≤ LinearMap.ker φ :=
+        Submodule.span_le.mpr fun x hx => LinearMap.mem_ker.mpr (hφB x hx)
+      exact LinearMap.mem_ker.mp (hle hzB)
+    linarith
+
+end Scott1964.MeasurementStructures.LinearInequalities
diff --git a/LeanPool/ScottMeasurement/LinearInequalities/Sequences.lean b/LeanPool/ScottMeasurement/LinearInequalities/Sequences.lean
new file mode 100644
index 0000000000..151abc3a23
--- /dev/null
+++ b/LeanPool/ScottMeasurement/LinearInequalities/Sequences.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.LinearInequalities.Definitions
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-!
+# Scott's explicit finite sequence conditions
+-/
+
+@[expose] public section
+
+open scoped BigOperators
+
+namespace Scott1964.MeasurementStructures.LinearInequalities
+
+variable {L : Type*} [AddCommGroup L] [Module ℝ L]
+
+/-- A realizing functional satisfies Scott's positive-weight condition (2). -/
+theorem Realizable.weightedSequenceCancellation {X N : Set L}
+    (hreal : Realizable X N) (hsym : Symmetric X) :
+    WeightedSequenceCancellation X N := by
+  obtain ⟨φ, hφ⟩ := hreal
+  intro n x c hx hN hc hsum
+  have hnonneg : ∀ i, 0 ≤ c i * φ (x i) :=
+    fun i ↦ mul_nonneg (hc i).le ((hφ (x i) (hx i)).mp (hN i))
+  have hzero : ∑ i, c i * φ (x i) = 0 := by
+    have := congrArg φ hsum
+    simpa only [map_sum, map_smul, smul_eq_mul, map_zero] using this
+  intro j
+  have hxzero : φ (x j) = 0 := by
+    have hterm : c j * φ (x j) = 0 :=
+      (Finset.sum_eq_zero_iff_of_nonneg fun i _ ↦ hnonneg i).mp hzero j (Finset.mem_univ j)
+    exact (mul_eq_zero.mp hterm).resolve_left (hc j).ne'
+  apply (hφ (-x j) (hsym (hx j))).mpr
+  simp [hxzero]
+
+/-- Condition (2) immediately implies the unit-weight condition (4). -/
+theorem WeightedSequenceCancellation.unweighted {X N : Set L}
+    (h : WeightedSequenceCancellation X N) :
+    UnweightedSequenceCancellation X N := by
+  intro n x hx hN hsum
+  apply h n x (fun _ ↦ 1) hx hN (fun _ ↦ zero_lt_one)
+  simpa using hsum
+
+/-- A realizing relation satisfies Scott's paired equal-sums condition (6). -/
+theorem RelationRealizable.sequenceCancellation {Y : Set L} {R : L → L → Prop}
+    (hreal : RelationRealizable Y R) : RelationSequenceCancellation Y R := by
+  obtain ⟨φ, hφ⟩ := hreal
+  intro n x y hx hy hR hsum
+  have hle : ∀ i, φ (y i) ≤ φ (x i) :=
+    fun i ↦ (hφ (x i) (hx i) (y i) (hy i)).mp (hR i)
+  have hsumφ : ∑ i, φ (x i) = ∑ i, φ (y i) := by
+    simpa only [map_sum] using congrArg φ hsum
+  intro j
+  have hhead : φ (x j) ≤ φ (y j) := by
+    have hall :=
+      (Finset.sum_eq_sum_iff_of_le (s := Finset.univ)
+        (fun i _ ↦ hle i)).mp hsumφ.symm
+    exact (hall j (Finset.mem_univ j)).ge
+  exact (hφ (y j) (hy j) (x j) (hx j)).mpr hhead
+
+end Scott1964.MeasurementStructures.LinearInequalities
diff --git a/LeanPool/ScottMeasurement/Preference/Cycle.lean b/LeanPool/ScottMeasurement/Preference/Cycle.lean
new file mode 100644
index 0000000000..0e55628827
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Preference/Cycle.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Order.Defs.Unbundled
+
+/-!
+# Local reductions in Scott's cycle argument
+
+These lemmas are the three local moves used on pp. 8--9 of Scott (1964).
+They are kept separate from the linear-inequality interface so that the
+finite-array cancellation proof does not depend on names in §1.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+theorem preference_transitive_of_quadA {A : Type u} {P : A → A → Prop}
+    (hirr : ∀ x, ¬ P x x)
+    (hquad : ∀ x y z w, P x y → P z w → P x w ∨ P z y) :
+    IsTrans A P := by
+  constructor
+  intro x y z hxy hyz
+  rcases hquad x y y z hxy hyz with hxz | hyy
+  · exact hxz
+  · exact (hirr y hyy).elim
+
+/-- Scott's first shortening move, for `z P x P y Q w`.
+Here `y Q w` abbreviates `¬ w P y`. -/
+theorem preference_shorten_ppq {A : Type u} {P : A → A → Prop}
+    (hquad : ∀ x y z w, P x y → P z x → P w y ∨ P z w) {z x y w : A}
+    (hzx : P z x) (hxy : P x y) (hyw : ¬ P w y) :
+    P z w := by
+  rcases hquad x y z w hxy hzx with hwy | hzw
+  · exact (hyw hwy).elim
+  · exact hzw
+
+/-- The rotated form of Scott's first shortening move, for `w Q z P x P y`.
+Here `w Q z` abbreviates `¬ z P w`. -/
+theorem preference_shorten_qpp {A : Type u} {P : A → A → Prop}
+    (hquad : ∀ x y z w, P x y → P z x → P w y ∨ P z w) {w z x y : A}
+    (hwz : ¬ P z w) (hzx : P z x) (hxy : P x y) :
+    P w y := by
+  rcases hquad x y z w hxy hzx with hwy | hzw
+  · exact hwy
+  · exact (hwz hzw).elim
+
+/-- Scott's alternating shortening move, for `x P y Q z P w`.
+Here `y Q z` abbreviates `¬ z P y`. -/
+theorem preference_shorten_pqp {A : Type u} {P : A → A → Prop}
+    (hquad : ∀ x y z w, P x y → P z w → P x w ∨ P z y) {x y z w : A}
+    (hxy : P x y) (hyz : ¬ P z y) (hzw : P z w) :
+    P x w := by
+  rcases hquad x y z w hxy hzw with hxw | hzy
+  · exact hxw
+  · exact (hyz hzy).elim
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Preference/Direct.lean b/LeanPool/ScottMeasurement/Preference/Direct.lean
new file mode 100644
index 0000000000..2bcd8c5756
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Preference/Direct.lean
@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Basic.Real.Basic
+public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Fintype.Card
+public import Mathlib.SetTheory.Cardinal.Finite
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.SplitIfs
+public import Mathlib.Order.Antisymmetrization
+
+/-!
+# Direct finite semiorder representation
+
+The order used here is the one introduced by Scott and Suppes (1958):
+`x ≼ y` says that every predecessor of `x` is a predecessor of `y`, and
+every successor of `y` is a successor of `x`.  Its antisymmetrization is
+the paper's quotient by substitutability.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+section WeakOrder
+
+variable {A : Type u} (P : A → A → Prop)
+
+/-- The Scott--Suppes weak order associated with a strict preference. -/
+def ScottWeakOrder (x y : A) : Prop :=
+  (∀ z, P z x → P z y) ∧ (∀ z, P y z → P x z)
+
+/-- Substitute alternatives have identical strict-preference profiles. -/
+def PreferenceSubstitute (x y : A) : Prop :=
+  (∀ z, P z x ↔ P z y) ∧ (∀ z, P x z ↔ P y z)
+
+theorem scottWeakOrder_refl (x : A) : ScottWeakOrder P x x :=
+  ⟨fun _ h ↦ h, fun _ h ↦ h⟩
+
+theorem scottWeakOrder_trans :
+    IsTrans A (ScottWeakOrder P) := by
+  constructor
+  intro x y z hxy hyz
+  exact ⟨fun w hwx ↦ hyz.1 w (hxy.1 w hwx),
+    fun w hzw ↦ hxy.2 w (hyz.2 w hzw)⟩
+
+theorem scottWeakOrder_total
+    (hA : ∀ x y z w, P x y → P z w → P x w ∨ P z y)
+    (hB : ∀ x y z w, P x y → P z x → P w y ∨ P z w) :
+    ∀ x y, ScottWeakOrder P x y ∨ ScottWeakOrder P y x := by
+  intro x y
+  classical
+  by_cases hxy : ScottWeakOrder P x y
+  · exact Or.inl hxy
+  by_cases hyx : ScottWeakOrder P y x
+  · exact Or.inr hyx
+  exfalso
+  unfold ScottWeakOrder at hxy hyx
+  rw [not_and_or] at hxy hyx
+  rcases hxy with hxy | hxy
+  · push Not at hxy
+    rcases hxy with ⟨z, hzx, hzyny⟩
+    rcases hyx with hyx | hyx
+    · push Not at hyx
+      rcases hyx with ⟨w, hwy, hwnx⟩
+      rcases hA z x w y hzx hwy with hzy | hwx
+      · exact hzyny hzy
+      · exact hwnx hwx
+    · push Not at hyx
+      rcases hyx with ⟨w, hxw, hnyw⟩
+      rcases hB x w z y hxw hzx with hyw | hzy
+      · exact hnyw hyw
+      · exact hzyny hzy
+  · push Not at hxy
+    rcases hxy with ⟨z, hyz, hnxz⟩
+    rcases hyx with hyx | hyx
+    · push Not at hyx
+      rcases hyx with ⟨w, hwy, hwnx⟩
+      rcases hB y z w x hyz hwy with hxz | hwx
+      · exact hnxz hxz
+      · exact hwnx hwx
+    · push Not at hyx
+      rcases hyx with ⟨w, hxw, hnyw⟩
+      rcases hA y z x w hyz hxw with hyw | hxz
+      · exact hnyw hyw
+      · exact hnxz hxz
+
+theorem preferenceSubstitute_iff :
+    PreferenceSubstitute P x y ↔
+      ScottWeakOrder P x y ∧ ScottWeakOrder P y x := by
+  constructor
+  · rintro ⟨hin, hout⟩
+    exact ⟨⟨fun z ↦ (hin z).mp, fun z ↦ (hout z).mpr⟩,
+      ⟨fun z ↦ (hin z).mpr, fun z ↦ (hout z).mp⟩⟩
+  · rintro ⟨hxy, hyx⟩
+    exact ⟨fun z ↦ ⟨hxy.1 z, hyx.1 z⟩,
+      fun z ↦ ⟨hyx.2 z, hxy.2 z⟩⟩
+
+theorem preference_implies_scottWeakOrder
+    (hirr : ∀ x, ¬P x x)
+    (hA : ∀ x y z w, P x y → P z w → P x w ∨ P z y)
+    {x y : A} (hxy : P x y) :
+    ScottWeakOrder P x y := by
+  have htrans : IsTrans A P := by
+    constructor
+    intro a b c hab hbc
+    rcases hA a b b c hab hbc with hac | hbb
+    · exact hac
+    · exact (hirr b hbb).elim
+  exact ⟨fun z hzx ↦ htrans.trans z x y hzx hxy, fun z hyz ↦ htrans.trans x y z hxy hyz⟩
+
+theorem scottWeakOrder_preference_scottWeakOrder
+    {x x₁ y₁ y : A} (hxx₁ : ScottWeakOrder P x x₁)
+    (hx₁y₁ : P x₁ y₁) (hy₁y : ScottWeakOrder P y₁ y) : P x y :=
+  hy₁y.1 x (hxx₁.2 y₁ hx₁y₁)
+
+end WeakOrder
+
+section FiniteStaircase
+
+/-- A finite relation whose lower sections are nested along a linear order
+has a unit-threshold representation.  This is the finite recursive core of
+the Scott--Suppes construction. -/
+theorem finite_staircase_representation
+    (A : Type u) [Finite A] [LinearOrder A] (P : A → A → Prop)
+    (hforward : ∀ {x y}, P x y → y < x)
+    (hmono : ∀ {x x' y y'}, x ≤ x' → y' ≤ y → P x y → P x' y') :
+    ∃ f : A → ℝ,
+      (∀ x y, P x y ↔ f x ≥ f y + 1) ∧
+      (∀ {x y}, x < y → f x < f y) := by
+  let := Fintype.ofFinite A
+  classical
+  induction hcard : Fintype.card A using Nat.strong_induction_on generalizing A with
+  | h n ih =>
+    by_cases hA : IsEmpty A
+    · let := hA
+      exact ⟨fun x ↦ isEmptyElim x, by simp, by simp⟩
+    · let : Nonempty A := not_isEmpty_iff.mp hA
+      let m : A := Finset.univ.max' Finset.univ_nonempty
+      let B := {x : A // x ≠ m}
+      by_cases hB : IsEmpty B
+      · refine ⟨fun _ ↦ 0, ?_, ?_⟩
+        · intro x y
+          have hx : x = m := by
+            by_contra hx
+            exact hB.false ⟨x, hx⟩
+          have hy : y = m := by
+            by_contra hy
+            exact hB.false ⟨y, hy⟩
+          subst x
+          subst y
+          simp only [ge_iff_le]
+          constructor
+          · intro hmm
+            exact (hforward hmm).false.elim
+          · norm_num
+        · intro x y hxy
+          exact (hxy.ne (by
+            have hx : x = m := by
+              by_contra hx
+              exact hB.false ⟨x, hx⟩
+            have hy : y = m := by
+              by_contra hy
+              exact hB.false ⟨y, hy⟩
+            simp [hx, hy])).elim
+      · let : Nonempty B := not_isEmpty_iff.mp hB
+        let PB : B → B → Prop := fun x y ↦ P x.1 y.1
+        have hcardB : Fintype.card B < n := by
+          have hc : Fintype.card B = Fintype.card A - 1 := by
+            simp [B]
+          have hpos : 0 < Fintype.card A := Fintype.card_pos
+          rw [← hcard]
+          omega
+        obtain ⟨g, hg, gmono⟩ :=
+          ih (Fintype.card B) hcardB B PB
+            (fun h ↦ hforward h)
+            (fun hxx' hyy' h ↦ hmono hxx' hyy' h)
+            (by simp only [Fintype.card_eq_nat_card])
+        let nonpref : Finset B := Finset.univ.filter fun x ↦ ¬P m x.1
+        let score : B → ℝ := fun x ↦ if P m x.1 then g x + 1 else g x
+        obtain ⟨b, -, hb⟩ :=
+          Finset.exists_max_image (Finset.univ : Finset B) score Finset.univ_nonempty
+        let top : ℝ :=
+          if hn : nonpref.Nonempty then
+            let j := nonpref.min' hn
+            (score b + (g j + 1)) / 2
+          else score b + 1
+        have hscore_lt {j : B} (hj : ¬P m j.1) :
+            score b < g j + 1 := by
+          apply lt_of_le_of_lt (hb b (Finset.mem_univ b))
+          dsimp [score]
+          split_ifs with hpb
+          · have hbj : b < j := by
+              apply lt_of_not_ge
+              intro hjb
+              exact hj (hmono le_rfl hjb hpb)
+            linarith [gmono hbj]
+          · have hnot : ¬PB b j := by
+              intro hbj
+              have hbm : b.1 ≤ m :=
+                Finset.le_max' Finset.univ b.1 (Finset.mem_univ b.1)
+              exact hj (hmono hbm le_rfl hbj)
+            have hlt := not_le.mp (mt (hg b j).mpr hnot)
+            linarith
+        have htop_score : score b < top := by
+          dsimp [top]
+          split_ifs with hn
+          · let j := nonpref.min' hn
+            have hj : ¬P m j.1 := by
+              have hjmem := nonpref.min'_mem hn
+              simpa [nonpref, j] using hjmem
+            have hs := hscore_lt hj
+            dsimp [j] at hs ⊢
+            linarith
+          · linarith
+        have htop_nonpref {j : B} (hj : ¬P m j.1) :
+            top < g j + 1 := by
+          dsimp [top]
+          split_ifs with hn
+          · let k := nonpref.min' hn
+            have hk_mem : k ∈ nonpref := nonpref.min'_mem hn
+            have hkj : k ≤ j := nonpref.min'_le _ (by simp [nonpref, hj])
+            have hgkj : g k ≤ g j := by
+              rcases hkj.eq_or_lt with rfl | hlt
+              · exact le_rfl
+              · exact (gmono hlt).le
+            have hk : ¬P m k.1 := by simpa [nonpref] using hk_mem
+            have hs := hscore_lt hk
+            dsimp [k] at hs hgkj ⊢
+            linarith
+          · exact (hn ⟨j, by simp [nonpref, hj]⟩).elim
+        let f : A → ℝ := fun x ↦ if hx : x = m then top else g ⟨x, hx⟩
+        refine ⟨f, ?_, ?_⟩
+        · intro x y
+          by_cases hx : x = m
+          · subst x
+            by_cases hy : y = m
+            · subst y
+              rw [show f m = top by simp [f]]
+              exact ⟨fun hmm ↦ (hforward hmm).false.elim, by simp⟩
+            · simp only [f, dite_eq_left rfl, dite_eq_right hy, ge_iff_le]
+              constructor
+              · intro hmy
+                have hsc : g ⟨y, hy⟩ + 1 = score ⟨y, hy⟩ := by
+                  simp [score, hmy]
+                rw [hsc]
+                exact (hb _ (Finset.mem_univ _)).trans htop_score.le
+              · intro hle
+                by_contra hmy
+                have hlt := htop_nonpref (j := ⟨y, hy⟩) hmy
+                linarith
+          · by_cases hy : y = m
+            · subst y
+              simp only [f, dite_eq_right hx, dite_eq_left rfl]
+              exact ⟨fun h ↦ ((not_lt_of_ge (Finset.le_max' Finset.univ x
+                (Finset.mem_univ x))) (hforward h)).elim, by
+                intro hbad
+                have hgs : g ⟨x, hx⟩ ≤ score ⟨x, hx⟩ := by
+                  dsimp [score]
+                  split_ifs <;> linarith
+                have hlt :=
+                  (hgs.trans (hb _ (Finset.mem_univ _))).trans_lt htop_score
+                linarith⟩
+            · simpa [f, hx, hy, PB] using hg ⟨x, hx⟩ ⟨y, hy⟩
+        · intro x y hxy
+          by_cases hy : y = m
+          · subst y
+            have hx : x ≠ m := hxy.ne
+            simp only [f, dite_eq_right hx, dite_eq_left rfl]
+            have hgs : g ⟨x, hx⟩ ≤ score ⟨x, hx⟩ := by
+              dsimp [score]
+              split_ifs <;> linarith
+            exact (hgs.trans (hb _ (Finset.mem_univ _))).trans_lt htop_score
+          · have hx : x ≠ m := by
+              intro hx
+              subst x
+              exact (not_lt_of_ge (Finset.le_max' Finset.univ y
+                (Finset.mem_univ y))) hxy
+            simpa [f, hx, hy] using gmono (show (⟨x, hx⟩ : B) < ⟨y, hy⟩ from hxy)
+
+end FiniteStaircase
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Preference/Intransitive.lean b/LeanPool/ScottMeasurement/Preference/Intransitive.lean
new file mode 100644
index 0000000000..176752c8b8
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Preference/Intransitive.lean
@@ -0,0 +1,312 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Preference.Direct
+public import Mathlib.Tactic.FieldSimp
+
+/-!
+# Scott's intransitive-indifference problem
+
+The definitions reproduce conditions `(1_P)`--`(3_P)` in §2.  The elementary
+direction of Theorem 2.1 is recorded here; the converse is supplied by the
+finite linear-inequality engine.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+/-- A strict preference relation is represented with discrimination threshold `1`. -/
+def RealizablePreference {A : Type u} (P : A → A → Prop) : Prop :=
+  ∃ f : A → ℝ, ∀ x y, P x y ↔ f x ≥ f y + 1
+
+/-- Scott 1964, condition `(1_P)`. -/
+def PrefIrrefl {A : Type u} (P : A → A → Prop) : Prop :=
+  ∀ x, ¬P x x
+
+/-- Scott 1964, condition `(2_P)`. -/
+def PrefQuadA {A : Type u} (P : A → A → Prop) : Prop :=
+  ∀ x y z w, P x y → P z w → P x w ∨ P z y
+
+/-- Scott 1964, condition `(3_P)`. -/
+def PrefQuadB {A : Type u} (P : A → A → Prop) : Prop :=
+  ∀ x y z w, P x y → P z x → P w y ∨ P z w
+
+/-- Realization with a strict margin above the conventional unit threshold. -/
+def RealizablePreferenceWithGap {A : Type u} (P : A → A → Prop) : Prop :=
+  ∃ f : A → ℝ, ∃ ε > 0, ∀ x y, P x y ↔ f x ≥ f y + 1 + ε
+
+/-- Scott's stronger conclusion following Theorem 2.1: the same unit
+threshold may be taken strict on every preferred pair. -/
+def StrictlyRealizablePreference {A : Type u} (P : A → A → Prop) : Prop :=
+  ∃ f : A → ℝ, ∀ x y, P x y ↔ f x > f y + 1
+
+theorem RealizablePreference.irrefl {A : Type u} {P : A → A → Prop}
+    (hP : RealizablePreference P) : PrefIrrefl P := by
+  rcases hP with ⟨f, hf⟩
+  intro x hxx
+  have := (hf x x).1 hxx
+  linarith
+
+theorem RealizablePreference.quadA {A : Type u} {P : A → A → Prop}
+    (hP : RealizablePreference P) : PrefQuadA P := by
+  rcases hP with ⟨f, hf⟩
+  intro x y z w hxy hzw
+  rw [hf] at hxy hzw
+  by_cases hxw : f w + 1 ≤ f x
+  · exact Or.inl ((hf x w).2 hxw)
+  · apply Or.inr
+    apply (hf z y).2
+    have hlt : f x < f w + 1 := lt_of_not_ge hxw
+    linarith
+
+theorem RealizablePreference.quadB {A : Type u} {P : A → A → Prop}
+    (hP : RealizablePreference P) : PrefQuadB P := by
+  rcases hP with ⟨f, hf⟩
+  intro x y z w hxy hzx
+  rw [hf] at hxy hzx
+  by_cases hwy : f y + 1 ≤ f w
+  · exact Or.inl ((hf w y).2 hwy)
+  · apply Or.inr
+    apply (hf z w).2
+    have hlt : f w < f y + 1 := lt_of_not_ge hwy
+    linarith
+
+theorem RealizablePreference.necessary {A : Type u} {P : A → A → Prop}
+    (hP : RealizablePreference P) :
+    PrefIrrefl P ∧ PrefQuadA P ∧ PrefQuadB P :=
+  ⟨hP.irrefl, hP.quadA, hP.quadB⟩
+
+/-- **Scott 1964, Theorem 2.1 (intransitive indifference).**
+
+The nonemptiness assumption in the source is unnecessary here.
+The converse uses the direct finite Scott--Suppes construction: quotient by
+substitutability, order the quotient by the weak order `ScottWeakOrder`, and
+represent its nested lower sections by a recursively constructed sequence. -/
+theorem theorem_2_1 {A : Type u} [Finite A] (P : A → A → Prop) :
+    RealizablePreference P ↔ PrefIrrefl P ∧ PrefQuadA P ∧ PrefQuadB P := by
+  let := Fintype.ofFinite A
+  constructor
+  · exact RealizablePreference.necessary
+  · rintro ⟨hirr, hA, hB⟩
+    classical
+    let : Preorder A :=
+      {
+      le x y := ScottWeakOrder P y x
+      le_refl x := scottWeakOrder_refl P x
+      le_trans x y z hxy hyz := (scottWeakOrder_trans P).trans z y x hyz hxy
+      lt x y := ScottWeakOrder P y x ∧ ¬ScottWeakOrder P x y
+      lt_iff_le_not_ge _ _ := Iff.rfl
+      }
+    let : Std.Total (α := A) (· ≤ ·) :=
+      ⟨fun x y ↦ scottWeakOrder_total P hA hB y x⟩
+    let Q := Antisymmetrization A (· ≤ ·)
+    let : Finite Q :=
+      Finite.of_surjective (toAntisymmetrization (α := A) (· ≤ ·))
+        (fun q ↦ ⟨ofAntisymmetrization (· ≤ ·) q,
+          toAntisymmetrization_ofAntisymmetrization (· ≤ ·) q⟩)
+    let : Fintype Q := Fintype.ofFinite Q
+    let PQ : Q → Q → Prop :=
+      fun x y ↦ P (ofAntisymmetrization (· ≤ ·) x)
+        (ofAntisymmetrization (· ≤ ·) y)
+    have hPQ_forward {x y : Q} (hxy : PQ x y) : y < x := by
+      let ox := ofAntisymmetrization (· ≤ ·) x
+      let oy := ofAntisymmetrization (· ≤ ·) y
+      have hle : y ≤ x := by
+        rw [← toAntisymmetrization_ofAntisymmetrization (· ≤ ·) y,
+          ← toAntisymmetrization_ofAntisymmetrization (· ≤ ·) x,
+          toAntisymmetrization_le_toAntisymmetrization_iff]
+        exact preference_implies_scottWeakOrder P hirr hA hxy
+      refine lt_of_le_of_ne hle ?_
+      intro heq
+      have hback : ScottWeakOrder P oy ox := by
+        have : x ≤ y := heq.ge
+        rw [← toAntisymmetrization_ofAntisymmetrization (· ≤ ·) x,
+          ← toAntisymmetrization_ofAntisymmetrization (· ≤ ·) y,
+          toAntisymmetrization_le_toAntisymmetrization_iff] at this
+        exact this
+      exact hirr ox (hback.1 ox hxy)
+    have hPQ_mono {x x' y y' : Q} (hxx' : x ≤ x') (hyy' : y' ≤ y)
+        (hxy : PQ x y) : PQ x' y' := by
+      have hx :
+          ScottWeakOrder P (ofAntisymmetrization (· ≤ ·) x')
+            (ofAntisymmetrization (· ≤ ·) x) := by
+        have hq :
+            toAntisymmetrization (· ≤ ·)
+                (ofAntisymmetrization (· ≤ ·) x) ≤
+              toAntisymmetrization (· ≤ ·)
+                (ofAntisymmetrization (· ≤ ·) x') := by
+          simpa only [toAntisymmetrization_ofAntisymmetrization] using hxx'
+        change ScottWeakOrder P
+          (ofAntisymmetrization (· ≤ ·) x')
+          (ofAntisymmetrization (· ≤ ·) x) at hq
+        exact hq
+      have hy :
+          ScottWeakOrder P (ofAntisymmetrization (· ≤ ·) y)
+            (ofAntisymmetrization (· ≤ ·) y') := by
+        have hq :
+            toAntisymmetrization (· ≤ ·)
+                (ofAntisymmetrization (· ≤ ·) y') ≤
+              toAntisymmetrization (· ≤ ·)
+                (ofAntisymmetrization (· ≤ ·) y) := by
+          simpa only [toAntisymmetrization_ofAntisymmetrization] using hyy'
+        change ScottWeakOrder P
+          (ofAntisymmetrization (· ≤ ·) y)
+          (ofAntisymmetrization (· ≤ ·) y') at hq
+        exact hq
+      exact scottWeakOrder_preference_scottWeakOrder P hx hxy hy
+    obtain ⟨g, hg, -⟩ :=
+      finite_staircase_representation Q PQ hPQ_forward hPQ_mono
+    refine ⟨fun x ↦ g (toAntisymmetrization (· ≤ ·) x), fun x y ↦ ?_⟩
+    let ox := ofAntisymmetrization (· ≤ ·)
+      (toAntisymmetrization (· ≤ ·) x)
+    let oy := ofAntisymmetrization (· ≤ ·)
+      (toAntisymmetrization (· ≤ ·) y)
+    have hx :
+        PreferenceSubstitute P x ox := by
+      apply (preferenceSubstitute_iff P).2
+      constructor
+      · have h :
+            toAntisymmetrization (· ≤ ·) ox ≤
+              toAntisymmetrization (· ≤ ·) x := by
+          simp [ox]
+        exact h
+      · have h :
+            toAntisymmetrization (· ≤ ·) x ≤
+              toAntisymmetrization (· ≤ ·) ox := by
+          simp [ox]
+        exact h
+    have hy :
+        PreferenceSubstitute P y oy := by
+      apply (preferenceSubstitute_iff P).2
+      constructor
+      · have h :
+            toAntisymmetrization (· ≤ ·) oy ≤
+              toAntisymmetrization (· ≤ ·) y := by
+          simp [oy]
+        exact h
+      · have h :
+            toAntisymmetrization (· ≤ ·) y ≤
+              toAntisymmetrization (· ≤ ·) oy := by
+          simp [oy]
+        exact h
+    rw [show P x y ↔ P ox oy from (hy.1 x).trans (hx.2 oy)]
+    exact hg _ _
+
+/-- Any positive discrimination threshold can be changed to `1` by a change
+of units, as noted immediately before §1. -/
+theorem realizablePreference_threshold_iff {A : Type u} (P : A → A → Prop)
+    {c : ℝ} (hc : 0 < c) :
+    (∃ f : A → ℝ, ∀ x y, P x y ↔ f x ≥ f y + c) ↔
+      RealizablePreference P := by
+  constructor
+  · rintro ⟨f, hf⟩
+    refine ⟨fun x ↦ f x / c, ?_⟩
+    intro x y
+    rw [hf]
+    constructor <;> intro h
+    · rw [show f y / c + 1 = (f y + c) / c by field_simp]
+      exact (div_le_div_iff_of_pos_right hc).2 h
+    · rw [show f y / c + 1 = (f y + c) / c by field_simp] at h
+      exact (div_le_div_iff_of_pos_right hc).1 h
+  · rintro ⟨f, hf⟩
+    refine ⟨fun x ↦ c * f x, ?_⟩
+    intro x y
+    rw [hf]
+    constructor <;> intro h
+    · nlinarith
+    · nlinarith
+
+/-- Rescaling any unit-threshold realization produces an arbitrary positive
+margin above the unit threshold. -/
+theorem RealizablePreference.withGap {A : Type u} {P : A → A → Prop}
+    (hP : RealizablePreference P) : RealizablePreferenceWithGap P := by
+  rcases hP with ⟨f, hf⟩
+  refine ⟨fun x ↦ 2 * f x, 1, by norm_num, ?_⟩
+  intro x y
+  rw [hf]
+  constructor <;> intro h <;> nlinarith
+
+theorem realizablePreferenceWithGap_iff {A : Type u} (P : A → A → Prop) :
+    RealizablePreferenceWithGap P ↔ RealizablePreference P := by
+  constructor
+  · rintro ⟨f, ε, hε, hf⟩
+    exact (realizablePreference_threshold_iff P (by linarith : 0 < 1 + ε)).mp
+      ⟨f, by simpa [add_assoc] using hf⟩
+  · exact RealizablePreference.withGap
+
+/-- On a finite set the boundary can be avoided altogether, as Scott notes
+after Theorem 2.1: preferred pairs lie strictly beyond the same unit
+threshold. -/
+theorem RealizablePreference.strict_of_finite {A : Type u} [Finite A] [Nonempty A]
+    {P : A → A → Prop} (hP : RealizablePreference P) :
+    StrictlyRealizablePreference P := by
+  let := Fintype.ofFinite A
+  classical
+  rcases hP with ⟨f, hf⟩
+  let values : Finset ℝ :=
+    (Finset.univ ×ˢ Finset.univ).image fun p : A × A ↦
+      if P p.1 p.2 then 0 else max 0 (f p.1 - f p.2)
+  have hvalues : values.Nonempty := by
+    let a : A := Classical.choice ‹Nonempty A›
+    exact ⟨if P a a then 0 else max 0 (f a - f a),
+      Finset.mem_image.mpr ⟨(a, a), by simp, rfl⟩⟩
+  let M : ℝ := values.max' hvalues
+  have hM_nonneg : 0 ≤ M := by
+    obtain ⟨v, hv⟩ := hvalues
+    have hv_nonneg : 0 ≤ v := by
+      rcases Finset.mem_image.mp hv with ⟨p, -, rfl⟩
+      split <;> simp
+    exact hv_nonneg.trans (Finset.le_max' values v hv)
+  have hM_lt_one : M < 1 := by
+    apply (Finset.max'_lt_iff values hvalues).mpr
+    intro v hv
+    rcases Finset.mem_image.mp hv with ⟨p, -, rfl⟩
+    split_ifs with hp
+    · norm_num
+    · have hlt : f p.1 - f p.2 < 1 := by
+        have := not_le.mp (mt (hf p.1 p.2).mpr hp)
+        linarith
+      exact max_lt (by norm_num) hlt
+  have hbound {x y : A} (hxy : ¬P x y) : f x - f y ≤ M := by
+    have hmem : max 0 (f x - f y) ∈ values := by
+      exact Finset.mem_image.mpr ⟨(x, y), by simp, by simp [hxy]⟩
+    exact (le_max_right 0 (f x - f y)).trans (Finset.le_max' values _ hmem)
+  let s : ℝ := 1 + (1 - M) / 2
+  have hs : 1 < s := by
+    dsimp [s]
+    linarith
+  refine ⟨fun x ↦ s * f x, fun x y ↦ ?_⟩
+  constructor
+  · intro hxy
+    have hdiff : 1 ≤ f x - f y := by
+      have := (hf x y).mp hxy
+      linarith
+    have hspos : 0 < s := lt_trans (by norm_num) hs
+    have : s ≤ s * (f x - f y) := by nlinarith
+    dsimp
+    nlinarith
+  · intro hstrict
+    by_contra hxy
+    have hd := hbound hxy
+    have hdiff_lt : f x - f y < 1 := by
+      have := not_le.mp (mt (hf x y).mpr hxy)
+      linarith
+    have hspos : 0 < s := lt_trans (by norm_num) hs
+    have hscaled : s * (f x - f y) ≤ 1 := by
+      by_cases hd0 : f x - f y ≤ 0
+      · nlinarith
+      · have hprod : s * (f x - f y) ≤ s * M :=
+          mul_le_mul_of_nonneg_left hd hspos.le
+        dsimp [s] at hprod ⊢
+        nlinarith [mul_nonneg (sub_nonneg.mpr hM_nonneg)
+          (sub_nonneg.mpr (le_of_lt hM_lt_one))]
+    dsimp at hstrict
+    nlinarith
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Probability/Atoms.lean b/LeanPool/ScottMeasurement/Probability/Atoms.lean
new file mode 100644
index 0000000000..3425eaafe9
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Atoms.lean
@@ -0,0 +1,253 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Order.Atoms
+public import Mathlib.Algebra.BigOperators.Pi
+public import Mathlib.Algebra.BigOperators.Ring.Finset
+public import LeanPool.ScottMeasurement.Probability.Basic
+
+/-!
+# Atom vectors for finite Boolean algebras
+
+Scott identifies an event with its `0`/`1` characteristic vector on the atoms.
+The cancellation identity in Theorem 4.1 is equality of sums of these vectors.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+open scoped BigOperators
+
+noncomputable section
+
+open Classical in
+/-- The real characteristic vector of an event on Boolean atoms. -/
+def atomVector {B : Type u} [BooleanAlgebra B] (x : B) :
+    {a : B // IsAtom a} → ℝ :=
+  fun a ↦ if (a : B) ≤ x then 1 else 0
+
+open Classical in
+@[simp]
+theorem atomVector_apply {B : Type u} [BooleanAlgebra B] (x : B)
+    (a : {a : B // IsAtom a}) :
+    atomVector x a = if (a : B) ≤ x then 1 else 0 :=
+  rfl
+
+theorem atomVector_bot {B : Type u} [BooleanAlgebra B] :
+    atomVector (⊥ : B) = 0 := by
+  classical
+  funext a
+  simp [atomVector, a.property.1]
+
+theorem atomVector_top {B : Type u} [BooleanAlgebra B] :
+    atomVector (⊤ : B) = 1 := by
+  classical
+  funext a
+  simp [atomVector]
+
+theorem atomVector_sup_of_disjoint {B : Type u} [BooleanAlgebra B]
+    {x y : B} (hxy : Disjoint x y) :
+    atomVector (x ⊔ y) = atomVector x + atomVector y := by
+  classical
+  funext a
+  have hatom := a.property
+  by_cases hx : (a : B) ≤ x
+  · have hny : ¬(a : B) ≤ y := by
+      classical
+      intro hy
+      have : (a : B) ≤ x ⊓ y := le_inf hx hy
+      rw [hxy.eq_bot] at this
+      exact hatom.1 (bot_unique this)
+    have hsup : (a : B) ≤ x ⊔ y := hx.trans le_sup_left
+    simp [atomVector, hx, hny, hsup]
+  · by_cases hy : (a : B) ≤ y
+    · have hsup : (a : B) ≤ x ⊔ y := hy.trans le_sup_right
+      simp [atomVector, hx, hy, hsup]
+    · have hsup : ¬(a : B) ≤ x ⊔ y := by
+        classical
+        intro ha
+        have hix : (a : B) ⊓ x = ⊥ := by
+          classical
+          rcases hatom.le_iff.mp inf_le_left with hbot | heq
+          · exact hbot
+          · exact False.elim (hx (by rw [← heq]; exact inf_le_right))
+        have hiy : (a : B) ⊓ y = ⊥ := by
+          classical
+          rcases hatom.le_iff.mp inf_le_left with hbot | heq
+          · exact hbot
+          · exact False.elim (hy (by rw [← heq]; exact inf_le_right))
+        have haeq : (a : B) ⊓ (x ⊔ y) = a := inf_eq_left.mpr ha
+        rw [inf_sup_left, hix, hiy, bot_sup_eq] at haeq
+        exact hatom.1 haeq.symm
+      simp [atomVector, hx, hy, hsup]
+
+theorem atomVector_injective {B : Type u} [BooleanAlgebra B] [Finite B] :
+    Function.Injective (atomVector : B → ({a : B // IsAtom a} → ℝ)) := by
+  classical
+  let := Fintype.ofFinite B
+  let _ : IsAtomic B := inferInstance
+  intro x y hxy
+  apply BooleanAlgebra.eq_iff_atom_le_iff.mpr
+  intro a ha
+  have h := congrFun hxy ⟨a, ha⟩
+  simp only [atomVector_apply] at h
+  constructor <;> intro hle
+  · by_contra hn
+    simp [hle, hn] at h
+  · by_contra hn
+    simp [hle, hn] at h
+
+/-- Distinct Boolean atoms are disjoint. -/
+theorem disjoint_atoms_of_ne {B : Type u} [BooleanAlgebra B]
+    (a b : {a : B // IsAtom a}) (hab : a ≠ b) :
+    Disjoint (a : B) b := by
+  classical
+  rw [disjoint_iff_inf_le]
+  rcases a.property.le_iff.mp inf_le_left with hbot | heq
+  · exact le_of_eq hbot
+  · have hab_le : (a : B) ≤ b := by
+      classical
+      rw [← heq]
+      exact inf_le_right
+    rcases b.property.le_iff.mp hab_le with ha0 | heqab
+    · exact False.elim (a.property.1 ha0)
+    · exact False.elim (hab (Subtype.ext heqab))
+
+theorem disjoint_atom_finset_sup {B : Type u} [BooleanAlgebra B]
+    (a : {a : B // IsAtom a}) (s : Finset {a : B // IsAtom a})
+    (ha : a ∉ s) :
+    Disjoint (a : B) (s.sup fun b ↦ (b : B)) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert b s hb ih =>
+      rw [Finset.sup_insert]
+      exact (disjoint_sup_right).2
+        ⟨disjoint_atoms_of_ne a b (by
+            intro hab
+            subst b
+            exact ha (Finset.mem_insert_self _ _)),
+          ih (fun has ↦ ha (Finset.mem_insert_of_mem has))⟩
+
+/-- A signed charge evaluates a supremum of distinct atoms as the sum of
+their charges. -/
+theorem IsSignedCharge.finset_sup_atoms
+    {B : Type u} [BooleanAlgebra B] {μ : B → ℝ}
+    (hμ : IsSignedCharge μ) (s : Finset {a : B // IsAtom a}) :
+    μ (s.sup fun a ↦ (a : B)) = ∑ a ∈ s, μ a := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp [hμ.bot]
+  | @insert a s ha ih =>
+      rw [Finset.sup_insert, hμ.additive _ _ (disjoint_atom_finset_sup a s ha),
+        Finset.sum_insert ha, ih]
+
+/-- Finite additivity evaluates a supremum of distinct atoms as the sum of
+their masses. -/
+theorem IsProbability.finset_sup_atoms
+    {B : Type u} [BooleanAlgebra B] {μ : B → ℝ}
+    (hμ : IsProbability μ) (s : Finset {a : B // IsAtom a}) :
+    μ (s.sup fun a ↦ (a : B)) = ∑ a ∈ s, μ a :=
+  hμ.isSignedCharge.finset_sup_atoms s
+
+open Classical in
+/-- The atoms below an event. -/
+def atomsBelow {B : Type u} [BooleanAlgebra B] [Fintype B] (x : B) :
+    Finset {a : B // IsAtom a} :=
+  Finset.univ.filter fun a ↦ (a : B) ≤ x
+
+theorem sup_atomsBelow {B : Type u} [BooleanAlgebra B] [Fintype B] (x : B) :
+    (atomsBelow x).sup (fun a ↦ (a : B)) = x := by
+  classical
+  let _ : IsAtomic B := inferInstance
+  apply BooleanAlgebra.eq_iff_atom_le_iff.mpr
+  intro a ha
+  constructor
+  · intro h
+    exact h.trans (Finset.sup_le fun b hb ↦
+      (Finset.mem_filter.mp hb).2)
+  · intro h
+    exact Finset.le_sup (f := fun b : {a : B // IsAtom a} ↦ (b : B))
+      (show ⟨a, ha⟩ ∈ atomsBelow x by simp [atomsBelow, h])
+
+/-- Every finitely additive signed charge is the sum of its atom charges. -/
+theorem IsSignedCharge.eq_sum_atoms
+    {B : Type u} [BooleanAlgebra B] [Fintype B] {μ : B → ℝ}
+    (hμ : IsSignedCharge μ) (x : B) :
+    μ x = ∑ a ∈ atomsBelow x, μ a := by
+  classical
+  calc
+    μ x = μ ((atomsBelow x).sup fun a ↦ (a : B)) := by
+      classical
+      rw [sup_atomsBelow]
+    _ = ∑ a ∈ atomsBelow x, μ a := hμ.finset_sup_atoms (atomsBelow x)
+
+/-- Every finitely additive probability is the sum of its atom masses. -/
+theorem IsProbability.eq_sum_atoms
+    {B : Type u} [BooleanAlgebra B] [Fintype B] {μ : B → ℝ}
+    (hμ : IsProbability μ) (x : B) :
+    μ x = ∑ a ∈ atomsBelow x, μ a :=
+  hμ.isSignedCharge.eq_sum_atoms x
+
+open Classical in
+/-- Pointwise equality of sums of event vectors is exactly Scott's
+atom-count identity. -/
+theorem sum_atomVector_eq_iff {B : Type u} [BooleanAlgebra B]
+    (n : ℕ) (x y : Fin n → B) :
+    (∑ i, atomVector (x i)) = ∑ i, atomVector (y i) ↔
+      ∀ a : B, IsAtom a →
+        (∑ i, if a ≤ x i then 1 else 0) =
+          (∑ i, if a ≤ y i then 1 else 0 : ℕ) := by
+  classical
+  have hcast (a : B) (z : Fin n → B) :
+      ((∑ i, if a ≤ z i then 1 else 0 : ℕ) : ℝ) =
+        ∑ i, (if a ≤ z i then 1 else 0 : ℝ) := by
+    rw [Nat.cast_sum]
+    apply Finset.sum_congr rfl
+    intro i hi
+    split_ifs <;> norm_num
+  constructor
+  · intro h a ha
+    have haeq := congrFun h ⟨a, ha⟩
+    simp only [Finset.sum_apply, atomVector_apply] at haeq
+    have hcounts :
+        ((∑ i, if a ≤ x i then 1 else 0 : ℕ) : ℝ) =
+          ((∑ i, if a ≤ y i then 1 else 0 : ℕ) : ℝ) := by
+      rw [hcast, hcast]
+      exact haeq
+    exact_mod_cast hcounts
+  · intro h
+    funext a
+    simp only [Finset.sum_apply, atomVector_apply]
+    have hcounts := congrArg ((↑) : ℕ → ℝ) (h a a.property)
+    simpa only [hcast] using hcounts
+
+/-- Scott 1964, literal condition `(4_B)`: cancellation is stated using
+equality of sums of the characteristic vectors themselves. -/
+def ProbVectorCancellation {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop) : Prop :=
+  ∀ (n : ℕ) (x y : Fin (n + 1) → B),
+    (∑ i, atomVector (x i)) = ∑ i, atomVector (y i) →
+      (∀ i, i ≠ 0 → R (x i) (y i)) → R (y 0) (x 0)
+
+/-- The literal vector-sum and atom-count formulations of `(4_B)` agree. -/
+theorem probVectorCancellation_iff_probCancellation
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} :
+    ProbVectorCancellation R ↔ ProbCancellation R := by
+  classical
+  constructor
+  · intro h n x y hcount hweak
+    exact h n x y ((sum_atomVector_eq_iff (n + 1) x y).2 hcount) hweak
+  · intro h n x y hsum hweak
+    exact h n x y ((sum_atomVector_eq_iff (n + 1) x y).1 hsum) hweak
+
+end
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Probability/Basic.lean b/LeanPool/ScottMeasurement/Probability/Basic.lean
new file mode 100644
index 0000000000..92c3370936
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Basic.lean
@@ -0,0 +1,207 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Basic.Real.Basic
+public import Mathlib.Order.Atoms
+public import Mathlib.Data.Fintype.Fin
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import LeanPool.ScottMeasurement.FinHead
+
+/-!
+# Finitely additive probabilities on Boolean algebras
+
+Scott's probabilities are real-valued and finitely additive.  This file deliberately
+does not use Mathlib's countably additive `MeasureTheory.Measure`: the source works
+with an arbitrary Boolean algebra and only finite disjoint unions.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+open scoped BigOperators
+
+/-- A normalized finitely additive probability on a Boolean algebra. -/
+structure IsProbability {B : Type u} [BooleanAlgebra B] (μ : B → ℝ) : Prop where
+  bot : μ ⊥ = 0
+  top : μ ⊤ = 1
+  additive : ∀ x y, Disjoint x y → μ (x ⊔ y) = μ x + μ y
+  nonnegative : ∀ x, 0 ≤ μ x
+
+/-- A finitely additive signed charge.  Unlike `IsProbability`, no
+nonnegativity or normalization is imposed. -/
+structure IsSignedCharge {B : Type u} [BooleanAlgebra B] (μ : B → ℝ) : Prop where
+  bot : μ ⊥ = 0
+  additive : ∀ x y, Disjoint x y → μ (x ⊔ y) = μ x + μ y
+
+/-- Forgetting positivity and normalization preserves finite additivity. -/
+theorem IsProbability.isSignedCharge {B : Type u} [BooleanAlgebra B]
+    {μ : B → ℝ} (hμ : IsProbability μ) : IsSignedCharge μ :=
+  ⟨hμ.bot, hμ.additive⟩
+
+/-- Nonnegativity of a finitely additive set function. -/
+def IsNonnegative {B : Type u} (μ : B → ℝ) : Prop :=
+  ∀ x, 0 ≤ μ x
+
+/-- Compatibility name for a finitely additive probability. -/
+def IsFinitelyAdditiveProbability {B : Type u} [BooleanAlgebra B] (μ : B → ℝ) : Prop :=
+  IsProbability μ
+
+/-- A qualitative ordering is represented exactly by a normalized additive function. -/
+def RealizableProbability {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : Prop :=
+  ∃ μ : B → ℝ, IsProbability μ ∧ ∀ x y, R x y ↔ μ x ≥ μ y
+
+/-- A qualitative relation is represented by a finitely additive signed
+charge, with no normalization or positivity requirement. -/
+def RealizableSignedCharge {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop) : Prop :=
+  ∃ μ : B → ℝ, IsSignedCharge μ ∧ ∀ x y, R x y ↔ μ x ≥ μ y
+
+/-- A probability representation is also a signed-charge representation. -/
+theorem RealizableProbability.realizableSignedCharge {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) : RealizableSignedCharge R := by
+  rcases hR with ⟨μ, hμ, hrep⟩
+  exact ⟨μ, hμ.isSignedCharge, hrep⟩
+
+/-- Scott's strict notation: `x ≻ y` means that `y` is not weakly preferred to `x`. -/
+def StrictlyPreferred {B : Type u} (R : B → B → Prop) (x y : B) : Prop :=
+  ¬R y x
+
+/-- Scott 1964, condition `(1_B)`: the certain event is strictly above the null event. -/
+def ProbNontrivial {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : Prop :=
+  R ⊤ ⊥ ∧ ¬R ⊥ ⊤
+
+/-- Scott 1964, condition `(2_B)`: every event is at least as likely as null. -/
+def ProbNonneg {B : Type u} [BooleanAlgebra B] (R : B → B → Prop) : Prop :=
+  ∀ x, R x ⊥
+
+/-- Scott 1964, condition `(3_B)`: qualitative probabilities are comparable. -/
+def ProbTotal {B : Type u} (R : B → B → Prop) : Prop :=
+  ∀ x y, R x y ∨ R y x
+
+open Classical in
+/-- Scott 1964, condition `(4_B)`.  The equality says that every atom occurs
+equally often on the two sides. -/
+def ProbCancellation {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop) : Prop :=
+  ∀ (n : ℕ) (x y : Fin (n + 1) → B),
+    (∀ a : B, IsAtom a →
+        (∑ i, if a ≤ x i then 1 else 0) =
+          (∑ i, if a ≤ y i then 1 else 0 : ℕ)) →
+      (∀ i, i ≠ finHead n → R (x i) (y i)) → R (y (finHead n)) (x (finHead n))
+
+/-- Transitivity, de Finetti's condition (iv). -/
+def ProbTransitive {B : Type u} (R : B → B → Prop) : Prop :=
+  ∀ ⦃x y z⦄, R x y → R y z → R x z
+
+/-- Invariance under adjoining one event disjoint from both sides, de Finetti's
+condition (v). -/
+def ProbDisjointUnionInvariant {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop) : Prop :=
+  ∀ ⦃x y z⦄, Disjoint z x → Disjoint z y →
+    (R x y ↔ R (x ⊔ z) (y ⊔ z))
+
+/-- De Finetti's five qualitative-probability axioms.  Condition (i) is
+literally `¬ R ⊥ ⊤`; it does not include Scott's additional `R ⊤ ⊥`
+conjunct from `(1_B)`. -/
+structure DeFinettiAxioms {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop) : Prop where
+  nontrivial : ¬R ⊥ ⊤
+  bottom : ∀ x, R x ⊥
+  total : ProbTotal R
+  transitive : ProbTransitive R
+  disjointUnionInvariant : ProbDisjointUnionInvariant R
+
+theorem IsProbability.compl {B : Type u} [BooleanAlgebra B] {μ : B → ℝ}
+    (hμ : IsProbability μ) (x : B) : μ xᶜ = 1 - μ x := by
+  classical
+  have hd : Disjoint x xᶜ := disjoint_compl_right
+  have h := hμ.additive x xᶜ hd
+  rw [sup_compl_eq_top, hμ.top] at h
+  linarith
+
+/-- A nonnegative signed charge is monotone on events. -/
+theorem IsSignedCharge.mono_of_nonnegative {B : Type u} [BooleanAlgebra B]
+    {μ : B → ℝ} (hμ : IsSignedCharge μ) (hn : IsNonnegative μ)
+    ⦃x y : B⦄ (hxy : x ≤ y) : μ x ≤ μ y := by
+  classical
+  have hd : Disjoint x (y \ x) := by
+    classical
+    rw [disjoint_iff_inf_le]
+    simp
+  have hy : x ⊔ (y \ x) = y := by
+    classical
+    exact sup_sdiff_cancel_right hxy
+  rw [← hy, hμ.additive _ _ hd]
+  exact le_add_of_nonneg_right (hn _)
+
+theorem IsProbability.mono {B : Type u} [BooleanAlgebra B]
+    {μ : B → ℝ} (hμ : IsProbability μ) ⦃x y : B⦄ (hxy : x ≤ y) :
+    μ x ≤ μ y :=
+  hμ.isSignedCharge.mono_of_nonnegative hμ.nonnegative hxy
+
+theorem IsProbability.le_one {B : Type u} [BooleanAlgebra B]
+    {μ : B → ℝ} (hμ : IsProbability μ) (x : B) : μ x ≤ 1 :=
+  by simpa [hμ.top] using hμ.mono (show x ≤ (⊤ : B) from le_top)
+
+theorem RealizableProbability.nonnegative {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    ∃ μ : B → ℝ, IsFinitelyAdditiveProbability μ ∧
+      ∀ x y, R x y ↔ μ x ≥ μ y :=
+  hR
+
+theorem RealizableProbability.probNonneg {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    ProbNonneg R := by
+  classical
+  rcases hR with ⟨μ, hμ, hrep⟩
+  intro x
+  apply (hrep x ⊥).2
+  simpa [hμ.bot] using hμ.nonnegative x
+
+theorem RealizableProbability.probTotal {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) : ProbTotal R := by
+  classical
+  rcases hR with ⟨μ, -, hrep⟩
+  intro x y
+  rcases le_total (μ y) (μ x) with h | h
+  · exact Or.inl ((hrep x y).2 h)
+  · exact Or.inr ((hrep y x).2 h)
+
+theorem RealizableProbability.probNontrivial {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    ProbNontrivial R := by
+  classical
+  rcases hR with ⟨μ, hμ, hrep⟩
+  constructor
+  · exact (hrep ⊤ ⊥).2 (by rw [hμ.top, hμ.bot]; norm_num)
+  · intro h
+    have := (hrep ⊥ ⊤).1 h
+    rw [hμ.top, hμ.bot] at this
+    norm_num at this
+
+theorem RealizableProbability.probTransitive {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) : ProbTransitive R := by
+  classical
+  rcases hR with ⟨μ, -, hrep⟩
+  intro x y z hxy hyz
+  exact (hrep x z).2 (((hrep y z).1 hyz).trans ((hrep x y).1 hxy))
+
+theorem RealizableProbability.disjointUnionInvariant {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    ProbDisjointUnionInvariant R := by
+  classical
+  rcases hR with ⟨μ, hμ, hrep⟩
+  intro x y z hzx hzy
+  rw [hrep x y, hrep (x ⊔ z) (y ⊔ z)]
+  rw [hμ.additive x z hzx.symm, hμ.additive y z hzy.symm]
+  constructor <;> intro h <;> linarith
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Probability/Finite.lean b/LeanPool/ScottMeasurement/Probability/Finite.lean
new file mode 100644
index 0000000000..c9a4f72706
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Finite.lean
@@ -0,0 +1,495 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Probability.Atoms
+public import LeanPool.ScottMeasurement.LinearInequalities.ScottTheorems
+
+/-!
+# Finite qualitative probability
+
+This file isolates the last step of Scott's proof: a separating functional on
+atom vectors is normalized to a finitely additive probability.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures
+
+open scoped BigOperators
+
+noncomputable section
+
+open LinearInequalities
+
+/-- Linear-functional representation of a qualitative relation on event
+characteristic vectors. -/
+def AtomLinearRepresentation {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop) : Prop :=
+  ∃ φ : ({a : B // IsAtom a} → ℝ) →ₗ[ℝ] ℝ,
+    ∀ x y, R x y ↔ φ (atomVector x) ≥ φ (atomVector y)
+
+open Classical in
+/-- Integration of atom vectors against arbitrary real-valued atom weights. -/
+def atomWeightFunctional {B : Type u} [BooleanAlgebra B] [Fintype B]
+    (μ : B → ℝ) : ({a : B // IsAtom a} → ℝ) →ₗ[ℝ] ℝ where
+  toFun v := ∑ a, v a * μ a
+  map_add' u v := by
+    classical
+    simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
+  map_smul' c v := by
+    classical
+    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
+    symm
+    rw [Finset.mul_sum]
+    apply Finset.sum_congr rfl
+    intro a ha
+    ring
+
+open Classical in
+@[simp]
+theorem atomWeightFunctional_apply
+    {B : Type u} [BooleanAlgebra B] [Fintype B] (μ : B → ℝ)
+    (v : {a : B // IsAtom a} → ℝ) :
+    atomWeightFunctional μ v = ∑ a, v a * μ a :=
+  rfl
+
+/-- Atom-weight integration also recovers an arbitrary signed charge. -/
+theorem atomWeightFunctional_atomVector_signed
+    {B : Type u} [BooleanAlgebra B] [Fintype B]
+    {μ : B → ℝ} (hμ : IsSignedCharge μ) (x : B) :
+    atomWeightFunctional μ (atomVector x) = μ x := by
+  classical
+  rw [hμ.eq_sum_atoms x]
+  simp only [atomWeightFunctional_apply, atomVector_apply, atomsBelow]
+  rw [Finset.sum_filter]
+  apply Finset.sum_congr rfl
+  intro a ha
+  by_cases hax : (a : B) ≤ x <;> simp [hax]
+
+theorem atomWeightFunctional_atomVector
+    {B : Type u} [BooleanAlgebra B] [Fintype B]
+    {μ : B → ℝ} (hμ : IsProbability μ) (x : B) :
+    atomWeightFunctional μ (atomVector x) = μ x :=
+  atomWeightFunctional_atomVector_signed hμ.isSignedCharge x
+
+theorem RealizableSignedCharge.atomLinearRepresentation
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : RealizableSignedCharge R) :
+    AtomLinearRepresentation R := by
+  classical
+  let := Fintype.ofFinite B
+  rcases hR with ⟨μ, hμ, hrep⟩
+  refine ⟨atomWeightFunctional μ, ?_⟩
+  intro x y
+  rw [atomWeightFunctional_atomVector_signed hμ,
+    atomWeightFunctional_atomVector_signed hμ]
+  exact hrep x y
+
+theorem RealizableProbability.atomLinearRepresentation
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    AtomLinearRepresentation R :=
+  hR.realizableSignedCharge.atomLinearRepresentation
+
+/-- A linear representation on atom vectors induces a signed charge directly.
+No division by the charge of `⊤` is needed. -/
+theorem signedCharge_of_atomLinearRepresentation
+    {B : Type u} [BooleanAlgebra B] {R : B → B → Prop}
+    (hR : AtomLinearRepresentation R) :
+    RealizableSignedCharge R := by
+  classical
+  rcases hR with ⟨φ, hrep⟩
+  let μ : B → ℝ := fun x ↦ φ (atomVector x)
+  refine ⟨μ, ?_, ?_⟩
+  · refine ⟨?_, ?_⟩
+    · simp [μ, atomVector_bot]
+    · intro x y hxy
+      simp only [μ, atomVector_sup_of_disjoint hxy, map_add]
+  · exact hrep
+
+/-- A nondegenerate atom-functional representation normalizes to a finitely
+additive probability without changing any comparisons. -/
+theorem probability_of_atomLinearRepresentation {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop}
+    (hR : AtomLinearRepresentation R)
+    (hnt : ProbNontrivial R) (hn : ProbNonneg R) :
+    RealizableProbability R := by
+  classical
+  rcases hR with ⟨φ, hrep⟩
+  have hbot : φ (atomVector (⊥ : B)) = 0 := by rw [atomVector_bot, map_zero]
+  have htop : φ (atomVector (⊤ : B)) > 0 := by
+    classical
+    have hge := (hrep ⊤ ⊥).1 hnt.1
+    have hnle := fun h ↦ hnt.2 ((hrep ⊥ ⊤).2 h)
+    rw [hbot] at hge hnle
+    exact lt_of_not_ge hnle
+  let μ : B → ℝ := fun x ↦ φ (atomVector x) / φ (atomVector (⊤ : B))
+  refine ⟨μ, ?_, ?_⟩
+  · refine ⟨?_, ?_, ?_, ?_⟩
+    · simp [μ, atomVector_bot]
+    · simp [μ, ne_of_gt htop]
+    · intro x y hxy
+      change φ (atomVector (x ⊔ y)) / φ (atomVector (⊤ : B)) =
+        φ (atomVector x) / φ (atomVector (⊤ : B)) +
+          φ (atomVector y) / φ (atomVector (⊤ : B))
+      rw [atomVector_sup_of_disjoint hxy, map_add, add_div]
+    · intro x
+      have hx := (hrep x ⊥).1 (hn x)
+      rw [hbot] at hx
+      exact div_nonneg hx htop.le
+  · intro x y
+    rw [hrep]
+    change φ (atomVector y) ≤ φ (atomVector x) ↔
+      φ (atomVector y) / φ (atomVector (⊤ : B)) ≤
+        φ (atomVector x) / φ (atomVector (⊤ : B))
+    exact (div_le_div_iff_of_pos_right htop).symm
+
+/-- Condition `(2_B)` makes the normalized signed measure nonnegative. -/
+theorem nonnegative_probability_of_atomLinearRepresentation
+    {B : Type u} [BooleanAlgebra B] {R : B → B → Prop}
+    (hR : AtomLinearRepresentation R) (hnt : ProbNontrivial R)
+    (hn : ProbNonneg R) :
+    ∃ μ : B → ℝ, IsFinitelyAdditiveProbability μ ∧
+      ∀ x y, R x y ↔ μ x ≥ μ y :=
+  probability_of_atomLinearRepresentation hR hnt hn
+
+open Classical in
+/-- Every atom-functional representation satisfies Scott's cancellation
+scheme.  This is the easy direction of the finite separation theorem. -/
+theorem AtomLinearRepresentation.cancellation
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : AtomLinearRepresentation R) :
+    ∀ (n : ℕ) (x y : Fin (n + 1) → B),
+      (∀ a : B, IsAtom a →
+        (∑ i, if a ≤ x i then 1 else 0) =
+          (∑ i, if a ≤ y i then 1 else 0 : ℕ)) →
+      (∀ i, i ≠ finHead n → R (x i) (y i)) →
+        R (y (finHead n)) (x (finHead n)) := by
+  classical
+  rcases hR with ⟨φ, hrep⟩
+  intro n x y hcount hweak
+  have hvectors :
+      (∑ i, atomVector (x i)) = ∑ i, atomVector (y i) :=
+    (sum_atomVector_eq_iff (n + 1) x y).2 hcount
+  have hsums :
+      ∑ i, φ (atomVector (x i)) = ∑ i, φ (atomVector (y i)) := by
+    classical
+    simpa only [map_sum] using congrArg φ hvectors
+  have hrest :
+      ∑ i ∈ (Finset.univ.erase (finHead n)),
+          φ (atomVector (y i)) ≤
+        ∑ i ∈ (Finset.univ.erase (finHead n)),
+          φ (atomVector (x i)) := by
+    classical
+    apply Finset.sum_le_sum
+    intro i hi
+    have hi0 : i ≠ finHead n := by simpa using (Finset.mem_erase.mp hi).1
+    exact (hrep (x i) (y i)).1 (hweak i hi0)
+  apply (hrep (y (finHead n)) (x (finHead n))).2
+  have hzero : finHead n ∈ Finset.univ := Finset.mem_univ _
+  have hx := Finset.sum_erase_add _ (fun i ↦ φ (atomVector (x i))) hzero
+  have hy := Finset.sum_erase_add _ (fun i ↦ φ (atomVector (y i))) hzero
+  linarith
+
+theorem AtomLinearRepresentation.probCancellation
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : AtomLinearRepresentation R) :
+    ProbCancellation R :=
+  hR.cancellation
+
+/-- The atom-count formulation can equivalently be supplied as an equality
+of sums of characteristic vectors. -/
+theorem ProbCancellation.of_atomVector_sum
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : ProbCancellation R)
+    (n : ℕ) (x y : Fin (n + 1) → B)
+    (hsum : (∑ i, atomVector (x i)) = ∑ i, atomVector (y i))
+    (hweak : ∀ i, i ≠ finHead n → R (x i) (y i)) :
+    R (y (finHead n)) (x (finHead n)) :=
+  hR n x y ((sum_atomVector_eq_iff (n + 1) x y).1 hsum) hweak
+
+/-- Scott cancellation alone implies reflexivity. -/
+theorem ProbCancellation.refl
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : ProbCancellation R) (x : B) :
+    R x x := by
+  classical
+  apply hR.of_atomVector_sum 0 (fun _ ↦ x) (fun _ ↦ x)
+  · rfl
+  · intro i hi
+    exact False.elim (hi (by simpa [finHead_eq_zero] using Fin.eq_zero i))
+
+/-- Scott cancellation implies de Finetti transitivity. -/
+theorem ProbCancellation.transitive
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : ProbCancellation R) :
+    ProbTransitive R := by
+  classical
+  intro x y z hxy hyz
+  let xs : Fin 3 → B := ![z, x, y]
+  let ys : Fin 3 → B := ![x, y, z]
+  apply hR.of_atomVector_sum 2 xs ys
+  · simp [xs, ys, Fin.sum_univ_succ]
+    abel
+  · intro i hi
+    fin_cases i
+    · exact False.elim (hi (finHead_eq_zero _).symm)
+    · exact hxy
+    · exact hyz
+
+/-- Scott cancellation gives both directions of de Finetti's invariance
+under adjoining a common disjoint event. -/
+theorem ProbCancellation.disjointUnionInvariant
+    {B : Type u} [BooleanAlgebra B]
+    {R : B → B → Prop} (hR : ProbCancellation R) :
+    ProbDisjointUnionInvariant R := by
+  classical
+  intro x y z hzx hzy
+  have hxz : atomVector (x ⊔ z) = atomVector x + atomVector z :=
+    atomVector_sup_of_disjoint hzx.symm
+  have hyz : atomVector (y ⊔ z) = atomVector y + atomVector z :=
+    atomVector_sup_of_disjoint hzy.symm
+  constructor
+  · intro hxy
+    let xs : Fin 2 → B := ![y ⊔ z, x]
+    let ys : Fin 2 → B := ![x ⊔ z, y]
+    apply hR.of_atomVector_sum 1 xs ys
+    · simp [xs, ys, Fin.sum_univ_succ, hxz, hyz]
+      abel
+    · intro i hi
+      fin_cases i
+      · exact False.elim (hi (finHead_eq_zero _).symm)
+      · exact hxy
+  · intro hxy
+    let xs : Fin 2 → B := ![y, x ⊔ z]
+    let ys : Fin 2 → B := ![x, y ⊔ z]
+    apply hR.of_atomVector_sum 1 xs ys
+    · simp [xs, ys, Fin.sum_univ_succ, hxz, hyz]
+      abel
+    · intro i hi
+      fin_cases i
+      · exact False.elim (hi (finHead_eq_zero _).symm)
+      · exact hxy
+
+/-! ## Reduction to Scott's explicit §1 relation theorem -/
+
+open Classical in
+/-- The event represented by an atom vector in the range of `atomVector`.
+Outside that range its value is immaterial. -/
+def eventOfAtomVector {B : Type u} [BooleanAlgebra B]
+    (v : {a : B // IsAtom a} → ℝ) : B :=
+  if h : ∃ x, atomVector x = v then Classical.choose h else ⊥
+
+@[simp]
+theorem eventOfAtomVector_atomVector
+    {B : Type u} [BooleanAlgebra B] [Finite B] (x : B) :
+    eventOfAtomVector (atomVector x) = x := by
+  classical
+  let := Fintype.ofFinite B
+  unfold eventOfAtomVector
+  split
+  · rename_i h
+    exact atomVector_injective (Classical.choose_spec h)
+  · rename_i h
+    exact False.elim (h ⟨x, rfl⟩)
+
+/-- The relation transported from events to their characteristic vectors. -/
+def AtomVectorRelation {B : Type u} [BooleanAlgebra B]
+    (R : B → B → Prop)
+    (u v : {a : B // IsAtom a} → ℝ) : Prop :=
+  R (eventOfAtomVector u) (eventOfAtomVector v)
+
+@[simp]
+theorem atomVectorRelation_atomVectors
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    (R : B → B → Prop) (x y : B) :
+    AtomVectorRelation R (atomVector x) (atomVector y) ↔ R x y := by
+  classical
+  let := Fintype.ofFinite B
+  simp [AtomVectorRelation]
+
+theorem atomVector_range_finite
+    {B : Type u} [BooleanAlgebra B] [Finite B] :
+    (Set.range (atomVector :
+      B → ({a : B // IsAtom a} → ℝ))).Finite := by
+  classical
+  let := Fintype.ofFinite B
+  exact Set.finite_range _
+
+theorem atomVector_range_rational
+    {B : Type u} [BooleanAlgebra B] :
+    IsRationalSet (Set.range (atomVector :
+      B → ({a : B // IsAtom a} → ℝ))) := by
+  classical
+  rintro v ⟨x, rfl⟩ a
+  by_cases h : (a : B) ≤ x
+  · exact ⟨1, by simp [atomVector, h]⟩
+  · exact ⟨0, by simp [atomVector, h]⟩
+
+theorem atomVectorRelation_complete
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : ProbTotal R) :
+    RelationComplete
+      (Set.range (atomVector :
+        B → ({a : B // IsAtom a} → ℝ)))
+      (AtomVectorRelation R) := by
+  classical
+  let := Fintype.ofFinite B
+  rintro u ⟨x, rfl⟩ v ⟨y, rfl⟩
+  simpa only [atomVectorRelation_atomVectors] using hR x y
+
+theorem atomVectorRelation_sequenceCancellation
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : ProbCancellation R) :
+    RelationSequenceCancellation
+      (Set.range (atomVector :
+        B → ({a : B // IsAtom a} → ℝ)))
+      (AtomVectorRelation R) := by
+  classical
+  intro n u v hu hv huv hsum j
+  let e : Equiv.Perm (Fin (n + 1)) := Equiv.swap (finHead n) j
+  let x : Fin (n + 1) → B := fun i ↦ eventOfAtomVector (u (e i))
+  let y : Fin (n + 1) → B := fun i ↦ eventOfAtomVector (v (e i))
+  have hxu : ∀ i, atomVector (x i) = u (e i) := by
+    classical
+    intro i
+    rcases hu (e i) with ⟨xi, hxi⟩
+    change atomVector (eventOfAtomVector (u (e i))) = u (e i)
+    rw [← hxi]
+    simp
+  have hyv : ∀ i, atomVector (y i) = v (e i) := by
+    classical
+    intro i
+    rcases hv (e i) with ⟨yi, hyi⟩
+    change atomVector (eventOfAtomVector (v (e i))) = v (e i)
+    rw [← hyi]
+    simp
+  change R (eventOfAtomVector (v j)) (eventOfAtomVector (u j))
+  apply hR.of_atomVector_sum n x y
+  · simp only [hxu, hyv]
+    rw [Equiv.sum_comp e, Equiv.sum_comp e, hsum]
+  · intro i hi
+    change R (eventOfAtomVector (u (e i))) (eventOfAtomVector (v (e i)))
+    exact huv (e i)
+
+theorem atomLinearRepresentation_of_relationRealizable
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop}
+    (hreal : RelationRealizable
+      (Set.range (atomVector :
+        B → ({a : B // IsAtom a} → ℝ)))
+      (AtomVectorRelation R)) :
+    AtomLinearRepresentation R := by
+  classical
+  let := Fintype.ofFinite B
+  rcases hreal with ⟨φ, hφ⟩
+  refine ⟨φ, ?_⟩
+  intro x y
+  simpa only [atomVectorRelation_atomVectors] using
+    hφ (atomVector x) (Set.mem_range_self x)
+      (atomVector y) (Set.mem_range_self y)
+
+/-- Scott's `(3_B)` and `(4_B)` produce a linear representation on atom
+vectors, without any positivity or nondegeneracy assumptions. -/
+theorem atomLinearRepresentation_of_total_cancellation
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop}
+    (htotal : ProbTotal R) (hcancel : ProbCancellation R) :
+    AtomLinearRepresentation R := by
+  classical
+  have hreal : RelationRealizable
+      (Set.range (atomVector :
+        B → ({a : B // IsAtom a} → ℝ)))
+      (AtomVectorRelation R) :=
+    (scott_theorem_1_3 atomVector_range_finite atomVector_range_rational).2
+      ⟨atomVectorRelation_complete htotal,
+        atomVectorRelation_sequenceCancellation hcancel⟩
+  exact atomLinearRepresentation_of_relationRealizable hreal
+
+theorem RealizableProbability.probCancellation
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    ProbCancellation R :=
+  hR.atomLinearRepresentation.probCancellation
+
+theorem RealizableProbability.finiteNecessary
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧ ProbCancellation R :=
+  ⟨hR.probNontrivial, hR.probNonneg, hR.probTotal, hR.probCancellation⟩
+
+theorem RealizableSignedCharge.finiteNecessary
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop} (hR : RealizableSignedCharge R) :
+    ProbTotal R ∧ ProbCancellation R := by
+  classical
+  have hlin := hR.atomLinearRepresentation
+  constructor
+  · rcases hlin with ⟨φ, hrep⟩
+    intro x y
+    exact (le_total (φ (atomVector y)) (φ (atomVector x))).imp
+      ((hrep x y).2) ((hrep y x).2)
+  · exact hlin.probCancellation
+
+/-- Scott's p.15 signed-measure claim: `(3_B)` and `(4_B)` are exactly the
+conditions for representation by a finitely additive signed charge. -/
+theorem scott_p15_signed_charge
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    (R : B → B → Prop) :
+    RealizableSignedCharge R ↔ ProbTotal R ∧ ProbCancellation R := by
+  classical
+  constructor
+  · exact RealizableSignedCharge.finiteNecessary
+  · rintro ⟨htotal, hcancel⟩
+    exact signedCharge_of_atomLinearRepresentation
+      (atomLinearRepresentation_of_total_cancellation htotal hcancel)
+
+/-- Scott's p.15 claim with literal vector-sum cancellation `(4_B)`. -/
+theorem scott_p15_signed_charge_vector
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    (R : B → B → Prop) :
+    RealizableSignedCharge R ↔ ProbTotal R ∧ ProbVectorCancellation R := by
+  classical
+  let := Fintype.ofFinite B
+  rw [scott_p15_signed_charge,
+    probVectorCancellation_iff_probCancellation]
+
+theorem probability_of_finite_axioms
+    {B : Type u} [BooleanAlgebra B] [Finite B]
+    {R : B → B → Prop}
+    (hnt : ProbNontrivial R) (hn : ProbNonneg R)
+    (htotal : ProbTotal R) (hcancel : ProbCancellation R) :
+    RealizableProbability R :=
+  probability_of_atomLinearRepresentation
+    (atomLinearRepresentation_of_total_cancellation htotal hcancel) hnt hn
+
+/-- **Scott 1964, Theorem 4.1 (subjective probability).** -/
+theorem theorem_4_1 {B : Type u} [BooleanAlgebra B] [Finite B]
+    (R : B → B → Prop) :
+    RealizableProbability R ↔
+      ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧ ProbCancellation R := by
+  classical
+  constructor
+  · exact RealizableProbability.finiteNecessary
+  · rintro ⟨hnt, hn, htotal, hcancel⟩
+    exact probability_of_finite_axioms hnt hn htotal hcancel
+
+/-- **Scott 1964, Theorem 4.1**, with `(4_B)` stated literally as equality
+of sums of atom vectors. -/
+theorem theorem_4_1_vector {B : Type u} [BooleanAlgebra B] [Finite B]
+    (R : B → B → Prop) :
+    RealizableProbability R ↔
+      ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧
+        ProbVectorCancellation R := by
+  classical
+  let := Fintype.ofFinite B
+  rw [theorem_4_1, probVectorCancellation_iff_probCancellation]
+
+end
+
+end Scott1964.MeasurementStructures
diff --git a/LeanPool/ScottMeasurement/Probability/Infinite/EventSpace.lean b/LeanPool/ScottMeasurement/Probability/Infinite/EventSpace.lean
new file mode 100644
index 0000000000..2071cfb7b9
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Infinite/EventSpace.lean
@@ -0,0 +1,395 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Probability.Basic
+public import Mathlib.Order.PrimeSeparator
+public import Mathlib.Topology.Bornology.BoundedOperation
+public import Mathlib.Topology.ContinuousMap.Bounded.Normed
+public import Mathlib.Analysis.LocallyConvex.Basic
+
+/-!
+# Universal event spaces for an infinite Boolean algebra
+
+This file supplies two complementary universal realizations of a Boolean algebra.
+
+* `PrimePoint B` and `stoneIndicator` are the usual Stone representation by
+  characteristic functions on prime ideals.  This representation is faithful and is
+  convenient for stating Scott's finite-sum cancellation condition.
+* `ProbabilityPoint B` and `eventVector` evaluate an event at every finitely additive
+  probability.  Their real span is a normed order-unit space on which probabilities
+  are exactly the point-evaluation positive normalized continuous linear functionals.
+
+The second realization is used for the direct state correspondence
+below.  Constructing the analogous functional on the Stone-indicator span requires
+the separate simple-function integration theorem for arbitrary finitely additive
+charges.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures.Probability.Infinite
+
+open scoped BoundedContinuousFunction
+open Set
+
+noncomputable section
+
+universe u
+
+variable (B : Type u) [BooleanAlgebra B]
+
+/-! ## The probability-evaluation event space -/
+
+/-- A point of the universal probability-evaluation space. -/
+def ProbabilityPoint :=
+  {μ : B → ℝ // IsFinitelyAdditiveProbability μ}
+
+instance instTopologicalSpaceProbabilityPoint : TopologicalSpace (ProbabilityPoint B) := ⊥
+
+theorem probabilityPoint_discrete_eq_bot :
+    instTopologicalSpaceProbabilityPoint B = ⊥ :=
+  rfl
+
+instance instDiscreteTopologyProbabilityPoint : DiscreteTopology (ProbabilityPoint B) where
+  eq_bot := probabilityPoint_discrete_eq_bot B
+
+theorem probabilityPoint_nonnegative (p : ProbabilityPoint B) (a : B) :
+    0 ≤ p.1 a :=
+  p.2.nonnegative a
+
+theorem probabilityPoint_le_one (p : ProbabilityPoint B) (a : B) :
+    p.1 a ≤ 1 :=
+  p.2.le_one a
+
+theorem eventVector_dist_le_one (a : B) (p q : ProbabilityPoint B) :
+    dist (p.1 a) (q.1 a) ≤ 1 := by
+  rw [Real.dist_eq, abs_sub_le_iff]
+  constructor <;>
+    linarith [probabilityPoint_nonnegative B p a,
+      probabilityPoint_nonnegative B q a,
+      probabilityPoint_le_one B p a,
+      probabilityPoint_le_one B q a]
+
+/-- The universal evaluation vector `μ ↦ μ(a)` of an event. -/
+def eventVector (a : B) : ProbabilityPoint B →ᵇ ℝ :=
+  BoundedContinuousFunction.mkOfDiscrete (fun p => p.1 a) 1
+    (eventVector_dist_le_one B a)
+
+/-- The real normed space generated by universal event-evaluation vectors. -/
+def EventSpan : Submodule ℝ (ProbabilityPoint B →ᵇ ℝ) :=
+  Submodule.span ℝ (Set.range (eventVector B))
+
+/-- The event vector as an element of `EventSpan`. -/
+def event (a : B) : EventSpan B :=
+  ⟨eventVector B a, Submodule.subset_span (Set.mem_range_self a)⟩
+
+/-! ## Stone points and indicator vectors -/
+
+/-- A Stone point of `B`, presented as a prime (equivalently maximal) ideal. -/
+structure PrimePoint where
+  /-- The ideal of events absent at this Stone point. -/
+  ideal : Order.Ideal B
+  isPrime : ideal.IsPrime
+
+instance : TopologicalSpace (PrimePoint B) := ⊥
+
+instance : DiscreteTopology (PrimePoint B) := ⟨rfl⟩
+
+/-- The `0`/`1` value of an event at a Stone point. -/
+def stoneValue (a : B) (p : PrimePoint B) : ℝ :=
+  @ite ℝ (a ∈ p.ideal) (Classical.propDecidable (a ∈ p.ideal)) 0 1
+
+/-- The characteristic vector of an event on the Stone points of `B`.
+
+The convention is that a point lies in the event `a` exactly when its prime ideal
+does not contain `a`.
+-/
+def stoneIndicator (a : B) : PrimePoint B →ᵇ ℝ :=
+  by
+    classical
+    exact BoundedContinuousFunction.mkOfDiscrete
+      (stoneValue B a) 1 (by
+        intro p q
+        simp only [stoneValue, Real.dist_eq]
+        split <;> split <;> norm_num)
+
+@[simp]
+theorem stoneIndicator_apply (a : B) (p : PrimePoint B) :
+    stoneIndicator B a p = stoneValue B a p :=
+  rfl
+
+@[simp]
+theorem stoneIndicator_bot : stoneIndicator B (⊥ : B) = 0 := by
+  classical
+  ext p
+  simp [stoneIndicator, stoneValue]
+
+@[simp]
+theorem stoneIndicator_top : stoneIndicator B (⊤ : B) = 1 := by
+  classical
+  ext p
+  have hp : (⊤ : B) ∉ p.ideal := p.isPrime.toIsProper.top_notMem
+  simp [stoneIndicator, stoneValue, hp]
+
+@[simp]
+theorem stoneIndicator_sup_of_disjoint {a b : B} (h : Disjoint a b) :
+    stoneIndicator B (a ⊔ b) = stoneIndicator B a + stoneIndicator B b := by
+  classical
+  ext p
+  have hp := p.isPrime
+  by_cases ha : a ∈ p.ideal
+  · by_cases hb : b ∈ p.ideal
+    · simp [stoneIndicator, stoneValue, ha, hb, Order.Ideal.sup_mem ha hb]
+    · have hab : a ⊔ b ∉ p.ideal := fun hs => hb (p.ideal.lower le_sup_right hs)
+      simp [stoneIndicator, stoneValue, ha, hb, hab]
+  · by_cases hb : b ∈ p.ideal
+    · have hab : a ⊔ b ∉ p.ideal := fun hs => ha (p.ideal.lower le_sup_left hs)
+      simp [stoneIndicator, stoneValue, ha, hb, hab]
+    · have hab : a ⊔ b ∉ p.ideal := fun hs => ha (p.ideal.lower le_sup_left hs)
+      have hnotboth : ¬(a ∉ p.ideal ∧ b ∉ p.ideal) := by
+        intro hn
+        have hi : a ⊓ b ∈ p.ideal := by
+          rw [h.eq_bot]
+          exact p.ideal.bot_mem
+        exact (hp.mem_or_mem hi).elim hn.1 hn.2
+      exact (hnotboth ⟨ha, hb⟩).elim
+
+/-- Stone indicators separate events, so the Stone representation is faithful. -/
+theorem stoneIndicator_injective : Function.Injective (stoneIndicator B) := by
+  classical
+  intro a b hab
+  apply le_antisymm
+  · by_contra hle
+    have hd : Disjoint
+        ((Order.PFilter.principal a : Order.PFilter B) : Set B)
+        ((Order.Ideal.principal b : Order.Ideal B) : Set B) := by
+      rw [Set.disjoint_left]
+      intro x hax hxb
+      exact hle ((Order.PFilter.mem_principal.mp hax).trans
+        (Order.Ideal.mem_principal.mp hxb))
+    obtain ⟨J, hJ, hbJ, hdis⟩ :=
+      DistribLattice.prime_ideal_of_disjoint_filter_ideal hd
+    let p : PrimePoint B := ⟨J, hJ⟩
+    have hbin : b ∈ J := hbJ Order.Ideal.mem_principal_self
+    have hain : a ∉ J := by
+      intro haJ
+      exact Set.disjoint_left.mp hdis
+        (show a ∈ Order.PFilter.principal a by
+          rw [Order.PFilter.mem_principal]) haJ
+    have := congrArg (fun f : PrimePoint B →ᵇ ℝ => f p) hab
+    simp [stoneIndicator, stoneValue, p, hbin, hain] at this
+  · by_contra hle
+    have hd : Disjoint
+        ((Order.PFilter.principal b : Order.PFilter B) : Set B)
+        ((Order.Ideal.principal a : Order.Ideal B) : Set B) := by
+      rw [Set.disjoint_left]
+      intro x hbx hxa
+      exact hle ((Order.PFilter.mem_principal.mp hbx).trans
+        (Order.Ideal.mem_principal.mp hxa))
+    obtain ⟨J, hJ, haJ, hdis⟩ :=
+      DistribLattice.prime_ideal_of_disjoint_filter_ideal hd
+    let p : PrimePoint B := ⟨J, hJ⟩
+    have hain : a ∈ J := haJ Order.Ideal.mem_principal_self
+    have hbin : b ∉ J := by
+      intro hbJ
+      exact Set.disjoint_left.mp hdis
+        (show b ∈ Order.PFilter.principal b by
+          rw [Order.PFilter.mem_principal]) hbJ
+    have := congrArg (fun f : PrimePoint B →ᵇ ℝ => f p) hab
+    simp [stoneIndicator, stoneValue, p, hbin, hain] at this
+
+/-- Equality of two finite sums of event indicators. -/
+def IndicatorSumEqual {ι : Type*} [Fintype ι] (x y : ι → B) : Prop :=
+  ∑ i, stoneIndicator B (x i) = ∑ i, stoneIndicator B (y i)
+
+theorem indicatorSumEqual_iff {ι : Type*} [Fintype ι] (x y : ι → B) :
+    IndicatorSumEqual B x y ↔
+      ∀ p : PrimePoint B,
+        ∑ i, stoneValue B (x i) p =
+          ∑ i, stoneValue B (y i) p := by
+  classical
+  constructor
+  · intro h p
+    have := congrArg (fun f : PrimePoint B →ᵇ ℝ => f p) h
+    simpa [IndicatorSumEqual, stoneIndicator, stoneValue] using this
+  · intro h
+    apply BoundedContinuousFunction.ext
+    intro p
+    simpa [IndicatorSumEqual, stoneIndicator, stoneValue] using h p
+
+/-- The two-valued finitely additive probability associated with a Stone point. -/
+def primeProbability (p : PrimePoint B) : ProbabilityPoint B := by
+  refine ⟨fun a => stoneValue B a p, ?_⟩
+  refine
+    { bot := by simp [stoneValue]
+      top := by
+        have hp : (⊤ : B) ∉ p.ideal := p.isPrime.toIsProper.top_notMem
+        simp [stoneValue, hp]
+      additive := ?_
+      nonnegative := ?_ }
+  · intro a b h
+    have hs := congrArg (fun f : PrimePoint B →ᵇ ℝ => f p)
+      (stoneIndicator_sup_of_disjoint B h)
+    simpa [stoneIndicator_apply] using hs
+  · intro a
+    simp only [stoneValue]
+    split <;> norm_num
+
+@[simp]
+theorem primeProbability_apply (p : PrimePoint B) (a : B) :
+    (primeProbability B p).1 a = stoneValue B a p :=
+  rfl
+
+@[simp]
+theorem eventVector_apply (a : B) (p : ProbabilityPoint B) :
+    eventVector B a p = p.1 a :=
+  rfl
+
+@[simp]
+theorem eventVector_bot : eventVector B (⊥ : B) = 0 := by
+  ext p
+  exact p.2.bot
+
+@[simp]
+theorem eventVector_top : eventVector B (⊤ : B) = 1 := by
+  ext p
+  exact p.2.top
+
+@[simp]
+theorem eventVector_sup_of_disjoint {a b : B} (h : Disjoint a b) :
+    eventVector B (a ⊔ b) = eventVector B a + eventVector B b := by
+  ext p
+  exact p.2.additive a b h
+
+/-- Probability-evaluation vectors are also a faithful representation of events. -/
+theorem eventVector_injective : Function.Injective (eventVector B) := by
+  intro a b hab
+  apply stoneIndicator_injective B
+  ext p
+  have h := congrArg (fun f : ProbabilityPoint B →ᵇ ℝ =>
+    f (primeProbability B p)) hab
+  exact h
+
+@[simp]
+theorem event_apply (a : B) (p : ProbabilityPoint B) :
+    (event B a : ProbabilityPoint B →ᵇ ℝ) p = p.1 a :=
+  rfl
+
+@[simp]
+theorem event_bot : event B (⊥ : B) = 0 := by
+  apply Subtype.ext
+  exact eventVector_bot B
+
+@[simp]
+theorem event_top_coe :
+    ((event B (⊤ : B) : EventSpan B) : ProbabilityPoint B →ᵇ ℝ) = 1 :=
+  eventVector_top B
+
+@[simp]
+theorem event_sup_of_disjoint {a b : B} (h : Disjoint a b) :
+    event B (a ⊔ b) = event B a + event B b := by
+  apply Subtype.ext
+  exact eventVector_sup_of_disjoint B h
+
+/-- Pointwise positivity for a functional on the event span. -/
+def IsPositive (L : EventSpan B →L[ℝ] ℝ) : Prop :=
+  ∀ f : EventSpan B,
+    (∀ p : ProbabilityPoint B, 0 ≤ (f : ProbabilityPoint B →ᵇ ℝ) p) →
+      0 ≤ L f
+
+/-- A positive normalized bounded linear functional on the universal event span. -/
+structure PositiveState where
+  /-- The continuous linear evaluator whose values on events give the probability. -/
+  functional : EventSpan B →L[ℝ] ℝ
+  positive : IsPositive B functional
+  normalized : functional (event B ⊤) = 1
+
+/-- Evaluation at a finitely additive probability is a positive normalized state. -/
+def probabilityToState (p : ProbabilityPoint B) : PositiveState B where
+  functional :=
+    (BoundedContinuousFunction.evalCLM ℝ p).comp (EventSpan B).subtypeL
+  positive := by
+    intro f hf
+    exact hf p
+  normalized := by
+    exact p.2.top
+
+@[ext]
+theorem PositiveState.ext {S T : PositiveState B}
+    (h : S.functional = T.functional) : S = T := by
+  cases S
+  cases T
+  simp_all
+
+/-- A positive normalized state restricts to a finitely additive probability on events. -/
+def stateToProbability (S : PositiveState B) : ProbabilityPoint B := by
+  refine ⟨fun a => S.functional (event B a), ?_⟩
+  refine
+    { bot := by simp
+      top := S.normalized
+      additive := ?_
+      nonnegative := ?_ }
+  · intro a b h
+    rw [event_sup_of_disjoint B h, map_add]
+  · intro a
+    apply S.positive
+    intro p
+    exact p.2.nonnegative a
+
+@[simp]
+theorem stateToProbability_apply (S : PositiveState B) (a : B) :
+    (stateToProbability B S).1 a = S.functional (event B a) :=
+  rfl
+
+@[simp]
+theorem stateToProbability_probabilityToState (p : ProbabilityPoint B) :
+    stateToProbability B (probabilityToState B p) = p := by
+  apply Subtype.ext
+  funext a
+  rfl
+
+theorem probabilityToState_stateToProbability (S : PositiveState B) :
+    probabilityToState B (stateToProbability B S) = S := by
+  cases S with
+  | mk L hpos hnorm =>
+      apply PositiveState.ext
+      apply ContinuousLinearMap.ext
+      intro f
+      change f.1 (stateToProbability B ⟨L, hpos, hnorm⟩) =
+        L f
+      refine Submodule.span_induction
+        (p := fun g hg =>
+          g (stateToProbability B ⟨L, hpos, hnorm⟩) =
+            L ⟨g, hg⟩) ?_ ?_ ?_ ?_ f.2
+      · intro g hg
+        rcases hg with ⟨a, rfl⟩
+        rfl
+      · change 0 = L 0
+        simp
+      · intro x y hx hy hx' hy'
+        change x (stateToProbability B ⟨L, hpos, hnorm⟩) +
+            y (stateToProbability B ⟨L, hpos, hnorm⟩) =
+          L (⟨x, hx⟩ + ⟨y, hy⟩)
+        rw [map_add, hx', hy']
+      · intro c x hx hx'
+        change c * x (stateToProbability B ⟨L, hpos, hnorm⟩) =
+          L (c • ⟨x, hx⟩)
+        rw [map_smul, hx']
+        simp [smul_eq_mul]
+
+/-- Finitely additive probabilities and positive normalized states on `EventSpan`
+are canonically equivalent. -/
+def probabilityStateEquiv : ProbabilityPoint B ≃ PositiveState B where
+  toFun := probabilityToState B
+  invFun := stateToProbability B
+  left_inv := stateToProbability_probabilityToState B
+  right_inv := probabilityToState_stateToProbability B
+
+end
+
+end Scott1964.MeasurementStructures.Probability.Infinite
diff --git a/LeanPool/ScottMeasurement/Probability/Infinite/HahnBanach.lean b/LeanPool/ScottMeasurement/Probability/Infinite/HahnBanach.lean
new file mode 100644
index 0000000000..04cf9a7218
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Infinite/HahnBanach.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import Mathlib.Analysis.LocallyConvex.Separation
+public import Mathlib.Analysis.Convex.Cone.Basic
+
+/-!
+# Hahn--Banach separation above a closed cone
+
+This is the analytic step used in the reconstructed infinite version of
+Scott's Theorem 4.1.  A closed convex set which is stable under translation
+by a closed cone and avoids zero admits a functional which is nonnegative on
+the cone and strictly positive on the set.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures.Probability.Infinite
+
+open Set
+
+noncomputable section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [LocallyConvexSpace ℝ E]
+
+/-- `K` is upward closed under translation by the cone `C`. -/
+def ConeUpperSet (C : ProperCone ℝ E) (K : Set E) : Prop :=
+  ∀ ⦃x c⦄, x ∈ K → c ∈ C → x + c ∈ K
+
+/-- The Hahn--Banach separation lemma in the exact form needed for Kelley's
+countable-cover argument. -/
+theorem exists_positive_separator_of_coneUpper
+    (C : ProperCone ℝ E) {K : Set E}
+    (hKne : K.Nonempty) (hKconv : Convex ℝ K) (hKclosed : IsClosed K)
+    (hKzero : (0 : E) ∉ K) (hupper : ConeUpperSet C K) :
+    ∃ f : StrongDual ℝ E,
+      (∀ c ∈ C, 0 ≤ f c) ∧ ∀ x ∈ K, 0 < f x := by
+  obtain ⟨f, u, hfu, hfK⟩ :=
+    geometric_hahn_banach_point_closed hKconv hKclosed hKzero
+  have hu : 0 < u := by simpa using hfu
+  rcases hKne with ⟨x₀, hx₀⟩
+  have hcone : ∀ c ∈ C, 0 ≤ f c := by
+    intro c hc
+    by_contra hneg
+    have hfc : f c < 0 := lt_of_not_ge hneg
+    have hden : 0 < -f c := neg_pos.mpr hfc
+    obtain ⟨n : ℕ, hn⟩ := exists_nat_gt ((f x₀ - u) / (-f c))
+    have hn' : f x₀ - u < (n : ℝ) * (-f c) :=
+      (div_lt_iff₀ hden).mp hn
+    have hnc : (n : ℝ) • c ∈ C :=
+      C.smul_mem hc (Nat.cast_nonneg n)
+    have hxnc : x₀ + (n : ℝ) • c ∈ K := hupper hx₀ hnc
+    have hsep := hfK _ hxnc
+    rw [map_add, map_smul, smul_eq_mul] at hsep
+    linarith
+  refine ⟨f, hcone, ?_⟩
+  intro x hx
+  exact hu.trans (hfK x hx)
+
+end
+
+end Scott1964.MeasurementStructures.Probability.Infinite
diff --git a/LeanPool/ScottMeasurement/Probability/Infinite/Kelley.lean b/LeanPool/ScottMeasurement/Probability/Infinite/Kelley.lean
new file mode 100644
index 0000000000..729c3e29fa
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Infinite/Kelley.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Probability.Infinite.HahnBanach
+public import Mathlib.Analysis.Normed.Module.Dual
+
+/-!
+# A generalized Kelley cover
+
+The countable cover below is the explicit Archimedean hypothesis used in the
+reconstructed infinite theorem.  Each layer is a closed convex upper set over
+the weak-comparison cone and is bounded away from zero.  Hahn--Banach supplies
+one positive separator per nonempty layer.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures.Probability.Infinite
+
+open Set
+
+noncomputable section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [LocallyConvexSpace ℝ E]
+
+/-- Countable Kelley cover of strict-comparison vectors above a closed weak
+comparison cone. -/
+structure KelleyCover (C : ProperCone ℝ E) (S : Set E) where
+  /-- Closed convex layers separating the strict comparisons from zero. -/
+  layer : ℕ → Set E
+  strictInCone : S ⊆ C
+  covers : S ⊆ ⋃ n, layer n
+  convex : ∀ n, Convex ℝ (layer n)
+  closed : ∀ n, IsClosed (layer n)
+  avoidsZero : ∀ n, (0 : E) ∉ layer n
+  upper : ∀ n, ConeUpperSet C (layer n)
+
+/-- Hahn--Banach produces a positive separator for every layer, with the zero
+functional used harmlessly on empty layers. -/
+theorem KelleyCover.exists_separator_family {C : ProperCone ℝ E} {S : Set E}
+    (h : KelleyCover C S) :
+    ∃ f : ℕ → StrongDual ℝ E,
+      (∀ n c, c ∈ C → 0 ≤ f n c) ∧
+      (∀ n x, x ∈ h.layer n → 0 < f n x) := by
+  classical
+  have hex : ∀ n, ∃ f : StrongDual ℝ E,
+      (∀ c, c ∈ C → 0 ≤ f c) ∧
+      (∀ x, x ∈ h.layer n → 0 < f x) := by
+    intro n
+    by_cases hne : (h.layer n).Nonempty
+    · obtain ⟨f, hfC, hfK⟩ :=
+        exists_positive_separator_of_coneUpper C hne
+          (h.convex n) (h.closed n) (h.avoidsZero n) (h.upper n)
+      exact ⟨f, hfC, hfK⟩
+    · refine ⟨0, by simp, ?_⟩
+      intro x hx
+      exact (hne ⟨x, hx⟩).elim
+  choose f hf using hex
+  exact ⟨f, fun n c hc ↦ (hf n).1 c hc, fun n x hx ↦ (hf n).2 x hx⟩
+
+/-- A summable positive combination of the layer separators is nonnegative on
+the weak cone and strictly positive on every covered strict vector. -/
+theorem KelleyCover.exists_combined_separator
+    {C : ProperCone ℝ E} {S : Set E} (h : KelleyCover C S) :
+    ∃ F : StrongDual ℝ E,
+      (∀ c ∈ C, 0 ≤ F c) ∧ ∀ x ∈ S, 0 < F x := by
+  classical
+  obtain ⟨f, hfC, hfK⟩ := h.exists_separator_family
+  let w : ℕ → ℝ := fun n ↦ (1 / 2 : ℝ) ^ n / (1 + ‖f n‖)
+  let g : ℕ → StrongDual ℝ E := fun n ↦ w n • f n
+  have hwpos : ∀ n, 0 < w n := by
+    intro n
+    exact div_pos (pow_pos (by norm_num) _) (by positivity)
+  have hgnorm : ∀ n, ‖g n‖ ≤ (1 / 2 : ℝ) ^ n := by
+    intro n
+    have hb : 0 ≤ (1 / 2 : ℝ) ^ n := (pow_nonneg (by norm_num) _)
+    have hd : 0 < 1 + ‖f n‖ := by positivity
+    have hr : ‖f n‖ / (1 + ‖f n‖) ≤ 1 :=
+      (div_le_one hd).2 (by linarith [norm_nonneg (f n)])
+    change ‖w n • f n‖ ≤ (1 / 2 : ℝ) ^ n
+    rw [norm_smul, Real.norm_eq_abs, abs_of_pos (hwpos n)]
+    calc
+      w n * ‖f n‖ =
+          (1 / 2 : ℝ) ^ n * (‖f n‖ / (1 + ‖f n‖)) := by
+            dsimp [w]
+            ring
+      _ ≤ (1 / 2 : ℝ) ^ n * 1 := mul_le_mul_of_nonneg_left hr hb
+      _ = (1 / 2 : ℝ) ^ n := mul_one _
+  have hgeom : Summable (fun n : ℕ ↦ (1 / 2 : ℝ) ^ n) :=
+    summable_geometric_of_norm_lt_one (by norm_num)
+  have hnormsum : Summable (fun n ↦ ‖g n‖) :=
+    Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) hgnorm hgeom
+  have hgsum : Summable g := Summable.of_norm hnormsum
+  let F : StrongDual ℝ E := ∑' n, g n
+  refine ⟨F, ?_, ?_⟩
+  · intro c hc
+    have happly := ((ContinuousLinearMap.apply ℝ ℝ) c).map_tsum hgsum
+    change F c = ∑' n, g n c at happly
+    rw [show F c = ∑' n, g n c from happly]
+    apply tsum_nonneg
+    intro n
+    change 0 ≤ w n * f n c
+    exact mul_nonneg (hwpos n).le (hfC n c hc)
+  · intro x hx
+    rcases Set.mem_iUnion.mp (h.covers hx) with ⟨n, hxn⟩
+    have heval : Summable (fun k ↦ g k x) := by
+      have hm := hgsum.map ((ContinuousLinearMap.apply ℝ ℝ) x)
+        ((ContinuousLinearMap.apply ℝ ℝ) x).continuous
+      change Summable (fun k ↦ g k x) at hm
+      exact hm
+    have hterm : 0 < g n x := by
+      change 0 < w n * f n x
+      exact mul_pos (hwpos n) (hfK n x hxn)
+    have hle : g n x ≤ ∑' k, g k x :=
+      heval.le_tsum n (fun k _ ↦ by
+        change 0 ≤ w k * f k x
+        exact mul_nonneg (hwpos k).le (hfC k x (h.strictInCone hx)))
+    have happly := ((ContinuousLinearMap.apply ℝ ℝ) x).map_tsum hgsum
+    change F x = ∑' k, g k x at happly
+    rw [show F x = ∑' k, g k x from happly]
+    exact hterm.trans_le hle
+
+end
+
+end Scott1964.MeasurementStructures.Probability.Infinite
diff --git a/LeanPool/ScottMeasurement/Probability/Infinite/Reconstructed.lean b/LeanPool/ScottMeasurement/Probability/Infinite/Reconstructed.lean
new file mode 100644
index 0000000000..f6eb596db8
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/Infinite/Reconstructed.lean
@@ -0,0 +1,233 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Probability.Infinite.EventSpace
+public import LeanPool.ScottMeasurement.Probability.Infinite.Kelley
+
+/-!
+# A modern reconstruction of the infinite probability theorem
+
+Scott's published 1964 paper states and proves the finite theorem, then only
+announces an unstated infinite extension. The result below adapts Kelley's
+method and is not presented as Scott's unpublished theorem.
+
+Weak comparisons generate a closed cone in the universal event span, expressed
+here by its continuous dual polar.  The additional generalized Kelley condition
+gives a countable cover of the strict comparisons by closed convex upper sets.
+This adapts the countable-cover/separation method of J. L. Kelley, *Measures on
+Boolean Algebras* (1959), but the event-span formulation, condition, and theorem
+statement are not attributed to Kelley. The real Hahn--Banach theorem in
+`HahnBanach.lean`, through
+`KelleyCover.exists_combined_separator`, then supplies one functional which is
+nonnegative on every weak comparison and positive on every strict comparison.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures.Probability.Infinite
+
+open Set
+
+noncomputable section
+
+universe u
+
+variable {B : Type u} [BooleanAlgebra B]
+
+/-- The signed event-span vector associated with the comparison of `x` to `y`. -/
+def comparisonVector (B : Type u) [BooleanAlgebra B] (x y : B) : EventSpan B :=
+  event B x - event B y
+
+/-- The closed weak-comparison cone, defined as the intersection of all closed
+dual half-spaces which contain the declared weak comparisons. -/
+def weakComparisonCone (R : B → B → Prop) : ProperCone ℝ (EventSpan B) :=
+  ⨅ (L : StrongDual ℝ (EventSpan B))
+    (_hL : ∀ x y, R x y → 0 ≤ L (comparisonVector B x y)),
+      (ProperCone.positive ℝ ℝ).comap L
+
+theorem mem_weakComparisonCone_iff {R : B → B → Prop} {v : EventSpan B} :
+    v ∈ weakComparisonCone R ↔
+      ∀ L : StrongDual ℝ (EventSpan B),
+        (∀ x y, R x y → 0 ≤ L (comparisonVector B x y)) →
+          0 ≤ L v := by
+  simp [weakComparisonCone]
+
+theorem comparisonVector_mem_weakComparisonCone {R : B → B → Prop}
+    {x y : B} (hxy : R x y) :
+    comparisonVector B x y ∈ weakComparisonCone R := by
+  rw [mem_weakComparisonCone_iff]
+  intro L hL
+  exact hL x y hxy
+
+/-- The set of vectors corresponding to source-strict comparisons
+`x ≻ y`, namely `¬ R y x`. -/
+def strictComparisonSet (R : B → B → Prop) : Set (EventSpan B) :=
+  {v | ∃ x y, StrictlyPreferred R x y ∧ v = comparisonVector B x y}
+
+theorem comparisonVector_mem_strictComparisonSet {R : B → B → Prop}
+    {x y : B} (hxy : StrictlyPreferred R x y) :
+    comparisonVector B x y ∈ strictComparisonSet R :=
+  ⟨x, y, hxy, rfl⟩
+
+/-- Concrete generalized Kelley condition used by this reconstruction: strict
+comparison vectors admit a countable Kelley cover above the closed weak cone. -/
+def GeneralizedKelleyCondition (R : B → B → Prop) : Prop :=
+  Nonempty (KelleyCover (weakComparisonCone R) (strictComparisonSet R))
+
+private theorem exists_reciprocal_le {r : ℝ} (hr : 0 < r) :
+    ∃ n : ℕ, (1 : ℝ) / (n + 1) ≤ r := by
+  obtain ⟨n : ℕ, hn⟩ := exists_nat_gt (1 / r)
+  refine ⟨n, ?_⟩
+  have hnpos : (0 : ℝ) < n + 1 := by positivity
+  rw [div_le_iff₀ hnpos]
+  have hr' : (1 : ℝ) < (n + 1) * r := by
+    have := (div_lt_iff₀ hr).mp hn
+    nlinarith
+  nlinarith
+
+private theorem realizable_generalizedKelley
+    {R : B → B → Prop} (hR : RealizableProbability R) :
+    GeneralizedKelleyCondition R := by
+  rcases hR with ⟨μ, hμ, hrep⟩
+  let p : ProbabilityPoint B := ⟨μ, hμ⟩
+  let L : StrongDual ℝ (EventSpan B) :=
+    (BoundedContinuousFunction.evalCLM ℝ p).comp (EventSpan B).subtypeL
+  let K : ℕ → Set (EventSpan B) :=
+    fun n => {v | (1 : ℝ) / (n + 1) ≤ L v}
+  refine ⟨{
+    layer := K
+    strictInCone := ?_
+    covers := ?_
+    convex := ?_
+    closed := ?_
+    avoidsZero := ?_
+    upper := ?_
+  }⟩
+  · rintro v ⟨x, y, hstrict, rfl⟩
+    apply comparisonVector_mem_weakComparisonCone
+    apply (hrep x y).2
+    exact le_of_not_gt (fun h => hstrict ((hrep y x).2 h.le))
+  · rintro v ⟨x, y, hstrict, rfl⟩
+    have hpos : 0 < L (comparisonVector B x y) := by
+      change 0 < μ x - μ y
+      apply sub_pos.mpr
+      exact lt_of_not_ge (fun h => hstrict ((hrep y x).2 h))
+    obtain ⟨n, hn⟩ := exists_reciprocal_le hpos
+    apply Set.mem_iUnion.mpr
+    exact ⟨n, hn⟩
+  · intro n
+    exact convex_halfSpace_ge L.toLinearMap.isLinear _
+  · intro n
+    exact isClosed_le continuous_const L.continuous
+  · intro n hz
+    change (1 : ℝ) / (n + 1) ≤ L 0 at hz
+    rw [map_zero] at hz
+    have : (0 : ℝ) < 1 / (n + 1) := by positivity
+    linarith
+  · intro n v c hv hc
+    dsimp [K] at hv ⊢
+    rw [map_add]
+    apply hv.trans
+    apply le_add_of_nonneg_right
+    rw [mem_weakComparisonCone_iff] at hc
+    apply hc L
+    intro x y hxy
+    change 0 ≤ μ x - μ y
+    exact sub_nonneg.mpr ((hrep x y).1 hxy)
+
+private theorem generalizedKelley_realizable
+    {R : B → B → Prop}
+    (hnt : ProbNontrivial R) (hnn : ProbNonneg R) (htot : ProbTotal R)
+    (hK : GeneralizedKelleyCondition R) :
+    RealizableProbability R := by
+  rcases hK with ⟨cover⟩
+  obtain ⟨F, hFweak, hFstrict⟩ := cover.exists_combined_separator
+  have htopStrict : StrictlyPreferred R (⊤ : B) ⊥ := hnt.2
+  have htopSet :
+      comparisonVector B (⊤ : B) ⊥ ∈ strictComparisonSet R :=
+    comparisonVector_mem_strictComparisonSet htopStrict
+  have htopPos : 0 < F (event B (⊤ : B)) := by
+    have := hFstrict _ htopSet
+    have hvec :
+        event B (⊤ : B) - event B (⊥ : B) = event B (⊤ : B) := by
+      rw [event_bot]
+      exact sub_zero (event B (⊤ : B))
+    rwa [comparisonVector, hvec] at this
+  let μ : B → ℝ := fun a => F (event B a) / F (event B (⊤ : B))
+  have hμ : IsProbability μ := by
+    refine {
+      bot := ?_
+      top := ?_
+      additive := ?_
+      nonnegative := ?_
+    }
+    · simp [μ]
+    · exact div_self htopPos.ne'
+    · intro x y hxy
+      simp only [μ]
+      rw [event_sup_of_disjoint B hxy, map_add, add_div]
+    · intro x
+      have hxcone :
+          comparisonVector B x ⊥ ∈ weakComparisonCone R :=
+        comparisonVector_mem_weakComparisonCone (hnn x)
+      have hxnonneg := hFweak _ hxcone
+      have : 0 ≤ F (event B x) := by
+        have hvec : event B x - event B (⊥ : B) = event B x := by
+          rw [event_bot]
+          exact sub_zero (event B x)
+        rwa [comparisonVector, hvec] at hxnonneg
+      exact div_nonneg this htopPos.le
+  refine ⟨μ, hμ, ?_⟩
+  intro x y
+  constructor
+  · intro hxy
+    have hcone :
+        comparisonVector B x y ∈ weakComparisonCone R :=
+      comparisonVector_mem_weakComparisonCone hxy
+    have hnonneg := hFweak _ hcone
+    change F (event B x) / F (event B ⊤) ≥
+      F (event B y) / F (event B ⊤)
+    exact (div_le_div_iff_of_pos_right htopPos).2 (by
+      have hmap := map_sub F (event B x) (event B y)
+      change 0 ≤ F (event B x - event B y) at hnonneg
+      linarith)
+  · intro hμxy
+    rcases htot x y with hxy | hyx
+    · exact hxy
+    · by_contra hnxy
+      have hstrict : StrictlyPreferred R y x := hnxy
+      have hset :
+          comparisonVector B y x ∈ strictComparisonSet R :=
+        comparisonVector_mem_strictComparisonSet hstrict
+      have hpos := hFstrict _ hset
+      have hlt : μ x < μ y := by
+        change F (event B x) / F (event B ⊤) <
+          F (event B y) / F (event B ⊤)
+        rw [div_lt_div_iff_of_pos_right htopPos]
+        have hmap := map_sub F (event B y) (event B x)
+        change 0 < F (event B y - event B x) at hpos
+        linarith
+      exact (not_lt_of_ge hμxy) hlt
+
+/-- If-and-only-if characterization of an infinite analogue of Scott's Theorem 4.1,
+adapting Kelley's 1959 separation method. It is not an attribution of an
+unpublished theorem to Scott. -/
+theorem reconstructed_infinite_theorem_4_1 (R : B → B → Prop) :
+    RealizableProbability R ↔
+      ProbNontrivial R ∧ ProbNonneg R ∧ ProbTotal R ∧
+        GeneralizedKelleyCondition R := by
+  constructor
+  · intro hR
+    exact ⟨hR.probNontrivial, hR.probNonneg, hR.probTotal,
+      realizable_generalizedKelley hR⟩
+  · rintro ⟨hnt, hnn, htot, hK⟩
+    exact generalizedKelley_realizable hnt hnn htot hK
+
+end
+
+end Scott1964.MeasurementStructures.Probability.Infinite
diff --git a/LeanPool/ScottMeasurement/Probability/KPSCounterexample.lean b/LeanPool/ScottMeasurement/Probability/KPSCounterexample.lean
new file mode 100644
index 0000000000..0edec0b841
--- /dev/null
+++ b/LeanPool/ScottMeasurement/Probability/KPSCounterexample.lean
@@ -0,0 +1,258 @@
+/-
+Copyright (c) 2026 Lars Warren Ericson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars Warren Ericson
+-/
+
+module
+
+public import LeanPool.ScottMeasurement.Probability.Finite
+
+/-!
+# The Kraft–Pratt–Seidenberg five-atom counterexample
+
+This file formalizes the simple ordering displayed in Section 4 of
+Kraft–Pratt–Seidenberg, *Intuitive Probability on Finite Sets* (1959).
+The five atoms `p q r s t` are represented by `0 1 2 3 4 : Fin 5`.
+
+The rank table below is the paper's displayed order, from the empty event
+through the full event.  Its four decisive comparisons are
+
+`qs < p`, `pq < rs`, `ps < tq`, and `rt < spq`.
+
+The finite de Finetti properties are checked by evaluating all events.
+The non-representability argument itself is symbolic: finite additivity
+turns the four strict event comparisons into four incompatible linear
+inequalities between singleton weights.
+-/
+
+@[expose] public section
+
+namespace Scott1964.MeasurementStructures.Probability.KPSCounterexample
+
+/-- The five outcomes in the Kraft--Pratt--Seidenberg example. -/
+abbrev Atom := Fin 5
+/-- Events are subsets of the five outcomes. -/
+abbrev Event := Finset Atom
+
+/-- Outcome `p` in the notation of the original rank table. -/
+def p : Atom := 0
+/-- Outcome `q` in the notation of the original rank table. -/
+def q : Atom := 1
+/-- Outcome `r` in the notation of the original rank table. -/
+def r : Atom := 2
+/-- Outcome `s` in the notation of the original rank table. -/
+def s : Atom := 3
+/-- Outcome `t` in the notation of the original rank table. -/
+def t : Atom := 4
+
+/-- Binary code for an event, with `p q r s t` as bits `0 1 2 3 4`. -/
+def eventCode (A : Event) : Nat :=
+  ∑ i ∈ A, 2 ^ i.val
+
+/-- Position in the strict 32-event order printed by KPS. -/
+def kpsRank (A : Event) : Nat :=
+  match eventCode A with
+  | 0  => 0   -- 1 (the empty event)
+  | 2  => 1   -- q
+  | 4  => 2   -- r
+  | 8  => 3   -- s
+  | 6  => 4   -- qr
+  | 10 => 5   -- qs
+  | 1  => 6   -- p
+  | 3  => 7   -- pq
+  | 12 => 8   -- rs
+  | 16 => 9   -- t
+  | 14 => 10  -- qrs
+  | 5  => 11  -- rp
+  | 9  => 12  -- ps
+  | 18 => 13  -- tq
+  | 7  => 14  -- qrp
+  | 20 => 15  -- rt
+  | 11 => 16  -- spq
+  | 24 => 17  -- st
+  | 13 => 18  -- rsp
+  | 22 => 19  -- qrt
+  | 26 => 20  -- qst
+  | 17 => 21  -- pt
+  | 15 => 22  -- qrsp
+  | 19 => 23  -- qpt
+  | 28 => 24  -- rst
+  | 30 => 25  -- qrst
+  | 21 => 26  -- rpt
+  | 25 => 27  -- spt
+  | 23 => 28  -- qrpt
+  | 27 => 29  -- qspt
+  | 29 => 30  -- rspt
+  | 31 => 31  -- pqrst
+  | _  => 0   -- unreachable for an event on five atoms
+
+/-- The weak comparison induced by the original 32-event rank table. -/
+def KPSLe (A B : Event) : Prop := kpsRank A ≤ kpsRank B
+/-- The strict comparison induced by the original 32-event rank table. -/
+def KPSLt (A B : Event) : Prop := kpsRank A < kpsRank B
+
+/-- The KPS order oriented as “at least as probable”, matching the shared
+qualitative-probability API. -/
+def KPSGe (A B : Event) : Prop := KPSLe B A
+
+instance : DecidableRel KPSLe := by
+  intro A B
+  unfold KPSLe
+  infer_instance
+
+instance : DecidableRel KPSLt := by
+  intro A B
+  unfold KPSLt
+  infer_instance
+
+instance : DecidableRel KPSGe := by
+  intro A B
+  unfold KPSGe
+  infer_instance
+
+/-- The table gives distinct ranks to all 32 events. -/
+theorem kpsRank_injective : Function.Injective kpsRank := by
+  decide +kernel +revert
+
+/-- Comparability (C). -/
+theorem comparable (A B : Event) : KPSLe A B ∨ KPSLe B A := by
+  simp only [KPSLe]
+  omega
+
+/-- Transitivity (T). -/
+theorem transitive {A B C : Event} :
+    KPSLe A B → KPSLe B C → KPSLe A C := by
+  simp only [KPSLe]
+  omega
+
+/-- The empty event is no more likely than every event. -/
+theorem empty_le (A : Event) : KPSLe ∅ A := by
+  exact Nat.zero_le _
+
+private theorem insert_invariance (A B : Event) (a : Atom)
+    (haA : a ∉ A) (haB : a ∉ B) :
+    KPSLe A B ↔ KPSLe (insert a A) (insert a B) := by
+  decide +kernel +revert
+
+/-- De Finetti's disjoint-union invariance (A). The finite check only concerns
+inserting one atom; induction gives arbitrary disjoint unions. -/
+theorem disjoint_union_invariance (A B C : Event)
+    (hCA : Disjoint C A) (hCB : Disjoint C B) :
+    KPSLe A B ↔ KPSLe (A ∪ C) (B ∪ C) := by
+  induction C using Finset.induction_on with
+  | empty => simp
+  | @insert a C ha ih =>
+      rw [Finset.disjoint_insert_left] at hCA hCB
+      have haAC : a ∉ A ∪ C := by simp [hCA.1, ha]
+      have haBC : a ∉ B ∪ C := by simp [hCB.1, ha]
+      exact (ih hCA.2 hCB.2).trans (by
+        simpa [Finset.union_insert] using insert_invariance (A ∪ C) (B ∪ C) a haAC haBC)
+
+theorem qs_lt_p : KPSLt {q, s} {p} := by decide +kernel
+theorem pq_lt_rs : KPSLt {p, q} {r, s} := by decide +kernel
+theorem ps_lt_tq : KPSLt {p, s} {t, q} := by decide +kernel
+theorem rt_lt_spq : KPSLt {r, t} {s, p, q} := by decide +kernel
+
+/-- Finite additivity determines every event from its singleton values. -/
+theorem measure_eq_sum_singletons {μ : Event → ℝ}
+    (hμ : IsProbability μ) (A : Event) :
+    μ A = ∑ i ∈ A, μ {i} := by
+  classical
+  induction A using Finset.induction_on with
+  | empty =>
+      simpa using hμ.bot
+  | @insert a A ha ih =>
+      calc
+        μ (insert a A) = μ ({a} ∪ A) := by rw [Finset.singleton_union]
+        _ = μ {a} + μ A := hμ.additive _ _
+          (Finset.disjoint_singleton_left.mpr ha)
+        _ = μ {a} + ∑ i ∈ A, μ {i} := by rw [ih]
+        _ = ∑ i ∈ insert a A, μ {i} := by simp [ha]
+
+/-- Strict numerical representation of the KPS strict order. -/
+def StrictlyRepresents (μ : Event → ℝ) : Prop :=
+  ∀ A B, KPSLt A B ↔ μ A < μ B
+
+/--
+No real finitely additive probability strictly represents the displayed
+Kraft–Pratt–Seidenberg order.
+-/
+theorem no_strictly_representing_probability :
+    ¬ ∃ μ : Event → ℝ,
+      IsProbability μ ∧ StrictlyRepresents μ := by
+  rintro ⟨μ, hμ, hrep⟩
+  have h1 : μ {q, s} < μ {p} := (hrep _ _).mp qs_lt_p
+  have h2 : μ {p, q} < μ {r, s} := (hrep _ _).mp pq_lt_rs
+  have h3 : μ {p, s} < μ {t, q} := (hrep _ _).mp ps_lt_tq
+  have h4 : μ {r, t} < μ {s, p, q} := (hrep _ _).mp rt_lt_spq
+  rw [measure_eq_sum_singletons hμ, measure_eq_sum_singletons hμ] at h1
+  rw [measure_eq_sum_singletons hμ, measure_eq_sum_singletons hμ] at h2
+  rw [measure_eq_sum_singletons hμ, measure_eq_sum_singletons hμ] at h3
+  rw [measure_eq_sum_singletons hμ, measure_eq_sum_singletons hμ] at h4
+  simp [p, q, r, s, t] at h1 h2 h3 h4
+  linarith
+
+theorem kpsGe_nontrivial : ¬KPSGe (⊥ : Event) ⊤ := by
+  decide +kernel
+
+theorem kpsGe_bottom (A : Event) : KPSGe A ⊥ :=
+  empty_le A
+
+theorem kpsGe_total : ProbTotal KPSGe := by
+  intro A B
+  exact (comparable B A).imp id id
+
+theorem kpsGe_transitive : ProbTransitive KPSGe := by
+  intro A B C hAB hBC
+  exact transitive hBC hAB
+
+theorem kpsGe_disjointUnionInvariant :
+    ProbDisjointUnionInvariant KPSGe := by
+  intro A B C hCA hCB
+  exact disjoint_union_invariance (A := B) (B := A) (C := C) hCB hCA
+
+/-- The exact KPS order satisfies de Finetti's five axioms, with condition
+(i) in its original weak form `¬ R ⊥ ⊤`. -/
+theorem kpsGe_deFinettiAxioms : DeFinettiAxioms KPSGe where
+  nontrivial := kpsGe_nontrivial
+  bottom := kpsGe_bottom
+  total := kpsGe_total
+  transitive := kpsGe_transitive
+  disjointUnionInvariant := kpsGe_disjointUnionInvariant
+
+theorem measure_strict_of_kpsLt {μ : Event → ℝ}
+    (hrep : ∀ A B, KPSGe A B ↔ μ A ≥ μ B)
+    {A B : Event} (hAB : KPSLt A B) :
+    μ A < μ B := by
+  have hBA : KPSGe B A := by
+    exact hAB.le
+  have hnAB : ¬KPSGe A B := by
+    simp only [KPSGe, KPSLe, KPSLt] at hAB ⊢
+    omega
+  have hle := (hrep B A).1 hBA
+  have hnle : ¬μ A ≥ μ B := fun h ↦ hnAB ((hrep A B).2 h)
+  linarith
+
+/-- No shared-API probability weakly represents the exact KPS “at least as
+probable” order.  The contradiction uses the paper's four decisive
+inequalities. -/
+theorem not_realizableProbability_kpsGe :
+    ¬RealizableProbability KPSGe := by
+  rintro ⟨μ, hμ, hrep⟩
+  apply no_strictly_representing_probability
+  refine ⟨μ, hμ, fun A B ↦ ?_⟩
+  constructor
+  · exact measure_strict_of_kpsLt hrep
+  · intro hlt
+    by_contra hnot
+    have hge : KPSGe A B := Nat.le_of_not_gt hnot
+    exact (not_lt_of_ge ((hrep A B).mp hge)) hlt
+
+/-- De Finetti's five axioms are insufficient for finite additive-probability
+representation. -/
+theorem deFinetti_axioms_insufficient :
+    DeFinettiAxioms KPSGe ∧ ¬RealizableProbability KPSGe :=
+  ⟨kpsGe_deFinettiAxioms, not_realizableProbability_kpsGe⟩
+
+end Scott1964.MeasurementStructures.Probability.KPSCounterexample
diff --git a/LeanPool/projects/scott-measurement.yaml b/LeanPool/projects/scott-measurement.yaml
new file mode 100644
index 0000000000..1fff2e8fb5
--- /dev/null
+++ b/LeanPool/projects/scott-measurement.yaml
@@ -0,0 +1,121 @@
+slug: scott-measurement
+title: Scott's measurement representation theorems
+summary: >-
+  Formalizes all eight numbered finite representation theorems of Dana Scott's
+  1964 Measurement Structures and Linear Inequalities. Develops a shared finite
+  separation and rational-cancellation engine, unit-threshold semiorder
+  representations, additive utility on pairs, ordered utility differences, and
+  normalized finitely additive probabilities on finite Boolean algebras. Includes
+  the Kraft-Pratt-Seidenberg five-atom counterexample to de Finetti's weaker
+  axioms and local real embeddings of finite subsets of ordered abelian groups.
+  A separately labelled modern infinite analogue assumes a generalized Kelley
+  condition: strict-comparison vectors have a countable cover by closed convex
+  upper sets avoiding zero above the weak-comparison cone. It is neither a
+  countably additive measure theorem nor an attribution of Scott's unpublished
+  infinite theorem. The infinite construction uses universal probability
+  evaluation vectors, with a proved faithful Stone representation and
+  probability-state correspondence. The upstream proofs were produced primarily
+  by AI agents under Lars Warren Ericson's direction and review.
+branch: measurement theory
+entry_module: LeanPool.ScottMeasurement
+authors:
+- Lars Warren Ericson
+source:
+  title: Measurement Structures and Linear Inequalities
+  authors:
+  - Dana Scott
+  url: https://github.com/catskillsresearch/scott1964
+  github_repo: catskillsresearch/scott1964
+  commit: 591e8a6a5d7d1ebf4cc761b4a1cb749b6480dfeb
+  announcement: https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000015&version=1
+  announcement_date: '2026-09-25T12:54:19Z'
+  completion_commit: 295e5620cb6193774a4ab8cd568b8003a3b582d6
+  completion_date: '2026-08-31T03:38:56Z'
+  citation: Journal of Mathematical Psychology 1 (1964), 233-247
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+- Scott1964.MeasurementStructures.theorem_4_1_vector
+main_results:
+- declaration: Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_1
+  informal: >-
+    For a finite symmetric subset X of a finite-dimensional real normed space,
+    membership in an arbitrary set N on X is represented by nonnegativity of a
+    linear functional if and only if every x in X has x or -x in N and every
+    zero sum of positively real-weighted vectors from X intersect N has all
+    their negatives in N.
+- declaration: Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_2
+  informal: >-
+    For a finite symmetric set of rational-valued vectors on a finite coordinate
+    type, the same linear realizability criterion uses unweighted zero sums,
+    with repetitions allowed, instead of arbitrary positive real weights.
+- declaration: Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_3
+  informal: >-
+    A relation on a finite set of rational-valued vectors on a finite coordinate
+    type is represented exactly by comparison of one real linear functional if
+    and only if it is complete and, whenever two equally indexed finite lists
+    have equal sums and every left vector is related to its right partner,
+    all the reverse comparisons also hold.
+- declaration: Scott1964.MeasurementStructures.LinearInequalities.scott_theorem_1_4
+  informal: >-
+    A relation on a finite rational vector set is represented by one real linear
+    functional if and only if it extends to its zero-inclusive additive submonoid closure
+    as a complete
+    relation preserving addition and satisfying Scott's cancellation axiom.
+- declaration: Scott1964.MeasurementStructures.theorem_2_1
+  informal: >-
+    On any finite set (allowing the empty case, unlike the source), a relation P admits real scores with P x y exactly
+    when the score of x is at least the score of y plus one if and only if P
+    is irreflexive and satisfies Scott's two four-alternative semiorder axioms.
+- declaration: Scott1964.MeasurementStructures.theorem_3_1
+  informal: >-
+    On the product of any two finite sets (also allowing empty coordinate types),
+    a relation admits an additive
+    representation f(x)+g(x') exactly when it is total and satisfies Scott's
+    cancellation scheme for independent permutations of the two coordinates.
+- declaration: Scott1964.MeasurementStructures.theorem_3_2
+  informal: >-
+    On any finite set (also allowing the empty case), a quaternary relation D is represented exactly by
+    comparisons f(x)-f(y) >= f(z)-f(w) for one real utility f if and only if D
+    is total and satisfies permutation cancellation and reversal.
+- declaration: Scott1964.MeasurementStructures.theorem_4_1_vector
+  informal: >-
+    A relation on a finite Boolean algebra is represented exactly by a
+    nonnegative normalized finitely additive real probability if and only if
+    the certain event is strictly above null, every event is at least null,
+    comparisons are total, and Scott's cancellation scheme holds whenever two
+    finite lists have equal sums of atom characteristic vectors.
+- declaration: Scott1964.MeasurementStructures.LinearInequalities.finite_local_real_embedding
+  informal: >-
+    Every finite subset of a linearly ordered abelian group has a real-valued
+    map reflecting its order and preserving every addition equation whose
+    three terms lie in the subset; this asserts a local map, not an embedding
+    of the entire group.
+- declaration: Scott1964.MeasurementStructures.Probability.KPSCounterexample.deFinetti_axioms_insufficient
+  informal: >-
+    The explicit Kraft-Pratt-Seidenberg order on the 32 events of five atoms
+    satisfies de Finetti's five qualitative-probability axioms but has no
+    normalized finitely additive real probability representing all comparisons.
+- declaration: Scott1964.MeasurementStructures.Probability.Infinite.reconstructed_infinite_theorem_4_1
+  informal: >-
+    On an arbitrary Boolean algebra, a relation admits an exact normalized
+    finitely additive real probability representation if and only if it is
+    nontrivial, nonnegative relative to null, total, and satisfies the stated
+    generalized Kelley cover condition on its universal event-span comparison
+    vectors. This is a modern analogue with an explicit extra analytic condition.
+- declaration: Scott1964.MeasurementStructures.Probability.Infinite.probabilityStateEquiv
+  informal: >-
+    Finitely additive probabilities on an arbitrary Boolean algebra are
+    canonically equivalent to positive normalized continuous linear
+    functionals on the real span of its universal probability-evaluation
+    vectors, equipped with the inherited supremum norm.
+tags:
+- measurement-theory
+- utility-representation
+- qualitative-probability
+msc:
+- 91B16
+- 91B06
+- 60A05
+- 52A20