Scott's 1964 paper Measurement Structures and Linear Inequalities gives a unified finite separation criterion for qualitative systems represented by homogeneous linear inequalities, with applications to intransitive indifference, ordered utility differences, and subjective probability. This report presents a Lean 4 / Mathlib formalization of all eight numbered theorems (1.1–1.4, 2.1, 3.1, 3.2, and 4.1), together with Scott's ordered-group and signed-charge remarks. The development comprises roughly 4,200 lines across 21 modules. It makes cancellation hypotheses explicit, formalizes the rational-to-integer reduction underlying finite sequence conditions, and verifies the incidence-vector constructions used by the three applications. Supplementary results include the Kraft–Pratt–Seidenberg counterexample to de Finetti's axioms and a clearly labelled modern infinite if-and-only-if characterization, adapting Kelley's 1959 method, under a generalized Kelley condition. Based on the literature audit in Section 3.5.10, that characterization provides the first explicit, self-contained realization of Scott's announced infinite extension in the published literature. The Lean library is sorry-free and introduces no project axioms beyond Mathlib's classical footprint. Large-language-model assistance was used in drafting and proof development, but every accepted declaration is checked by Lean's kernel under the pinned toolchain. The complete source and reproducible build pipeline are publicly available with this report.

83 pages

*Catskills Research Company
**Google Research
***Unaffiliated

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu