All missions

Motivation

In this paper we study the subset of generalized quantum measurements on finite dimensional systems known as local operations and classical communication (LOCC). While LOCC emerges as the natural class of operations in many important quantum information tasks, its mathematical structure is complex and difficult to characterize. Here we provide a precise description of LOCC and related operational classes in terms of quantum instruments. Our formalism captures both finite round protocols as well as those that utilize an unbounded number of communication rounds. While the set of LOCC is not topologically closed, we show that finite round LOCC constitutes a compact subset of quantum operations. Additionally we show the existence of an open ball around the completely depolarizing map that consists entirely of LOCC implementable maps. Finally, we demonstrate a two-qubit map whose action can be approached arbitrarily close using LOCC, but nevertheless cannot be implemented perfectly.

This mission is the statement-level formalization of Everything You Always Wanted to Know About LOCC (But Were Afraid to Ask) (arXiv:1210.4583v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is An explicit two-qubit instrument in the closure of LOCC but outside LOCC (Abstract; §§4.1,4.3, Eqs.(10)–(12), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Lemma 2, Eq.(20); Appendix B pp.19–21: A source-correct strict-decrease domain, or a definition of nontrivial measurement depending on the input state. (source-ambiguity)

Selected references

• Everything You Always Wanted to Know About LOCC (But Were Afraid to Ask), arXiv:1210.4583v2, https://arxiv.org/abs/1210.4583v2

Motivation

In view of controlling finite dimensional open quantum systems, we provide a unified Lie-semigroup framework describing the structure of completely positive trace-preserving maps. It allows (i) to identify the Kossakowski-Lindblad generators as the Lie wedge of a subsemigroup, (ii) to link properties of Lie semigroups such as divisibility with Markov properties of quantum channels, and (iii) to characterise reachable sets and controllability in open systems. We elucidate when time-optimal controls derived for the analogous closed system already give good fidelities in open systems and when a more detailed knowledge of the open system (e.g., in terms of the parameters of its Kossakowski-Lindblad master equation) is actually required for state-of-the-art optimal-control algorithms. -- As an outlook, we sketch the structure of a new, potentially more efficient numerical approach explicitly making use of the corresponding Lie wedge.

This mission is the statement-level formalization of Lie-Semigroup Structures for Reachability and Control of Open Quantum Systems (arXiv:0811.3906v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The generated Markovian semigroup has the full channel tangent wedge (Theorem III.3, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

30 results of the paper are not stated yet, because the library lacks an interface they need:

• Lemma II.1: Accepted source-matched theorem for Lemma II.1 (provenance boundary) (hard)
• Theorem II.1: Missing Ad_K invariance of c (source-ambiguity)
• Proposition II.1: Accepted source-matched theorem for Proposition II.1 (provenance boundary) (hard)
• Proposition II.2: Accepted source-matched theorem for Proposition II.2 (provenance boundary) (hard)
• Theorem II.2: Accepted source-matched theorem for Theorem II.2 (provenance boundary) (hard)
• Theorem II.3: Accepted source-matched theorem for Theorem II.3 (provenance boundary) (hard)
• Theorem II.4: Accepted source-matched theorem for Theorem II.4 (provenance boundary) (hard)
• Theorem II.5: Accepted source-matched theorem for Theorem II.5 (provenance boundary) (hard)
• Theorem II.6: Accepted source-matched theorem for Theorem II.6 (provenance boundary) (hard)
• Corollary II.1: Accepted source-matched theorem for Corollary II.1 (provenance boundary) (hard)
• Corollary II.2: Accepted source-matched theorem for Corollary II.2 (provenance boundary) (hard)
• Theorem III.1: Independent x/y control indexing and original-result provenance (source-ambiguity)
• Theorem III.2: Accepted source-matched theorem for Theorem III.2 (provenance boundary) (hard)
• Proposition III.1: Accepted source-matched theorem for Proposition III.1 (provenance boundary) (hard)
• Theorem III.4: Dimension-qualified nondivisibility theorem (source-ambiguity)
• Corollary III.2: Dimension-qualified failure of Lie-subsemigroup generation (source-ambiguity)
• Corollary III.3: Dimension-qualified local failures and non-semialgebra wedge (source-ambiguity)
• Corollary III.4: Nonvacuous fixed-semigroup identity neighborhood and generator signs (source-ambiguity)
• Corollary III.5: Endpoint representations versus one fixed exponential trajectory (source-ambiguity)
• Resume: A specified genericity space and canonical dissipator gauge (source-ambiguity)
• Proposition III.2: Nontrivial homogeneous space for the smallest-positive-scaling conclusion (source-ambiguity)
• Corollary III.6: Canonical dissipator gauge and a definition of generic (source-ambiguity)
• Reachability-product: Accepted source-matched theorem for Reachability-product (provenance boundary) (hard)
• Remark II.1: Accepted source-matched theorem for Remark II.1 (provenance boundary) (hard)
• Remark II.3: Accepted source-matched theorem for Remark II.3 (provenance boundary) (hard)
• Trace-norm-contraction: Accepted source-matched theorem for Trace-norm-contraction (provenance boundary) (hard)
• Purity-unitality: Accepted source-matched theorem for Purity-unitality (provenance boundary) (hard)
• Remark III.1: Accepted source-matched theorem for Remark III.1 (provenance boundary) (hard)
• Markovian-stratification: Dimension scope and explicit interior/strict-inclusion witnesses (source-ambiguity)
• Scalar-decay-optimal-time: Quantitative almost-uniform decay and attained argmax domain (source-ambiguity)

Selected references

• Lie-Semigroup Structures for Reachability and Control of Open Quantum Systems, arXiv:0811.3906v4, https://arxiv.org/abs/0811.3906v4

Motivation

The classical capacity of a noisy optical channel is the maximum rate at which information can be transmitted reliably, given a constraint on the mean input energy. For the ubiquitous bosonic Gaussian channels, which include standard models of loss and noise in fibre and free-space optical links, determining this rate requires addressing whether entanglement between channel uses or non-Gaussian signals can outperform Gaussian encodings. More precisely, the question is whether the energy-constrained Holevo information is additive across arbitrarily many channel uses and coincides with its Gaussian counterpart. We answer these fundamental questions in the affirmative for every single-mode bosonic Gaussian channel at every input energy. Namely, we prove that independently prepared Gaussian states with Gaussian-distributed random displacements achieve the capacity, including in the low-energy regime where squeezing the signals competes with encoding information in their displacement. Our proof connects an entanglement inequality to a sharp, additive lower bound on output entropy. We then characterise communication above capacity: under a strict total photon-number cutoff, the probability of correct decoding decreases exponentially with the number of channel uses, and we derive explicit bounds on the decay exponent. When only the mean photon number is constrained, a simple energy-rescaling formula determines exactly the entire asymptotic rate--error trade-off: the capacity at mean photon number $N$ and allowed average decoding error $ε$ equals the vanishing-error capacity at mean photon number $N/(1-ε)$. Together, these results identify the ultimate limits of classical communication for some of the most fundamental models of optical communication. △ Less

This mission is the statement-level formalization of Classical Capacity of Single-Mode Bosonic Gaussian Channels (arXiv:2610.22308v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Affine envelope and joint convexity of the moment-resolved entropy (Eq. (18), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

27 results of the paper are not stated yet, because the library lacks an interface they need:

• Corollary 3 (pp.5,12), resolving the p.1 paper-result seed: capacities and water-filling: bosonic channels, arbitrary probability ensembles, Gaussian displacement ensembles, and operational classical capacity (hard)
• Theorem 1: output entropy from second moments: finite-energy Fock states, raw quadrature quadratic-form moments, von Neumann entropy, and squeezed vacua (hard)
• Theorem 2: moment-resolved Gaussian optimality: continuous bosonic ensembles and product Gaussian displacement ensembles (hard)
• Corollary 4: finite correlated blocks: passive Fock-space implementation of a common noise diagonalizer and repeated-block capacity (hard)
• Unnumbered §IV: positive mode costs and marginal-gain rule: weighted-energy bosonic ensemble capacity and actual Gaussian Holevo energy functions (hard)
• Unnumbered Eq.(22) and Appendix E.1: operational limit of chain memory channels: growing chain Gaussian channels and operational coding capacity along a nonidentical sequence (hard)
• Proposition 5: tight Gaussian reference: infinite-dimensional relative entropy and a constructed optimal Gaussian reference (hard)
• Unnumbered Eq.(24), Appendix F: uniqueness and quantitative stability: bosonic ensemble Holevo deficit, trace norm, marginals and Gaussian reference tensor powers (hard)
• Theorem 6: exact nonzero-error capacity: operational nonzero-error capacity for bosonic mean-energy code sequences (hard)
• Proposition 7: exponential cutoff strong converse: bosonic photon-cutoff codes and their operational capacity (hard)
• Proposition 8: mixed-state affine entropy bound: mixed bosonic bipartite states and unbounded annihilation-operator quadratic forms (hard)
• Lemma 9: quadrature-dependent dilation expectation: symplectic Fock unitaries, their Stinespring action, and quadrature-dependent quadratic-form expectations (hard)
• Proposition 10: growing-memory converse and error trade-off: uniform Gaussian dilations and operational codes along growing memory blocks (hard)
• Fact 11: Gaussification commutes with Gaussian channels: Gaussification as an actual normalized Gaussian Fock state with prescribed moments (hard)
• Proposition 12: transfer from cutoff to mean energy: arbitrary bosonic-input channels, bounded decoding POVMs, and cutoff-code success supremum (hard)
• Lemma 13: energy-preserving positive-filter coding inequality: Stinespring image filters and projective operator tensor norm on infinite Fock factors (hard)
• Lemma 14: uniform exponential moments for symplectic unitaries: symplectic unitary tensor powers and extended nonnegative photon-exponential expectations (hard)
• Proposition 15: approximating energy image filters: positive finite-rank energy-image filters and finite-local-support approximants on Fock tensor factors (hard)
• Proposition 16: computable filter exponent: actual cutoff-code success exponent, Gaussian dilation constants and true capacity function (hard)
• Proposition 17: explicit photon-tail bound: canonical Gaussian channel outputs on arbitrary cutoff states and decoding success (hard)
• Lemma 18: output photon-number moments: extended output photon-number moments for arbitrary entangled cutoff Fock states (hard)
• Proposition 19: converse for optimal Gaussian signal family: actual displaced squeezed Gaussian codewords and infinite-dimensional Petz Renyi expressions (hard)
• Unnumbered Appendix B: energy-preserving canonical reduction: Fock implementations of input phase rotations and output symplectic transformations (hard)
• Unnumbered G8: photon-subspace dimension and channel-independent bound: photon-subspace Hilbert dimension and channel-independent cutoff decoding success (hard)
• Unnumbered H44: approach of the filter exponent to capacity: dilation-dependent H43 filter exponent using true operational Gaussian capacity (hard)
• Unnumbered H45: weak photon tails: averaged photon-tail weight, actual cutoff-code supremum and vacuum-mixture code sequence (hard)
• Unnumbered H46–H47: fixed multimode Gaussian channels: fixed finite-mode Gaussian channels and regularized operational bosonic capacity (hard)

Selected references

• Classical Capacity of Single-Mode Bosonic Gaussian Channels, arXiv:2610.22308v1, https://arxiv.org/abs/2610.22308v1

Motivation

We give a representation for entanglement-breaking channels in separable Hilbert space that generalizes the "Kraus decomposition with rank one operators" and use it to describe the complementary channels. We also give necessary and sufficient condition of entanglement-breaking for a general quantum Gaussian channel. Application of this condition to one-mode channels provides several new cases where the additivity conjecture holds in full generality.

This mission is the statement-level formalization of Entanglement-breaking channels in infinite dimensions (arXiv:0802.0235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Radon–Nikodym representation of a POVM (Lemma 1: Radon–Nikodym representation of a POVM (9)–(10), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

18 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 2: Gaussian entanglement-breaking criterion and representation (30)–(31): Normal Gaussian trace-class channels, Gaussian states and trace-norm measure-and-prepare integral (hard)
• Theorem 1: continuous densely defined rank-one representation (17)–(18): Measurable trace-class preparation from densely defined algebraic functionals (hard)
• Proposition 1: sign of coherent information for (anti-)degradable channels: Genuine complementary trace-class channels and finite-entropy coherent information (hard)
• Unnumbered: explicit Stinespring isometry and complementary kernel: Vector-valued L2 Stinespring realization and scalar integral-operator kernel (hard)
• Example: spectral L2 measure-and-prepare channel and complementary Schur kernel: Canonical trace-class L2 diagonal and spectral measure-and-prepare map (hard)
• Unnumbered: every entanglement-breaking channel is anti-degradable: Explicit entanglement-breaking antidegrading map on the full L2 environment trace class (hard)
• Unnumbered: sharp Gaussian observable iff noise vanishes: Joint spectral measure of unbounded commuting quadratures with symplectic outcome transport (hard)
• Proposition 2: covariant operator density of a nonsingular Gaussian observable: Gaussian trace-class seed state and displaced covariant operator density (hard)
• Proposition 3: explicit Gaussian Naimark dilation (24)–(26): Gaussian ancillary Weyl system, normal partial-state evaluation and sharp joint spectral dilation (hard)
• Unnumbered: complete positivity condition for Gaussian channel parameters (29): Normal trace-class realization of the Weyl channel characteristic law (hard)
• Unnumbered: necessary PPT inequalities and Gaussian output PPT property (35): Partial transpose and Gaussian state law on a completed reference tensor product (hard)
• Unnumbered: isotropic K gives a sharp-measurement c-q channel: Sharp quadrature PVM and displaced Gaussian preparation channel (hard)
• Unnumbered claim: arbitrary sharp peaking around every outcome point: Correct outcome range in the arbitrary sharp-peaking claim (source-ambiguity)
• Unnumbered: complete one-mode entanglement-breaking thresholds A, B1, B2, C, D: Actual canonical Gaussian channels and Gaussian unitary equivalence (hard)
• Unnumbered: constrained chi-capacity additivity for the classified one-mode regimes: Extended constrained Holevo capacity for generalized ensembles and channel tensor products (hard)
• Unnumbered: entanglement-breaking channels have zero quantum capacity: Operational unconstrained quantum capacity on separable trace-class channels (hard)
• Unnumbered: energy-constrained tensor-power additivity and single-letter classical capacity (8): Formal spectral-energy constraints, tensor-power classical codes and extended constrained Holevo capacity on full trace-class channels (hard)
• Unnumbered conditional discussion: Gaussian-optimizer capacity formula: Scope of the Gaussian optimizer conjecture used for operational capacity (source-ambiguity)

Selected references

• Entanglement-breaking channels in infinite dimensions, arXiv:0802.0235v1, https://arxiv.org/abs/0802.0235v1

Motivation

The work is devoted to study of quantum mutual information and coherent information -- the two important characteristics of quantum communication channel. Appropriate definitions of these quantities in the infinite-dimensional case are given and their properties are studied in detail. Basic identities relating quantum mutual information and coherent information of a pair of complementary channels are proved. An unexpected continuity property of quantum mutual information and coherent information following from the above identities is observed. An upper bound for the coherent information is obtained.

This mission is the statement-level formalization of Mutual and coherent informations for infinite-dimensional quantum channels (arXiv:1004.2495v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: complementary-channel mutual-information identity (22) (Theorem 1: complementary-channel mutual-information identity (22), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Mutual and coherent informations for infinite-dimensional quantum channels, arXiv:1004.2495v2, https://arxiv.org/abs/1004.2495v2

Motivation

We analyse two possible definitions of the squashed entanglement in an infinite-dimensional bipartite system: direct translation of the finite-dimensional definition and its universal extension. It is shown that the both definitions produce the same lower semicontinuous entanglement measure possessing all basis properties of the squashed entanglement on the set of states having at least one finite marginal entropy. Is also shown that the second definition gives an adequate extension of this measure to the set of all states of infinite-dimensional bipartite system. A general condition relating continuity of the squashed entanglement to continuity of the quantum mutual information is proved and its corollaries are considered. Continuity bound for the squashed entanglement under the energy constraint on one subsystem is obtained by using the tight continuity bound for conditional mutual information (proved in the Appendix by using Winter's technique). It is shown that the same continuity bound is valid for the entanglement of formation. As a result the asymptotic continuity of the both entanglement measures under the energy constraint on one subsystem is proved.

This mission is the statement-level formalization of Squashed entanglement in infinite dimensions (arXiv:1507.08964v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Compactness of bipartite states from both marginal sets (Lemma 1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

25 results of the paper are not stated yet, because the library lacks an interface they need:

• Lemma 3: contraction bound for MI and conditional entropy: Homogeneous extended spectral entropy and MI; finite-first-marginal conditional entropy; contraction conjugation (hard)
• Proposition 1 A–C: universal extension of continuous monotones: Coherent finite-system monotone families, general quantum instruments, finite-rank compressions and EM1–EM8 (hard)
• Corollary 1: universal entanglement of formation is the continuous convex roof: Continuous pure-state convex roof and universal finite-rank formation extension (hard)
• Unnumbered consequence after Corollary 1: formation equality iff lower semicontinuity: Discrete and continuous formation roofs as actual extended-valued functions (hard)
• Lemma 4 A–B: finite versus infinite extension systems: Extended MI, finite-projection CQMI, direct and finite-ancilla squashed infima (hard)
• Unnumbered consequence of Lemma 4: criterion for finite-ancilla and direct functions to coincide: Globally defined direct and finite-ancilla squashed functions (hard)
• Proposition 2 A–D: properties of direct infinite-dimensional squashed entanglement: Full direct squashed-entanglement function, EM2–EM8 and entropy-restricted trace-norm topology (hard)
• Proposition 2A literal convex-hull scope (deferred source ambiguity): Literal Proposition 2A convex-hull scope (source-ambiguity)
• Lemma 5: contraction and postselection bounds for CQMI: Homogeneous extended CQMI, contraction filtering, and positive-trace postselection (hard)
• Abstract main result pinned to Proposition 3 A–D: universal squashed entanglement: Universal squashed extension and exact entanglement-measure predicates (hard)
• Corollary 2: squashed entanglement is bounded by the corresponding formation roof: Both squashed functions and both formation roofs on full state spaces (hard)
• Proposition 4 A–C: continuity equivalences and dominated convergence: Extended-valued MI and all squashed variants with sequential topology and uniform finite-ancilla gaps (hard)
• Lemma 6 A–B: lower semicontinuity and continuity of bounded-ancilla functions (normalization correction): Bounded-ancilla squashed function and correctly normalized extended liminf gaps (hard)
• Lemma 7: MI continuity implies upper semicontinuity of direct E_sq: Direct squashed-entanglement function and extended MI along arbitrary trace-norm sequences (hard)
• Corollary 3: preservation of the continuity conditions by local operations: Trace-nonincreasing CP local operations and eventual normalized output sequences (hard)
• Corollary 4: dominated local images of the limiting state: Local quantum operations, operator domination and squashed continuity (hard)
• Corollary 5: one finite subsystem and explicit continuity modulus: All squashed variants with one arbitrary infinite subsystem (hard)
• Corollary 6 A–C: energy-constrained equality and continuity: Extended one-marginal energy expectation, partition trace and both pairs of entanglement functions (hard)
• Proposition 5: common energy-constrained continuity bound for E_sq and E_F: Actual Gibbs maximizer, form-energy state domain and both entanglement measures (hard)
• Remark 4: uniform continuity of both energy-constrained entanglement measures: Real-valued entanglement restrictions to the full form-energy set with trace-norm uniformity (hard)
• Corollary 7: asymptotic continuity under an A-only mean-energy bound: Correlated tensor-power density states, sum Hamiltonian form energy and normalized entanglement differences (hard)
• Lemma 8 (Appendix): energy-constrained CQMI continuity bound: Arbitrary-state extended CQMI and one-marginal form-energy/Gibbs interfaces (hard)
• Remark 5: uniform continuity of CQMI under an A-only energy bound: Trace-norm uniform structure and finite real CQMI on the A-only energy set (hard)
• Remark 6: oscillator leading term and informal asymptotic tightness: Quantified full oscillator CQMI bound and asymptotic-tightness regime (source-ambiguity)
• Remark 6: explicit mixed-state witnesses for the CQMI lower modulus: Actual mixed Gibbs states, pure-state purification and extended CQMI on flagged mixtures (hard)

Selected references

• Squashed entanglement in infinite dimensions, arXiv:1507.08964v5, https://arxiv.org/abs/1507.08964v5

Motivation

A classification of one-mode Gaussian channels is given up to canonical unitary equivalence. A complementary to the quantum channel with additive classical Gaussian noise is described providing an example of one-mode Gaussian channel which is neither degradable nor anti-degradable.

This mission is the statement-level formalization of One-mode quantum Gaussian channels (arXiv:quant-ph/0607051v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Six canonical forms of one-mode Gaussian channels after displacement removal (§1, unnumbered Theorem, pp.2–4, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

15 results of the paper are not stated yet, because the library lacks an interface they need:

• §2 A1, pp.4–5: thermal replacer and swap-dilation weak complement (hard)
• §2 A2, (6)–(7): the actual A2 mixed-thermal dilation and its environment channel (hard)
• §2 B1, Gaussian covariance and entropy calculation: actual diagonal Gaussian input densities, pure-dilation outputs and spectral entropy (hard)
• §2 B1, degradability and infinite capacity: operational unconstrained quantum capacity and a genuine degrading normal channel (hard)
• §2 C, attenuation/amplification models: mixed-thermal attenuation/amplification joint dilations and additive-noise composition (hard)
• §2 D, phase conjugation model: the actual phase-conjugating dilation as an amplifier weak complement (hard)
• §3, (8)–(9): trace-norm Gaussian displacement integration for every trace-class input (hard)
• §3, (10)–(11): H-valued weighted-L2 unitary, both partial traces and the actual complementary kernel (hard)
• §3, (12)–(14): self-adjoint environmental generators and CCR with legitimate domains (hard)
• §3, (15)–(16) and six generator outputs: joint system/ancilla conjugation and domain-correct canonical dynamics (hard)
• §3, (17), proof pp.9–10: the actual all-input additive-noise complementary channel (hard)
• §3, complementary covariance and four eigenvalues: actual thermal complementary output covariance tied to its four spectral values (hard)
• §3, (18)–(19): infinite-dimensional spectral entropy and exchange entropy of actual output densities (hard)
• §3, F(N), vacuum value and limit: thermal coherent information linked to actual channel entropies (hard)
• §3, Nc=0.99 exp(-1), also p.7: two operational positive capacities and normal-channel (anti)degradability (hard)

Selected references

• One-mode quantum Gaussian channels, arXiv:quant-ph/0607051v2, https://arxiv.org/abs/quant-ph/0607051v2

Motivation

In this paper we give a general integral representation for separable states in the tensor product of infinite dimensional Hilbert spaces and provide the first example of separable states that are not countably decomposable. We also prove the structure theorem for the quantum communication channels that are entanglement-breaking, generalizing the finite-dimensional result of M. Horodecki, Ruskai and Shor. In the finite dimensional case such channels can be characterized as having the Kraus representation with operators of rank 1. The above example implies existence of infinite-dimensional entanglement-breaking channels having no such representation.

This mission is the statement-level formalization of Separability and Entanglement-Breaking in Infinite Dimensions (arXiv:quant-ph/0504204v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Separable states are precisely probability mixtures of product states (§2, equation (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

9 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 1: A valid compactness statement for the printed arbitrary set P (source-ambiguity)
• Theorem 2: Normalized weakly countably additive POVM on an arbitrary complete separable metric outcome space and its trace-pairing probability laws (hard)
• §3, paragraph after Theorem 2: Countable weak-effect and trace-norm rank-one Kraus sums, plus the constructed faithful-reference state (9) (hard)
• §3, unnumbered existence result: A genuine infinite-dimensional channel witness and the exact countable rank-one Kraus predicate (hard)
• §4, equations (12)–(14): The position spectral measure E(B), canonical L¹ diagonal density, and the fixed channel (12) (hard)
• Conjecture: A proof of density of W in all separable states (source-ambiguity)
• Theorem 4, equations (20)–(21): Infinite-dimensional extended Umegaki relative entropy, finite-ensemble Holevo capacity, and the channel (12) (hard)
• Theorem 4 proof, equations (22)–(23): The exact range of the constructed rotation channel (12) on all states and all L¹ probability densities (hard)
• Theorem 4 proof, finite-entropy conclusion: Extended von Neumann entropy on arbitrary trace-class states and its trace-norm restriction to the closed output range (hard)

Selected references

• Separability and Entanglement-Breaking in Infinite Dimensions, arXiv:quant-ph/0504204v1, https://arxiv.org/abs/quant-ph/0504204v1

Motivation

We give trade-offs between classical communication, quantum communication, and entanglement for processing information in the Shannon-theoretic setting. We first prove a unit-resource capacity theorem that applies to the scenario where only the above three noiseless resources are available for consumption or generation. The optimal strategy mixes the three fundamental protocols of teleportation, super-dense coding, and entanglement distribution. We then provide an achievable rate region and a matching multi-letter converse for the direct static capacity theorem. This theorem applies to the scenario where a large number of copies of a noisy bipartite state are available (in addition to consumption or generation of the above three noiseless resources). Our coding strategy involves a protocol that we name the classically-assisted state redistribution protocol and the three fundamental protocols. We finally provide an achievable rate region and a matching mutli-letter converse for the direct dynamic capacity theorem. This theorem applies to the scenario where a large number of uses of a noisy quantum channel are available in addition to the consumption or generation of the three noiseless resources. Our coding strategy combines the classically-enhanced father protocol with the three fundamental unit protocols.

This mission is the statement-level formalization of Trading classical communication, quantum communication, and entanglement in quantum Shannon theory (arXiv:0901.3038v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-block converse with explicit continuity corrections and a common classical refinement (Appendix F, (106)–(107), and both proof chains on PDF p.25, PDF p. 24). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

14 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 1: unit resource capacity region: Operational simultaneous signed unit-resource conversion region (hard)
• Theorem 2: direct static capacity theorem: Operational static conversion region and full regularized CASR union (hard)
• Theorem 3: direct dynamic capacity theorem: Operational dynamic three-resource region and full regularized CEF union (hard)
• Lemma 1: classically-assisted quantum state redistribution: Operational static primitive achievability for a remote instrument (hard)
• Corollary 4: grandmother resource inequality: Operational entanglement-distillation rates with both communication costs (hard)
• Lemma 3: additivity inclusion with a noiseless entangled state: Static operational helper families at all real ebit rates (hard)
• Lemma 4: additivity inclusion with a noiseless quantum channel: Dynamic operational helper families at all real forward-qubit rates (hard)
• Lemma 5: additivity inclusion with a noiseless entangled state: Static operational helper families in the noisy-teleportation quadrant (hard)
• Lemma 6: additivity inclusion with a noiseless quantum channel: Dynamic operational helper families in the assisted entanglement quadrant (hard)
• §VIII.A: erased-state optimal trade-off and single-letterization: A valid all-parameter erased-state optimal boundary (source-ambiguity)
• §VIII.B: dephasing full dynamic single-letterization: Operational dephasing capacity and unrestricted one-copy CEF state union (hard)
• §VII.C: benefit of coding with charged classical communication: Operational positive assisted capacity and the two closed wasting-allowed strategy regions (hard)
• §VII.C: claimed constant excess ebit cost: The target-rate domain and optimization convention for a constant entanglement-cost difference (source-ambiguity)
• Appendix A, (85)–(88): displayed finite-block static converse: A consistently scaled finite-block static converse with explicit error terms (source-ambiguity)

Selected references

• Trading classical communication, quantum communication, and entanglement in quantum Shannon theory, arXiv:0901.3038v3, https://arxiv.org/abs/0901.3038v3

Motivation

Tournaments and contests reward agents by their relative standing: sales bonuses for the top performers, promotions, prizes for the first to finish, research competitions. Since Lazear and Rosen (Rank-order tournaments as optimum labor contracts, 1981) such rank-order incentives have been a standard object in economics and operations research, and the design question of which reward schedule elicits which behaviour is central to the area. With a large population, the strategic interaction becomes a mean field game: each agent responds to the distribution of the others' outcomes rather than to individual opponents.

Bayraktar and Zhang (Terminal Ranking Games, arXiv:1906.09628v2, 2020; Mathematics of Operations Research 2021) study such a game in continuous time. Each player steers a Brownian project value by costly effort and is paid at a fixed terminal time according to her own value, her rank in the population, and the population mean. Their main result solves the equilibrium semi-explicitly. Related earlier work treats rank-based rewards by completion time (Bayraktar, Cvitanić and Zhang, Large tournament games, 2019) and by terminal rank in a strong formulation (Bayraktar and Zhang, A rank-based mean field game in the strong formulation, 2016).

Setting

Fix a horizon $T>0$, a cost coefficient $c>0$, a volatility $\sigma>0$ and an initial value $x_0\in\mathbb R$. On a probability space $(\Omega,P)$ let $B$ be a real Brownian motion, and let $X_T=x_0+\sigma B_T$ be the terminal project value under zero effort.

A reward function $R(x,r,m)$ depends on the player's terminal value $x$, her rank $r\in[0,1]$ and the population mean $m$; it is weakly increasing in each argument. The class $\mathcal R_b$ collects the bounded ones. For a population law $\mu$ on $\mathbb R$ with c.d.f. $F_\mu$ and mean $m_\mu$, write $R_\mu(x)=R(x,F_\mu(x),m_\mu)$: the payment received at terminal value $x$ when the others are distributed as $\mu$.

Effort changes the law of the path. In the weak formulation used by the paper, a control is a probability measure $Q$ equivalent to $P$, and the quadratic effort cost becomes the relative entropy $H(Q|P)$. Given the population law $\tilde\mu$, the single player's value is

$$V(R,\tilde\mu)=\sup_{Q\sim P}\ E^Q\big[R_{\tilde\mu}(X_T)\big]-2c\sigma^2H(Q\,|\,P). \tag{2.3}$$

A law $\mu$ is an equilibrium if it is a fixed point of the best response: some optimal $Q$ for $V(R,\mu)$ gives $X_T$ the law $\mu$.

The goal concerns the subclass $\mathcal R^{rm}_b$ of bounded rewards $R(r,m)$ that do not depend on $x$ and are continuous in $m$. Let $N$ be the standard normal c.d.f., $N^{-1}$ its quantile function, $q_\mu(r)=\inf\{x:r\le F_\mu(x)\}$ the quantile function of $\mu$, and

$$y_m(r)=\frac{\int_0^r e^{-R(z,m)/2c\sigma^2}dz}{\int_0^1 e^{-R(z,m)/2c\sigma^2}dz},\qquad g(m)=x_0+\sigma\sqrt T\int_0^1N^{-1}(y_m(r))\,dr .$$

Formalization targets

Goal: Theorem 3.2 (pp. 7–8)

For $R\in\mathcal R^{rm}_b$:

1. an equilibrium exists;
2. $\mu$ is an equilibrium if and only if it has a finite mean $m_\mu$ and

$$q_\mu(r)=x_0+\sigma\sqrt T\,N^{-1}\big(y_{m_\mu}(r)\big)\quad(0<r<1),\qquad m_\mu=g(m_\mu); \tag{3.2–3.3}$$

3. for every equilibrium, $V(R,\mu)=2c\sigma^2\ln\beta(\mu)=-2c\sigma^2\ln\int_0^1e^{-R(z,m_\mu)/2c\sigma^2}dz$, where $\beta(\mu)=\int f_0(y)e^{R_\mu(y)/2c\sigma^2}dy$ and $f_0$ is the $\mathcal N(x_0,\sigma^2T)$ density.

No uniqueness is claimed.

Milestones

• (2.6), p. 5: $V(R,\tilde\mu)=\sup_{\mu\sim P_T}\int R_{\tilde\mu}\,d\mu-2c\sigma^2H(\mu|\mathcal N(x_0,\sigma^2T))$, for $R\in\mathcal R_b$.
• Proposition 2.1, p. 5: the best response exists, its terminal law has density $f_0e^{R_{\tilde\mu}/2c\sigma^2}/\beta(\tilde\mu)$, and $V(R,\tilde\mu)=2c\sigma^2\ln\beta(\tilde\mu)$, for $R\in\mathcal R_b$.
• Theorem 3.1, p. 7: $\mu$ is an equilibrium iff it has a strictly positive density $f_\mu=f_0e^{R_\mu/2c\sigma^2}/\beta(\mu)$, for $R\in\mathcal R_b$.
• Proof of Theorem 3.2, p. 8: $|(g(m)-x_0)/\sigma\sqrt T|\le C\int_0^1|N^{-1}|=C\sqrt{2/\pi}$ with $C=\exp(\|R(1,\cdot)-R(0,\cdot)\|_\infty/2c\sigma^2)$.
• Proof of Theorem 3.2, p. 8: $g$ is continuous on the compact interval containing its range.

Significance

The theorem reduces an infinite-dimensional fixed point, over laws on $\mathbb R$ defined through a control problem on path space, to a scalar equation for the mean. Everything else is explicit: the equilibrium law is a reparametrized Gaussian quantile, and the game value is a closed form in $R$. The paper's later results build on this: the comparison of game values under the Lorenz order of rewards (Theorem 4.1), the characterization of rewards that realize a target equilibrium (Theorem 5.1), and the tournament design problems of Section 5 all start from (3.2) and the value formula.

The result is proved in the paper, partly by appeal to the literature on Schrödinger bridges; Proposition 2.1 is stated there without proof. None of it is formalized. A formal development would supply the first machine-checked mean field equilibrium of a rank-based game, the entropic weak formulation of a control problem with a terminal reward, and a verified explicit solution against which numerical schemes can be checked.

Difficulty

The reduction from path measures to terminal laws, (2.6), needs the disintegration of $Q$ along $X_T$ (the Schrödinger bridge) and the chain rule for relative entropy; only one inequality follows from data processing. The best response is a Gibbs variational principle on the line, but the optimizer must be lifted back to path space and every optimizer must be shown to have the same terminal law. In Theorem 3.2 the characterization requires inverting $y(r)=N((q_\mu(r)-x_0)/\sigma\sqrt T)$, which in turn requires differentiating through a quantile function when $R$ is only monotone in $r$, not continuous. Existence needs integrability of $N^{-1}$, which is unbounded at both ends, uniformly in $m$, and continuity of $g$ by dominated convergence. The natural shortcut, treating the equilibrium as a density solving (3.1), does not prove the theorem: the equilibrium is defined through the control problem, and connecting the two is the content of the milestones.

Formalization scope

All declarations live in the namespace TerminalRank.Equilibrium, in one definitions module Model. Conventions:

• $\Omega$ is an arbitrary measurable space with a probability measure $P$ under which $B:\mathbb R_{\ge0}\to\Omega\to\mathbb R$ satisfies Mathlib's IsBrownianReal. This is the paper's Wiener space up to relabelling, and also covers its Remark 2.1 (larger filtrations). $T$ has type ℝ≥0, and $\sigma>0$ (the paper needs only $\sigma\ne0$).
• Rewards are real-valued, and the bounded reward classes carry a uniform bound; monotonicity and boundedness are required for ranks $r\in[0,1]$ only. Three milestones, stated in the paper for general $R\in\mathcal R$, are specialized to $R\in\mathcal R_b$, where the reward expectation in (2.3) is defined; the goal assumes $R\in\mathcal R^{rm}_b\subset\mathcal R_b$ anyway. The population law has a finite first moment wherever the paper uses $R_\mu$; equilibrium includes this condition.
• Relative entropy is Mathlib's klDiv, valued in $[0,\infty]$. The suprema in (2.3) and (2.6) run over measures with finite entropy; the excluded ones have value $-\infty$ in the paper, so nothing changes.
• The quantile is the left-continuous inverse $\inf\{x:r\le F(x)\}$, and (3.2) is required for $r\in(0,1)$. The goal states the finiteness of the mean of $\mu$ explicitly; it holds for every equilibrium.

$V$, optimality and equilibrium are defined from the path-space problem (2.3). A formalization that defines them by (2.6), (2.9) or (3.1), or replaces $(\Omega,P,B)$ by a single Gaussian variable, would make the milestones definitional and is ruled out.

Needed infrastructure: Gibbs variational principle (published on the platform as DonskerVaradhan.integral_sub_klDiv_le_log_integral_exp and DonskerVaradhan.klDiv_tilted_self_eq), disintegration and the chain rule for klDiv, Brownian bridges, change of variables for quantile functions, and $E|Z|=\sqrt{2/\pi}$. The quantile and Brownian-bridge lemmas are reusable well beyond this mission. Contributions toward any milestone, and auxiliary lemmas on these tools, are welcome.

Selected references

• E. Bayraktar and Y. Zhang, Terminal Ranking Games, arXiv:1906.09628v2, 2020; Mathematics of Operations Research, 2021. https://arxiv.org/abs/1906.09628
• E. Bayraktar, J. Cvitanić and Y. Zhang, Large tournament games, Annals of Applied Probability 29(6), 2019. https://doi.org/10.1214/19-AAP1490
• E. Bayraktar and Y. Zhang, A rank-based mean field game in the strong formulation, Electronic Communications in Probability 21, 2016. https://doi.org/10.1214/16-ECP24
• E. P. Lazear and S. Rosen, Rank-order tournaments as optimum labor contracts, Journal of Political Economy 89(5), 1981. https://doi.org/10.1086/261010
• H. Föllmer, Random fields and diffusion processes, École d'Été de Probabilités de Saint-Flour XV–XVII, Lecture Notes in Mathematics 1362, Springer, 1988. https://doi.org/10.1007/BFb0086180
• Y. Chen, T. T. Georgiou and M. Pavon, On the relation between optimal transport and Schrödinger bridges: a stochastic control viewpoint, Journal of Optimization Theory and Applications 169, 2016. https://doi.org/10.1007/s10957-015-0803-z

Motivation

The Zero-Core Theorem establishes a fundamental structural property of Ramsey graph colorings: the obstruction preventing extension of the champion R(5,5) coloring from n=43 to n=44 is fully distributed across all constraints, with no individual bottleneck.

This is the first formalization of an essential core theorem in Ramsey theory.

Setting

Given an infeasible constraint system S = {c₁, ..., cₘ}, a constraint cᵢ is essential if S \ {cᵢ} is feasible. The essential core 𝓔 ⊆ S is the set of all essential constraints.

Formalization target

Goal: Prove that the essential core of the K₄₄ extension problem is empty (𝓔 = ∅).

The champion K₄₃ coloring (with 137 monochromatic K₅ violations) contains 2,480 monochromatic K₄ subgraphs. The theorem proves that removing any single K₄ constraint from this system leaves it infeasible.

Significance

This demonstrates that R(5,5) = 43 is a "deep" combinatorial fact arising from holistic constraint interaction, not from any individual forcing constraint. The distributed nature of the obstruction connects to permutation-invariant energy barriers in optimization landscapes.

Difficulty

The theorem requires:

1. Defining constraint systems and feasibility
2. Formalizing the essential core concept
3. Proving infeasibility is preserved under single-constraint removal
4. Computational verification across 2,480 cases

Formalization scope

• Constraint satisfaction problems
• Graph coloring extensions
• Essential core theory
• Computational proof certificates

Selected references

• Daugherty, B. et al. Falsification of R(8,8) > 293: Exhaustive Max-Clique Verification. Zenodo, 2026. DOI: 10.5281/zenodo.19414435
• Exoo, G. A lower bound for R(5,5). J. Graph Theory, 1989.

Motivation

A nonzero-sum game can have several Nash equilibria with different cost vectors. Selecting one equilibrium before asking how the game behaves over time loses information and may make a proposed dynamic rule depend on that selection. Feinstein, Rudloff and Zhang study the entire set of equilibrium cost vectors and ask whether it can be evaluated consistently after the game is stopped. Their continuous-time result is Theorem 3.9 of the pinned preprint, which the authors identify as the main result of the paper. It follows a discrete-time set-value principle developed earlier in the same work. The question is relevant to stochastic games whose controls use the observed path history and whose players need not share an objective.

Setting

Fix a horizon $T>0$, a positive state dimension $d$, and a positive number $N$ of players. The canonical path space is

$$\Omega=\{\omega\in C([0,T];\mathbb R^d):\omega_0=0\}.$$

Its coordinate process is $B_t(\omega)=\omega_t$. The measure $\mathbb P_0$ is Wiener measure, and $\mathcal F_t$ is the filtration generated by the coordinates through time $t$, augmented by Borel $\mathbb P_0$-null events. Each player $i$ has a nonempty convex action set $A_i$. A control profile $\alpha=(\alpha^1,\ldots,\alpha^N)$ consists of progressively measurable, $A_i$-valued processes. A unilateral deviation may be any such process for that player.

The drift $b$ depends on the entire profile, while player $i$'s running cost $f_i$ depends on that player's own action. The terminal cost vector is $\xi$. Assumption 3.1 requires progressive measurability and boundedness of these data. Assumption 3.6 requires uniform continuity in time and path history, and uniform continuity in actions. For a history $(t,\omega)$, concatenation $\omega\otimes_t\widetilde\omega$ holds the old path through $t$ and continues with the increment path afterward. The paper changes measure from $\mathbb P_0$ with a Girsanov density $M^{t,\omega,\alpha}_{T-t}$, then defines the cost $J_i(t,\omega,\alpha)$ as the expected shifted terminal cost plus running cost.

An $\varepsilon$-equilibrium is a profile whose cost for every player is at most $\varepsilon$ above the cost of every unilateral deviation. Let $O_\varepsilon(y)$ be the open Euclidean ball of radius $\varepsilon$ around $y$. The set value is the intersection of the relaxed value sets

$$\mathbb V_\varepsilon(t,\omega) =\bigcup_{\alpha\in NE_\varepsilon(t,\omega)} O_\varepsilon(J(t,\omega,\alpha)),\qquad \mathbb V(t,\omega)=\bigcap_{\varepsilon>0}\mathbb V_\varepsilon(t,\omega).$$

The open lower envelope $\widehat{\mathbb V}_\varepsilon$ is the union of $\mathbb V_{\varepsilon'}$ over $0<\varepsilon'<\varepsilon$. These objects are defined even if the game has no exact equilibrium.

Formalization targets

The target is Theorem 3.9 in the form (3.12) treated in its proof, at the zero history and initial time. For a stopping time $\tau$ with $\tau(0)>0$, let $J(\tau,\eta;0,0,\alpha)$ denote the cost of the game stopped at $\tau$ with bounded $\mathcal F_\tau$-measurable terminal vector $\eta$. The claim is

$$\mathbb V(0,0)=\bigcap_{\varepsilon>0} \left\{y:\begin{array}{l} \exists\eta,\alpha\quad \alpha\in NE_\varepsilon(\tau,\eta;0,0),\\ y\in O_\varepsilon(J(\tau,\eta;0,0,\alpha)),\\ \mathbb P_0\!\left(\eta\notin \widehat{\mathbb V}_\varepsilon(\tau,B)\right)\le\varepsilon \end{array}\right\}.$$

The seven milestones reproduce Proposition 3.4, the density moment bound (3.6), the cost-continuity estimate (3.4), Theorem 3.7(i), Theorem 3.8, and both parts of Lemma 3.10. They cover compactness, regularity and measurability of the set value, as well as approximation of stopping data and controls.

Significance

The equality relates the set of full-horizon equilibrium costs to stopped games whose terminal payoff is approximately compatible with the continuation set value. It gives a dynamic characterization without choosing a particular equilibrium. The relaxation by the same $\varepsilon$ in equilibrium, value ball and exceptional-event probability is part of the result; removing one of those terms changes the game being characterized.

The result is proved in the cited preprint. The mission asks for machine-checked proofs of the stated theorem and its supporting results. The reusable development includes canonical finite-horizon Wiener paths, their augmented filtration, path concatenation, progressive control profiles, a coordinatewise stochastic integral interface, and set-valued equilibrium costs. The published Ethier–Kurtz definition of the Itô-integral relation is reused; it supplies a definition, not a proof of this paper's results.

Difficulty

At a stopping time, the continuation value is a set that depends on the observed path. A pointwise description does not by itself show that membership in this random set is measurable at the stopping time. Equilibrium conditions also compare a profile against every progressively measurable unilateral deviation, so their stability cannot be reduced to a comparison of finitely many actions. The Girsanov density introduces another dependency: its stochastic integral and the resulting costs must be genuine integrable random variables before inequalities between cost vectors have their intended meaning.

Formalization scope

Lean represents $\mathbb R^d$ and $\mathbb R^N$ by Euclidean spaces, with Euclidean norms on costs and the action product. Paths are continuous maps on $[0,T]$ constrained to start at zero. The canonical process is clamped outside the horizon only to make its notation total. The Wiener law is pinned by Brownian finite-dimensional distributions through $T$ and independence of coordinate processes. The filtration adds Borel null sets, so it remains a sub-σ-algebra of the Borel space. Time-indexed controls live on $[0,T]$; the stopping times themselves use WithTop ℝ and are constrained to that interval.

Concatenation uses the second increment strictly after $t$, resolving the overlapping endpoint in the printed indicator formula. Player $i$'s running cost takes only $a_i$. The moduli in Assumption 3.6 are common and uniform in the variables specified there. The stopped running cost integrates to $\tau-t$, with an empty interval contributing zero only outside the theorem's admissible range. The goal uses bounded measurable representatives of $L^\infty$ terminal payoffs; changing a representative on a null set leaves the expected costs and exceptional probability unchanged.

The statement must retain the full Girsanov density, all progressive deviations, the open envelope $\widehat{\mathbb V}_\varepsilon$, and a nonzero player count. A default-zero integral for a nonintegrable payoff, an arbitrary measure in place of Wiener measure, or a restricted deviation class would trivialize or alter it. Solvers can contribute the integrability and stochastic-integral existence facts needed to establish that the definitions have their intended values, followed by proofs of the listed milestones and goal.

Selected references

• Zachary Feinstein, Birgit Rudloff and Jianfeng Zhang, Dynamic Set Values for Nonzero Sum Games with Multiple Equilibriums, arXiv preprint arXiv:2002.00449v2, 2020, §§3.1–3.3. Preprint.
• Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 5, §2. Publisher record.

Why this limit matters

A controller of a large population may choose a separate action for each participant while all participants experience the same random environment. The resulting optimization problem has a growing state space: with $N$ participants, the state records $N$ paths and $N$ controls. A McKean–Vlasov control problem replaces the empirical distribution of those participants by a conditional distribution given the common noise. Djete, Possamaï and Tan prove that this replacement preserves the optimal value asymptotically, even when the participants have different initial laws and the average of those laws does not converge along the full sequence. Their result is Theorem 3.6(iii) of the 2020 preprint, published in 2022.

The distinction between common and individual noise matters for this claim. Conditional on the common noise, particles can still be correlated through a controller that observes the full particle system. The paper's limit theorem concerns the supremum over all admissible predictable particle controls, rather than one prescribed feedback rule. This is the setting in which a finite population optimization problem can approximate its limiting stochastic control problem. The adjacent Proposition 3.7 describes how the limiting value changes with the initial law.

Setting

Fix a time horizon $T>0$, state dimension $n\ge1$, individual noise dimension $d\ge1$, and common noise dimension $\ell\ge0$. Let $A$ be a nonempty Polish control space with base point $a_0$. A state or noise path belongs to $C^k=C([0,T],\mathbb R^k)$, with its uniform norm. The coefficients $b,\sigma,\sigma_0$ determine the drift, individual diffusion and common diffusion; $L$ and $g$ determine running and terminal rewards. The Wasserstein distance $\mathcal W_p$ measures the discrepancy between probability laws with finite $p$th moments.

For an initial law $\nu$, the strong problem lives on the canonical space $\Omega=\mathbb R^n\times C^d\times C^\ell$. Its initial state has law $\nu$, and $W,B$ are independent Brownian noises relative to the canonical past. An admissible control $\alpha$ is predictable and has finite expected integrated $p$th power of its distance from $a_0$. The state $X^\alpha$ solves the controlled equation (2.3). Its coefficients use the conditional law $\bar\mu_t^\alpha$ of the stopped state path and current control given the history of $B$; its terminal reward uses the conditional law $\mu_T^\alpha$ of the stopped state path. The strong value $V_S(\nu)$, equation (2.4), is the supremum of expected reward over those controls and their solutions. These definitions appear in Section 2.1.

For $N\ge1$, the particle problem has initial laws $\nu^1,\ldots,\nu^N$, separate Brownian noises $W^i$, and one shared $B$. Each particle follows equation (2.16) with the empirical state-control law $\varphi_t^N=N^{-1}\sum_i\delta_{(X^i_{t\wedge\cdot},\alpha_t^i)}$ inside its coefficients. The terminal reward uses the empirical state-path law $\varphi_t^{N,X}$. Equation (2.17) defines $V_S^N(\nu^1,\ldots,\nu^N)$ as the supremum of the average expected reward. The empirical laws are built from the very particles whose equations use them; they are not outside inputs. See Section 2.4.

Formalization targets

The goal is the value comparison in Theorem 3.6(iii), equation (3.3):

$$\lim_{N\to\infty}\left|V_S^N(\nu^1,\ldots,\nu^N)-V_S\!\left(\frac1N\sum_{i=1}^N\nu^i\right)\right|=0.$$

The hypotheses include Assumptions 2.1 and 2.12, an embedding $A\subset\mathbb R^j$ for some $j\ge1$, continuity of $L$ and $g$, and a uniform bound on the averages of the initial $p'$th moments, where $p'>p\ge2$. The goal does not assume that the averaged initial laws converge. The milestones are the value lower bounds of Propositions 4.15 and 4.16, the subsequence value limit used in equation (4.44), and the initial-law stability statement (3.4) of Proposition 3.7. Each milestone records the particular clause formalized when its printed result contains additional conclusions. Theorem 3.6 and its proof give the source order.

What the result provides

The theorem compares two optimization problems, rather than only the law of a fixed controlled particle system. The comparison permits heterogeneous initial distributions and keeps the common noise in both models. Proposition 3.7 gives a separate stability statement for the limiting value when initial laws converge in $\mathcal W_p$ with uniformly bounded $p'$th moments. Together these statements identify which finite population values are represented by the limiting control formulation. They are proved in the paper; the open task here is a machine checked derivation from faithful statements.

The formal development fixes the interfaces for conditional laws, predictable controls, path dependent coefficients, Brownian Itô integrals, empirical probability laws and extended real rewards. Those interfaces can support later formalizations of common-noise control and propagation of chaos. The present mission does not state Theorem 3.1(i), the approximation clauses of Theorem 3.1(ii)–(iii), Theorem 3.6(ii), or the “In particular” sentence after Proposition 3.7's equation (3.4). Their different conclusions require further canonical and relaxed-control structures, and the last sentence has a topology ambiguity documented in the paper notes.

Main difficulty

The usual fixed-control convergence question is smaller than the target: particle controls may depend on every observed particle and on the common noise, and the target takes a supremum before comparing values. The conditional law in the limiting equation depends on its own solution, while the empirical law in each particle equation depends on the full coupled particle system. Dropping either dependence changes the optimization problem. Uniform $p'$th moment control must also coexist with unbounded rewards and the extended real convention for their expectations. The source proof invokes compactness and equivalence between strong, weak and relaxed formulations; formalizing those links is substantial work beyond compiling the goal statement.

Formalization scope

Lean uses EuclideanSpace and continuous maps on $[0,T]$ for the path spaces, and Frobenius norms for diffusion matrices. The control type carries a Polish Borel metric and a base point. $\mathcal P_p$ is a finite-lintegral moment condition, and $\mathcal W_p$ takes values in $\mathbb R_{\ge0}\cup\{\infty\}$. Values are extended real suprema over admissible controls and actual solutions. Rewards use the paper's convention $\infty-\infty=-\infty$, rather than a default zero integral. Particle counts are positive; Lean player index zero denotes the paper's player one. The case $\ell=0$ remains included.

Assumption 2.1 includes the displayed Lipschitz, growth and coercive bounds, Borel measurability, nonanticipativity, and lower semicontinuity. Assumption 2.12 factors the coefficients through the state marginal, with $\sigma_0$ independent of the control. The paper leaves the topology behind “continuous” unnamed; the formalization uses sequential $\mathcal W_p$ continuity on finite-moment laws. Its $A\subset\mathbb R^j$ is read as an isometric embedding. Solutions have continuous paths and are adapted to the completed canonical filtration, while conditional laws use the raw common-noise filtration. The goal states finiteness of both values so its real absolute difference is defined. Equation (4.44) is posed in the subsequence form used by its proof. These choices and the source's printed slips are detailed in the moderation notes.

The interface rules out a free conditional-law flow, a free particle empirical measure, and an uncharacterized Brownian law. The weak and relaxed formulations appear only as context for the paper's proof; this proposal contains the strong and particle layers needed by the four selected milestones. Contributions to the omitted equivalence and compactness results are welcome once their canonical-space definitions have been audited.

Selected references

• Mao Fabrice Djete, Dylan Possamaï and Xiaolu Tan, McKean–Vlasov optimal control: limit theory and equivalence between different formulations, Mathematics of Operations Research, 2022; arXiv:2001.00925v2. The formal statements use this preprint's pagination and equation numbers.

Motivation

Off-policy evaluation (OPE) asks for the long-run value of a target decision policy, using only data collected under a different policy. It arises wherever running the target policy is expensive or unsafe: a new treatment rule in medicine, a new recommendation or pricing rule, a candidate controller in reinforcement learning. Importance-sampling estimators reweight whole trajectories. Their variance grows exponentially with the horizon, the curse of horizon (Liu et al. 2018, arXiv:1810.12429).

Kallus and Uehara (arXiv:1909.05850, Operations Research 2022) treat infinite-horizon discounted OPE as a semiparametric estimation problem. They derive the efficiency bound under three models: non-Markov, time-varying Markov and time-invariant Markov (MDP). They then propose double reinforcement learning (DRL), an estimator that combines a q-function estimate with an estimate of the ratio between the discounted state visitation of the target policy and the state distribution of the data. In the MDP model it attains the efficiency bound. This mission formalizes the transition-sampling version of that result, Theorem 6.

Timeline:

• 2016: Jiang and Li (arXiv:1511.03722) and Thomas and Brunskill (arXiv:1604.00923) give doubly robust OPE estimators for finite horizons, built on trajectory-wise importance weights.
• 2018: Liu, Li, Tang and Zhou (arXiv:1810.12429) replace trajectory weights by stationary state-distribution ratios, removing the exponential dependence on the horizon, but without efficiency guarantees.
• 2018: Chernozhukov et al. (arXiv:1608.00060) formalize cross-fitting and Neyman orthogonality for estimation with machine-learned nuisances (double machine learning).
• 2019–2022: Kallus and Uehara derive the MDP efficiency bound (Theorem 3) and prove that cross-fitted DRL attains it (Theorem 6), also under trajectory sampling with mixing (Theorems 10–13).

Setting

States lie in a measurable space $S$ and actions in a measurable space $A$. A time-invariant MDP is a transition kernel $p(s'\mid s,a)$ and a reward kernel $p(r\mid s,a)$ with rewards in $[0,R_{\max}]$. A policy $\pi(a\mid s)$ is a kernel from $S$ to $A$. Fix a discount $\gamma\in[0,1)$, a known target policy $\pi_e$ with known initial law $p^{(0)}_{\pi_e}$, and a behavior policy $\pi_b$.

The estimand is the normalized discounted value

$$\rho^{\pi_e}=\lim_{T\to\infty}\Big(\sum_{t=0}^T\gamma^t\Big)^{-1}\mathbb E_{p_{\pi_e}}\Big[\sum_{t=0}^T\gamma^tr_t\Big].$$

The q-function is $q(s,a)=\mathbb E_{p_{\pi_e}}[\sum_k\gamma^kr_k\mid s_0=s,a_0=a]$, and $v(s)=\int q(s,a)\,\pi_e(da\mid s)$. The discounted visitation is $p^{(\infty)}_{\pi_e,\gamma}=(1-\gamma)\sum_t\gamma^t p^{(t)}_{\pi_e}$, where $p^{(t)}_{\pi_e}$ is the law of $s_t$.

Transition sampling. The data are i.i.d. observations $O_i=(s,a,r,s')$ with law $p_{\pi_b}$: $s\sim p^{(0)}_{\pi_b}$, $a\sim\pi_b(\cdot\mid s)$, and, given $(s,a)$, independently $r\sim p(\cdot\mid s,a)$ and $s'\sim p(\cdot\mid s,a)$. The law of $s'$ may differ from that of $s$.

The density ratios are $\eta(s,a)=\pi_e(a\mid s)/\pi_b(a\mid s)$ and $w(s)=p^{(\infty)}_{\pi_e,\gamma}(s)/p^{(0)}_{\pi_b}(s)$. For candidate nuisances $w',q'$, with $v'(s)=\int q'(s,a)\pi_e(da\mid s)$, the estimating function is

$$\psi(s,a,r,s';w',q')=(1-\gamma)\,\mathbb E_{p^{(0)}_{\pi_e}}[v'(s_0)]+w'(s)\eta(s,a)\big(r+\gamma v'(s')-q'(s,a)\big).$$

The cross-fitted estimator $\hat\rho_{\rm DRL}(\mathcal M_3)$ splits the sample into two folds. It fits $\hat w^{[j]},\hat q^{[j]}$ on fold $j$ and averages $\psi$ over all observations, each evaluated at the nuisances of the other fold. The efficient influence function is $\phi_{\rm eff}=w(s)\eta(s,a)(r+\gamma v(s')-q(s,a))$, and the efficiency bound is $\mathrm{EB}(\mathcal M_3)=\mathbb E[\phi_{\rm eff}^2]$.

Formalization targets

Goal: Theorem 6

Assume the following:

• $w\le C_w$ and $p_{b,S'}\le C_{S'}p_{b,S}$ (6a);
• $\eta\le C_\eta$ (added);
• $\hat w^{[j]},\hat q^{[j]}$ lie in $[0,C_w]$ and $[0,R_{\max}/(1-\gamma)]$ (6b);
• $\|\hat w^{[j]}-w\|_2,\|\hat q^{[j]}-q\|_2=o_p(1)$ (6c);
• $\sqrt n\,\|\hat w^{[j]}-w\|_2\|\hat q^{[k]}-q\|_2=o_p(1)$ for all $j,k\in\{0,1\}$ (6d, equivalent to common envelopes for both folds).

Then

$$\sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)-\frac1{\sqrt n}\sum_{i<n}\phi_{\rm eff}(O_i)\xrightarrow{p}0,\qquad \sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)\xrightarrow{d}N\big(0,\mathrm{EB}(\mathcal M_3)\big).$$

No rate exponent or learner class is fixed. Only the product rate enters.

Milestones, in proof order

1. Lemma 1 (forward): $\mathbb E[\gamma w(s)\eta(s,a)f(s')-w(s)f(s)]+(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[f]=0$ for bounded measurable $f$.
2. $\rho^{\pi_e}=\mathbb E[w(s)\eta(s,a)r]$ (p. 16).
3. Eq. (5): $\mathbb E[\psi(w',q)]=(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[v]=\rho^{\pi_e}$ for every bounded $w'$.
4. $\psi(w,q)=\rho^{\pi_e}+\phi_{\rm eff}$ pointwise (p. 22).
5. Eqs. (6)–(8): $\mathbb E[\psi(w,q')]=\rho^{\pi_e}$ for every bounded $q'$.
6. Jensen step, corrected: $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}C_\eta}\,\|\hat q-q\|_2$.
7. Term (30): $|\mathbb E\psi(\hat w,\hat q)-\rho^{\pi_e}|\le C_\eta(1+\gamma\sqrt{C_{S'}C_\eta})\|\hat w-w\|_2\|\hat q-q\|_2$.
8. Term (28), variance: $\operatorname{var}[\psi(\hat w,\hat q)-\psi(w,q)]\le2a^2\|\hat w-w\|_2^2+2b^2\|\hat q-q\|_2^2$.
9. Term (28) is $o_p(1)$: the centred fold empirical process at the opposite fold's nuisances vanishes.

Significance

Theorem 6 shows that, in a Markov model, a $\sqrt n$-consistent and efficient OPE estimator exists whose variance scales with the number of observed transitions, not trajectories. It requires no complexity (Donsker or entropy) restriction on the nuisance estimators, only a product rate. Any black-box learners with $\|\hat w-w\|_2\|\hat q-q\|_2=o_p(n^{-1/2})$, which allows two subparametric rates, give asymptotically valid confidence intervals at the efficiency bound. The mixed-bias identities (Eqs. (5)–(8)) and Lemma 1 are the same ingredients used by later minimax and adversarial estimators of $w$ and $q$.

The result is proved in the paper; nothing here is presented as open. As far as is known, none of it has a machine-checked proof: no off-policy evaluation, density-ratio characterization or cross-fitting asymptotics exists in Mathlib or on the platform. Formalizing it checks the appendix argument, which is short and contains errors (below). It also produces a reusable layer: kernel-based discounted MDPs on general measurable spaces, discounted visitation measures, and the cross-fitting plus Slutsky template that other double-machine-learning results share.

Difficulty

The obvious route is "the estimator equals the oracle average $\mathbb P_n\psi(w,q)$ plus negligible terms, then apply the CLT". Two of its steps are not routine.

First, the negligible terms are random functions evaluated at random data. The empirical-process term (28) is controlled only conditionally on the other fold, through a conditional Chebyshev argument that needs the independence structure of the split. Treating $\hat w,\hat q$ as fixed functions loses exactly this.

Second, the bias term (30) is second order only because of the mixed-bias structure. That structure rests on Lemma 1, a change-of-measure identity between the discounted visitation of $\pi_e$ and the data distribution. The printed constants are wrong. The Jensen step $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}}\|\hat q-q\|_2$ fails when $\eta$ is large: with one state, $\pi_b$ uniform on two actions and $\pi_e$ a point mass, the left side is $1$ and the right side is $1/\sqrt2$. The bound by $\|\hat w-w\|_2\|\eta\|_2\|\hat q-q\|_2$ is not a valid inequality for a triple product. Both need a bound $\eta\le C_\eta$, which the mission adds.

Formalization scope

• Spaces and kernels. $S$, $A$ are measurable spaces, the action σ-algebra countably generated (for Mathlib's jointly measurable Kernel.rnDeriv). The MDP, the policies and the observation law are Mathlib kernels and measures. The paper's base measures are not used.
• Ratios. $w$ and $\eta$ are toReal of Radon–Nikodym derivatives, not free functions satisfying an identity. Overlap ($\pi_e(\cdot\mid s)\ll\pi_b(\cdot\mid s)$, $p^{(\infty)}_{\pi_e,\gamma}\ll p^{(0)}_{\pi_b}$) is a standing assumption.
• Objects. $q$ is the discounted series, not "a solution of the Bellman equation". $\rho^{\pi_e}$ is the limit of normalized discounted sums, not $(1-\gamma)\mathbb E[v]$ or $\mathbb E[w\eta r]$; those identities are milestones. The discounted visitation is the measure $(1-\gamma)\sum_t\gamma^tp^{(t)}_{\pi_e}$, the limit of the paper's normalized averages.
• Cross-fitting. The folds are $\{i<\lfloor n/2\rfloor\}$ and the rest. Each learner is a jointly measurable function of its own fold's observations only. Rates are convergence in probability of the actual random $L^2$ errors.
• Conclusion. "RAL and efficient" is posed as asymptotic linearity with influence function $\phi_{\rm eff}$ plus the normal limit. Regularity needs the tangent-space framework of Theorem 3 and is not posed.
• Ruled out. The oracle statement with $\hat w=w$, $\hat q=q$ is an i.i.d. CLT for a fixed function and drops the theorem's content. It is not an acceptable substitute for the goal.
• Infrastructure needed. Linearity and Fubini for kernel compositions; summation of discounted occupancies; conditional Chebyshev for cross-fitted empirical processes; Slutsky (TendstoInDistribution with TendstoInMeasure) and Mathlib's i.i.d. CLT tendstoInDistribution_inv_sqrt_mul_sum_sub. The occupancy and Lemma 1 layer and the cross-fitting template are reusable beyond this mission. Proofs of any milestone, and helper lemmas on kernel powers and discounted sums, are welcome.

Selected references

• N. Kallus and M. Uehara, Efficiently Breaking the Curse of Horizon in Off-Policy Evaluation with Double Reinforcement Learning, Operations Research 70(6), 2022; arXiv:1909.05850v6 (2023). https://arxiv.org/abs/1909.05850
• Q. Liu, L. Li, Z. Tang and D. Zhou, Breaking the Curse of Horizon: Infinite-Horizon Off-Policy Estimation, NeurIPS 2018. https://arxiv.org/abs/1810.12429
• V. Chernozhukov, D. Chetverikov, M. Demirer, E. Duflo, C. Hansen, W. Newey and J. Robins, Double/Debiased Machine Learning for Treatment and Structural Parameters, The Econometrics Journal 21(1), 2018. https://arxiv.org/abs/1608.00060
• N. Jiang and L. Li, Doubly Robust Off-Policy Value Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1511.03722
• P. Thomas and E. Brunskill, Data-Efficient Off-Policy Policy Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1604.00923