Saturation factor one for even Spin groups
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
For $G=Spin(2n)$ over C, $n\geq 2$, and dominant integral weights $\lambda ,\mu ,\nu $ whose sum belongs to the root lattice, does the existence of a G-invariant in $V(N\lambda )\otimes V(N\mu )\otimes V(N\nu )$ for some integer $N\geq 1$ imply the existence of one in $V(\lambda )\otimes V(\mu )\otimes V(\nu )$?Short English statement
For $G=Spin(2n)$ over C, $n\geq 2$, and dominant integral weights $\lambda ,\mu ,\nu $ whose sum belongs to the root lattice, does the existence of a G-invariant in $V(N\lambda )\otimes V(N\mu )\otimes V(N\nu )$ for some integer $N\geq 1$ imply the existence of one in $V(\lambda )\otimes V(\mu )\otimes V(\nu )$?Sources
- S1 OpenAI, manuscript citation page. Source of the formulation motivating this local problem. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Tensor-Saturation-for-Even-Spin-Groups-September-24-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2523
The main type-D saturation theorem proves equivalence of invariant existence before and after every positive dilation for dominant integral weights with sum in Q(D_n). The requested implication for some N is one direction of exactly that equivalence. Within these assumptions, this is a claimed affirmative answer to the stated question.
Saturation factor one for even Spin groups
OpenAI's claim
OpenAI presents a proof in the selected manuscript. For $\operatorname{Spin}(2n)$, $n\geq2$, a tensor invariant at a dilated triple is claimed to imply one at the original triple when the weight sum belongs to the root lattice.Mathematical statement of the claimed result
Result 1.
For $G=\operatorname{Spin}(2n)$, $n\ge2$, let $P_+$ be its dominant integral weights and $Q$ its type-$D_n$ root lattice. Take $\lambda,\mu,\nu\in P_+$ with $\lambda+\mu+\nu\in Q$. The claim is saturation with factor one: \[ (V(\lambda)\otimes V(\mu)\otimes V(\nu))^G\ne0 \quad\Longleftrightarrow\quad (V(N\lambda)\otimes V(N\mu)\otimes V(N\nu))^G\ne0 \] for every positive integer $N$. Here $V(\lambda)$ denotes the irreducible highest-weight module; the root-lattice condition is retained.Outline of the argument
The proof constructs reflected weight schedules and resolves the type-D parity obstruction by joining signed-root components. Rank-two reorderings keep the modified schedule admissible, exterior and minuscule column constructions turn it into nonzero intertwiners, and a preprojective-module reduction removes common zero coordinates.Formal verification
Family 204 has no Lean scope page in this release. Its selected result is not presented as formalized. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.Status caveat
OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.Sources
- OpenAI, Tensor saturation for even spin groups, 2026-09-24; citation key
OAI:Tensor-Saturation-for-Even-Spin-Groups-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - OpenAI catalogue entry.