# Invariant projections, hyperinvariant subspaces, and transitive algebras

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Invariant-projection counterexamples for every irrational rotation](../../preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf)
- [Backward intertwiners and a transitive commutant](../../preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf)

## Scope

For every irrational rotation angle $\theta\in(0,1)$, the formalization constructs a continuous nonnegative circle weight with a single zero and logarithmic integral $-\infty$ whose weighted rotation is nonzero and quasinilpotent. In its associated hyperfinite type $\mathrm{II}_1$ factor, the operator has no nontrivial invariant projection: $(1-p)Tp=0$ forces $p=0$ or $p=1$. The linked statements also include an earlier existence construction, a product realization, and the selected product model's Brown measure $\delta_0$.

The formalization for the companion paper [Backward intertwiners and a transitive commutant](../../preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf) gives, on every separable infinite-dimensional complex Hilbert space, a nonzero quasinilpotent operator whose commutant is transitive, proper, and closed in the strong operator topology. Thus no nontrivial closed subspace is invariant under every operator in the commutant.

The hyperinvariant-subspace problem asks whether every bounded operator on a complex Hilbert space has a nontrivial closed subspace invariant under every operator that commutes with it. The formalization gives a negative answer on every separable infinite-dimensional complex Hilbert space: there is a nonzero quasinilpotent operator with a transitive commutant. Its commutant is a proper unital operator algebra closed in the strong operator topology. The construction therefore has no nonzero proper closed hyperinvariant subspace.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finite-factor invariant-projection counterexample | [FiniteFactor.lean](../ComparatorChallenges/FiniteFactor.lean) |
| Quasinilpotent operator with transitive commutant | [BackwardIntertwiners.lean](../ComparatorChallenges/BackwardIntertwiners.lean) |
| Continuous-weight invariant-projection counterexample | [ContinuousCircleWeight.lean](../ComparatorChallenges/ContinuousCircleWeight.lean) |
| Quasinilpotent operator with a transitive commutant | [HyperinvariantSubspaces.lean](../ComparatorChallenges/HyperinvariantSubspaces.lean) |
| Invariant-projection counterexamples for every irrational rotation | [IrrationalRotation.lean](../ComparatorChallenges/IrrationalRotation.lean) |
| Brown measure of the selected product weighted shift | [ProductBrown.lean](../ComparatorChallenges/ProductBrown.lean) |
| Quasinilpotent operator without a hyperinvariant subspace | [HyperinvariantSubspaces.lean](../ComparatorChallenges/HyperinvariantSubspaces.lean) |