Quantization of unitaries preserving the positive subspace onto itself

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.unitary_onto_quantization

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

prove2quantum

Let $(E,E_+,\theta)$ be reflection positive, let $q:E_+\to\widehat E$ be its canonical quotient, and let $U$ be a unitary operator with $UE_+=E_+$ . Then:

If $\theta U\theta=U$ , the induced operator $\widehat U$ is unitary.
If $\theta U\theta=U^{-1}$ , the induced operator satisfies $\widehat U^2=1$ . There are closed orthogonal complementary subspaces $F,G\subseteq E$ , invariant under $\theta,U,U^{-1}$ , giving reflection-positive triples $(F,F\cap E_+,\theta|_F)$ and $(G,G\cap E_+,\theta|_G)$ , such that $\widehat G=0$ and $(U|_F)^2=1$ .

E=F\oplus G,\qquad q(G\cap E_+)=\{0\},\qquad U^2|_F=1.

The equation involving $q$ expresses $\widehat G=0$ , because the reflected form on $G\cap E_+$ is the restricted ambient form. This statement keeps both alternatives and the existence of the invariant decomposition.

The positive subspace also splits as $E_+=(E_+\cap F)\oplus(E_+\cap G)$ , so the decomposition is a direct sum of reflection-positive triples.

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 2.4, PDF p. 9. Both alternatives and the invariant decomposition
are retained. The Hilbert sum is orthogonal and Eplus splits into its
intersections with F and G. The zero OS space of G is expressed by vanishing of the canonical
quotient on G intersect Eplus. No erroneous formula for G from the proof is used. -/
theorem unitary_onto_quantization [hHilbert : CompleteSpace E] (r : ReflectionData E) (U : E ≃ₗᵢ[ℂ] E)
    (hOnto : r.plus.map U.toLinearMap = r.plus) :
    ((∀ x, r.theta (U (r.theta x)) = U x) →
      ∃ V : OS r ≃ₗᵢ[ℂ] OS r, ∀ v : r.plus,
        ∃ hv : U (v : E) ∈ r.plus, V (osQ r v) = osQ r ⟨U v, hv⟩) ∧
    ((∀ x, r.theta (U (r.theta x)) = U.symm x) →
      ∃ A : OS r →L[ℂ] OS r,
        (∀ v : r.plus, ∃ hv : U (v : E) ∈ r.plus,
          A (osQ r v) = osQ r ⟨U v, hv⟩) ∧
        A.comp A = ContinuousLinearMap.id ℂ (OS r) ∧
        ∃ F G : Submodule ℂ E,
          IsClosed (F : Set E) ∧ IsClosed (G : Set E) ∧
          Disjoint F G ∧ F ⊔ G = ⊤ ∧
          Submodule.IsOrtho F G ∧
          r.plus = (r.plus ⊓ F) ⊔ (r.plus ⊓ G) ∧
          F.map r.theta.toLinearMap = F ∧ G.map r.theta.toLinearMap = G ∧
          F.map U.toLinearMap = F ∧ G.map U.toLinearMap = G ∧
          F.map U.symm.toLinearMap = F ∧ G.map U.symm.toLinearMap = G ∧
          (∀ v : r.plus, (v : E) ∈ G → osQ r v = 0) ∧
          (∀ v ∈ F, U (U v) = v)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

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

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 $P\subseteq E$ be a closed complex linear subspace, and let $\theta:E\to E$ be a complex linear isometric bijection such that $\theta^2x=x$ for every $x\in E$ and $\operatorname{Re}\langle\theta x,x\rangle\geq0$ for every $x\in P$ . Let $H$ be the separated completion of $P$ equipped with the reflected form $(x,y)\mapsto\langle\theta x,y\rangle$ and its seminorm $x\mapsto\sqrt{\operatorname{Re}\langle\theta x,x\rangle}$ , and write $q:P\to H$ for the canonical complex linear map into this completion, which identifies vectors at zero seminorm distance. For every complex linear isometric bijection $U:E\to E$ satisfying $U(P)=P$ , both of the following implications hold: (i) if $\theta(U(\theta x))=Ux$ for every $x\in E$ , then there exists a complex linear isometric bijection $V:H\to H$ such that, for every $v\in P$ , $Uv$ belongs to $P$ and $V(q(v))=q(Uv)$ ; (ii) if $\theta(U(\theta x))=U^{-1}x$ for every $x\in E$ , then there exists a continuous complex linear map $A:H\to H$ such that, for every $v\in P$ , $Uv$ belongs to $P$ and $A(q(v))=q(Uv)$ , such that $A\circ A=\operatorname{id}_H$ , and such that there exist closed complex linear subspaces $F,G\subseteq E$ satisfying all of

F\cap G=\{0\},\qquad F+G=E,\qquad \langle f,g\rangle=0\quad\text{for every }f\in F,\ g\in G,

P=(P\cap F)+(P\cap G),

\theta(F)=F,\quad \theta(G)=G,\quad U(F)=F,\quad U(G)=G,\quad U^{-1}(F)=F,\quad U^{-1}(G)=G,

q(v)=0\quad\text{for every }v\in P\cap G,\qquad U(Uv)=v\quad\text{for every }v\in F.

Here each occurrence of $q(Uv)$ uses $Uv$ as an element of $P$ , with its membership supplied by the asserted existence of a membership proof. No nonzero or positive-dimensional assumption is imposed on $E$ , $P$ , $H$ , $F$ , or $G$ ; zero spaces 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