Open Research Index

gleason-finite-lean

Zayn Blore

Palomar Registrypalomar/PALOMAR-2026-10-01-000010Oct 1, 2026math-phscore 0

A machine-checked proof of Gleason's theorem in finite dimensions. On a complex Hilbert space of dimension at least 3, every frame function on the orthogonal projections has the form P ↦ Re Tr(ρP) for exactly one density operator ρ. The statement is Kim Morrison's lean-eval problem gleason_theorem_finite, unchanged. The proof follows Cooke, Keane and Moran's elementary proof of Gleason's core lemma for matrices on ℂᴺ, then moves the result to operators by taking matrices in an orthonormal basis.

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-10-01-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-01-000010/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-10-01-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'