Lemma 5.2.1 — the OSR operators lie in the OSR algebra

Proved

BaconThesis.DFS.lemma_5_2_1

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

decoherenceoperator-algebrasp2o-gran-per-chapterp2o-plan-bookp2o-strengthenedp2o-v1quantum-information

Let $\mathcal H_S$ , $\mathcal H_E$ be finite dimensional and let

H=\sum_{\alpha}S_\alpha\otimes B_\alpha

for a finite family of system operators $S_\alpha$ and environment operators $B_\alpha$ , with evolution operator $U(t)=\exp[-iHt]$ . Then for every time $t$ and all environment vectors $\varphi,\psi$ , the system operator $\langle\varphi|U(t)|\psi\rangle=(I\otimes\langle\varphi|)U(t)(I\otimes|\psi\rangle)$ belongs to the OSR algebra $\mathcal A$ , the complex associative algebra generated by the $S_\alpha$ and the identity $I$ .

In particular every OSR operator $A_{(\mu,\nu)}(t)=\sqrt{p_\nu}\langle\mu|U(t)|\nu\rangle$ , for every environment initial state and every basis, lies in $\mathcal A$ . This reduces questions about the system's evolution under every environment initial condition to the structure of the algebra $\mathcal A$ .

Formalization Note The tensor product is the Kronecker product on pairs, system first; $\mathcal A$ is Algebra.adjoin ℂ (Set.range Sα).

Differences from the source:

generalization: the OSR operators A_{(µ,ν)}(t) = √p_ν⟨µ|U(t)|ν⟩ (|µ⟩ a basis, ρ_E(0) = ∑_ν p_ν|ν⟩⟨ν|) → ⟨φ|U(t)|ψ⟩ for all environment vectors φ, ψ; reason: the book's operators are the case φ = |µ⟩, ψ = √p_ν|ν⟩
generalization: B_α Hermitian, linearly independent, trace-orthonormal and complete, H a Hamiltonian → no condition on the B_α or on H; reason: the book's expansions are among those covered
generalization: the evolution time t → every real t; reason: includes every t ≥ 0
encoding: α = 0, …, A → a finite index type ι; reason: Lean convention; same instances

Preamble

import Mathlib
import Definitions.Def_BaconThesis_DFS_osrOp
import Definitions.Def_BaconThesis_DFS_osrAlgebra

open scoped Kronecker

Formal statement

namespace BaconThesis.DFS

/-- **Lemma 5.2.1: the OSR operators lie in the OSR algebra.**
Bacon, *Decoherence, Control, and Symmetry in Quantum Computers*, arXiv:quant-ph/0305025v1,
Lemma 5.2.1, p.69 (PDF p.86): for evolution due to a Hamiltonian with expansion
`H = ∑_α S_α ⊗ B_α` (eq. (5.1)), the OSR operators `Aᵢ(t)` are elements of the complex associative
algebra generated by the `S_α` plus the identity `I`.

For every finite family of system operators `S_α` and environment operators `B_α`, every time
`t` and all environment vectors `φ`, `ψ`, the operator `⟨φ|U(t)|ψ⟩` (`osrOp`) of
`H = ∑_α S_α ⊗ B_α` belongs to the subalgebra generated by the `S_α`.

**Formalization Note.** The book's OSR operators are `A_{(µ,ν)}(t) = osrOp H t |µ⟩ (√p_ν|ν⟩)`
(eq. (2.11)); the statement covers all `φ`, `ψ`. No condition is placed on the `B_α`
(the book takes them Hermitian, linearly independent and trace-orthonormal) nor on `H`, and
`t` is any real number. The tensor product is `Matrix.kronecker` on `s × e`, system first. -/
theorem lemma_5_2_1 {s e ι : Type} [Fintype s] [DecidableEq s] [Fintype e] [DecidableEq e]
    [Fintype ι]
    (Sα : ι → Matrix s s ℂ) (Bα : ι → Matrix e e ℂ) (t : ℝ) (φ ψ : e → ℂ) :
    osrOp (∑ α, Sα α ⊗ₖ Bα α) t φ ψ ∈ osrAlgebra Sα := by sorry

end BaconThesis.DFS

Source

Bacon, Decoherence, Control, and Symmetry in Quantum Computers, arXiv:quant-ph/0305025v1, Lemma 5.2.1, p.69 (PDF p.86), with eq. (5.1), p.68 (PDF p.85)

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph