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.