Surjective time-zero quantization, multiplicativity, and the Markov identity

Open

QAlgorithms.Papers.Independent.Intakethird100.P92.markov_characterization

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)$ , with $E_0$ cyclic. Let $P:E\to E_0$ be the orthogonal projection, put $\varphi(t)=PU_tP^*$ , and let $\Gamma=q|_{E_0}$ . Let $P_+,P_0,P_-$ be the orthogonal projections onto $E_+,E_0,\theta(E_+)$ . The following are equivalent: $\Gamma$ is onto (and hence unitary); $\varphi$ is multiplicative on $(0,\infty)$ ; and

P_+P_0P_-=P_+P_-.

If these conditions hold, then for every real $t$ ,

\varphi(t)=\Gamma^*\widehat U_{|t|}\Gamma.

In particular, $\Gamma$ intertwines the positive-time compression and the OS semigroup. Also $E=N\oplus E_0\oplus\theta(N)$ orthogonally, $E_+$ is maximal among $\theta$ -positive linear subspaces, and $E_+$ is the closed linear span of $U_tE_0$ , $t>0$ .

All projections and $\Gamma$ are computed from the original data. The Markov identity and maximality are conclusions, not fields of an assumed realization.

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.17, PDF pp. 15--16: all three equivalent conditions and all
three consequences. The operator identity in (a) is expressed through every
matrix coefficient, so it does not require an assumed adjoint for Gamma. -/
theorem markov_characterization [hHilbert : CompleteSpace E] (r : ReflectionData E) (U : ReflectionGroup r)
    (hCyclic : IsCyclic U.group (timeZero r)) :
    (Function.Surjective (timeZeroQuotient r) ↔ CompressionMultiplicative r U) ∧
    (Function.Surjective (timeZeroQuotient r) ↔ MarkovCondition r) ∧
    (Function.Surjective (timeZeroQuotient r) →
      (∃ J : timeZero r ≃ₗᵢ[ℂ] OS r, ∀ v, J v = timeZeroQuotient r v) ∧
      (∀ t : ℝ, ∀ v w : timeZero r,
        inner ℂ (v : E) ((timeZeroCompression r U t w : timeZero r) : E) =
          inner ℂ (timeZeroQuotient r v) (quantized r U ⟨|t|, abs_nonneg t⟩ (timeZeroQuotient r w))) ∧
      (∀ t : ℝ≥0, ∀ v : timeZero r,
        timeZeroQuotient r (timeZeroCompression r U t v) = quantized r U t (timeZeroQuotient r v)) ∧
      (osNull r ⊔ timeZero r ⊔ (osNull r).map r.theta.toLinearMap = ⊤) ∧
      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) ∧
      (∀ F : Submodule ℂ E, r.plus ≤ F →
        (∀ v : F, 0 ≤ (inner ℂ (r.theta (v : E)) (v : E)).re) → F = r.plus) ∧
      (orbitSpan U.group (timeZero r) (Set.Ioi 0)).topologicalClosure = r.plus) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P92

end

Source

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

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 satisfying $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for every $v\in E_+$ . 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 every orbit map, $U_t(E_+)\subseteq E_+$ for $t\geq0$ , and $\theta U_t\theta=U_{-t}$ . Set $Z=\{v\in E_+:\theta v=v\}$ , and assume that the closure of the complex linear span of $\{U_tv:t\in\mathbb R,\ v\in Z\}$ is $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, write $q_0=q|_Z$ , and set $N=\{v\in E_+:q(v)=0\}\subseteq E$ . Write $\Pi_F$ for the ambient-valued orthogonal projection onto a closed subspace $F$ , with the convention that it is zero for nonclosed $F$ , and put $C_t(v)=P_Z(U_tv)$ for $v\in Z$ , where $P_Z$ takes values in $Z$ . For each $t\geq0$ , let $A_t$ be a chosen continuous complex linear operator on $H_r$ satisfying $A_tq(v)=q(U_tv)$ for every $v\in E_+$ , if one exists, and zero otherwise. Then both equivalences hold:

q_0\text{ is surjective} \quad\Longleftrightarrow\quad \bigl(\forall s,t>0,\ C_{s+t}=C_s\circ C_t\bigr), \qquad q_0\text{ is surjective} \quad\Longleftrightarrow\quad \Pi_{E_+}\Pi_Z\Pi_{\theta(E_+)} =\Pi_{E_+}\Pi_{\theta(E_+)}.

Furthermore, if $q_0$ is surjective, there exists a complex linear isometric bijection $J:Z\to H_r$ satisfying $Jv=q_0(v)$ for every $v\in Z$ ; for every real $t$ and every $v,w\in Z$ ,

\langle v,C_tw\rangle_E = \langle q_0(v),A_{|t|}q_0(w)\rangle_{H_r};

for every $t\geq0$ and every $v\in Z$ , $q_0(C_tv)=A_tq_0(v)$ ; the subspace sum $N+Z+\theta(N)$ equals $E$ ; each of the pairs $(N,Z)$ , $(N,\theta(N))$ , and $(Z,\theta(N))$ is orthogonal in $E$ ; every complex linear subspace $F\subseteq E$ containing $E_+$ and satisfying $\operatorname{Re}\langle\theta v,v\rangle\geq0$ for every $v\in F$ equals $E_+$ ; and

\overline{\operatorname{span}_{\mathbb C}\{U_tv:t>0,\ v\in Z\}}=E_+.

The multiplicativity equivalence uses strictly positive times, the intertwining identity includes time zero, and the inner product identity covers all real times through $|t|$ .

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