An eventual-entry criterion for density after OS quantization

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.eventual_entry_density

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

prove2quantum

Let $U$ be a reflection-positive strongly continuous unitary one-parameter group on $(E,E_+,\theta)$ , and let $q:E_+\to\widehat E$ be the canonical quotient. Let $D\subseteq E_+$ be a linear subspace invariant under $U_t$ for all $t>0$ . If

\{v\in E_+:\text{there is }T>0\text{ with }U_Tv\in D\}

is dense in $E_+$ , then $q(D)$ is dense in $\widehat E$ .

This is a density criterion on the original positive subspace; no cyclicity or prior density of $q(D)$ is assumed.

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.6, PDF p. 11. Density of the eventual-entry set in Eplus implies
density of the canonical image q(D), without assuming that density. -/
theorem eventual_entry_density [hHilbert : CompleteSpace E] (r : ReflectionData E) (U : ReflectionGroup r)
    (D : Submodule ℂ E) (hD : D ≤ r.plus)
    (hInv : ∀ t : ℝ, 0 < t → ∀ v ∈ D, U.group.op t v ∈ D)
    (hDense : Dense {v : r.plus | ∃ T : ℝ, 0 < T ∧ U.group.op T v ∈ D}) :
    Dense (quotientImage r D) := 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.6

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 a complex linear isometric bijection satisfying $\theta^2=\mathrm{id}$ and $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for every $v\in E_+$ ; these constitute the reflection data $r$ . Let $(U_t)_{t\in\mathbb R}$ be complex linear isometric bijections satisfying $U_0=\mathrm{id}$ , $U_{s+t}=U_sU_t$ , continuity of $t\mapsto U_tv$ for every $v\in E$ , $U_t(E_+)\subseteq E_+$ for every $t\geq0$ , and $\theta U_t\theta=U_{-t}$ ; these constitute $U$ . Write $H_r$ for the separated completion of a copy of $E_+$ with the possibly degenerate inner product $(v,w)\mapsto\langle\theta v,w\rangle$ , and $q:E_+\to H_r$ for its canonical complex linear map. For every complex linear subspace $D\subseteq E$ , suppose that $D\subseteq E_+$ , that $U_t v\in D$ for every real $t>0$ and every $v\in D$ , and that

\{v\in E_+:\text{there exists a real }T>0\text{ with }U_Tv\in D\}

is dense in $E_+$ in its inherited topology from $E$ . Then $\{q(v):v\in E_+,\ v\in D\}$ is dense in $H_r$ . The entry time $T$ may depend on $v$ , and no nonzero or nondegeneracy condition is imposed on these spaces or on $q$ .

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