SIC-POVMs, a Stark Conjecture, and the 12th: A Formalization via Paraconsistent Belnap Multilattices

Abstract

This paper establishes, inside the Lean 4 proof assistant, a three-level formal identification. The levels are: (i) Belnap multilattice axioms for Weyl–Heisenberg covariant SIC-POVMs at $d=2^n$; (ii) the Zauner conjecture; and (iii) the mixed-signature Stark conjecture for the ray class field $K_d=\mathbb{Q}(\sqrt{(d-3)(d+1)})$, a real-quadratic case of Hilbert's Twelfth Problem. Fiducials are unit-normalized and satisfy $(d+1)|\langle\psi,D_{a,b}\psi\rangle|^2=1$. The equivalence hilbert_embedding_equiv_zauner is proved by rfl: the Belnap embedding into $\mathbb{C}^{2^n}$ and the Zauner conjecture at $d=2^n$ are definitionally the same proposition. The Belnap skeleton (orbit size $4^n$, Frobenius closure $\mu\circ\delta=\mathrm{id}$, join-equiangularity, Born rule) contains zero sorries. Open arithmetic content is marked by named gap axioms for Stark units on WH frames; a proof of Stark would close all three levels at once. For dimension $d=12$ we prove SICPOVM_Exists 12 outright. We construct an exact fiducial in a finitely presented $\mathbb{Q}$-algebra, verify 143 overlap identities with native_decide, and transfer everything to $\mathbb{C}^{12}$ along a ring homomorphism. The theorem crystal_forces_d12_sic depends on no axiom beyond Lean 4's standard foundations and compiler trust. This is, to our knowledge, the first machine-checked SIC-POVM existence in any dimension. For the frontier dimension $d=2048=2^{11}$ the transport apparatus is formalized and sorry-free. It includes a forward map $\varphi\colon B^{\oplus 11}\to\mathbb{C}^{2048}$, a reduction $\psi$ with $\psi\circ\varphi=\mathrm{id}$, a conditional reduction to Stark, and a non-real character obstruction that blocks the false branch. Unconditional existence remains open; the machinery that surrounds it is closed.