{"id":"palomar/PALOMAR-2026-09-25-000015","url":"https://github.com/catskillsresearch/scott1964/tree/2c35b7d2b7f5d60c20381a2f497bb0ab7d4d0a1f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000015-v1.json","repo":"https://github.com/catskillsresearch/scott1964","tags":["cs.LO","math.LO","econ.TH","msc:91C05","msc:15A39","msc:91B16","msc:68V20","measurement-theory","linear-inequalities","lean-formalization"],"score":0,"title":"Formalization of Scott's Measurement Structures and Linear Inequalities in Lean 4","trust":"high","domain":"cs.LO","source":"palomar","authors":["Lars Warren Ericson","Dana S. Scott","Vijay D'Silva","Brian Milnes"],"reviews":0,"subject":"cs.LO","summary":"A Lean 4 / mathlib formalization of Dana Scott's 1964 paper *Measurement Structures and Linear Inequalities* (Journal of Mathematical Psychology 1 (1964), 233–247). The paper derives necessary and sufficient conditions for three finite representation problems — intransitive indifference, ordered differences, and subjective probability — from the general solvability criterion for finite systems of linear inequalities. The development also covers Scott's ordered-group and signed-charge remarks, literal vector cancellation, and the KPS obstruction to de Finetti's five axioms. Every compared…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Measurement Structures and Linear Inequalities","identifier":"","relationship":"formalizes"},{"title":"Measures on Boolean Algebras","identifier":"","relationship":"adapts"}]}