Whole-cycle quantum time reversal

Open

QAlgorithms.Papers.Independent.Intakethird100.P15.wholeCycle_timeReversal

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

prove2quantum

Let $\mathcal H$ be a nonzero complex Hilbert space with a nonempty finite or countable complete orthonormal basis real in a fixed conjugation. The self-adjoint Hamiltonian $H(t)$ is real in that conjugation, periodic with period $t_0>0$ , and satisfies $H(-t)=H(t)$ . Start at this symmetry origin and observe an integer number of full cycles. Let $U$ be the well-defined unitary strong limit of the chronological infinitesimal slice products, with each slice equal to $\exp(+i\tau H/\hbar)$ and $\hbar>0$ .

For every finite slicing at the symmetry origin, and for its unitary strong limit, the adjoint equals entrywise conjugation in the fixed real basis:

U^\dagger=\overline U.

Explicitly, $\langle i|U^\dagger|j\rangle=\overline{\langle i|U|j\rangle}$ for all basis labels $i,j$ ; equivalently $U_{ij}=U_{ji}$ . The same coefficient identity holds for each finite chronological slice product.

This is the reversal identity underlying the fluctuation relations, derived from the real Hamiltonians and palindromic slicing.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P15

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P15

open MeasureTheory Filter

open QAlgorithms.Papers.Independent.Information100.P37 (transition)

open QAlgorithms.Papers.Independent.Support21.P03 (reflectedLaw)

open QAlgorithms.Papers.Independent.Next46.P01 (extendedExpectation)

open scoped ENNReal Topology

universe u v w

variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]

variable {ι : Type v} {Ω : Type w} [MeasurableSpace Ω]

/-- Kurchan, PDF p.2, (3). Finite slice products and their well-defined unitary
strong limit have adjoint equal to entrywise conjugation in the fixed real basis.
The inverse of a unitary is its adjoint; scalar `star` is complex conjugation.
This derives reversal rather than including reversal in `CyclicDrive`. -/
theorem wholeCycle_timeReversal [Countable ι] [Nonempty ι]
    (b : HilbertBasis ι ℂ E) (d : CyclicDrive (Ω := Ω) b) :
    (∀ n i j,
      inner ℂ (b i) ((chronologicalEvolution (List.ofFn (d.slices n))).symm (b j)) =
        star (inner ℂ (b i) (chronologicalEvolution (List.ofFn (d.slices n)) (b j)))) ∧
    (∀ i j, inner ℂ (b i) (d.evolution.symm (b j)) =
      star (inner ℂ (b i) (d.evolution (b j)))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P15

Source

A Quantum Fluctuation Theorem, arXiv:cond-mat/0007360v2, PDF p. 2, Whole-cycle time reversal, (3)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $E$ be a complex Hilbert space, $\Omega$ a measurable space, and $(b_i)_{i\in\iota}$ a Hilbert basis with $\iota$ countable and nonempty. The given cyclic drive consists of a period $T>0$ , a number $\hbar>0$ , a cycle count $C\in\mathbb N$ , and, for every real $t$ , spectral data $(\mu_t,h_t,F_t)$ , where $\mu_t$ is a measure on $\Omega$ , $h_t:\Omega\to\mathbb R$ is measurable, and $F_t:E\to L^2(\mu_t;\mathbb C)$ is a complex linear isometric bijection such that each $F_t b_i$ is real almost everywhere. These entire spectral data satisfy $H_{t+T}=H_t$ and $H_{-t}=H_t$ . For every $n\in\mathbb N$ there are surjective complex linear isometries $V_{n,r}$ , $0\le r\le n$ ; writing $\Delta_n=CT/(n+1)$ and $t_{n,r}=(r+\tfrac12)\Delta_n$ , they satisfy, for all $x,y\in E$ ,

\langle x,V_{n,r}y\rangle = \int_\Omega \overline{F_{t_{n,r}}x(s)} e^{\,i(\Delta_n/\hbar)h_{t_{n,r}}(s)} F_{t_{n,r}}y(s)\,d\mu_{t_{n,r}}(s).

The drive also supplies a surjective complex linear isometry $U$ such that $U_nx\to Ux$ for every $x\in E$ , where $U_n=V_{n,n}\circ\cdots\circ V_{n,0}$ . The theorem asserts

\forall n\in\mathbb N,\ \forall i,j\in\iota,\qquad \langle b_i,U_n^{-1}b_j\rangle =\overline{\langle b_i,U_n b_j\rangle}, \qquad \forall i,j\in\iota,\qquad \langle b_i,U^{-1}b_j\rangle =\overline{\langle b_i,U b_j\rangle}.

The cycle count $C=0$ is 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