Three equivalent cyclicity criteria for a forward-invariant subspace

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.cyclicity_criteria

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $E$ be a complex Hilbert space, let $U$ be an algebraic unitary one-parameter group on $E$ , and let $F\subseteq E$ be a linear subspace invariant under $U_t$ for every $t>0$ . The following three conditions are equivalent:

The negative-time translates $U_tF$ , $t<0$ , span a dense subspace of $E$ .
There is a dense linear subspace $D\subseteq E$ such that for every $v\in D$ there is a real threshold $T_v$ with $U_tv\in F$ for all $t\geq T_v$ .
$F$ is $U$ -cyclic, meaning that its full real-time orbit has dense linear span.

\overline{\operatorname{span}\!\bigcup_{t<0}U_tF}=E\quad\Longleftrightarrow\quad (2)\quad\Longleftrightarrow\quad\overline{\operatorname{span}\!\bigcup_{t\in\mathbb R}U_tF}=E.

This criterion requires neither closedness of $F$ , reflection positivity, nor strong continuity.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P92

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P92

open scoped ComplexConjugate BigOperators NNReal ENNReal

open MeasureTheory

attribute [local instance] Classical.propDecidable

universe u v

variable (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]

variable {E}

/-- Lemma 3.5, PDF p. 11. Eplus is an arbitrary algebraic subspace; neither
closedness, reflection positivity, nor continuity is assumed. The large-time
threshold in the middle condition depends on the vector. -/
theorem cyclicity_criteria [hHilbert : CompleteSpace E] (U : RealUnitaryAction (E := E)) (F : Submodule ℂ E)
    (hF : ∀ t : ℝ, 0 < t → ∀ x ∈ F, U.op t x ∈ F) :
    ((orbitSpan U F (Set.Iio 0)).topologicalClosure = ⊤ ↔
      ∃ D : Submodule ℂ E, Dense (D : Set E) ∧
        ∀ v : D, ∃ T : ℝ, ∀ t : ℝ, T ≤ t → U.op t v ∈ F) ∧
    ((∃ D : Submodule ℂ E, Dense (D : Set E) ∧
        ∀ v : D, ∃ T : ℝ, ∀ t : ℝ, T ≤ t → U.op t v ∈ F) ↔ IsCyclic U F) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 11, Lemma 3.5

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $E$ be a complete complex inner product space, and let $U_t:E\to E$ , indexed by $t\in\mathbb R$ , be complex linear surjective isometries satisfying $U_0x=x$ and $U_{s+t}x=U_s(U_tx)$ for every $s,t\in\mathbb R$ and $x\in E$ . Let $F\subseteq E$ be a complex linear subspace such that $U_tx\in F$ for every strictly positive real $t$ and every $x\in F$ . For a set $S\subseteq\mathbb R$ , write $M_S=\operatorname{span}_{\mathbb C}\{U_tv:t\in S,\ v\in F\}$ . The theorem asserts the conjunction of the following two equivalences:

\overline{M_{(-\infty,0)}}=E \quad\Longleftrightarrow\quad \exists\,D\subseteq E\text{ a complex linear subspace},\ \overline D=E\ \text{and}\ \forall v\in D\ \exists T\in\mathbb R\ \forall t\in\mathbb R,\ t\geq T\Longrightarrow U_tv\in F,

and

\left( \exists\,D\subseteq E\text{ a complex linear subspace},\ \overline D=E\ \text{and}\ \forall v\in D\ \exists T\in\mathbb R\ \forall t\in\mathbb R,\ t\geq T\Longrightarrow U_tv\in F \right) \quad\Longleftrightarrow\quad \overline{M_{\mathbb R}}=E.

Here closures use the norm topology of $E$ , the threshold $T$ may depend on $v$ and may be any real number, $F$ need not be closed, and no continuity assumption on $t\mapsto U_tx$ is imposed.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph