Formalization of Scott’s Measurement Structures and Linear Inequalities in Lean 4

<p dir="ltr"><b>Abstract:</b> Scott’s 1964 paper <i>Measurement Structures and Linear Inequalities</i> 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.