Density and orthogonal geometry of the time-zero subspace

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.time_zero_density

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

prove2quantum

Let $(E,E_+,\theta)$ be reflection positive, with canonical quotient $q$ , null space $N$ , and $E_0=\{v\in E_+:\theta v=v\}$ . If a linear subspace $D\subseteq E_0$ has dense image in $\widehat E$ , then $D$ is dense in $E_0$ and $q(E_0)=\widehat E$ . Moreover,

N=E_+\cap E_0^\perp=E_+\cap\theta(E_+)^\perp,

and $N\oplus E_0\oplus\theta(N)$ is an orthogonal direct sum and a closed subspace of $E$ .

No group or cyclicity hypothesis is imposed, and the final closed subspace is not asserted to be all of $E$ .

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.16, PDF p. 15. No one-parameter group or cyclicity assumption.
The final orthogonal sum is asserted closed, without asserting it is all of E. -/
theorem time_zero_density [hHilbert : CompleteSpace E] (r : ReflectionData E) (D : Submodule ℂ E)
    (hD : D ≤ timeZero r) (hDense : Dense (quotientImage r D)) :
    D.topologicalClosure = timeZero r ∧
    quotientImage r (timeZero r) = Set.univ ∧
    osNull r = r.plus ⊓ (timeZero r).orthogonal ∧
    osNull r = r.plus ⊓ (r.plus.map r.theta.toLinearMap).orthogonal ∧
    Submodule.IsOrtho (osNull r) (timeZero r) ∧
    Submodule.IsOrtho (osNull r) ((osNull r).map r.theta.toLinearMap) ∧
    Submodule.IsOrtho (timeZero r) ((osNull r).map r.theta.toLinearMap) ∧
    IsClosed ((osNull r ⊔ timeZero r ⊔ (osNull r).map r.theta.toLinearMap :
      Submodule ℂ E) : Set E) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

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

Read-back

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

Let $E$ be a complete complex inner product space, let $E_+\subseteq E$ be a closed complex linear subspace, and let $\theta:E\to E$ be an involutive complex linear isometric bijection satisfying $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for every $v\in E_+$ . Let $H_r$ be the separated completion of $E_+$ for the possibly degenerate inner product $\langle\theta v,w\rangle$ , let $q:E_+\to H_r$ be its canonical map, and set

Z=\{v\in E_+:\theta v=v\},\qquad N=\{v\in E_+:q(v)=0\},

viewing both as subspaces of $E$ . For every complex linear subspace $D\subseteq E$ , if $D\subseteq Z$ and $\{q(v):v\in E_+,\ v\in D\}$ is dense in $H_r$ , then all of the following hold:

\overline D=Z,\qquad \{q(v):v\in Z\}=H_r,\qquad N=E_+\cap Z^\perp,\qquad N=E_+\cap\theta(E_+)^\perp.

Moreover, $N$ is orthogonal to $Z$ , $N$ is orthogonal to $\theta(N)$ , $Z$ is orthogonal to $\theta(N)$ , and the subspace $N+Z+\theta(N)$ is closed in $E$ . Here closures and orthogonal complements are taken in the original space $E$ , and orthogonality of two subspaces means that every vector in one has zero inner product with every vector in the other. Zero subspaces and a zero completion are included.

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