Finite quantum designs: mutually unbiased bases, SIC-POVMs, and the Welch and Gerzon bounds
A Lean 4 development of two structures of finite-dimensional quantum information, in the vocabulary of google-deepmind/formal-conjectures (Open Quantum Problems 13 and 23; the fourteen definitions restated character for character under their Apache-2.0 license, see NOTICE). A basis of C^d is a unitary matrix whose columns are the basis vectors; two bases U, V are mutually unbiased when every entry of U^* V has squared norm 1/d; HasMUBs d k says k pairwise unbiased bases exist and IsMaxMUBCount d k that k is the largest such number. Theorems: for d >= 2, HasMUBs d m implies m = 2; for a…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-16-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000014/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-16-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'