OS quantization commutes with fixed-vector reduction

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.quantization_reduction

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 assume that $E_+$ is $U$ -cyclic. Let $E_{\mathrm{fix}}$ consist of vectors fixed by all $U_t$ , and let $\widehat E_{\mathrm{fix}}$ consist of vectors fixed by all positive-time operators of the computed OS semigroup. Then $E_{\mathrm{fix}}\subseteq E_0$ , the canonical restriction $q|_{E_{\mathrm{fix}}}$ is a unitary isomorphism onto $\widehat E_{\mathrm{fix}}$ , and

E_{\mathrm{fix}}=\bigcap_{t>0}U_tE_+.

The unitary map is the restriction of the actual quotient, and its surjectivity is a conclusion. Cyclicity excludes the counterexamples discussed in Example 3.10.

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}

/-- Proposition 3.8, PDF pp. 11--12. The canonical fixed-space map is unitary
onto the quantized fixed space, and the intersection identity is in the original
Hilbert space. Cyclicity of Eplus is essential. -/
theorem quantization_reduction [hHilbert : CompleteSpace E] (r : ReflectionData E) (U : ReflectionGroup r)
    (hCyclic : IsCyclic U.group r.plus) :
    unitaryFixedSubspace U.group ≤ timeZero r ∧
    (∃ J : unitaryFixedSubspace U.group ≃ₗᵢ[ℂ] quantizedFixed r U,
      ∀ v : unitaryFixedSubspace U.group, ∃ hv : (v : E) ∈ r.plus,
        (J v : OS r) = osQ r ⟨v, hv⟩) ∧
    unitaryFixedSubspace U.group =
      ⨅ t : {t : ℝ // 0 < t}, r.plus.map (U.group.op t.val).toLinearMap := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

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

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$ be an involutive complex linear isometric bijection of $E$ with $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for all $v\in E_+$ . Let $(U_t)_{t\in\mathbb R}$ be a group of complex linear isometric bijections with $U_0=\mathrm{id}$ , $U_{s+t}=U_sU_t$ , continuous orbit maps, $U_t(E_+)\subseteq E_+$ for $t\geq0$ , and $\theta U_t\theta=U_{-t}$ . Suppose that the closure in $E$ of the complex linear span of $\{U_tv:t\in\mathbb R,\ v\in E_+\}$ is all of $E$ . Let $H_r$ be the separated completion of $E_+$ for the possibly degenerate inner product $\langle\theta v,w\rangle$ , with canonical map $q:E_+\to H_r$ . For each $t\geq0$ , define $A_t:H_r\to H_r$ to be a chosen continuous complex linear operator satisfying $A_tq(v)=q(U_tv)$ for every $v\in E_+$ , if such an operator exists, and the zero operator otherwise. Define

F=\{v\in E:U_tv=v\text{ for every }t\in\mathbb R\},\qquad Z=\{v\in E_+:\theta v=v\},\qquad G=\{\xi\in H_r:A_t\xi=\xi\text{ for every }t>0\}.

Then $F\subseteq Z$ ; there exists a complex linear isometric bijection $J:F\to G$ such that, for every $v\in F$ , there exists a witness that $v\in E_+$ and, using that membership to apply $q$ , $Jv=q(v)$ as elements of $H_r$ ; and

F=\bigcap_{t>0}U_t(E_+).

The intersection and the definition of $G$ range over every strictly positive real time, excluding zero.

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