Reflection-positive Hilbert space geometry

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.reflection_geometry

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

prove2quantum

Let $E$ be a complex Hilbert space, $E_+$ a closed complex subspace, and $\theta$ a unitary involution whose reflected form is positive semidefinite on $E_+$ . Let $\widehat E$ be the separated completion for this form, $q:E_+\to\widehat E$ its canonical map, $N=\ker q$ viewed in $E$ , and $E_0=\{v\in E_+:\theta v=v\}$ . The range of $q$ is dense, and for every $v\in E_+$ ,

\|qv\|^2=\langle\theta v,v\rangle,\qquad\|qv\|\leq\|v\|,\qquad \|qv\|=\|v\|\iff\theta v=v.

Moreover, $N$ is both the zero set of the reflected quadratic form and its radical; $N=E_+\cap\theta(E_+)^\perp$ , and $E_0=E_+\cap\theta(E_+)$ . Every linear subspace of $E_+$ on which $q$ preserves norm is contained in $E_0$ .

These identities specify the null space and the maximal isometric part of OS quantization. Pairings in the Lean statement use Mathlib's conjugate-linear first argument.

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}

/-- The geometric identities following Definition 1.1, PDF p. 5.
The printed reversed signs on theta eigenvectors are corrected by the displayed
norm calculation: theta(vplus)=vplus and theta(vminus)=-vminus. -/
theorem reflection_geometry [hHilbert : CompleteSpace E] (r : ReflectionData E) :
    DenseRange (osQ r) ∧
    (∀ v : r.plus,
      ‖osQ r v‖ ^ 2 = (inner ℂ (r.theta (v : E)) (v : E)).re ∧
      ‖osQ r v‖ ≤ ‖(v : E)‖ ∧
      (‖osQ r v‖ = ‖(v : E)‖ ↔ r.theta (v : E) = (v : E))) ∧
    (∀ v : r.plus, ((v : E) ∈ osNull r ↔
      inner ℂ (r.theta (v : E)) (v : E) = 0) ∧
      ((v : E) ∈ osNull r ↔ ∀ w : r.plus,
        inner ℂ (r.theta (w : E)) (v : E) = 0)) ∧
    osNull r = r.plus ⊓ (r.plus.map r.theta.toLinearMap).orthogonal ∧
    timeZero r = r.plus ⊓ r.plus.map r.theta.toLinearMap ∧
    (∀ F : Submodule ℂ E, ∀ hF : F ≤ r.plus,
      (∀ v : F, ‖osQ r ⟨v, hF v.property⟩‖ = ‖(v : E)‖) →
      F ≤ timeZero r) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, PDF p. 5, 1.1.geometry

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 $r$ consist of a closed complex linear subspace $H_+$ and a complex linear surjective isometry $\theta$ satisfying $\theta^2=I$ and $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for every $v\in H_+$ . Let $\mathcal H_r$ be the separated completion of $H_+$ with form $[v,w]=\langle\theta v,w\rangle$ and seminorm $\sqrt{\operatorname{Re}\langle\theta v,v\rangle}$ , and let $q:H_+\to\mathcal H_r$ be the canonical complex linear map. Define $N=\{v\in H_+:q(v)=0\}$ , regarded as a subspace of $E$ , and $H_0=H_+\cap\{v\in E:\theta v=v\}$ . The theorem asserts all of the following: $q(H_+)$ is dense in $\mathcal H_r$ ; every $v\in H_+$ satisfies

\|q(v)\|^2=\operatorname{Re}\langle\theta v,v\rangle,\qquad \|q(v)\|\leq\|v\|,\qquad \bigl(\|q(v)\|=\|v\|\ \Longleftrightarrow\ \theta v=v\bigr);

every $v\in H_+$ satisfies both

v\in N\ \Longleftrightarrow\ \langle\theta v,v\rangle=0, \qquad v\in N\ \Longleftrightarrow\ \langle\theta w,v\rangle=0\text{ for every }w\in H_+;

the subspace identities $N=H_+\cap(\theta(H_+))^\perp$ and $H_0=H_+\cap\theta(H_+)$ hold, where the orthogonal complement uses the original inner product of $E$ ; and for every complex linear subspace $F\subseteq E$ with $F\subseteq H_+$ , if $\|q(v)\|=\|v\|$ for every $v\in F$ , then $F\subseteq H_0$ . No nonzero-vector or nonzero-subspace restriction 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