Invariant-projection counterexamples for every irrational rotation

Formalization

• OpenAI, Invariant projections, hyperinvariant subspaces, and transitive algebras: Lean scope note (OpenAI Math Release, lean/docs/293.md, 2026-10-06). Describes the Lean scope for this paper: a continuous circle weight at every irrational angle whose weighted rotation is nonzero, quasinilpotent and has no nontrivial invariant projection in $R_\theta$, plus a product realization and the product model's Brown measure $\delta_0$. [family-level]
• OpenAI math release, IrrationalRotation.lean (Comparator challenge, commit adc7f12, 2026). Comparator statement file with prescribed_irrational_counterexample (Theorem 1.1 for every irrational $\theta\in(0,1)$) and product_realization; the theorem bodies in this statement file are sorry.

Possibly relevant literature (found by the agent, not checked)

• G. Androulakis and A. Flattot, Hyperinvariant subspace for weighted composition operator on $L^p([0,1]^d)$ (arXiv:0809.4429, 2008). Proves hyperinvariant subspaces for Bishop-type weighted composition operators $vf\circ\tau$ with ergodic $\tau$ and generalized-polynomial weights under a discrepancy condition; a related class to the weighted rotations $Uf(V)$ of Theorem 1.1, though acting on $L^p([0,1]^d)$ rather than in $R_\theta$.
• I. B. Jung, E. Ko and C. Pearcy, Hyperinvariant subspaces for a class of quasinilpotent operators (Studia Math. 245 (2019) 289–296, doi:10.4064/sm171209-18-1). Gives hyperinvariant subspaces for a structurally defined subclass of quasinilpotent Hilbert-space operators; the quasinilpotent operator of the corollary on transitive commutants must lie outside that subclass.
• Sa Ge Lee, The Hyperinvarinat Subspace Problem (arXiv:2306.13940, 2023). Short preprint whose abstract claims to solve the hyperinvariant subspace problem for Hilbert spaces; bears on the paper's corollary that a nonzero quasinilpotent operator without nontrivial hyperinvariant subspace exists.

Digests and expositions

• Ying Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics (arXiv:2610.17090, 2026-10-12). Section 9.4.3 surveys family 293, listing the "endpoint-conditioned convolution obstruction" and the affiliated-transport lemma from this paper as extracted instruments, and notes the paper's estimates were not independently verified for the survey. [family-level]
• Claude Opus 5.5 / Open Mathematics Courses, A backward intertwiner and a transitive commutant (Open Mathematics Courses, n.d.). This lesson develops the backward-intertwiner and transitivity argument and explains the connection to the companion's invariant-projection theorem, which the course does not prove; the site states that independent review is incomplete. [AI-generated per source] [family-level]