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.
<!-- *** Custom HTML *** --> We associate to a regular system of weights a weighted projective line over an algebraically closed field of characteristic zero in two different ways. One is defined as a quotient stack via a hypersurface singularity for a regular system of weights and the other is defined via the signature of the same regular system of weights. The main result in this paper is that if a regular system of weights is of dual type then these two weighted projective lines have equivalent abelian categories of coherent sheaves. As a corollary, we can show that the triangulated categories of the graded singularity associated to a regular system of weights has a full exceptional collection, which is expected from homological mirror symmetries. The main theorem of this paper will be generalized to more general one, to the case when a regular system of weights is of genus zero, which will be given in [5]. Since we need more detailed study of regular systems of weights and some knowledge of algebraic geometry of Deligne–Mumford stacks there, the author write a part of the result in this paper to which another simple proof based on the idea by Geigle–Lenzing [2] can be applied.
We first study the module structure of the free Lie algebra $L(V)$ in characteristic zero under the action of the general linear group. Here we give a new, purely combinatorial, proof of Klyachko's celebrated theorem on Lie representations using the Kra\\'{s}kiewicz-Weyman theorem.\n\nWe then give a new factorisation of the Dynkin-Specht-Wever\nidempotent and use this to prove that $L_2(L_k(V))$ is a $KG$-module direct summand of $L_{2k}(V)$, for $G$ an arbitrary group, $K$ a field of characteristic $p \\nmid k$ and $V$ a $KG$-module. For finite-dimensional modules $V$, this follows immediately from the Decomposition Theorem of Bryant and Schocker. We consider a small example of this theorem, namely the sixth Lie power over a field of\ncharacteristic $3$. Here we show explicitly that $L_6(V)$ decomposes into a direct sum of the modules $L_3(L_2(V))$ and $L_2(V) \\otimes S_2(V) \\otimes S_2(V)$, where $S_2(V)$ denotes the symmetric square of $V$. We give a description, up to isomorphism, of the modules $B_{p^mk}$ occurring in the Decomposition Theorem.\n\nFinally, we apply our knowledge of Lie powers to a group theoretic problem. We show that the torsion subgroup $t_c$ of the quotient $\\gamma_c R/ [\\gamma_c R, F]$ is bounded as follows, for $c=2p^m$ or $c=3p^m$, where $p$ is an arbitrary prime, $m\\geq 0$:\n\n\\begin{eqnarray*}\n2t_{2p^m} = 0 \\;\\;\\;\\mbox{provided } G=F/R \\mbox{ has no 2-torsion and no p-torsion,}\\\\\n3t_{3p^m} = 0 \\;\\;\\;\\mbox{provided } G=F/R \\mbox{ has no 3-torsion\nand no p-torsion.}\n\\end{eqnarray*}\n\nThus, we have that $\\gamma_6 R/ [\\gamma_6 R, F]$ is torsion-free, provided that $G=F/R$ has no elements of order $2$ or $3$.
We prove a lifting theorem (from any characteristic p to characteristic zero) for holomorphic Picard modular forms of any weight and level. The proof makes use of the knowledge of the geometry of the toroidal compactification of the Picard modular surface.
We consider algebras over a field $k$ of characteristic zero. The article is concerned with the isomorphism of graded vectorspaces \[ H(\gl(A))\iso\wedge (HC(A)[-1]) \] between the Lie algebra homology of matrices and the free graded commutative algebra on the cyclic homology of the $k$-algebra $A$, shifted down one degree. For unital algebras this isomorphism is a classical result obtained by Loday and Quillen and independently by Tsygan. For $H$-unital algebras, it is known to hold too, as is that the proof follows from results of Hanlon's. However, to our knowledge, the proof is not immediate, and has not been published. In this paper we fill this gap in the literature by offering a detailed proof. Moreover we establish the isomorphism in the general setting of ($H$-unital) pro-algebras.