All missions

Motivation

Gelfand duality identifies compact Hausdorff spaces with commutative unital C*-algebras: a space $X$ corresponds to the algebra $C(X)$ of continuous complex functions, and continuous maps correspond contravariantly to unital *-homomorphisms (Gelfand 1941; in categorical form, Negrepontis 1971). Measure theory has an analogous expectation. A measurable space with a σ-ideal of negligible sets yields the commutative von Neumann algebra $L^\infty$ of bounded measurable functions modulo equality almost everywhere, and every commutative von Neumann algebra should arise in this way. Making that expectation precise as an equivalence of categories requires deciding which measurable spaces to allow and which maps between them to identify.

Timeline. Stone (1936–1937) established the duality between Boolean algebras and Stone spaces, and between complete Boolean algebras and extremally disconnected ones. Segal (1951) introduced localizable measure spaces. Dixmier (1951) characterized the Gelfand spectra of commutative von Neumann algebras as the hyperstonean spaces. Loomis (1947) and Sikorski (1948) represented σ-complete Boolean algebras as measurable sets modulo meager sets on their Stone spaces. Von Neumann (1932), Maharam (1958), Ionescu Tulcea (1965), Vesterstrøm–Wils (1969), Edgar (1976) and Graf (1980) gave criteria for lifting homomorphisms of measure algebras to point maps. Pavlov (arXiv:2005.05284, J. Pure Appl. Algebra) assembled these ingredients into one equivalence of categories. That equivalence is the subject of this mission.

Setting

An enhanced measurable space $(X,M,N)$ is a set $X$, a σ-algebra $M$ of subsets of $X$, and a σ-ideal $N\subseteq M$ of the power set $2^X$, the negligible sets. A premap $f\colon(X,M,N)\to(X',M',N')$ is a map defined on a conegligible subset of $X$ with $f^*M'\subseteq M$ and $f^*N'\subseteq N$. Two premaps are weakly equal almost everywhere, $f\approx g$, when $f^*m\oplus g^*m\in N$ for every $m\in M'$. The space is compact if some compact class $K\subseteq M$ (a family with the finite intersection property for all subfamilies) has a non-negligible member inside every non-negligible measurable set. It is strictly localizable if it is isomorphic, through premaps, to a coproduct of a small family of spaces carrying faithful finite measures. CSLEMS is the category of compact strictly localizable spaces with $\approx$-classes of premaps.

A frame is a complete lattice in which finite meets distribute over arbitrary joins; the category of locales is the opposite of the category of frames. A complete Boolean algebra is localizable if $1$ is the supremum of the elements $a$ for which $aA$ carries a finite faithful continuous valuation. MLoc, the category of measurable locales, is the full subcategory of locales on the localizable Boolean algebras. A hyperstonean locale is a Stonean locale (coherent, regular, $\neg x\vee\neg\neg x=1$) in which every nonzero open has a positive normal valuation not vanishing on it. A hyperstonean space is a sober space whose locale of opens is hyperstonean. HStoneanLoc and HStonean take open maps as morphisms. CVNA is the category of commutative von Neumann algebras (C*-algebras with a predual) and normal unital *-homomorphisms.

Formalization targets

Goal: Theorem 1.1

$$\mathsf{HStonean}\simeq\mathsf{HStoneanLoc},\qquad \mathsf{HStoneanLoc}\simeq\mathsf{MLoc},\qquad \mathsf{CSLEMS}\simeq\mathsf{MLoc},\qquad \mathsf{MLoc}\simeq\mathsf{CVNA}^{\mathrm{op}}.$$

The goal is the existence of the four equivalences. It does not fix the functors.

The four equivalences with their functors

• Proposition 2.72: the equivalence $\mathsf{HStonean}\simeq\mathsf{HStoneanLoc}$ is implemented by the locale of opens $\Omega$.
• Proposition 2.73: the equivalence $\mathsf{HStoneanLoc}\simeq\mathsf{MLoc}$ is implemented by the compact opens $\mathrm{COpen}$.
• Theorem 3.20: the equivalence $\mathsf{MLoc}\simeq\mathsf{CVNA}^{\mathrm{op}}$ has inverse $\mathsf{ProjLoc}$, given by projections and restriction.
• Theorem 5.19: the equivalence $\mathsf{CSLEMS}\simeq\mathsf{MLoc}$ is implemented by $\mathsf{ML}$, the functor $(X,M,N)\mapsto M/N$, $f\mapsto f^*$.

Supporting milestones

The supporting milestones, in proof order:

• normal valuations versus continuous valuations on compact opens (Lemma 2.58);
• localizability through valuations (Lemma 2.53);
• completeness of $\mathsf{ProjAlg}(A)$ (Proposition 3.8);
• $A_*$ as continuous valuations (Proposition 3.9);
• $\mathsf{ProjAlg}$ as a functor (Lemma 3.11);
• σ-complete algebras with faithful valuations (Lemma 4.55);
• strict localizability implies localizability (Proposition 4.54);
• compactness of induced subspaces (Lemma 4.61);
• measurable images (Proposition 4.65);
• $\mathrm{TM}$ on hyperstonean spaces (Proposition 5.4);
• $\mathsf{ML}$ on morphisms (Lemma 5.11);
• the isomorphism $(X,M,N)\cong\mathrm{Spec}(\mathsf{ML}(X,M,N))$ (Proposition 5.16).

Significance

The result. Theorem 1.1 replaces commutative von Neumann algebras, a class of operator algebras, by measurable locales, which are pointless spaces. It also gives a point-set model, CSLEMS, in which morphisms are measurable maps modulo a null relation. With it, constructions on commutative von Neumann algebras can be carried out measure-theoretically and transported back: products, pushforwards of measures, and the identification of the predual with valuations. It also explains why the obvious choices fail. With localizable instead of strictly localizable spaces, with equality almost everywhere instead of weak equality, or without compactness, the measure-theoretic category is not dual to CVNA (Remarks 4.23 and 5.18).

Formalization. The theorem is proved in the paper. None of the five categories, and none of the equivalences, has a machine-checked form in Mathlib or on the platform. Mathlib has W*-algebras (WStarAlgebra), locales, Stonean spaces and Baire-measurable sets, but no normal homomorphisms, measure algebras or lifting theorems. The published module QAlgorithms_Papers_Independent_Support21_P20 formalizes this paper's valuations, enhanced measurable spaces and premaps, and poses several lemmas, three of which are milestones here. Completing the mission means formalizing Stone and Stonean duality for locales, the spectral theory of commutative von Neumann algebras through projections, and the von Neumann–Maharam lifting theorem for strictly localizable spaces.

Difficulty

The equivalences in §2 restrict classical dualities and are mostly bookkeeping once those dualities are available. Even so, Mathlib's Stone duality is not stated for locales with open maps. The central difficulty is Proposition 5.16. An object of CSLEMS must be isomorphic, through point maps, to the Stone spectrum of its own measure algebra. In one direction this needs a lifting $M/N\to M$ that is a Boolean homomorphism, and that uses strict localizability through the von Neumann–Maharam theorem. In the other direction it needs a point map from the spectrum back to $X$, constructed from the compact class. The natural first idea, choosing representatives class by class, does not give a homomorphism: liftings exist only through a transfinite construction. A second difficulty is Lemma 5.11. A Boolean homomorphism induced by a measurable map preserves countable suprema, but in general it does not preserve arbitrary ones (Remark 5.12). Compactness and the measurable image of Proposition 4.65 are what rule this out.

Formalization scope

All five categories live in one universe, with objects in Type u. The encoding commits to these conventions:

• CSLEMS. Morphisms are partial premaps (X → Option Y) modulo weak equality almost everywhere. Theorem 1.1's bullet speaks of maps of sets, but with total maps the theorem is false: $(\mathrm{pt},2^{\mathrm{pt}},2^{\mathrm{pt}})$ has no map to $\varnothing$ (Remarks 4.9, 4.15). Strict localizability uses a small index family and isomorphism in PreEMS; the faithful finite measures of its σ-finite pieces are countably additive maps $M\to\mathbb C$ with absolutely convergent sums (Remark 4.29), because Definition 4.28's saturation clause alone would also admit merely finitely additive ones. Compactness quantifies over arbitrary subfamilies, not countable ones.
• MLoc. The full subcategory of Mathlib's Locale on localizable Boolean algebras.
• HStoneanLoc and HStonean. Morphisms are open frame maps (Definition 2.15) and open continuous maps. Hyperstonean spaces are sober spaces whose frame of opens is hyperstonean.
• CVNA. Commutative CStarAlgebras with WStarAlgebra. Normality is stated as "pulls normal functionals back to normal functionals", which is equivalent to Definition 3.3 by Sakai's uniqueness of the predual.
• No nontriviality. The empty space, the one-element Boolean algebra and the zero algebra are allowed.

The equivalence milestones assert an equivalence together with a description of its functor. They never take a functor as a hypothesis, so none of the statements reduces to rfl or to an instance argument.

Reusable parts:

• the CSLEMS category, with the category laws of Propositions 4.7 and 4.14 proved inline;
• the quotient $M/N$ and the pull-back;
• $\mathrm{TM}$ and the Stone spectrum;
• the projection Boolean algebra.

Contributions are welcome at every level: proofs of the milestones, Stone and Stonean duality for locales, and a lifting theorem.

Selected references

• D. Pavlov, Gelfand-type duality for commutative von Neumann algebras, J. Pure Appl. Algebra 226 (2022); arXiv:2005.05284v3. https://arxiv.org/abs/2005.05284
• J. Dixmier, Sur certains espaces considérés par M. H. Stone, Summa Brasil. Math. 2 (1951), 151–182.
• M. H. Stone, Algebraic characterizations of special Boolean rings, Fund. Math. 29 (1937), 223–303. https://eudml.org/doc/212943
• I. E. Segal, Equivalences of measure spaces, Amer. J. Math. 73 (1951), 275–313. https://doi.org/10.2307/2372178
• D. Maharam, On a theorem of von Neumann, Proc. Amer. Math. Soc. 9 (1958), 987–994. https://doi.org/10.1090/S0002-9939-1958-0105479-6
• D. H. Fremlin, Measure Theory, Vol. 3 (Measure algebras), Torres Fremlin, 2002.
• P. T. Johnstone, Stone Spaces, Cambridge University Press, 1982.
• S. Sakai, C*-algebras and W*-algebras, Springer, 1971.

Motivation

In quantum mechanics, a system that interacts with an environment is described by a density matrix: a positive semidefinite complex matrix of trace one. When nothing is known about the joint state of the system and its environment, a natural model is to take that joint state to be a uniformly random pure state and to trace out the environment. The resulting law on density matrices, the induced measure of Życzkowski and Sommers (Życzkowski–Sommers 2001), is a standard model of a "typical" mixed state. It is used in quantum information to study the typical entanglement of bipartite pure states, as in Page's conjecture on average entropy (Page 1993).

Nechita (arXiv:quant-ph/0702154v3, Ann. Henri Poincaré 2007) studies the asymptotics of this ensemble. In the regime where the system dimension $n$ and the environment dimension $k(n)$ grow proportionally, the spectrum of the random density matrix, magnified by $cn$, has the same almost sure limit as the spectrum of a Wishart matrix: the Marchenko–Pastur law (Marchenko–Pastur 1967). The mission formalizes this result (Theorem 5) together with the chain of statements the paper uses to derive it.

Setting

Throughout, $\mathcal N_{\mathbb C}(0,1)$ denotes the law of $Z = X + iY$ where $X, Y$ are independent real Gaussians of mean $0$ and variance $1/2$, so that $\mathbb E|Z|^2 = 1$.

• Wishart matrix. If $X$ is an $n \times k$ complex matrix with i.i.d. $\mathcal N_{\mathbb C}(0,1)$ entries, $W = XX^*$ is a Wishart matrix of parameters $n$ and $k$.
• Pure states. A pure state of $\mathbb C^m$ is a ray $|\psi\rangle$: a nonzero vector up to a nonzero scalar factor. Its pure density matrix is $|\psi\rangle\langle\psi| = \psi\psi^*/\|\psi\|^2$, a rank-one orthogonal projection. The set $E_m$ of pure states carries a unique probability measure $\nu_m$ invariant under all unitaries $U \in U(m)$.
• Induced measure. Let $\mathcal H = \mathbb C^n$ (the system) and $\mathcal K = \mathbb C^k$ (the environment). If $|\psi\rangle$ has law $\nu_{nk}$ on the pure states of $\mathcal H\otimes\mathcal K$, the law of

$$\rho = \operatorname{Tr}_{\mathcal K}\,|\psi\rangle\langle\psi|$$

is the induced measure $\mu_{n,k}$ on $n\times n$ density matrices. Here $\operatorname{Tr}_{\mathcal K}$ is the partial trace over the environment.

• Empirical spectral measure. For an $n \times n$ matrix $A$ with eigenvalues $\lambda_1(A), \dots, \lambda_n(A)$ (counted with multiplicity) and a scale $s$, put $L^s(A) = \frac1n\sum_i \delta_{s\lambda_i(A)}$.
• Marchenko–Pastur law. For $c > 0$, with $a = (\sqrt c-1)^2$ and $b = (\sqrt c+1)^2$,

$$\mu_c = \max\{1-c,0\}\,\delta_0 + \frac{\sqrt{(x-a)(b-x)}}{2\pi x}\,\mathbf 1_{[a,b]}(x)\,dx .$$

Formalization targets

Goal: Theorem 5 (p. 14)

Let $c \in (0,\infty)$, let $k(n)$ be integers with $k(n)/n \to c$, and let $\rho_n$ have law $\mu_{n,k(n)}$ for every $n$. Then, almost surely,

$$L_n = \frac1n\sum_{i=1}^n \delta_{c\,n\,\lambda_i(\rho_n)} \;\Longrightarrow\; \mu_c \quad \text{weakly}.$$

Milestones, in the order the proof uses them

1. Proposition 1 (p. 4): $\nu_n$ exists and is unique.
2. Proposition 2, item 1 (p. 4): the class of a vector with law $\mathcal N^n_{\mathbb C}(0,I_n)$ has law $\nu_n$.
3. Eq. (12) (p. 6): if the coordinates $\psi_{ij}$ are arranged in an $n \times k$ matrix $X$, then $\operatorname{Tr}_{\mathcal K}|\psi\rangle\langle\psi| = XX^*/\operatorname{Tr}(XX^*)$.
4. Lemma 1 (p. 6): if $X$ has i.i.d. $\mathcal N_{\mathbb C}(0,1)$ entries, then $XX^*/\operatorname{Tr}(XX^*)$ has law $\mu_{n,k}$.
5. Eq. (24) (p. 9): the eigenvalues of $W/\operatorname{Tr} W$ are $\lambda_i/\sum_j\lambda_j$.
6. Theorem 2 (p. 8, quoted from Haagerup–Thorbjørnsen): almost surely, $\frac1n\sum_i\delta_{n^{-1}\lambda_i(W_n)} \Rightarrow \mu_c$ for Wishart matrices $W_n$ of parameters $n$ and $k(n)$.
7. Lemma 2, (45) (p. 13): $\operatorname{Tr} W_n/(n\,k(n)) \to 1$ almost surely.
8. The perturbation step (p. 14, eqs. (51)–(53)): dilating the atoms of a weakly convergent sequence by factors $t_n \to 1$ does not change a compactly supported weak limit.

Significance

The result. Theorem 5 says that the reduced state of a large random bipartite pure state has a deterministic spectral profile at scale $1/(cn)$. When $c < 1$, the environment is smaller than the system, and an atom of mass $1-c$ at $0$ records that $\rho_n$ has rank $k(n) < n$. When $c \ge 1$, the spectrum fills the interval $[a, b]$. The result transfers the classical Wishart limit to the induced measure, and with it quantitative information on the typical entanglement spectrum of bipartite pure states.

Formalizing it. The theorem is proved on paper, and none of it is machine-checked. The mission produces the induced-measure layer in Lean: complex Gaussian matrices, the invariant law on pure states, the partial-trace construction of $\mu_{n,k}$, and the Marchenko–Pastur law with its atom. Lemma 1 and eq. (12) connect these objects to Wishart matrices. The step that needs the most new library is Theorem 2, the Marchenko–Pastur theorem itself, which the paper quotes without proof. The perturbation step is posed as a statement about weak convergence. The paper argues it through convergence of moments, and in that argument weak convergence of $L_n^W$ is used as if it gave convergence of moments. The statement posed here is true as stated and needs no moment control.

Difficulty

The reduction from Theorem 5 to Theorem 2 is short on paper. The work lies elsewhere.

• Theorem 2 is a full random-matrix limit theorem. It needs a method that identifies the limit (moments, Stieltjes transforms, or free probability) and concentration strong enough to give almost sure convergence with no coupling between different $n$.
• Proposition 1 needs the invariant measure on complex projective space and a uniqueness argument for it. Mathlib's Haar-measure uniqueness is stated for groups, not for homogeneous spaces of $U(n)$.
• Lemma 1 needs the unitary invariance of the complex Gaussian vector $\mathcal N^{nk}_{\mathbb C}(0,I)$ and the image of a law under partial trace.

The naive route of "taking moments" in the perturbation step fails: weak convergence does not give convergence of moments, so (52)–(53) cannot be compared without extra tightness or moment bounds.

Formalization scope

• Pure states. Rays of $\mathbb C^m$ are represented by their rank-one projections (IsPureDensity: Hermitian, idempotent, trace one). A law on $E_m$ is a probability measure on $m\times m$ complex matrices carried by that set. Unitary invariance is invariance under $\rho \mapsto U\rho U^*$ (IsPureStateLaw).
• Induced law. "$\rho$ has law $\mu_{n,k}$" is the predicate HasInducedLaw: the law of $\rho$ is the image under the partial trace of some unitarily invariant law on pure states of $\mathbb C^n\otimes\mathbb C^k$. Proposition 1 makes this law unique.
• Indexing and partial trace. $\mathbb C^n\otimes\mathbb C^k$ is indexed by Fin n × Fin k with the environment on the right. The partial trace is the published WildeQIT.partialTraceRight. $\mathcal N_{\mathbb C}(0,1)$ is the published SpikedWishart.SoftEdge.stdComplexGaussian, with variance $1/2$ per real coordinate.
• Eigenvalues and convergence. Eigenvalues are roots of the characteristic polynomial, counted with multiplicity. Weak convergence is $\int f\,dL_n \to \int f\,d\mu_c$ for all bounded continuous $f$, with one null set for all $f$.
• Disclosed conventions. The hypotheses hold for $n \ge 1$ with $k(n)\ge 1$, since there are no pure states in dimension $0$. All random matrices live on one probability space, and nothing is assumed about their joint law across different $n$: the paper never couples them, and the almost sure statements hold for every coupling.
• Trivializations ruled out. Three trivializing formalizations are excluded:
  • stating the law of $\rho_n$ through the Wishart formula $W_n/\operatorname{Tr}W_n$, which would make Lemma 1 a hypothesis;
  • dropping the atom of $\mu_c$ or leaving the limit measure free;
  • stating "for each $f$, almost surely" in place of one null set for all $f$.

Solvers are welcome to contribute in four places:

• the general measure-theoretic pieces: Gaussian invariance, image laws under partial trace, and the dilation lemma, which are reusable beyond this mission;
• the deterministic linear algebra of eqs. (12) and (24);
• Lemma 2 through Borel–Cantelli;
• any proof of Theorem 2.

Selected references

• I. Nechita, Asymptotics of random density matrices, Ann. Henri Poincaré 8 (2007); arXiv:quant-ph/0702154v3. https://arxiv.org/abs/quant-ph/0702154v3
• K. Życzkowski, H.-J. Sommers, Induced measures in the space of mixed quantum states, J. Phys. A 34 (2001) 7111–7125. https://doi.org/10.1088/0305-4470/34/35/335
• U. Haagerup, S. Thorbjørnsen, Random matrices with complex Gaussian entries, Expo. Math. 21 (2003) 293–335. https://doi.org/10.1016/S0723-0869(03)80036-1
• V. A. Marchenko, L. A. Pastur, Distribution of eigenvalues for some sets of random matrices, Math. USSR-Sb. 1 (1967) 457–483. https://doi.org/10.1070/SM1967v001n04ABEH001994
• D. N. Page, Average entropy of a subsystem, Phys. Rev. Lett. 71 (1993) 1291–1294. https://doi.org/10.1103/PhysRevLett.71.1291

Motivation

The ultimate rates of quantum communication over optical fibre — how many secret bits or entangled pairs per channel use a lossy line can carry with unlimited local operations and classical communication (LOCC) — are bounded through a technique called teleportation stretching (Pirandola, Laurenza, Ottaviani, Banchi, arXiv:1510.08863). The idea is that if a channel $\mathcal E$ can be simulated by teleporting its input through a fixed resource state $\rho_{\mathcal E}$, then any adaptive protocol using $\mathcal E$ $n$ times can be rewritten as LOCC acting on $\rho_{\mathcal E}^{\otimes n}$, and every LOCC monotone of $\rho_{\mathcal E}$ bounds the protocol's output.

For the pure-loss channel the natural resource is the Choi state $\mathcal I\otimes\mathcal E_\eta(\Phi_{\rm EPR})$ of an ideal Einstein–Podolsky–Rosen state, which is not a normalizable state: it is the limit $\xi\to1$ of two-mode squeezed states and has infinite energy. R. Namiki (arXiv:1603.05292, 2016) observed that this limit can be avoided for lossy channels. Finite-squeezing teleportation, in the Braunstein–Kimble scheme (Braunstein and Kimble, PRL 80, 869, 1998), does not teleport perfectly, but its imperfection is itself a pure loss. Composing it with a second pure-loss channel therefore reproduces the target channel exactly, with a finite-energy resource.

Setting

A single bosonic mode is described on the Fock space $\ell^2(\mathbb N)$ with number basis $|n\rangle$. Every operator is handled through its number-basis kernel $K(m,n)=\langle m|X|n\rangle$; an operator on two modes has kernel $K((r,b),(r',b'))$, the first index labelling the first mode.

• The displacement $D(z)=e^{za^\dagger-\bar z a}$, $z\in\mathbb C$, has explicit matrix entries $\langle m|D(z)|n\rangle$; conjugation $\mathcal L_{D(z)}(X)=D(z)XD(z)^\dagger$ acts on kernels by matrix products.
• The pure-loss channel $\mathcal E_\eta$, $\eta\in(0,1)$, is the vacuum beam splitter of transmissivity $\eta$: $a\mapsto\sqrt\eta\,a$ with vacuum noise. $\mathcal I\otimes\mathcal E_\eta$ applies it to the second mode.
• The two-mode squeezed state with parameter $\xi\in(0,1)$ is $|\psi_\xi\rangle=\sqrt{1-\xi^2}\sum_{n\ge0}\xi^n|n\rangle|n\rangle$ on modes $(A',B)$.
• The CV-Bell states are $|\Phi_\beta\rangle=(\mathbb 1\otimes D^\dagger(\beta))|\Phi_0\rangle$ with $|\Phi_0\rangle=(2\pi)^{-1/2}\sum_n|n\rangle|n\rangle$; they are improper vectors with $\iint|\Phi_\beta\rangle\langle\Phi_\beta|\,dx\,dp=\mathbb 1$, where $\beta=(x+ip)/\sqrt2$.

Alice holds a two-mode state $\rho_{RS}$ ($S$ the signal, $R$ a reference) and Alice and Bob share a resource $\omega_{A'B}$. The unnormalized branch for outcome $\beta$ is the kernel on $(R,B)$

$$\langle\Phi_\beta|_{SA'}(\rho\otimes\omega)|\Phi_\beta\rangle_{SA'}=\frac1{2\pi}\sum_{n,n',k,k'}\langle n|D(\beta)|k\rangle\,\rho\big((\cdot,n),(\cdot,n')\big)\,\omega\big((k,\cdot),(k',\cdot)\big)\,\overline{\langle n'|D(\beta)|k'\rangle}.$$

Formalization targets

Goal: the Theorem (26)–(27), corrected protocol

For $0<\eta<\xi^2<1$ put $\eta'=\eta/\xi^2$ and $\rho_{\mathcal E'}=\mathcal I\otimes\mathcal E_{\eta'}(\psi_\xi)$, the effective Choi state. For every two-mode density $\rho_{AB}$,

$$\mathcal I\otimes\mathcal E_\eta(\rho_{AB})=\iint_{\mathbb R^2}\mathcal L_{\mathbb 1\otimes D(\sqrt{\eta'}\xi\bar\beta)}\Big(\langle\Phi_\beta|_{SA'}(\rho_{AB}\otimes\rho_{\mathcal E'})|\Phi_\beta\rangle_{SA'}\Big)\,dx\,dp ,$$

entry by entry, with every series and integral convergent, and $\eta\le\eta'<1$. The parameters and the protocol are independent of $\rho_{AB}$.

Milestones

1. (18) Displacement covariance: $\mathcal E_\eta(D(\beta)\rho D^\dagger(\beta))=D(\sqrt\eta\beta)\mathcal E_\eta(\rho)D^\dagger(\sqrt\eta\beta)$ for every density.
2. Composition (App. B): $\mathcal E_\eta\circ\mathcal E_{\eta'}=\mathcal E_{\eta\eta'}$.
3. (20), coherent input, corrected: $\langle\Phi_\beta|(|\alpha\rangle\langle\alpha|\otimes\psi_\xi)|\Phi_\beta\rangle=\frac{1-\xi^2}{2\pi}e^{-(1-\xi^2)|\alpha-\bar\beta|^2}|\xi(\alpha-\bar\beta)\rangle\langle\xi(\alpha-\bar\beta)|$.
4. (22), coherent input: the weights $\frac{1-\xi^2}{2\pi}e^{-(1-\xi^2)|\alpha-\bar\beta|^2}$ integrate to $1$ over $dx\,dp$.
5. (23), coherent input, corrected: after $\mathcal E_\eta$ the branch of milestone 3 becomes the same weight times $|\sqrt\eta\xi(\alpha-\bar\beta)\rangle\langle\sqrt\eta\xi(\alpha-\bar\beta)|$.
6. (24), every density, corrected: $\iint D(\sqrt\eta\xi\bar\beta)\,\mathcal E_\eta(T_{\beta,\xi}\rho T_{\beta,\xi}^\dagger)\,D^\dagger(\sqrt\eta\xi\bar\beta)\,dx\,dp=\mathcal E_{\eta\xi^2}(\rho)$.

Significance

The result. The Theorem shows that one use of a pure-loss channel, on any input including half of an entangled state, is reproduced exactly by LOCC on the finite-energy state $\mathcal I\otimes\mathcal E_{\eta'}(\psi_\xi)$. In the paper's §II.C this is the step that would let entanglement-measure bounds for $n$ adaptive channel uses be evaluated on a genuine density operator, without the limit $\xi\to1$ that the ideal-EPR argument needs. The relation (24) also makes precise in which sense the realistic teleportation family $\{T_{\beta,\xi}\}$ is not teleportation-stretching in the finite-dimensional sense, yet simulates the channel after an outcome-dependent displacement.

Formalizing it. The result is proved in the paper by a short computation through the Glauber–Sudarshan $P$ representation, which is heuristic for nonclassical inputs. No machine-checked version exists. A formal proof requires an argument valid for every density operator, together with all convergence statements. The formalization also records a sign slip: with the paper's own definitions (4), (16), (A4) and $D(\beta)=e^{\beta a^\dagger-\beta^*a}$, the step $\langle\alpha^*|D(\beta)=\langle\alpha^*+\beta^*|$ in (20) should read $\langle\alpha^*-\beta|$. Consequently (20) and (23) hold with $\alpha-\bar\beta$ in place of $\alpha+\beta$, and the correction in (24) is $D(\sqrt\eta\xi\bar\beta)$ rather than $D^\dagger(\sqrt\eta\xi\beta)$; a numerical evaluation of the printed (24) for the input $0.6|0\rangle+0.8i|1\rangle$ gives an error of $0.38$ in the output matrix, against $8\times10^{-5}$ (grid-limited) for the corrected one. The Theorem itself, existential in the protocol, is unaffected.

Difficulty

The obvious route is the paper's: write $\rho=\int P_\alpha|\alpha\rangle\langle\alpha|\,d^2\alpha$, compute everything for coherent states, and integrate. For nonclassical states $P$ is not a function, or even a measure, so this route is not a proof; passing from coherent inputs to all densities needs a density or continuity argument in trace norm, with interchange of the outcome integral and the infinite Fock series. The Bell projection itself is a contraction against improper vectors, here encoded as an absolutely convergent four-fold series whose convergence for arbitrary trace-class inputs is part of the work. Finally, the composition $\mathcal E_\eta\circ\mathcal E_{\eta'}=\mathcal E_{\eta\eta'}$ and the covariance (18) are standard on covariance matrices but must be established on number-basis kernels, where they are identities between infinite series with binomial weights.

Formalization scope

• Representation. All states and outputs are number-basis kernels. Inputs are bounded operators on $\ell^2(\mathbb N)$ or $\ell^2(\mathbb N\times\mathbb N)$ satisfying the published density predicates (trace class, self-adjoint, positive, unit trace), from QAlgorithms_Papers_Independent_Dependency50_P39; the loss channel is the vacuum-loss kernel of QAlgorithms_Papers_Independent_Frontier30_P21; coherent states use its coherentDensity.
• Bell projection. It is the Fock form of (16) with (A4), with the factor $(2\pi)^{-1}$ explicit; the CV-Bell states are not formalized as vectors. The outcome is $\beta=(x+ip)/\sqrt2$ and the average is over $\mathbb R\times\mathbb R$ with Lebesgue measure, the paper's $dx\,dp$.
• Conventions. The resource has Alice's mode $A'$ first and Bob's mode $B$ second; the loss of $\rho_{\mathcal E'}$ acts on $B$. Every series is asserted summable and every integrand integrable as part of the conclusion, so default values of divergent series or non-integrable functions never satisfy a statement.
• Corrected sign. Milestones (20), (23), (24) and the goal use $\alpha-\bar\beta$ and the correction $D(\sqrt{\eta'}\xi\bar\beta)$, as explained above.
• Coherent-input restriction. Milestones (20), (22), (23) are stated for coherent inputs ($P$ a point mass), because the $P$ representation (19) is not available for general states; (24) and the goal are stated for every density, as printed.
• LOCC. The general class of LOCC maps is not formalized; $\Lambda$ is the explicit protocol of (24). An existential "there is a map $\Lambda$ with $\Lambda(\rho_{\mathcal E'})=\mathcal I\otimes\mathcal E_\eta(\rho_{AB})$" would be trivially true (take $\Lambda$ constant) and is ruled out by stating the protocol, with $\eta'$, $\xi$ and the correction fixed before $\rho_{AB}$; likewise the Bell branch is the defining series, never its closed form.
• Not covered. The thermal-loss and amplifier versions (§III, (30)–(33)), the $n$-use relative-entropy bound (§II.C), and the finite-dimensional review (§II.A). The statement $\mathcal E_\eta(|\alpha\rangle\langle\alpha|)=|\sqrt\eta\alpha\rangle\langle\sqrt\eta\alpha|$ used inside (20) is the existing Open goal Frontier30.P21.coherentOutput and is not posed again.
• Reusable parts. Proofs of displacement covariance and of channel composition on Fock kernels, and summability lemmas for displacement matrices against trace-class kernels, are useful beyond this mission; contributions of such lemmas are welcome.

Selected references

• R. Namiki, Teleportation stretching for single-mode Gaussian channels, arXiv:1603.05292v1, 2016. https://arxiv.org/abs/1603.05292
• S. Pirandola, R. Laurenza, C. Ottaviani, L. Banchi, Fundamental limits of repeaterless quantum communications, arXiv:1510.08863v3, 2015. https://arxiv.org/abs/1510.08863
• S. L. Braunstein, H. J. Kimble, Teleportation of continuous quantum variables, Phys. Rev. Lett. 80, 869, 1998. https://doi.org/10.1103/PhysRevLett.80.869

Motivation

Quantum technologies usually prepare a desired state by isolating a system and driving it with carefully timed unitary operations; coupling to an environment is treated as noise. Dissipative state preparation reverses this view: one engineers the system–environment coupling so that the open-system dynamics itself drives every initial state into a prescribed target state. Because the target is a fixed point that attracts all initial conditions, the preparation needs no initialization and is self-correcting against perturbations that leave the dynamics unchanged.

In 2008 three closely related papers made this programme concrete. Diehl, Micheli, Kantian, Kraus, Büchler and Zoller showed how cold atoms can be driven into condensed many-body states by engineered dissipation (arXiv:0803.1482); Verstraete, Wolf and Cirac showed that dissipative dynamics can perform universal quantum computation and prepare matrix product and PEPS states (arXiv:0803.1447); and Kraus, Büchler, Diehl, Kantian, Micheli and Zoller, Preparation of entangled states by quantum Markov processes (arXiv:0803.1463), gave the general uniqueness criteria and the explicit construction this mission formalizes. The last paper's central claim is that every pure state of $n$ qubits is the unique stationary state of an explicitly given Markovian process, and that this process relaxes on a time scale independent of $n$.

Setting

A quantum Markov process on a $d$-dimensional Hilbert space is a master equation $\dot\rho = \mathcal L(\rho)$ for a density matrix $\rho$ (a positive semidefinite $d\times d$ complex matrix of trace one). In the paper's Eq. (2) the generator, or Liouvillian, is

$$\mathcal L_{H,c_l}(\rho) = -i[H,\rho] + \sum_l g_l\bigl(2c_l\rho c_l^\dagger - c_l^\dagger c_l\rho - \rho c_l^\dagger c_l\bigr),$$

where $H$ is a Hermitian matrix (the Hamiltonian), the $c_l$ are arbitrary complex matrices (the jump operators) and $g_l$ are rates. The solution is $\rho(t) = e^{t\mathcal L}(\rho(0))$. The paper writes $P = \sum_l g_l c_l^\dagger c_l$, $Q = P - iH$ and $\mathcal E(\rho) = 2\sum_l g_l c_l\rho c_l^\dagger$.

A stationary state is a density matrix with $\mathcal L(\rho) = 0$. A vector annihilated by every $c_l$ and an eigenvector of $H$ is a dark vector; the set $D = K(P)\cap ES(H)$ of dark vectors, when it is a subspace (all dark vectors share one eigenvalue $E$ of $H$), yields the dark states, the density matrices with range inside $D$.

For $n$ qubits, $\sigma_-^{(k)} = \mathbb 1\otimes\dots\otimes|0\rangle_k\langle1|\otimes\dots\otimes\mathbb 1$ lowers qubit $k$ from $|1\rangle$ to $|0\rangle$. Given any unitary $U$, the target is $|\Psi\rangle = U|0^n\rangle$, which ranges over all pure states, and the construction of §IV uses the $n$ jump operators $c_k = U\sigma_-^{(k)}U^\dagger$ with rates $g_k$. The relaxation time $T_{\mathrm{relax}}$ is the inverse of the least value of $-\operatorname{Re}\mu$ over the nonzero eigenvalues $\mu$ of $\mathcal L$.

Formalization targets

Goal: unique, attractive, and fast

For $n\ge1$, any unitary $U$ and rates $g_1,\dots,g_n>0$:

$$\text{(a)}\quad \forall H = H^\dagger \text{ with } H|\Psi\rangle = E|\Psi\rangle:\qquad \mathcal L_{H,c_k}(\rho) = 0,\ \rho \text{ a density matrix} \iff \rho = |\Psi\rangle\langle\Psi|;$$ $$\text{(b)}\quad e^{t\mathcal L_{\{c_k\}}}(\rho)\xrightarrow[t\to\infty]{}|\Psi\rangle\langle\Psi| \text{ for every density matrix } \rho;\qquad \text{(c)}\quad T_{\mathrm{relax}} = \frac{1}{\min_k g_k}.$$

Clause (a) allows every Hamiltonian that has the target as an eigenvector; (b) and (c) concern the purely dissipative process $H = 0$, the one the paper solves explicitly.

Milestones

1. Dark states are stationary (§II, p. 2).
2. Theorem 1 (p. 2): $\mathcal L(|\Phi\rangle\langle\Phi|) = 0$ iff $Q^\dagger|\Phi\rangle = \lambda|\Phi\rangle$ and $c_l|\Phi\rangle = \lambda_l|\Phi\rangle$ with $\sum_l g_l|\lambda_l|^2 = \operatorname{Re}\lambda$.
3. $D' = D$ (p. 3, footnote [35]): $Q^\dagger\psi = i\lambda\psi$ with $\lambda$ real iff $\psi$ is dark.
4. Theorem 2 (p. 3): if no nonzero subspace $S\perp D$ satisfies $c_lS\subseteq S$ for all $l$, the only stationary states are the dark states.
5. Dark vectors of $\{c_k\}$ (§IV, p. 4): $c_k\varphi = 0$ for all $k$ iff $\varphi\in\mathbb C|\Psi\rangle$.
6. The monomial claim (§IV, p. 4): for $\chi\perp|0^n\rangle$, $\chi\ne0$, some product $P$ of the $\sigma_-^{(k)}$ has $\langle0^n|P|\chi\rangle\ne0$.
7. Unitary covariance (§IV.A, p. 4): $\mathcal L_{\{U\sigma_-^{(k)}U^\dagger\}}(\sigma) = U\mathcal L_{\{\sigma_-^{(k)}\}}(U^\dagger\sigma U)U^\dagger$.
8. One qubit (§IV.A, p. 4): eigenvalues $0, -2g, -g, -g$ on $|0\rangle\langle0|, \sigma_z, \sigma_x, \sigma_y$.
9. Product spectrum (§IV.A, p. 4): the explicit operators $U(\sigma_{i_1}^{(1)}\otimes\cdots\otimes\sigma_{i_n}^{(n)})U^\dagger$ form an eigenbasis, with eigenvalues $\sum_k\lambda_{i_k}$; these are exactly $-\sum_k m_kg_k$, $m_k\in\{0,1,2\}$.

Significance

The result. The goal shows that dissipative preparation is universal for pure states: no pure state, however entangled, is out of reach, and the required jump operators are written down explicitly. Clause (c) states that the time to reach the target is governed by the weakest single coupling and does not grow with the number of qubits. Theorems 1 and 2 are general tools independent of the construction: Theorem 1 characterizes every pure stationary state of every Lindblad generator, and Theorem 2 is a checkable sufficient condition for the absence of other stationary states. The later sections of the paper (stabilizer and graph states, PEPS and the AKLT state, a driven condensate, the $\eta$-condensate) apply these tools to physically local processes.

Formalizing it. The results are classical and proved in the paper, partly in sketched form ("straightforward", "the same arguments as above"). No machine-checked proof of any of them is known. The formalization supplies complete arguments for the sketched steps, fixes the guards the printed statements omit (listed below), and produces a reusable layer of statements about the spectrum and stationary states of Lindblad generators on finite-dimensional spaces.

Difficulty

The first idea for uniqueness is to show that the target is the only pure stationary state, using Theorem 1. That is not enough: a Lindblad generator can have mixed stationary states even when its pure stationary state is unique (with Hermitian jump operators the maximally mixed state is always stationary, Eq. (4)). Excluding mixed stationary states is the content of Theorem 2, whose proof requires a positivity argument for $Q^\dagger\rho + \rho Q$ and a decomposition of $\rho$ along $D\oplus D^\perp$.

For convergence, uniqueness of the stationary state does not suffice either: a purely imaginary eigenvalue would make $e^{t\mathcal L}(\rho)$ oscillate forever. Clauses (b) and (c) need the full spectrum of the $4^n$-dimensional Liouvillian, obtained by reducing to $U = \mathbb 1$ and decoupling into $n$ single-qubit problems; in Lean this means relating the eigenvalues of a generator on $2^n\times 2^n$ matrices to those of tensor factors.

Formalization scope

The generator, the semigroup $e^{t\mathcal L}$ (matrix exponential of the Liouvillian as a linear map), and the predicates stationary (density matrix with $\mathcal L\rho = 0$), attractive and lazy (nonzero subspace invariant under all jump operators) are reused from the published definition QAlgorithms_Papers_Independent_Dependency50_P16. That layer normalizes the dissipator as $\sum_k V_k\rho V_k^\dagger - \frac12\{V_k^\dagger V_k,\rho\}$; the paper's rates enter through jump operators $V_l = \sqrt{2g_l}\,c_l$, which reproduces Eq. (2) exactly. Operators are complex $d\times d$ matrices, states are vectors in $\mathbb C^d$, and $n$ qubits are indexed by $\{0,\dots,2^n-1\}$ with qubit 1 the most significant bit; $|0^n\rangle$ is the basis vector of index $0$. Density matrices are positive semidefinite of trace one, and $|\psi\rangle\langle\psi|$ is formed without normalization, so unit norm is assumed where the paper says "state". Convergence is entrywise.

Conventions added to the paper and disclosed in each statement:

• rates $g_l>0$ (the paper allows $g_\ell\ge0$; with a zero rate Theorem 1 and uniqueness fail);
• Theorem 2 quantifies over nonzero subspaces (the zero subspace would make its hypothesis unsatisfiable), and keeps the standing assumption that $D$ is a subspace, as a fixed eigenvalue $E$;
• $n\ge1$ in clause (c); the relaxation rate is a least element and must be positive before its reciprocal is a finite relaxation time;
• "$|\varphi\rangle = U|0^n\rangle$" is read up to a scalar, and the single-qubit "iff $\sigma_i\in\Sigma_k$" as four eigen-equations.

A trivializing formalization is ruled out: the target is not fixed to $U = \mathbb 1$, the jump operators are the conjugated $U\sigma_-^{(k)}U^\dagger$ and not $\sigma_-^{(k)}$, clause (a) quantifies over all Hamiltonians with the target as eigenvector rather than only $H = 0$, and the relaxation time refers to the actual nonzero spectrum of the generator.

A complete development needs: properties of the Lindblad generator under unitary conjugation; positivity arguments for completely positive maps on matrices; the tensor-product structure of $2^n\times 2^n$ matrices over qubit wires; and the spectrum and diagonalizability of a sum of commuting single-site generators. The spectral and stationary-state lemmas are reusable for any finite-dimensional open-system mission. Contributions to any milestone, and alternative proofs of Theorem 2 or of the spectrum, are welcome.

Selected references

• B. Kraus, H. P. Büchler, S. Diehl, A. Kantian, A. Micheli, P. Zoller, Preparation of entangled states by quantum Markov processes, Phys. Rev. A 78 (2008); arXiv:0803.1463v3. https://arxiv.org/abs/0803.1463
• S. Diehl, A. Micheli, A. Kantian, B. Kraus, H. P. Büchler, P. Zoller, Quantum states and phases in driven open quantum systems with cold atoms, Nature Physics 4 (2008). https://arxiv.org/abs/0803.1482
• F. Verstraete, M. M. Wolf, J. I. Cirac, Quantum computation and quantum-state engineering driven by dissipation, Nature Physics 5 (2009). https://arxiv.org/abs/0803.1447
• E. Malvetti et al., Reachability, coolability, and stabilizability of open Markovian quantum systems with fast unitary control, 2023; arXiv:2308.00561. https://arxiv.org/abs/2308.00561
• G. Lindblad, On the generators of quantum dynamical semigroups, Comm. Math. Phys. 48 (1976). https://doi.org/10.1007/BF01608499
• V. Gorini, A. Kossakowski, E. C. G. Sudarshan, Completely positive dynamical semigroups of N-level systems, J. Math. Phys. 17 (1976). https://doi.org/10.1063/1.522979

Motivation

In a system driven away from equilibrium, a force changes a reference state and a dynamics, while a corresponding flux records the transported quantity. Statistical mechanics asks how the mean flux changes under a small force. A second question is whether the matrix of these changes is symmetric when the underlying dynamics admit time reversal. Jakšić, Pillet and Rey-Bellet derive both answers at a fixed, finite observation time from a generalized Evans–Searles fluctuation symmetry for classical dynamical systems in their 2010 preprint, §4. This finite-time statement does not require a large-time limit, a stationary nonequilibrium state, or an asymptotic fluctuation theorem.

The paper first develops the entropy cocycle and its time-reversal properties for a single system. Its Proposition 3.3 gives a scalar finite-time Evans–Searles identity. Section 4 lets the dynamics and reference state depend on a vector of forces and introduces a vector of fluxes. Proposition 4.6, the target here, is the section’s stated finite-time Green–Kubo and Onsager result Jakšić, Pillet and Rey-Bellet, pp. 18–21.

Setting

Fix a positive integer $N$ and a measurable configuration space $M$. Each force vector $X\in\mathbb R^N$ determines a continuous-time measurable flow $\phi_X^s:M\to M$, a probability state $\omega_X$, and an entropy-production observable $\sigma_X$. The evolved states of each system are equivalent to $\omega_X$, and the regularity assumption (E1) makes $\sigma_X$ the derivative of the evolved-state density in $L^1(\omega_X)$. The family also has a measurable flux vector $\Phi_X=(\Phi_X^{(1)},\ldots,\Phi_X^{(N)})$ satisfying the flux relation $\sigma_X=X\cdot\Phi_X$ almost everywhere. These are the family and flux conventions of §4.1 Jakšić, Pillet and Rey-Bellet, pp. 17–18.

At equilibrium, $X=0$. Assumption (T1) says only that $\omega_0$ is invariant under $\phi_0^s$; no stationarity is imposed on $\omega_X$ for nonzero $X$. Assumption (T2) gives each $X$-system a possibly different time reversal $\vartheta_X$ preserving $\omega_X$, reversing the flow, and sending $\Phi_X$ to $-\Phi_X$ almost everywhere. For $t>0$, the $X$-system time average is

$$\langle\Phi_X^{(j)}\rangle_t=\frac1t\int_0^t\omega_X(\Phi_X^{(j)}\circ\phi_X^s)\,ds,$$

and its force derivative at equilibrium is $L_{jkt}=\left.\partial_{X_k}\langle\Phi_X^{(j)}\rangle_t\right|_{X=0}$. The equilibrium correlation with indices $j,k$ is $C_{jk}(s)=\omega_0(\Phi_0^{(k)}(\Phi_0^{(j)}\circ\phi_0^s))$. Thus the time-shifted factor carries index $j$.

The generalized Evans–Searles functional is the log-Laplace transform of the actual integrated flux,

$$g_t(X,Y)=\log\omega_X\!\left(\exp\left[-Y\cdot\int_0^t\Phi_X\circ\phi_X^s\,ds\right]\right),$$

with extended real values when the exponential moment diverges. Proposition 4.3 states $g_t(X,Y)=g_t(X,X-Y)$ under (T1)–(T2) Jakšić, Pillet and Rey-Bellet, p. 19.

Formalization targets

Generalized finite-time symmetry

Proposition 4.2 relates the law $P_X^t$ of the averaged flux to its reflection $\bar P_X^t$ for nonzero $t$: $d\bar P_X^t/dP_X^t(s)=e^{-tX\cdot s}$. Proposition 4.3 states the equivalent symmetry of $g_t$. Lemma 4.4 is a calculus statement about a $C^{1,2}$ function with that symmetry. These are the three new numbered milestones; the earlier entropy-cocycle results, Propositions 3.1, 3.2 and 3.8, are reused as published references Jakšić, Pillet and Rey-Bellet, pp. 8–12, 19.

Finite-time response

The goal is all of Proposition 4.6, at each fixed $t>0$:

$$X\mapsto\langle\Phi_X\rangle_t\text{ is differentiable at }0,\qquad L_{jkt}=\frac12\int_{-t}^{t}C_{jk}(s)\left(1-\frac{|s|}{t}\right)ds,\qquad L_{jkt}=L_{kjt}.$$

The first clause is the paper’s assumption (T3) as a conclusion. The second is the finite-time Green–Kubo formula and the third the finite-time Onsager reciprocity relation Jakšić, Pillet and Rey-Bellet, pp. 20–21.

Significance

The formula determines the first-order response matrix from correlations measured entirely in the equilibrium system. Its triangular weight records a finite observation window. Reciprocity then says that cross-responses agree after exchanging the flux and force coordinates. Both statements are exact at fixed time, so they can be used before an asymptotic transport coefficient is known to exist Jakšić, Pillet and Rey-Bellet, Proposition 4.6 and Remarks 1–2, pp. 20–21.

The paper proves these claims. The formalization task is to express and eventually verify the known result, including the dependent family of states and flows, the extended log moment, and all three clauses of the proposition. The published §3 definitions and cocycle statements provide a reusable base. A checked §4 development would also expose general measure and calculus lemmas for finite-time fluctuation relations. At drafting, these new statements compile as open Lean theorems; compilation does not supply their proofs.

Difficulty

The symmetry is an equality of potentially infinite log moments, while the response matrix uses real derivatives near the origin. Local finiteness must justify passage between those two regimes. The paper’s $C^{1,2}$ convention includes five families of continuous partial derivatives, including both orders of mixed differentiation, but does not demand two $X$ derivatives. Treating it as ordinary $C^2$ would change the theorem.

There is also a measure-theoretic gap between a time integral of fluxes inside an expectation and an integral of expectations over time. A formal statement must control that interchange and the two-time correlation integral. Stationarity is available only at equilibrium, although both the state and flow vary with $X$ in the response derivative. The one-line formula for $\langle f\rangle_t$ on p. 20 leaves its state implicit; the first display of the proof on p. 21 and the entropy balance used in (4.30) identify it as the $X$-system state for $f=\Phi_X$ Jakšić, Pillet and Rey-Bellet, pp. 20–21.

Formalization scope

The Lean family uses $\mathbb R^N$ as Fin N → ℝ with $N>0$, a measurable type $M$, and one published RegularSystem M for each $X$. That type supplies (F1), (F2), (C), and (E1); the new family supplies the flux relation and almost-everywhere time integrability of each coordinate on finite intervals, so the paper's integrated flux is defined. Observable identities in the flux relation and time reversal are $\omega_X$-almost everywhere. The law $P_X^t$ is the pushforward of $\omega_X$ under the integrated flux divided by $t$. The log-Laplace transform uses a nonnegative integral and EReal, retaining $+\infty$; a real conversion occurs only on a neighborhood where finiteness is stated.

The goal requires $t>0$, since its triangular kernel and time average refer to $[0,t]$. Proposition 4.2 requires $t\ne0$ because $P_X^t$ otherwise contains a division by zero; Proposition 4.3 includes $t=0$. To make the correlation and Fubini steps meaningful, equilibrium flux coordinates are assumed in $L^2(\omega_0)$ and the $X$-system flux is locally integrable on $[0,t]\times M$ near $X=0$. These are labeled analytic hypotheses, not new physical symmetry assumptions. Coordinate partials are derivatives along coordinate lines, with existence as well as continuity asserted for the five families on an open neighborhood.

The target uses the actual log-Laplace transform and the force derivative of the actual time average. It imposes stationarity only at $X=0$, uses equilibrium correlations, and keeps precisely $C^{1,2}$ regularity. The family interface and the calculus and integration lemmas needed to prove the milestones are reusable; contributions that close any of the numbered milestones or the analytic interchange obligations fit this scope.

Selected references

• V. Jakšić, C.-A. Pillet and L. Rey-Bellet, Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical Systems, arXiv preprint arXiv:1009.3248v2, 2010. Preprint.

Motivation

Integrals of polynomial functions of the matrix entries of a random element of a compact group appear across mathematical physics and probability: in random matrix theory (moments of Haar-distributed unitary, orthogonal and symplectic matrices), in lattice gauge theory (the link integrals of $U(N)$ gauge fields), and in quantum information (averages of quantum channels over random unitaries, twirling, unitary designs). Weingarten first computed asymptotics of such integrals for $U(N)$ in 1978 (Weingarten, J. Math. Phys. 19 (1978)); Collins (IMRN 2003) and Collins–Śniady (CMP 2006) gave exact formulas for the unitary, orthogonal and symplectic groups in terms of what is now called the Weingarten function.

The survey of Collins, Matsumoto and Novak, The Weingarten Calculus (arXiv:2109.14890), isolates the single statement underneath all these formulas, valid for every compact group and every finite-dimensional unitary representation. This mission formalizes that statement, Theorem 2.1 of the survey, together with the steps of its proof as written in Section 2.

Setting

Let $G$ be a compact Hausdorff topological group and $\mu$ its Haar probability measure, the unique Borel probability measure on $G$ invariant under left translation. Let $H=\mathbb{C}^N$ with its standard orthonormal basis $e_1,\dots,e_N$, and let $U:G\to\mathrm U(N)$ be a continuous group homomorphism into the unitary $N\times N$ matrices. Its matrix elements are $U_{xy}(g)=\langle e_x,U(g)e_y\rangle$, the $(x,y)$ entry of $U(g)$.

Fix $d\in\mathbb N$. A multi-index is a function $i:[d]\to[N]$; the set of them is $\mathrm{Fun}(d,N)$. The Weingarten integrals of degree $d$ are

$$I_{ij}=\int_G\prod_{x=1}^d U_{i(x)j(x)}(g)\,d\mu(g),\qquad i,j\in\mathrm{Fun}(d,N).$$

The tensor power $H^{\otimes d}$ has the orthonormal basis $e_i=e_{i(1)}\otimes\cdots\otimes e_{i(d)}$, and the tensor-power matrix $U^{\otimes d}(g)$ has entries $U^{\otimes d}_{ij}(g)=\prod_{x=1}^dU_{i(x)j(x)}(g)$. The invariant tensors are

$$(H^{\otimes d})^G=\{t\in H^{\otimes d}: U^{\otimes d}(g)\,t=t\ \text{for all }g\in G\},$$

and the Haar average is the matrix $P=\int_GU^{\otimes d}(g)\,d\mu(g)$. Given vectors $a_1,\dots,a_m\in H^{\otimes d}$, let $A=[\langle e_i,a_x\rangle]$ be the $N^d\times m$ matrix whose columns are their coordinates, $A^*$ its conjugate transpose, $A^*A=[\langle a_x,a_y\rangle]$ their Gram matrix, and, when it is invertible, $W=(A^*A)^{-1}$ the Weingarten matrix of $a_1,\dots,a_m$.

Formalization targets

Goal: Theorem 2.1 (p. 4)

If $a_1,\dots,a_m$ is a basis of $(H^{\otimes d})^G$, then for all $i,j\in\mathrm{Fun}(d,N)$

$$I_{ij}=\sum_{x,y=1}^mA_{ix}\,W_{xy}\,A^*_{yj}.$$

The identity is exact and holds for every compact group, every continuous unitary representation, every degree $d$ and every choice of basis; nothing is fixed beyond the data.

Milestones (Section 2, pp. 3–4)

1. $I_{ij}=P_{ij}$: the Weingarten integrals are the matrix elements of the Haar average.
2. $P^*=P$, $P^2=P$, and $\operatorname{im}P=(H^{\otimes d})^G$: $P$ is the orthogonal projection onto the invariant tensors (the existing platform theorem that a Haar average of a compact group representation is an idempotent fixing exactly the invariant vectors is included as a supporting reference item).
3. For linearly independent columns, the selfadjoint idempotent with image $\operatorname{span}\{a_x\}$ is $A(A^*A)^{-1}A^*$.

Significance

Theorem 2.1 reduces a family of analytic problems — Haar integrals of polynomials in matrix entries — to two algebraic ones: find a basis of the invariant tensors of $G$ in $H^{\otimes d}$ (classical invariant theory), and invert its Gram matrix. For $U(N)$ the invariants come from Schur–Weyl duality and the Weingarten matrix becomes the Weingarten function on permutations; for $O(N)$ and $Sp(N)$ the invariants are indexed by pair partitions; for the symmetric group $S(N)$ acting by permutation matrices the invariants are indicators of set partitions. Each of these case-specific formulas, surveyed in Sections 3–5 of the paper, is an instance of Theorem 2.1, so a formal proof of the theorem is the common entry point for formalizing any of them.

The theorem is classical and its proof is elementary once stated; it is not open. No machine-checked proof is known to exist in Mathlib or on this platform: Mathlib has Haar measure, unitary groups and Gram matrices (including the equivalence of linear independence with invertibility of the Gram matrix), but not the averaging projection of a representation in matrix form nor the formula $A(A^*A)^{-1}A^*$ for orthogonal projections. The mission produces both as reusable lemmas and the Fundamental Theorem itself.

Difficulty

The argument is short on paper; the formal work sits in three places. First, selfadjointness of $P$ needs $\int_GF(g^{-1})\,d\mu=\int_GF(g)\,d\mu$, i.e. unimodularity of a compact group, which Mathlib does not provide as an instance for non-commutative groups. Second, identifying the image of $P$ with the invariant tensors needs both directions: invariant vectors are fixed by $P$, and every vector $Pt$ is invariant, which uses left invariance of $\mu$ inside a matrix-valued Bochner integral. Third, the projection formula needs invertibility of $A^*A$ from linear independence and an argument that a selfadjoint idempotent is determined by its image. Commuting the integral with matrix entries and products is routine but must be done with care for the matrix norm chosen.

Formalization scope

• $H$ is $\mathbb C^N$ with its standard basis (a finite-dimensional Hilbert space with a specified orthonormal basis is the same thing after identification); $U$ is a monoid homomorphism G →* Matrix.unitaryGroup (Fin N) ℂ, assumed continuous. Indices are 0-based: $[N]$ is Fin N, multi-indices are Fin d → Fin N, tensors are (Fin d → Fin N) → ℂ.
• $G$ carries [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [BorelSpace G], and $\mu$ is a Haar measure that is a probability measure. Right invariance is not assumed; it is a consequence that solvers must prove.
• $d$ ranges over all of $\mathbb N$, including $d=0$, where both sides equal $1$; the paper takes $d$ positive.
• The inner product is conjugate-linear in the first slot, so $A^*_{yj}=\overline{A_{jy}}$ and $A^*$ is Mathlib's conjugate transpose.
• $P$ is a Bochner integral of matrices, taken with the entrywise sup norm; in finite dimension the integral is independent of the norm.
• The basis hypothesis is two hypotheses: LinearIndependent ℂ a and span (range a) = invariants U d, with the invariant subspace defined from the representation. Without independence Mathlib's matrix inverse returns $0$ on a singular Gram matrix, and the statement would be false; it is therefore not a trivializing gap but a necessary hypothesis.
• Correction. The paper says "a basis $a_1,\dots,a_m$ of $(H)^{\otimes d}$"; the same paragraph calls the $a_x$ "the basic invariants", and with a basis of all of $H^{\otimes d}$ the right-hand side would be the identity. The formal statement uses a basis of $(H^{\otimes d})^G$.
• A trivializing formalization — defining the Weingarten integral as $AWA^*$, defining the invariant space as the image of $P$, or assuming that $P$ projects onto the span of the $a_x$ — is excluded: the left side is the Haar integral of the product of matrix elements written out, and the invariant space is defined by $U^{\otimes d}(g)t=t$.

Needed infrastructure: matrix-valued Bochner integrals commuting with entries and with matrix multiplication; unimodularity of compact groups; the orthogonal-projection formula. All three are reusable well beyond this mission, and contributions of these general lemmas are welcome.

Selected references

• B. Collins, S. Matsumoto, J. Novak, The Weingarten Calculus, arXiv preprint, 2021. https://arxiv.org/abs/2109.14890
• D. Weingarten, Asymptotic behavior of group integrals in the limit of infinite rank, J. Math. Phys. 19 (1978), 999–1001. https://doi.org/10.1063/1.523807
• B. Collins, Moments and cumulants of polynomial random variables on unitary groups, the Itzykson–Zuber integral, and free probability, Int. Math. Res. Not. 2003, no. 17, 953–982. https://doi.org/10.1155/S107379280320917X
• B. Collins, P. Śniady, Integration with respect to the Haar measure on unitary, orthogonal and symplectic group, Comm. Math. Phys. 264 (2006), 773–795. https://doi.org/10.1007/s00220-006-1554-3

Motivation

Classical Hamiltonian mechanics describes an observable by a function on a phase space. Its Poisson bracket gives observables a Lie algebra: the bracket is antisymmetric and satisfies the Jacobi identity. In multisymplectic geometry, a higher-degree differential form replaces the symplectic two-form, and the appropriate observables may themselves be differential forms. This occurs in the geometric description of classical field theories, where quantities associated with spatially extended objects are naturally expressed through forms rather than functions. Baez, Hoffnung and Rogers use this setting to examine the classical bosonic string in their paper, §§1 and 5.

The same paper shows why the usual Lie algebra of observables is too narrow for a 2-plectic space. One bracket of Hamiltonian one-forms satisfies the Jacobi identity but is antisymmetric only up to an exact form; another is antisymmetric but has a Jacobi identity only up to an exact form. Theorem 4.3 packages the first bracket and its exact correction into a hemistrict Lie 2-algebra. The result is known mathematically; the mission is to give its construction a machine-checked statement and proof in Lean for a finite-dimensional vector-space model Baez–Hoffnung–Rogers, §§3–4.

Setting

Let $E$ be a finite-dimensional real normed vector space. A 2-plectic form $\omega$ on $E$ is a smooth three-form with $d\omega=0$ such that $\iota_v\omega=0$ implies $v=0$ at each point. The interior product $\iota_v$ places $v$ in the first argument of the form. This is the $n=2$ case of Definition 2.1 in the preprint, p. 6.

A smooth one-form $F$ is Hamiltonian when a smooth vector field $v_F$ satisfies

$$dF=-\iota_{v_F}\omega.$$

Nondegeneracy makes $v_F$ unique. Write $\operatorname{Ham}(E,\omega)$ for the vector space of these forms. The hemi-bracket is $\{F,G\}_h=\mathcal L_{v_F}G$, where $\mathcal L_v$ is the Lie derivative. On functions its left and right actions are $\{F,f\}_h=\mathcal L_{v_F}f$ and $\{f,F\}_h=0$. The alternator is the function $S_{F,G}=-(\iota_{v_F}G+\iota_{v_G}F)$. These formulas are Definitions 3.1 and 3.3 and the data preceding Theorem 4.3 on pp. 11 and 16–17.

A Lie 2-algebra here has a two-term chain complex $L_0\xleftarrow{d}L_1$, a bracket on its available degrees, an alternator witnessing antisymmetry up to chain homotopy, and a Jacobiator witnessing the Jacobi relation up to chain homotopy. Four further coherence diagrams constrain these homotopies. “Hemistrict” means that the Jacobiator is the identity homotopy, represented by the zero degree-one map Definitions 4.1–4.2, pp. 15–16.

Formalization targets

Hemistrict structure on Hamiltonian one-forms

For every 2-plectic $(E,\omega)$, Theorem 4.3 constructs a hemistrict Lie 2-algebra with all components fixed:

$$L_0=\operatorname{Ham}(E,\omega),\qquad L_1=C^\infty(E),\qquad d_L f=df,\qquad [F,G]=\{F,G\}_h,$$ $$[F,f]=\mathcal L_{v_F}f,\qquad [f,F]=0,\qquad S_{F,G}=-(\iota_{v_F}G+\iota_{v_G}F),\qquad J_{F,G,H}=0.$$

The existential goal fixes the carriers and every operation; the Lie 2-algebra structure then requires the chain-map identities, the homotopy identities, and all four coherence equations. The milestones isolate the source statements that supply the main geometric identities: uniqueness of $v_F$, Hamiltonian exact forms, Proposition 3.6, the bracket’s chain-map behavior, a mixed Jacobi identity, and the third coherence diagram Theorem 4.3 and its proof, pp. 17–18.

Significance

The theorem identifies the algebraic structure carried by 2-plectic observables. In particular, it retains the exact-form discrepancy in antisymmetry as an explicit operation instead of losing it by quotienting forms. The paper compares this hemistrict construction with a semistrict construction and then studies their relation; the present result is the first of those two constructions Theorems 4.3–4.6, pp. 17–19.

A formal proof would connect Mathlib’s exterior derivative on alternating forms to a reusable calculus of interior products, Lie derivatives, Hamiltonian vector fields, and higher algebraic coherence. The preprint already proves the theorem. The local proposal supplies statements for its finite-dimensional normed-space case; a proof in Lean and an extension from vector spaces to general smooth manifolds are further work. The current mission does not assert the separate semistrict theorem or the string application.

Difficulty

The obvious attempt to make Hamiltonian one-forms into a conventional Lie algebra fails: for the hemi-bracket, $\{F,G\}_h+\{G,F\}_h$ can be a nonzero exact form. The correction must also agree with the bracket on functions and with the Jacobi relation across degrees. A degree-zero calculation alone therefore does not establish a Lie 2-algebra. Its chain-map conditions and four coherence diagrams impose further identities involving the exterior derivative, Lie derivatives and the Hamiltonian vector fields Proposition 3.6 and Definition 4.1, pp. 12, 15–16.

Formalization scope

Lean uses $E$ with NormedAddCommGroup, NormedSpace ℝ E and FiniteDimensional ℝ E, in place of the paper’s arbitrary smooth manifold $X$. Forms, functions and vector fields are defined on all of $E$, and smoothness means ContDiff ℝ smooth with smooth the $C^\infty$ degree. This is the disclosed scope cut. The Lean name for the paper’s $\omega$ is Ω; this avoids a notation conflict from the imported definition module.

Mathlib represents a $k$-form as a function into a continuous alternating $k$-linear map. Its extDeriv supplies the exterior derivative, while the published ContWeatherall.grad supplies $df$ for functions. Interior product inserts in the first slot. The Lie derivative of a one-form uses its derivative and the derivative of the vector field, so Cartan’s identity is a mathematical assertion rather than the definition of the Lie derivative. The bracket of vector fields uses $[V,W]=DW\cdot V-DV\cdot W$. The two-term chain complex uses the paper’s ordinary graded tensor-product differential and signed switch. Every formal statement about hamVF restricts its form to Hamiltonian inputs, where nondegeneracy gives a unique vector field; the default value on other inputs has no role in the theorem.

The goal requires all operations to have the paper’s values and requires every Lie 2-algebra axiom. An arbitrary pre-existing Lie 2-algebra or a structure with unconstrained operations would not establish this result. Reusable contributions include differential-form identities and the algebraic two-term interface. The separate semi-bracket construction and general-manifold extension remain outside this proposal.

Selected references

• J. C. Baez, A. E. Hoffnung and C. L. Rogers, Categorified Symplectic Geometry and the Classical String, preprint arXiv:0808.0246v1, 2008; published in Communications in Mathematical Physics 293 (2010), 701–725. Preprint.