---
title: "Chain Obstructions and Deflation in the Invariant Subspace Problem"
author: "Larsen James Close"
date: "2026-03-09"
doi: "10.5281/zenodo.18917058"
canonical: "https://larsenclose.com/research/chain-obstructions/"
pdf: "https://larsenclose.com/papers/chain-obstructions.pdf"
zenodo: "https://doi.org/10.5281/zenodo.18917058"
---

# Chain Obstructions and Deflation in the Invariant Subspace Problem

**Abstract.** Reformulates the invariant subspace problem as a fixed-point problem on the lattice of closed subspaces and provides a structural analysis of chain-based methods. Proves that chains from both extremes of the lattice are forced to triviality — the Adámek construction and its dual are both structurally obstructed. Identifies stabilization and properness as jointly sufficient conditions for nontrivial invariant subspaces, and proves three new sufficient conditions: a deflation theorem, a lattice intermediate value theorem, and a descending chain condition theorem. The deflation theorem abstracts the order-theoretic component of Lomonosov's theorem. Independence results show the abstract lattice axiom system neither forces nor precludes nontrivial fixed points. Formalized in Lean 4 with zero sorry.

---
The ISP formalization (four files within the multi-paper code archive
(Close 2026e)) is available at DOI: 10.5281/zenodo.18915083. The Zenodo
record covers all three companion papers
(Close 2026b, 2026c); the ISP formalization comprises four files
(`InvariantSubspace.lean`, `InvariantSubspaceOrbits.lean`,
`InvariantSubspaceDeep.lean`, `ISPOperatorBridge.lean`) within the
larger repository.

# 1 Introduction

The invariant subspace problem (ISP) asks whether every bounded linear operator
$T$ on a separable infinite-dimensional complex Hilbert space $H$ has a nontrivial
closed invariant subspace—a closed subspace $V$ with $\{0\} \subsetneq V
\subsetneq H$ and $T(V) \subseteq V$. The problem has been open for Hilbert
spaces since at least the 1950s, despite major partial results for compact
operators (Aronszajn and Smith 1954), operators commuting with compact operators
(Lomonosov 1973), and various spectral conditions (Brown et al. 1979).
Counterexamples exist for general Banach spaces (Enflo 1987; Read 1985), but
the Hilbert space case remains unresolved.

We approach the ISP as a *fixed-point problem on a lattice*. The lattice
$\mathcal{L}$ of closed subspaces of $H$, ordered by inclusion, is a complete
lattice with bottom element $\bot = \{0\}$ and top element $\top = H$. The
orbit-closure map $F(V) = \overline{\operatorname{span}\{T^n v : v \in V,\, n \geq 0\}}$
is a monotone endomorphism of $\mathcal{L}$ satisfying $F(\bot) = \bot$ and
$F(\top) = \top$. The fixed points of $F$ are precisely the closed invariant
subspaces of $T$, and the ISP asks whether a fixed point exists strictly
between $\bot$ and $\top$.

This is a fixed-point problem—but the standard fixed-point theorems fail to
resolve it. Tarski's theorem (Tarski 1955) guarantees that $F$ has fixed
points, but they could all be trivial ($\bot$ or $\top$). The Adámek initial
algebra construction (Adámek 1974) builds the *least* fixed point by iterating
$F$ from $\bot$, but since $F(\bot) = \bot$, the chain is constant at $\bot$:
the least fixed point is trivial. The challenge is finding *intermediate* fixed
points.

This paper provides a structural analysis of what chain-based methods can and
cannot achieve for the ISP. Our main results are:

1. **Extremal chains are obstructed.** The Adámek chain from $\bot$ is constant
   at $\bot$ (Theorem 3.1), and its dual from $\top$ is constant at $\top$
   (Theorem 3.3). These are structural features, not accidental failures.

2. **Chain classification.** Every chain-based approach to the ISP falls into
   one of three types: bottom-up, top-down, or intermediate. The first two
   produce only trivial results; orbit chains from intermediate starting points
   are the *unique* viable chain-based method (Theorem 3.5).

3. **Three new sufficient conditions.**

   - The *deflation theorem*: if a proper pre-fixed point exists whose
     deflation chain avoids $\bot$, there is a nontrivial fixed point
     (Theorem 5.3).
   - The *lattice intermediate value theorem*: if a post-fixed point $u$ lies
     below a pre-fixed point $v$, there is a fixed point in $[u, v]$
     (Theorem 6.1).
   - The *DCC theorem*: under the descending chain condition, a proper
     pre-fixed point with non-collapsing deflation yields a nontrivial fixed
     point (Theorem 6.3).

4. **Independence.** The existence of nontrivial fixed points is independent
   of the abstract deep-lattice axiom system: both ISP success and ISP failure
   are consistent with any enrichment of the lattice structure that does not
   introduce analytic hypotheses (Theorem 7.1). These independence results
   concern the abstract lattice axiom system only; they are not independence
   results for the Hilbert-space invariant subspace problem itself.

The deflation theorem recovers the order-theoretic template abstracted from
Lomonosov's theorem
(Lomonosov 1973): the compact-operator commutation hypothesis provides the
proper pre-fixed point that the deflation theorem requires (Section 5.4).

These results identify where the difficulty of the ISP actually lives—not in
the existence of fixed points (Tarski guarantees those) but in their *location*
between the extremes. The lattice framework cannot resolve the ISP on its own
(the independence results show this), but it precisely identifies what
additional analytic input is needed: an intermediate starting point whose orbit
chain stabilizes below $\top$.

All results in this paper are formalized in Lean 4 with no `sorry` statements
(unresolved proof obligations). The formalization spans four files totaling
approximately 4000 lines of verified code.

# 2 The Lattice Framework

## 2.1 The subspace lattice

Let $T$ be a bounded linear operator on a Hilbert space $H$. The collection
$\mathcal{L}$ of closed subspaces of $H$, ordered by inclusion, forms a
complete lattice with:

- $\bot = \{0\}$ (the trivial subspace),
- $\top = H$ (the whole space),
- $V \vee W = \overline{V + W}$ (closure of the sum),
- $V \wedge W = V \cap W$ (intersection).

Define the *orbit-closure map* $F : \mathcal{L} \to \mathcal{L}$ by
$$
F(V) = \overline{\operatorname{span}\{T^n v : v \in V,\, n \geq 0\}}.
$$

Then $F$ is monotone ($V \subseteq W$ implies $F(V) \subseteq F(W)$),
$F(\bot) = \bot$ (since $T^n(0) = 0$ for all $n$), and $F(\top) = \top$
(since $V \subseteq F(V)$ for all $V$, so $H \subseteq F(H)$). The fixed
points of $F$—subspaces $V$ with $F(V) = V$—are precisely the closed
invariant subspaces of $T$.

The ISP asks: does there exist $V \in \mathcal{L}$ with $\bot < V < \top$ and
$F(V) = V$?

## 2.2 Abstract lattice axioms

We axiomatize the structure needed for the ISP analysis. The minimal axiom
system (corresponding to the Lean typeclass `InvariantLattice`) requires:

**Definition 2.1 (Invariant lattice).** An *invariant lattice* is a bounded
partial order $(\mathcal{L}, \leq, \bot, \top)$ with $\bot \neq \top$,
equipped with a monotone endomorphism $F : \mathcal{L} \to \mathcal{L}$
satisfying $F(\bot) = \bot$.

The reflexivity, transitivity, and antisymmetry of $\leq$, together with
$\bot \leq V$ and $V \leq \top$ for all $V$, are part of the axioms. The
condition $\bot \neq \top$ ensures the underlying space is nonzero.

For deeper results, we enrich this structure progressively:

**Definition 2.2 (Orbit lattice).** An *orbit lattice* extends an invariant
lattice with:

- Binary join $\sup(U, V)$ satisfying the usual least-upper-bound properties.
- Countable directed join $\omega$-$\sup : (\mathbb{N} \to \mathcal{L}) \to \mathcal{L}$ with each element below the join, and the join least among upper bounds.
- *Scott continuity*: $F(\omega$-$\sup\, s) = \omega$-$\sup\,(F \circ s)$ for every non-decreasing chain $s$.

**Definition 2.3 (Deep lattice).** A *deep lattice* extends an orbit lattice
with:

- Binary meet $\inf(U, V)$ satisfying the usual greatest-lower-bound properties.
- Countable decreasing infimum $\omega$-$\inf : (\mathbb{N} \to \mathcal{L}) \to \mathcal{L}$ with each element above the infimum, and the infimum greatest among lower bounds.
- *Co-continuity*: $F(\omega$-$\inf\, s) = \omega$-$\inf\,(F \circ s)$ for every non-increasing chain $s$.
- $F(\top) = \top$.

Each axiom system is formalized as a Lean 4 typeclass (`InvariantLattice`,
`OrbitLattice`, `DeepLattice`). Every theorem states its required axiom level
explicitly.

## 2.3 Pre-fixed and post-fixed points

**Definition 2.4.** Let $(\mathcal{L}, F)$ be an invariant lattice.

- $V$ is *pre-fixed* if $F(V) \leq V$. (Lean: `IsPreFixed`)
- $V$ is *post-fixed* if $V \leq F(V)$. (Lean: `IsPostFixed`)
- $V$ is a *fixed point* if $F(V) = V$. (Lean: `IsFixedPoint`)
- $V$ is *nontrivial* if $V \neq \bot$ and $V \neq \top$. (Lean: `IsNontrivial`)
- $V$ is a *proper pre-fixed point* if $V$ is pre-fixed, $V \neq \bot$, and $V \neq \top$. (Lean: `IsProperPreFixed`)

Every fixed point is both pre-fixed and post-fixed, and the converse holds by
antisymmetry. Pre-fixed points are "upper bounds on invariance": $F$ contracts
them. Post-fixed points are "lower bounds on invariance": $F$ expands them.

In the abstract lattice setting, post-fixed means $V \leq F(V)$. For the
concrete orbit-closure map, this becomes
$V \subseteq F(V) = \overline{\operatorname{span}\{T^n v : v \in V,\, n \geq 0\}}$,
which is automatic since the $n = 0$ term contributes $V$ itself. Thus, in the
operator case, the nontrivial structural content lies not in post-fixedness
alone but in pre-fixedness ($F(V) \leq V$, i.e., $T$-invariance),
stabilization, and interval constraints.

**Proposition 2.5.** *In any deep lattice, $\bot$ and $\top$ are both fixed
points of $F$.*

*Proof.* $F(\bot) = \bot$ by axiom, and $F(\top) = \top$ by axiom. $\square$

# 3 The Extremal Obstructions

This section establishes the first main result: standard chain methods from
the extremes of the lattice are structurally incapable of finding nontrivial
fixed points.

## 3.1 The Adámek chain from ⊥

The Adámek initial algebra construction (Adámek 1974) builds the least fixed
point of an endofunctor by iterating from the initial object. In our setting,
this gives the chain $\bot, F(\bot), F^2(\bot), \ldots$

**Theorem 3.1 (Adámek chain triviality).** *In any invariant lattice with
$F(\bot) = \bot$, the Adámek chain is constant at $\bot$: $F^n(\bot) = \bot$
for all $n \in \mathbb{N}$.*

*Proof.* By induction. The base case $F^0(\bot) = \bot$ is immediate. For the
inductive step, if $F^n(\bot) = \bot$, then $F^{n+1}(\bot) = F(\bot) = \bot$.
$\square$

*Lean name:* `adamek_chain_trivial` (in `InvariantSubspace`).

The standard categorical construction for finding least fixed points gives
*only* the trivial fixed point when applied to the ISP. This is not a failure
of the construction—it is a structural feature. The orbit closure of $\{0\}$
is $\{0\}$, so iterating $F$ from $\bot$ never leaves $\bot$.

**Corollary 3.2.** *No iterate of the Adámek chain from $\bot$ is nontrivial.*

*Lean name:* `adamek_insufficient_for_isp`.

## 3.2 The dual obstruction from ⊤

The dual construction iterates $F$ downward from $\top$: the chain $\top,
F(\top), F^2(\top), \ldots$

**Theorem 3.3 (Dual chain triviality).** *In any deep lattice with
$F(\top) = \top$, the descending chain from $\top$ is constant at $\top$:
$F^n(\top) = \top$ for all $n \in \mathbb{N}$.*

*Proof.* By induction, identical in structure to Theorem 3.1. If
$F^n(\top) = \top$, then $F^{n+1}(\top) = F(\top) = \top$. $\square$

*Lean name:* `dual_chain_trivial` (in `InvariantSubspaceDeep`).

**Corollary 3.4.** *No element of the descending chain from $\top$ is
nontrivial.*

*Lean name:* `dual_chain_insufficient`.

## 3.3 The chain classification theorem

**Theorem 3.5 (Chain classification).** *In a deep lattice, let
$s : \mathbb{N} \to \mathcal{L}$ be any chain satisfying $s(n+1) = F(s(n))$
for all $n$. If $s(0) \in \{\bot, \top\}$, then $s(n) \in \{\bot, \top\}$ for
all $n$.*

*Proof.* By induction on $n$. The base case holds by hypothesis. For the
inductive step, if $s(n) = \bot$, then $s(n+1) = F(\bot) = \bot$; if
$s(n) = \top$, then $s(n+1) = F(\top) = \top$. In either case
$s(n+1) \in \{\bot, \top\}$. $\square$

*Lean name:* `chain_from_extreme_trivial`.

**Corollary 3.6.** *No iterative $F$-chain starting from $\bot$ or $\top$
produces a nontrivial element.*

*Lean name:* `no_nontrivial_from_extremes`.

This theorem classifies all possible chain-based proof strategies for the ISP
into three types:

(a) **Bottom-up (Adámek):** $s(0) = \bot$. Killed by $F(\bot) = \bot$.
(b) **Top-down (dual Adámek):** $s(0) = \top$. Killed by $F(\top) = \top$.
(c) **Intermediate orbit chains:** $s(0) = a$ with $\bot < a < \top$. The
    *only* viable type.

The difficulty of the ISP is not in the chain method itself—it is in
*choosing the starting point*.

# 4 Orbit Chains and the Reduction to Two Conditions

## 4.1 Orbit chains from intermediate starting points

Given $a \in \mathcal{L}$ with $\bot < a < \top$, define the *orbit chain*
from $a$:
$$
s_a(0) = a, \qquad s_a(n+1) = \sup\bigl(s_a(n),\, F(s_a(n))\bigr).
$$
*Lean name:* `orbitChain`.

The join ensures the chain is non-decreasing: $s_a(n) \leq s_a(n+1)$ for all
$n$ (since $s_a(n) \leq \sup(s_a(n), F(s_a(n)))$). This is stronger than
pure $F$-iteration, which need not be monotone without the join. In the
concrete Hilbert space setting where $F$ is extensive ($V \subseteq F(V)$ for
all $V$, since the orbit closure contains $V$ itself), the join is redundant:
$\sup(V, F(V)) = F(V)$. The two constructions coincide for the orbit-closure
map.

**Proposition 4.1.** *The orbit chain is non-decreasing, and $a \leq s_a(n)$
for all $n$.*

*Lean names:* `orbitChain_mono`, `le_orbitChain`.

The *orbit closure* is the $\omega$-sup of the chain:
$\overline{O}(a) = \omega\text{-}\sup\, s_a$.

**Proposition 4.2.** *In any orbit lattice, the orbit closure $\overline{O}(a)$
is $F$-invariant: $F(\overline{O}(a)) \leq \overline{O}(a)$.*

*Proof.* By Scott continuity, $F(\omega\text{-}\sup\, s_a) =
\omega\text{-}\sup\,(F \circ s_a)$. Each
$F(s_a(n)) \leq s_a(n+1) \leq \omega\text{-}\sup\, s_a$, so
$\omega\text{-}\sup\,(F \circ s_a) \leq \omega\text{-}\sup\, s_a$. $\square$

*Lean name:* `orbit_closure_invariant`.

## 4.2 The two-condition reduction

**Theorem 4.3 (Orbit chain nontriviality).** *In an orbit lattice, let
$a \in \mathcal{L}$ with $a \neq \bot$. Suppose:*

*(i) **Stabilization:** there exists $n$ with $s_a(n) = s_a(n+1)$.*
*(ii) **Properness:** $s_a(n) \neq \top$ for all $n$.*

*Then there exists a nontrivial $F$-invariant element $V = s_a(n)$ with
$F(V) \leq V$, $V \neq \bot$, and $V \neq \top$.*

*Proof.* Let $n$ be the stabilization index. Then
$s_a(n) = s_a(n+1) = \sup(s_a(n), F(s_a(n)))$, which implies
$F(s_a(n)) \leq s_a(n)$ (since the join did not grow). The element $s_a(n)$ is
nonzero because $a \leq s_a(n)$ and $a \neq \bot$. It is proper by
hypothesis (ii). $\square$

*Lean name:* `orbit_nontrivial_if_bounded`.

The ISP thus reduces to: for every bounded operator $T$ on separable Hilbert
space, does there exist an intermediate starting point $a$ whose orbit chain
satisfies both stabilization and properness?

**Theorem 4.4 (Orbit failure dichotomy).** *Assume excluded middle. If the ISP
fails (no nontrivial $F$-invariant element exists), then for every
$a \neq \bot$, the orbit chain from $a$ either never stabilizes or reaches
$\top$.*

*Lean name:* `orbit_failure_modes`.

The converse direction is immediate: any nontrivial invariant subspace $V$ is
recovered by the orbit chain from itself, which stabilizes at step 0 (since
$\sup(V, F(V)) = V$ when $F(V) \leq V$).

*Lean name:* `invariant_is_orbit_fixed`.

## 4.3 The operator-lattice bridge

The operator-lattice bridge (`ISPOperatorBridge`) formalizes the translation
from operator-theoretic hypotheses to lattice conditions. Each classical
operator class maps to a specific lattice path:

- **Compact operators** provide starting points through eigenspaces: if
  a nonzero compact operator $K$ commuting with $T$ has a nonzero eigenvalue
  $\lambda$ (guaranteed by Riesz theory when $K$ is not quasinilpotent),
  the eigenspace $\ker(K - \lambda I)$ is finite-dimensional, $T$-invariant,
  and proper. Since $T$-invariance makes this eigenspace already a fixed
  point of $F$, the deflation chain is trivially constant. The DCC theorem
  (Theorem 6.3) applies (finite-dimensional subspaces satisfy DCC);
  non-collapse is a separate hypothesis in the formalization. The
  quasinilpotent case (spectrum $= \{0\}$, e.g., the Volterra operator)
  falls outside this eigenspace template; Lomonosov's proof handles it
  via Schauder's theorem rather than eigenspaces.
  (Lean: `compact_yields_deflation_setup`, `compact_isp`)

- **Normal operators** provide invariant spectral subspaces directly through
  spectral projections—these are fixed points of $F$ by construction, not by
  the deflation mechanism. The spectral theorem gives simultaneous pre-fixed and
  post-fixed data, which trivializes the lattice IVT to the degenerate interval
  $[V, V]$ for a fixed point $V$.
  (Lean: `normal_isp`, `normal_gives_ivt_data`)

- **Polynomially compact operators** (where $p(T)$ is compact for some nonzero
  polynomial $p$) follow the same lattice path as compact operators: the
  eigenspaces of $p(T)$ refine to $T$-invariant subspaces, giving proper
  pre-fixed points with DCC.
  (Lean: `polycompact_isp`)

- **General operators** (no algebraic hypothesis) admit only the orbit chain
  path: both stabilization and properness must be supplied as hypotheses,
  neither following from general monotonicity.
  (Lean: `general_isp`)

Three non-example models demonstrate that each hypothesis is necessary:

- **Two-element lattice** ($\{\bot, \top\}$, $F = \mathrm{id}$): no
  intermediate elements exist, so all lattice paths fail.
  (Lean: `two_no_isp`)
- **Four-element lattice** ($\{\bot, \mathrm{low}, \mathrm{high}, \top\}$,
  $F(\mathrm{high}) = \mathrm{low}$, $F(\mathrm{low}) = \bot$): a proper
  pre-fixed point exists ($\mathrm{high}$) but the deflation chain collapses
  to $\bot$, showing non-collapse is essential.
  (Lean: `four_deflation_collapses`, `four_no_nontrivial_fixed`)
- **ThreeB lattice** ($\{\bot, \mathrm{mid}, \top\}$,
  $F(\mathrm{mid}) = \top$): a post-fixed point exists but no proper pre-fixed
  point, showing the lattice IVT requires both sides.
  (Lean: `postfixed_insufficient_for_isp`)

The classification is exhaustive (Lean: `classification_exhaustive`) and the
non-examples are jointly independent (Lean: `nonexamples_independent`). The
point of the bridge is not to reprove the analytic theorems but to isolate the
order-theoretic slot where each analytic argument enters.

# 5 The Deflation Theorem

## 5.1 Pre-fixed points as starting candidates

A proper pre-fixed point $v$ satisfies $F(v) \leq v$ with $\bot < v < \top$.
Such a $v$ is "too big" for $F$: the map contracts it. Define the *deflation
chain* from $v$:
$$
d_v(0) = v, \qquad d_v(n+1) = F(d_v(n)).
$$
*Lean name:* `deflationChain`.

**Proposition 5.1.** *If $v$ is pre-fixed, the deflation chain is
non-increasing: $d_v(n+1) \leq d_v(n)$ for all $n$.*

*Proof.* By induction. The base step: $d_v(1) = F(v) \leq v = d_v(0)$ by the
pre-fixed hypothesis. The inductive step: if $d_v(n+1) \leq d_v(n)$, then
$d_v(n+2) = F(d_v(n+1)) \leq F(d_v(n)) = d_v(n+1)$ by monotonicity of $F$.
$\square$

*Lean name:* `deflationChain_decreasing`.

The *deflation infimum* is $w = \omega\text{-}\inf\, d_v$. By co-continuity:
$$
F(w) = F\bigl(\omega\text{-}\inf\, d_v\bigr) = \omega\text{-}\inf\,(F \circ d_v) = \omega\text{-}\inf\,(d_v \circ \mathrm{succ}) = \omega\text{-}\inf\, d_v = w.
$$

The last equality holds because shifting a non-increasing chain by one does not
change its infimum: since $d_v$ is non-increasing, any lower bound of
$d_v \circ \mathrm{succ}$ is also a lower bound of $d_v$, giving
$\omega\text{-}\inf\,(d_v \circ \mathrm{succ}) = \omega\text{-}\inf\, d_v$.

**Proposition 5.2.** *If $v$ is pre-fixed, the deflation infimum
$w = \omega\text{-}\inf\, d_v$ is a fixed point of $F$.*

*Lean name:* `deflationInf_is_fixed`.

## 5.2 The deflation theorem

**Theorem 5.3 (Deflation theorem).** *In a deep lattice, let $v$ be a pre-fixed
point with $v \neq \top$, and let $w = \omega\text{-}\inf\, d_v$ be the
deflation infimum. If $w \neq \bot$, then $w$ is a nontrivial fixed point:
$F(w) = w$, $w \neq \bot$, and $w \neq \top$.*

*Proof.* The element $w$ is a fixed point by the preceding proposition.
The hypothesis gives $w \neq \bot$. For $w \neq \top$: since $w \leq v$ (as
the infimum of a chain starting at $v$) and $v \neq \top$, if $w = \top$ then
$\top \leq v$, giving $v = \top$ by antisymmetry with $v \leq \top$, a
contradiction. $\square$

*Lean name:* `deflation_theorem`.

The key condition is that the deflation chain must *not* converge all the way
down to $\bot$. If it stops above $\bot$, the limit is a nontrivial invariant
subspace. If it reaches $\bot$, the theorem gives no information.

The unconditional form packages this:

**Corollary 5.4.** *If there exists a proper pre-fixed point $v$ with
$\omega\text{-}\inf\, d_v \neq \bot$, the ISP holds.*

*Lean name:* `deflation_gives_isp`.

## 5.3 Novelty of the deflation theorem

Prior sufficient conditions for the ISP—compactness (Aronszajn and Smith 1954),
normality, spectral decomposition—are *analytic*: they use properties of the
operator specific to Hilbert space. The deflation theorem is purely
*order-theoretic*. It works in any complete lattice with a monotone,
co-continuous endomorphism satisfying $F(\bot) = \bot$ and $F(\top) = \top$. No
inner product, no topology, no compactness. The deflation infimum being a fixed
point is a consequence of Knaster–Tarski applied to $[\bot, v]$; the novelty
is identifying deflation non-collapse as a sufficient condition for the ISP and
demonstrating its connection to Lomonosov's theorem, not the underlying lattice
mechanism.

The analytic content enters only when verifying the hypotheses: does a specific
operator have a proper pre-fixed point whose deflation chain avoids $\bot$?
The deflation theorem separates the ISP into two questions:

(i) **Existence:** Does a proper pre-fixed point exist? (Is there a proper
    closed subspace $V$ with $T(V) \subseteq V$?)
(ii) **Non-collapse:** Does the deflation chain avoid $\bot$? (Does the
     sequence $V, T(V), T^2(V), \ldots$ fail to converge to $\{0\}$?)

Question (i) is often easy—many operators have proper invariant subspaces for
routine reasons (kernels of $T - \lambda I$ for eigenvalues $\lambda$, for
instance). Question (ii) is the hard part: it requires some form of
"non-nilpotency" of the restriction of $T$ to $V$.

## 5.4 Connection to Lomonosov's theorem

Lomonosov's theorem (Lomonosov 1973) states: if $T$ commutes with a nonzero
compact operator $K$, then $T$ has a nontrivial invariant subspace. The
original proof uses Schauder's fixed-point theorem to find a fixed point of a
map on a compact convex set.

The order-theoretic connection is as follows. When $K$ is not quasinilpotent,
the compact-operator hypothesis provides a starting point: $K$ has a nonzero
eigenvalue $\lambda$ (by Riesz theory), and $\ker(K - \lambda I)$ is a
finite-dimensional invariant subspace of $K$. Since $T$ commutes with $K$,
the subspace $\ker(K - \lambda I)$ is $T$-invariant—hence already a fixed
point of $F$, not merely a pre-fixed point. It is proper because $K$ is compact
on an infinite-dimensional space (so its eigenspaces are finite-dimensional,
hence $\neq H$). Since the starting point is already a fixed point, the
deflation chain is trivially constant, so the DCC theorem is vacuously applicable but adds nothing. Non-collapse is taken as a separate hypothesis in the
formalization (Lean: `compact_isp`), not derived from compactness. The
formalization separates non-collapse as an explicit hypothesis from the
compact-operator data, maintaining this distinction at the type level.

When $K$ is quasinilpotent (spectrum $= \{0\}$), this eigenspace route is
unavailable. Lomonosov's original proof handles this case via Schauder's
fixed-point theorem on a compact convex set, which does not pass through the
eigenspace-to-lattice translation. The formalization takes the eigenspace data
as axiomatic input (`CompactOperatorData`), so it correctly restricts to the
non-quasinilpotent case.

The point of the connection is not that deflation discovers the subspace but
that the order-theoretic template—proper pre-fixed point with non-collapsing
deflation—is exactly what the compact-operator hypothesis provides. The
analytic content of Lomonosov's theorem—that commutation with a compact
operator supplies this starting point—is not replaced but *contextualized*:
the deflation theorem identifies what that analytic hypothesis is doing in
order-theoretic terms.

We emphasize the precise scope of this connection. The deflation theorem is more
general *in the lattice setting*: it applies to any proper pre-fixed point with
non-collapsing deflation, regardless of the source. But Lomonosov's theorem
includes the analytic step of *constructing* the pre-fixed point from the
compact operator, which the lattice framework does not address. This does not
reprove Lomonosov's theorem. It isolates the order-theoretic endpoint of the
argument: once analytic input supplies a proper pre-fixed point with
non-collapsing deflation, the lattice conclusion follows.

# 6 The Lattice IVT and DCC Theorem

## 6.1 Lattice intermediate value theorem

**Theorem 6.1 (Lattice intermediate value theorem).** *In a deep lattice, let
$u$ be post-fixed ($u \leq F(u)$) and $v$ be pre-fixed ($F(v) \leq v$) with
$u \leq v$. Then there exists a fixed point $W$ with $u \leq W \leq v$.*

*Proof.* Consider the deflation chain from $v$: $d_v(0) = v$,
$d_v(n+1) = F(d_v(n))$. We claim $u \leq d_v(n)$ for all $n$. The base case
is $u \leq v = d_v(0)$. For the inductive step, if $u \leq d_v(n)$, then
$u \leq F(u) \leq F(d_v(n)) = d_v(n+1)$ using the post-fixed hypothesis and
monotonicity. The deflation infimum $W = \omega\text{-}\inf\, d_v$ is a fixed
point (by Proposition 5.2), and $u \leq W$ (since $u$ is a lower bound for the
chain) and $W \leq v$ (as the infimum of a chain starting at $v$). $\square$

*Lean name:* `lattice_ivt`.

**Corollary 6.2 (Nontrivial IVT).** *If additionally $u \neq \bot$ and
$v \neq \top$, then the fixed point $W$ is nontrivial.*

*Proof.* $W \neq \bot$ because $u \leq W$ and $u \neq \bot$. $W \neq \top$
because $W \leq v$ and $v \neq \top$. $\square$

*Lean name:* `nontrivial_ivt`.

This is a constructive localization of Tarski's theorem to a specific interval.
Tarski says fixed points exist; the lattice IVT says *where* to find one when
you have both a post-fixed and a pre-fixed point. In ISP terms: if you can find
both a "too small" subspace ($F$ expands it) and a "too big" subspace ($F$
contracts it) with the small one contained in the big one, there is an
invariant subspace between them. This is the order-theoretic analogue of the
intermediate value theorem: a monotone function that goes up and then comes down
must cross the diagonal.

The IVT also interacts with orbit chains from Section 4. The orbit chain
builds *up* from a starting point; the deflation chain builds *down*. When
$a \leq v$ with $v$ pre-fixed, one can show $\overline{O}(a) \leq v$ by
induction (Lean: `orbitClosure_below_prefixed`). This gives the interval
$\omega\text{-}\inf\, d_v \leq \overline{O}(a) \leq v$: the orbit closure and
the deflation infimum squeeze toward the fixed points from opposite directions.
For the ISP, this means that finding a compatible post-fixed/pre-fixed pair not
only guarantees a fixed point exists in the interval—it also constrains where
the orbit chain must converge, narrowing the search.

## 6.2 The DCC theorem

**Theorem 6.3 (DCC theorem).** *In a deep lattice satisfying the descending
chain condition (every non-increasing chain stabilizes), let $v$ be a pre-fixed
point with $v \neq \top$. If the deflation chain from $v$ stabilizes at a point
different from $\bot$, then the ISP holds.*

*Proof.* By DCC, the deflation chain $d_v$ stabilizes at some index $n$:
$d_v(n) = d_v(n+1) = F(d_v(n))$, so $d_v(n)$ is a fixed point. The
non-collapse hypothesis gives $d_v(n) \neq \bot$. For $d_v(n) \neq \top$:
since $d_v(n) \leq v$ and $v \neq \top$, if $d_v(n) = \top$ then
$\top \leq v$, giving $v = \top$, a contradiction. $\square$

*Lean name:* `dcc_deflation_isp`.

The DCC holds automatically in the lattice of subspaces of a
*finite*-dimensional space (all descending chains of subspaces are finite). In
this setting, the deflation chain always stabilizes; the only question is
whether it reaches $\bot$—which is the non-nilpotency condition. The DCC
theorem thus connects the deflation framework to finite-dimensional invariant
subspace theory.

The precise dividing line is:

- **DCC + non-nilpotent restriction:** ISP holds. The deflation chain
  stabilizes above $\bot$.
- **DCC + nilpotent restriction:** The deflation chain reaches $\bot$. No
  information.

# 7 Independence Results

## 7.1 Nontrivial fixed points are independent of the deep-lattice axioms

**Theorem 7.1 (Independence).** *The existence of nontrivial fixed points is
independent of the abstract deep-lattice axiom system: both ISP success and ISP
failure are consistent with the deep lattice axioms.*

*Proof.* We exhibit two models.

**Model 1 (ISP failure):** The two-element lattice $\{\bot, \top\}$ with
$F = \mathrm{id}$. This satisfies all deep lattice axioms ($F$ is monotone,
$F(\bot) = \bot$, $F(\top) = \top$, $F$ is both Scott-continuous and
co-continuous). Both elements are fixed points, but neither is
nontrivial—there are no intermediate elements.

**Model 2 (ISP success):** The three-element lattice $\{\bot, m, \top\}$ with
$\bot < m < \top$ and $F = \mathrm{id}$. This satisfies all deep lattice
axioms, and $m$ is a nontrivial fixed point. $\square$

*Lean name:* `isp_independent_deep`.

The two-element lattice witnesses failure vacuously — no intermediate
elements exist. A richer failure model (e.g., a four-element lattice where
$F$ maps all intermediate elements to $\bot$) can also be constructed, but
the two-element model suffices for formal independence.

This result appears at three levels of axiom strength, all compiling at
`[propext]` only (Layer 0):

- `InvariantLattice`: `isp_independent_of_lattice`
  (in `InvariantSubspace`)
- `OrbitLattice`: `orbit_isp_independent`
  (in `InvariantSubspaceOrbits`)
- `DeepLattice`: `isp_independent_deep`
  (in `InvariantSubspaceDeep`)

(Earlier versions of these proofs required `Classical.choice`; the current
formalization eliminates this dependency via a typeclass refactoring
described in Section 9.2.)

`Classical.choice` was eliminated via an `OrbitLattice` typeclass split that
removed the choice dependency from the model constructions. The same two
models (two-element and three-element lattices) work at every level.

## 7.2 What the independence results show

The independence results demonstrate that the open status of the ISP is not an
artifact of weak axioms. Even with the full deep lattice axiom
system—monotonicity, Scott continuity, co-continuity, meets, joins,
$\omega$-sup, $\omega$-inf, $F(\bot) = \bot$, $F(\top) = \top$—the existence
of nontrivial fixed points remains underdetermined. Additional *analytic*
hypotheses (compactness, spectral properties, the specific geometry of Hilbert
space) are genuinely needed.

This is a model-theoretic underdetermination result for the abstract lattice
framework, not a set-theoretic independence result for the Hilbert-space ISP
itself.

## 7.3 What resolves ISP in each direction

The following additional hypotheses force ISP success:

- Compact operator hypothesis (Aronszajn–Smith (Aronszajn and Smith 1954)):
  eigenspace provides a starting point where compactness guarantees
  stabilization.
- Normal operator hypothesis: spectral decomposition provides invariant
  spectral subspaces directly.
- Proper pre-fixed point with deflation avoiding $\bot$ (Theorem 5.3).
- Post-fixed below pre-fixed in a nontrivial interval (Theorem 6.1).
- DCC + proper pre-fixed + non-nilpotent restriction (Theorem 6.3).

What would force ISP failure:

- Enflo-type constructions on Banach spaces (Enflo 1987) (not Hilbert space).
- No known construction on Hilbert space.

The open question is: does the specific geometry of separable
infinite-dimensional Hilbert space guarantee one of the sufficient conditions
above? The lattice framework identifies which conditions to check but cannot
answer this question on its own.

# 8 Related Work

## 8.1 The ISP literature

Aronszajn and Smith (Aronszajn and Smith 1954) proved the ISP for compact operators
using the fact that eigenspaces of compact operators on infinite-dimensional
spaces are finite-dimensional. Bernstein and Robinson (Bernstein and Robinson 1966)
extended this to polynomially compact operators using nonstandard analysis.
Lomonosov (Lomonosov 1973) established the ISP for operators commuting with a
nonzero compact operator, using Schauder's fixed-point theorem. Brown, Chevreau,
and Pearcy (Brown et al. 1979) proved the ISP for contractions whose
spectrum contains the unit circle.

Enflo (Enflo 1987) constructed a counterexample to the ISP on a Banach space,
and Read (Read 1985) gave a counterexample on $\ell^1$. The Argyros–Haydon
construction (Argyros and Haydon 2011) of hereditarily indecomposable spaces showed
that on certain Banach spaces, every operator is a scalar plus a compact
operator, so the ISP holds by Lomonosov's theorem. Chalendar and Partington
(Chalendar and Partington 2011) surveyed modern approaches.

The problem remains open for separable infinite-dimensional Hilbert spaces.

## 8.2 Lattice-theoretic fixed-point theory

Tarski's fixed-point theorem (Tarski 1955) establishes that every monotone
endomorphism on a complete lattice has a complete lattice of fixed points.
Adámek's initial algebra theorem (Adámek 1974) constructs the least fixed point
via $\omega$-chains from the initial object. Cousot and Cousot
(Cousot and Cousot 1979) developed abstract interpretation, using ascending and
descending chains of approximations to compute fixed points of monotone
operators on lattices. The ascending and descending chain methods of abstract
interpretation correspond to our bottom-up and top-down chains; the chain
classification theorem (Theorem 3.5) explains why these methods produce only
extremal fixed points in the ISP setting.

## 8.3 What this paper adds

Prior lattice-theoretic work on fixed points focuses on *finding* fixed points
(Tarski, Adámek, Knaster). This paper focuses on *locating* fixed points
between the extremes, which is what the ISP requires.

The chain classification theorem (Theorem 3.5) is new: to our knowledge, no
prior work proves that extremal chains are structurally obstructed for ISP-type
problems. The classification identifies orbit chains from intermediate starting
points as the unique viable chain-based method.

The deflation theorem (Theorem 5.3) provides a new sufficient condition not
present in the existing ISP literature. Prior sufficient conditions require
analytic hypotheses (compactness, spectral structure); the deflation theorem
requires only the existence of a proper pre-fixed point with non-collapsing
deflation.

The lattice IVT (Theorem 6.1) localizes Tarski's theorem to a specific
interval, giving a constructive method for finding fixed points between a
post-fixed point and a pre-fixed point. This localization appears implicit in
Tarski's proof but has not, to our knowledge, been stated as an explicit
sufficient condition for the ISP.

The operator-lattice bridge (Section 4.3) provides a formal class-by-class
translation from operator hypotheses to lattice conditions, with necessity
countermodels for each path. This goes beyond abstract lattice theory: it
identifies exactly which lattice theorem each classical ISP result uses, and
proves that the hypotheses cannot be weakened.

# 9 Discussion

## 9.1 What the framework reveals about the ISP

The difficulty of the ISP is not in the *existence* of fixed points (Tarski
guarantees those) but in their *location*. The chain classification
(Theorem 3.5) shows that standard iterative methods are structurally
insufficient—the starting point must be intermediate, which requires analytic
input. The deflation theorem (Theorem 5.3) and the lattice IVT (Theorem 6.1)
provide the structural conditions under which intermediate fixed points exist;
the independence results (Theorem 7.1) show that these conditions cannot be
derived from the lattice axioms alone.

The framework thus decomposes the ISP into a clean interface: the lattice
theory provides the *structural machinery* (chain classification, deflation,
interval localization), and the analytic theory must provide the *input* (an
intermediate starting point, a proper pre-fixed point, or a post-fixed/pre-fixed
pair).

## 9.2 The role of formalization

All results are formalized in Lean 4 with zero `sorry`, zero
`Classical.choice`, and zero custom axioms. The ISP independence results,
formerly dependent on `Classical.choice`, now compile at `[propext]` following
a typeclass refactoring that separated model-construction code from classical
infrastructure. The formalization forces precision about exactly which lattice
properties are used by each theorem. The independence results are genuine
independence—both models are constructively exhibited—not merely "we did not
find a proof."

The four Lean files correspond to the axiom hierarchy and the operator bridge:

- `InvariantSubspace`: base results on the invariant lattice. Adámek chain
  triviality, basic independence.
- `InvariantSubspaceOrbits`: orbit chains on the orbit lattice.
  Stabilization/properness reduction, failure mode dichotomy.
- `InvariantSubspaceDeep`: deflation, IVT, chain classification, DCC theorem,
  strengthened independence on the deep lattice.
- `ISPOperatorBridge`: operator class axiomatizations, translation theorems,
  classification, and three necessity countermodels.

All files are self-contained (no imports) and use no axioms beyond those
declared in their respective typeclasses. The independence theorems
(`isp_independent_of_lattice`, `orbit_isp_independent`, `isp_independent_deep`,
`nonexamples_independent`) all compile at `[propext]` only—`Classical.choice`
was eliminated via an `OrbitLattice` typeclass split. The `orbit_failure_modes`
theorem explicitly passes excluded middle as a hypothesis rather than invoking
it globally. All core lattice theorems—chain classification, deflation, IVT,
DCC—compile at `[]` (no axioms beyond the kernel), while only the
independence and model-construction results require `[propext]`. This makes the
stratification visible: the mathematical machinery is constructive; the
independence witnesses use extensional equality of propositions.

## 9.3 Open questions

1. Does every bounded operator on separable Hilbert space have a proper
   pre-fixed point whose deflation chain avoids $\bot$? An affirmative answer
   would solve the ISP via the deflation theorem.

2. Can the DCC theorem (Theorem 6.3) be extended to infinite-dimensional
   settings by replacing DCC with a weaker chain condition?

3. Is there an operator on Hilbert space with *no* proper pre-fixed points?
   Such an operator would satisfy $F(V) \not\leq V$ for every
   nontrivial $V$—a significant structural constraint. This is perhaps the
   sharpest new question the framework raises: if no such operator exists, the
   deflation theorem applies universally and the ISP reduces entirely to the
   non-collapse condition. An operator $T$ with no proper pre-fixed points
   would itself be a counterexample to the ISP, since every nontrivial
   invariant subspace is a proper fixed point, hence a proper pre-fixed point.
   The value of Question 3 is that it isolates the deflation non-collapse
   condition as the remaining degree of freedom once the pre-fixed point is
   granted, sharpening the search for operators that violate the non-collapse
   condition, which is the remaining open parameter in the deflation
   framework.

4. Can the lattice IVT (Theorem 6.1) be applied in general: do compatible
   post-fixed and pre-fixed points always exist for arbitrary operators?

# 10 Conclusion

The chain classification theorem identifies the structural landscape of the
ISP: chains from the extremes are doomed, and the only viable chain-based
approach starts from an intermediate element. The deflation theorem, lattice
IVT, and DCC theorem provide three new sufficient conditions for the existence
of nontrivial invariant subspaces, all purely order-theoretic. The independence
results show that these conditions cannot be derived from the lattice structure
alone—analytic input is genuinely required.

The framework identifies where the analytic content of the ISP enters: not in
the chain method itself, but in the *choice of starting point*. The invariant
subspace problem is hard not because fixed points are hard to find, but because
the right starting points are hard to choose. The lattice fixed-point framework
developed here is part of a broader program (Close 2026a) analyzing the
fold/unfold asymmetry of reflexive objects across mathematical domains;
applications to computability theory and complexity are developed in companion
papers (Close 2026b, 2026c).
The orbit-closure map's pre-fixed/post-fixed structure is an instance of the
fold/unfold asymmetry developed in Close (2026c); the deflation theorem
corresponds to the fold-dominant regime where contraction overcomes expansion.

# Appendix A: Axiom Profiles

The following table lists the axiom profile of each formalized theorem as
reported by Lean's `#print axioms` command. A profile of `[]` means the theorem
uses no axioms beyond the Lean kernel; `[propext]` means only propositional
extensionality is used. No theorem in the formalization uses `Classical.choice`
or any custom axiom.

File abbreviations: IS = `InvariantSubspace`,
ISO = `InvariantSubspaceOrbits`,
ISD = `InvariantSubspaceDeep`,
OB = `ISPOperatorBridge`.

| Theorem | Lean name | Profile | File |
|---|---|---|---|
| Adámek chain triviality | `adamek_chain_trivial` | `[]` | IS |
| Dual chain triviality | `dual_chain_trivial` | `[]` | ISD |
| Chain classification | `chain_from_extreme_trivial` | `[]` | ISD |
| Orbit nontriviality | `orbit_nontrivial_if_bounded` | `[]` | ISO |
| Orbit failure dichotomy | `orbit_failure_modes` (EM explicit) | `[]` | ISO |
| Deflation theorem | `deflation_theorem` | `[]` | ISD |
| Lattice IVT | `lattice_ivt` | `[]` | ISD |
| DCC theorem | `dcc_deflation_isp` | `[]` | ISD |
| Compact deflation setup | `compact_yields_deflation_setup` | `[]` | OB |
| Compact ISP | `compact_isp` | `[]` | OB |
| Normal ISP | `normal_isp` | `[]` | OB |
| Independence (base) | `isp_independent_of_lattice` | `[propext]` | IS |
| Independence (orbit) | `orbit_isp_independent` | `[propext]` | ISO |
| Independence (deep) | `isp_independent_deep` | `[propext]` | ISD |
| Non-example independence | `nonexamples_independent` | `[propext]` | OB |

All core lattice theorems (chain classification, deflation, IVT, DCC) and all
operator-bridge translations compile at `[]`. Only the independence results and
model constructions require `[propext]`, used for extensional equality of
propositions in the finite countermodels. `Classical.choice` was eliminated from
the independence proofs via an `OrbitLattice` typeclass split that separated
model-construction code from classical infrastructure.

# References

- Adámek, Jiří. 1974. "Free Algebras and Automata Realizations in the Language
  of Categories and Functors." *Comment. Math. Univ. Carolin.* 15: 589–602.
- Argyros, Spiros A., and Richard G. Haydon. 2011. "A Hereditarily
  Indecomposable $\mathcal{L}_\infty$-Space That Solves the
  Scalar-Plus-Compact Problem." *Acta Math.* 206 (1): 1–54.
- Aronszajn, N., and K. T. Smith. 1954. "Invariant Subspaces of Completely
  Continuous Operators." *Ann. Of Math. (2)* 60: 345–50.
- Bernstein, Allen R., and Abraham Robinson. 1966. "Solution of an Invariant
  Subspace Problem of K. T. Smith and P. R. Halmos." *Pacific J. Math.* 16:
  421–31.
- Brown, Scott W., Bernard Chevreau, and Carl Pearcy. 1979. "On the Structure
  of Contraction Operators. II." *J. Funct. Anal.* 32 (3): 271–91.
- Chalendar, Isabelle, and Jonathan R. Partington. 2011. *Modern Approaches to
  the Invariant-Subspace Problem*. Vol. 188. Cambridge Tracts in Mathematics.
  Cambridge University Press.
- Close, Larsen James. 2026a. *The Point*. Lean 4 formalization, 42 files.
  <https://doi.org/10.5281/zenodo.18878239>.
- Close, Larsen James. 2026b. *The Axiom Profile of Computation*. Manuscript.
- Close, Larsen James. 2026c. *Reflexive Compression Boundaries in Graded
  Categories*. Manuscript.
- Close, Larsen James. 2026e. *Witness Extraction Asymmetry Across Logic,
  Complexity, and Fixed-Point Mathematics*. Multi-paper code archive, Lean 4
  formalization, 93 files. <https://doi.org/10.5281/zenodo.18915083>.
- Cousot, Patrick, and Radhia Cousot. 1979. "Systematic Design of Program
  Analysis Frameworks." *Conference Record of the Sixth Annual ACM
  SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, 269–82.
- Enflo, Per. 1987. "On the Invariant Subspace Problem for Banach Spaces."
  *Acta Math.* 158 (3–4): 213–313.
- Lomonosov, V. I. 1973. "Invariant Subspaces for the Family of Operators
  Which Commute with a Completely Continuous Operator." *Funktsional. Anal. I
  Prilozhen.* 7 (3): 55–56.
- Read, C. J. 1985. "A Solution to the Invariant Subspace Problem on the Space
  $\ell_1$." *Bull. London Math. Soc.* 17 (4): 305–17.
- Tarski, Alfred. 1955. "A Lattice-Theoretical Fixpoint Theorem and Its
  Applications." *Pacific J. Math.* 5 (2): 285–309.