Open Research Index

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

Lars Warren Ericson, Dana S. Scott, Vijay D'Silva, Brian Milnes

Palomar Registrypalomar/PALOMAR-2026-09-25-000015Sep 25, 2026cs.LOscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-25-000015
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-25-000015/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-25-000015/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'