OpenAI claim summary for Math-2816

Bounded recovery of modular spectral averages

OpenAI's claim

When a faithful normal state's centralizer is scalar, positive modular-band averages are claimed to have uniformly bounded algebra witnesses, implying spectral rigidity and a separable type-III_1 bicentralizer theorem. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

For a type-$\mathrm{III}_1$ factor $M$ with separable predual and any faithful normal state $\phi$, OpenAI claims $\operatorname{BC}(M,\phi)=\mathbb C1$. The bicentralizer consists of $a$ whose commutators with every uniformly bounded sequence $w_n$ converge strongly to zero whenever $\|w_n\phi-\phi w_n\|_{M_*}\to0$. Its bounded-recovery theorem separately takes any von Neumann $M$ with faithful normal $\phi$ and $M_\phi=\mathbb C1$. On $H=L^2(M)$ put $\xi=\phi^{1/2}$, $D=\log\Delta_\phi$, $U_t=e^{itD}$ and fix the mean $m_tf(t)=\lim_{k\to\omega}(2k)^{-1}\int_{-k}^kf(t)\,dt$ for a free ultrafilter. Given fixed $T\in B(H)$, $s\in\mathbb R$, $\delta_n>0$ with $\delta_n\to0$ and unit vectors $h_n$ supported spectrally in $[s-\delta_n,s+\delta_n]$, it claims \[ \limsup_nm_t\|TU_th_n\|^2>0 \quad\Longrightarrow\quad \exists(n_j),v_j\in M,C_*<\infty,\eta>0:\ \|v_j\|\le C_*,\ \|Tv_j\xi\|\ge\eta, \] with $v_j\xi$ supported in $[s-4\delta_{n_j},s+4\delta_{n_j}]$. No bicentralizer hypothesis is needed in the recovery theorem.

Outline of the argument

Manuscript 1 (family 290, 2026-09-23): Modular orbit averages and independent phases give second- and fourth-moment control for initially unbounded spectral representatives. Polar truncation produces bounded witnesses, and Fourier filtering restores their shrinking spectral support. Applying these witnesses to intertwining defects restricts the joint spectrum of modular and flow generators; scalarity of the centralizer eliminates the remaining nontrivial flow possibilities.

Formal verification

For family 290, the scope page documents the following selections. The selected modular recovery statement widens shrinking spectral bands by a factor four while keeping algebra elements uniformly bounded and their tested images nonzero. It assumes the stated scalar-centralizer representation and does not select absolute bicentralizer triviality. This entry does not assert that the selected declarations formalize every part of manuscript 1's main conclusion. Its selected declaration also covers the clause used for this problem. Comparator files: BoundedRecovery.lean. Declarations: OAI.BoundedRecovery.bounded_recovery.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, Bounded recovery for modular spectral averages, 2026-09-23; citation key OAI:Bounded-recovery-for-modular-spectral-averages-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: rec:bounded.
• Family 290: Lean scope.
• Comparator BoundedRecovery.json.
• Comparator BoundedRecovery.lean.
• OpenAI catalogue entry.