{"id":"palomar/PALOMAR-2026-10-04-000004","url":"https://github.com/Dengnifer/MIPStarRE-QPBT/tree/179a37893d2a037cce0587ea932f5da819c7d78c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-04-000004-v1.json","repo":"https://github.com/Dengnifer/MIPStarRE-QPBT","tags":["quant-ph","msc:81P45","quantum-complexity","mip-star","quantum-information","lean-formalization"],"score":0,"title":"Quantum Pauli basis test","trust":"high","domain":"quant-ph","source":"palomar","authors":["Ruixuan Deng"],"reviews":0,"subject":"quant-ph","summary":"A Lean 4 formalization of the quantum Pauli basis test from MIP*=RE. The comparator-configured results give a value-one symmetric projective consistent commuting strategy, quantum soundness of the simultaneous low-degree test, soundness of the Pauli basis test up to local isometries with the explicit deltaQld error, and the corresponding qubit-coordinate form.","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true,"formalizes":[{"title":"MIP*=RE","identifier":"arXiv:2001.04383","relationship":"formalizes"}]}