OpenAI claim summary for Math-2310

The Dirac-Brown invariant-subspace problem: a defect-attainment reduction

OpenAI's claim

At every fixed irrational rotation angle, a continuous nonnegative weight with one zero and divergent negative logarithmic integral is claimed to produce a nonzero quasinilpotent operator without factor-invariant projections. 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 each irrational $\theta\in(0,1)$, let $R_\theta$ be the tracial von Neumann algebra generated by unitaries $U,V$ with $VU=e^{2\pi i\theta}UV$ and $\tau(U^mV^n)=0$ for nonzero integer pairs. OpenAI claims a continuous $f:S^1\to[0,1]$ such that \[ f^{-1}(0)=\{1\},\qquad\int_{S^1}\log f\,dm=-\infty,\qquad (1-p)Uf(V)p=0\ \Longrightarrow\ p\in\{0,1\} \] for every projection $p\in R_\theta$, with normalized Haar measure $m$. Thus the zero-determinant operator $Uf(V)$ has no nontrivial invariant subspace whose projection belongs to $R_\theta$; arbitrary ambient invariant subspaces are not the quantified class.

Outline of the argument

Manuscript 1 (family 293, 2026-09-27): Rare, increasingly deep drops define a measurable model whose invariance equations cannot reconcile a surviving central convolution coefficient with a suppressed infinite tail. Mixed-radix couplings control the orbit-pair tests at the prescribed angle. Smoothing the drops changes their logarithms by a measurable coboundary; an affiliated intertwiner transfers any invariant projection, preserving trace and hence the obstruction.

Formal verification

For family 293, the scope page documents the following selections. The rotation selection gives quasinilpotent weighted operators with no proper invariant projection in the associated finite factor. The backward-intertwiner selection gives a proper strong-closed transitive commutant on each separable infinite-dimensional Hilbert space; Brown-measure and product variants are documented separately. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: BackwardIntertwiners.lean, ContinuousCircleWeight.lean, FiniteFactor.lean, HyperinvariantSubspaces.lean, IrrationalRotation.lean, ProductBrown.lean. Declarations: OAI.BackwardIntertwiners.direct_algebra_corollary, OAI.ContinuousCircleWeight.main_theorem, OAI.FiniteFactor.main_theorem, OAI.Hyperinvariant.main_theorem, OAI.Invariant233.Results.prescribed_irrational_counterexample, OAI.Invariant233.Results.product_realization, OAI.FiniteFactor.productBrown.

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, Invariant-projection counterexamples for every irrational rotation, 2026-09-27; citation key OAI:Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 293: Lean scope.
• Comparator BackwardIntertwiners.json.
• Comparator BackwardIntertwiners.lean.
• Comparator ContinuousCircleWeight.json.
• Comparator ContinuousCircleWeight.lean.
• Comparator FiniteFactor.json.
• Comparator FiniteFactor.lean.
• Comparator HyperinvariantSubspaces.json.
• Comparator HyperinvariantSubspaces.lean.
• Comparator IrrationalRotation.json.
• Comparator IrrationalRotation.lean.
• Comparator ProductBrown.json.
• Comparator ProductBrown.lean.
• OpenAI catalogue entry.