OpenAI claim summary for Math-2800

Constructible tame eigensheaves with regular monodromy

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 014; 2026-10-05), the asserted result is that tame regular-unipotent, geometrically dense parameters admit nonzero constructible perverse Hecke eigensheaves with one Borel-level point for the specified simply connected groups and characteristic hypotheses.

Mathematical statement of the claimed result

Manuscript 1.

Let $k=\overline{\mathbb F}_q$ have characteristic $p$, $E=\overline{\mathbb Q}_{\ell}$ with $\ell\ne p$, and let $X_0/\mathbb F_q$ be smooth projective geometrically connected of genus at least two with rational point $x_0$. Set $X=(X_0)_k$, $x=(x_0)_k$ and $U=X\setminus\{x\}$. Let $G_0$ be split simple simply connected, with Borel $B_0$, and write $G,B$ for base changes. The characteristic hypotheses are: a nondegenerate invariant symmetric form on $\mathfrak g$ whose restriction to the central Lie algebra of each Levi is nondegenerate; the Chevalley-restriction isomorphism $k[\mathfrak m]^M\simeq k[\operatorname{Lie}(T_M)]^{W_M}$ for every Levi; semisimple Lie-algebra centralizers are Levi subgroups; and over every extension field each nilpotent Lie-algebra element lies in a parabolic unipotent-radical Lie algebra.

For a continuous Zariski-dense parameter $\rho:\pi_1^{\rm et}(U)\to\widehat G(L)$, $L/\mathbb Q_{\ell}$ finite, require trivial wild inertia and tame monodromy \[ \rho(\gamma)=\exp(t_{\ell}(\gamma)N),\qquad \dim Z_{\widehat G}(N)=\operatorname{rank}(\widehat G), \] with nilpotent $N$ and $t_{\ell}:I_x\to\mathbb Z_{\ell}$. On the stack $\mathcal A=\operatorname{Bun}_{G,B,x}(X)$, the claim gives a nonzero locally constructible perverse $E$-adic sheaf $M$ with nilpotent parabolic singular support and \[ \operatorname{Hecke}_{I,(V_i)}(M)\simeq M\boxtimes\mathop{\boxtimes}_{i\in I}(V_i)_{\rho} \quad\hbox{on }\mathcal A\times U^I \] for every finite set $I$ and representations $V_i$ of $\widehat G$. The eigenisomorphisms respect units, convolution, permutations and collision-diagonal fusion. No Frobenius descent of $\rho$ is assumed. The nilpotent cone consists of Higgs fields with nilpotent generic value and residue in the Borel unipotent radical.

Outline of the argument

For manuscript 1 (family 014; 2026-10-05), the parameter is glued through a separating node to an unramified family. Two specializations and transverse Hecke cuts detect a nonzero flag-level object; unipotent monodromy on the enhancement torus permits descent to ordinary Borel level.

Formal verification

No Lean formalization is listed at this snapshot for manuscript 1 (family 014; 2026-10-05).

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, Constructible tame Hecke eigensheaves in positive characteristic, 2026-10-05; citation key OAI:Constructible-tame-Hecke-eigensheaves-in-positive-characteristic-October-5-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main, eq:main-eigen.
• OpenAI catalogue entry.