All missions

Motivation

In atomic dynamic routing, indivisible agents (vehicles, packets, travellers) enter a network over time and travel along fixed routes. Each road admits a limited number of agents per unit of time, so agents queue at its entrance. A basic question for traffic models, packet-switching networks and dynamic routing games is how long an agent can stay in the network, its residence time. Upper bounds on residence times are what make it possible to bound queue lengths and the price of anarchy in dynamic routing games.

Greedy packet scheduling, where an edge never idles while packets wait for it, was studied by Cidon, Kutten, Mansour and Peleg (SIAM J. Comput. 1995), who showed that cycles can make delays large, and by Mansour and Patt-Shamir (J. Algorithms 1993), who bounded delivery times when every route is a shortest path. Cao, Chen, Chen and Wang (MOR 2022) prove a bound for arbitrary routes on acyclic networks. It holds under any rule that decides which waiting agent may leave next, and agents may keep entering forever. Their Theorem 1 is the goal of this mission. The paper then uses it to show that equilibria of three dynamic routing games on series-parallel networks have bounded queues (§6).

Setting

A network $G=(V,E)$ is a finite directed multigraph (parallel edges allowed) that is acyclic. Every edge has unit length and unit capacity. A path is a sequence of edges, each starting where the previous one ends. $L_{vw}$ is the number of edges of a longest $v$-$w$ path.

Time is discrete, $0,1,2,\dots$. Agents form a set $\Delta$, possibly infinite. At each time finitely many agents enter. Agent $i$ enters at time $r_i$ at his origin $o_i$ and follows a fixed route, a nonempty $o_i$-$d_i$ path. The tail of each edge holds a buffer. Two rules govern the dynamics:

• (A1) an agent reaching a vertex that is not his destination enters the buffer of his next edge at once;
• (A2) at every integer time, whenever a buffer is nonempty, exactly one agent leaves it and reaches the head of the edge one time unit later; the others wait.

No rule says which agent leaves. Every choice consistent with (A2) is an admissible run. An agent exits $G$ on reaching his destination. His residence time is his exit time minus his entry time (Definition 1).

Fix a focal agent $\zeta$ with entry time $r$. $G_\zeta$ is the subnetwork formed by all $o_\zeta$-$d_\zeta$ paths. For an integer time $r_0$:

• $A_{\zeta,p}$ is the set of agents who enter after time $r$ and use an edge of $G_\zeta$;
• $B_{\zeta,p}(r_0)$ is the set of agents $i\neq\zeta$ who entered by time $r$, are still inside $G$ at time $r_0$, and use an edge of $G_\zeta$.

An agent exits $G_\zeta$ when he reaches the head of the last edge of his route lying in $G_\zeta$.

Formalization targets

Goal: Theorem 1 (p. 7)

For every admissible run and every integer $r_0\ge r$: if no agent of $A_{\zeta,p}$ exits $G_\zeta$ before $\zeta$ exits $G$, then

$$t_\zeta\ \le\ r_0+L_{o_\zeta d_\zeta}+\bigl|B_{\zeta,p}(r_0)\bigr|,$$

where $t_\zeta$ is the exit time of $\zeta$.

Milestones (§3.2, p. 9)

When $\zeta$ is still inside $G$ at $r_0$, the proof follows tokens: imaginary markers that $\zeta$ produces from time $r_0$ on, and that travel with the agents leaving buffers ((s1), (s2), p. 8). The milestones are the paper's statements about them, with $L=L_{o_\zeta d_\zeta}$:

1. (p1) each agent holds at most one token, and a buffer never contains more tokens than agents;
2. (p2) the agent leaving $\zeta$'s buffer always holds exactly one token;
3. (p3) after $r_0$, $\zeta$ produces a new token only while he waits;
4. Claim 1 the induction step of Lemma 1 at the vertices where token $k$ departs right after a smaller token;
5. Lemma 1 token $k$ departs every vertex $v$ of its trail inside $G_\zeta$ by time $r_0+(L-L_{vd_\zeta}+k-1)$;
6. token exit token $k$ exits $G_\zeta$ by time $r_0+(L+k-1)$.

Significance

The result. The bound does not depend on the rule that selects the leaving agent, so it covers every queueing discipline at once: FIFO, global agent priorities, and the edge-priority rules of earlier dynamic routing games. With $r_0=r$ and no later entrants on $G_\zeta$, it gives Corollary 1: the residence time of $\zeta$ is at most $L_{o_\zeta d_\zeta}+|B_{\zeta,p}(r)|$. Example 1 (p. 8) shows that the bound can be attained. The freedom in $r_0$ is what §6 uses to show that queue lengths stay bounded at equilibria of dynamic routing games on series-parallel networks.

Formalizing it. The theorem is proved on paper. No machine-checked version is known to exist, and the platform has no rule-free model of atomic dynamic routing. The mission adds that model: a run is a set of leave times constrained by (A1)–(A2), not a fixed simulation. It also adds the multi-token process and the paper's chain of statements leading to Theorem 1.

Difficulty

The obvious argument is wrong. One might reason that $\zeta$ travels at most $L_{o_\zeta d_\zeta}$ edges and each earlier agent delays him at most once, giving the bound at once. The paper notes (p. 7) that this intuition fails even with two agents: a single agent can delay $\zeta$ more than $|\Delta|$ times, because delays propagate through other buffers. Bounding the total therefore means tracking chains of delays across the network rather than charging each delay to one agent.

Formally, the hard parts are:

• the run is only constrained, not determined;
• the token process is defined by recursion over time, using the unique leaver of each buffer;
• (p1)–(p3) are invariants proved by induction on time;
• Lemma 1 combines induction on the token index with longest-path inequalities in an acyclic graph.

Formalization scope

• Model. Network V E (tail and head maps) with finite V, E and a hypothesis Acyclic: no nonempty closed walk. Paths are edge lists. longest v w is the supremum of path lengths in $\mathbb N$; it is a maximum wherever it is used.

• Runs. RunData holds entry times, routes, origins and destinations, and leave times leave i j in $\mathbb N\cup\{\infty\}$ for the $j$-th edge of $i$'s route, numbered from $0$. IsADR states that:

  • routes are nonempty origin–destination paths;
  • finitely many agents enter per time;
  • nobody leaves a buffer before entering it;
  • (A2) holds, as unique existence of the leaver of each nonempty buffer at each time.

  Agents form an arbitrary type and may be infinitely many. An agent may never be served (leave time $\infty$), as in the paper, so the theorem also asserts that $\zeta$ exits.

• Derived objects. Exit times, $G_\zeta$, $A_{\zeta,p}$, $B_{\zeta,p}(r_0)$ and the exit time from $G_\zeta$ are definitions computed from the run, never free parameters. $|B_{\zeta,p}(r_0)|$ is Set.ncard of a set that is finite under IsADR.

• Tokens. The token milestones assume that $\zeta$ is inside $G$ at $r_0$, as §3.1 requires when starting the construction. Tokens are indexed from $1$. A new token gets index one plus the number produced so far. Bounds with subtraction are written additively over $\mathbb N$, e.g. $s+L_{vd_\zeta}+1\le r_0+L+k$, which is the same inequality over the integers.

• Ruled out. None of these is used, since each proves a different statement: a fixed tie-breaking rule (FIFO or priorities), exit times as free parameters, finitely many agents, or dropping acyclicity, which Remark 2 shows is necessary.

Contributions welcome: proofs of the token invariants, of Lemma 1, and of the goal. The network and run definitions can be reused for the paper's other results (Theorem 2 on uniform capacities, the routing games of §5–6).

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Bounding residence times for atomic dynamic routings, Mathematics of Operations Research, 2022 (accepted manuscript: WRAP 160244). https://doi.org/10.1287/moor.2021.1242 , https://wrap.warwick.ac.uk/160244
• Y. Mansour, B. Patt-Shamir, Greedy packet scheduling on shortest paths, Journal of Algorithms 14(3):449–465, 1993.
• I. Cidon, S. Kutten, Y. Mansour, D. Peleg, Greedy packet scheduling, SIAM Journal on Computing 24(1):148–157, 1995.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4:1–4:26, 2018.

Motivation

We characterize the bath resources needed to supply repeated uses of a fixed finite-dimensional quantum channel in a closed device. For each horizon $T$, one bath, one initial state and one repeated unitary are fixed before the user. Each output is returned before the next input arrives; no reset, discard, fresh ancilla or uncounted controller is available. Approximation error must vanish against arbitrary adaptive users with quantum memory and references. Writing $r=\lim \log_2(R_T)/T$ for the bath dimension rate and $s=\lim S(ω_T)/T$ for the actual initial entropy rate, we prove that the achievable region is exactly $s\ge 0$, $r+s\ge h$ and $r-s\geκ$. Here $h$ is maximum entropy exchange and $κ$ is a smoothed independent-reference extension cost, with the zero-error limit taken before the supremum over full-rank inputs. Its exact fixed-input form is an affine transform of the zero-leakage quantum privacy funnel. The minimum dimension rate is $(h+κ)/2$. The proof combines entropy converses, a bath-dimension-independent support repair, and a closed adaptive implementation of encoder-only fully quantum Slepian--Wolf recycling. All seeds, clocks, workspace and retained residues are counted. Worked examples include dephasing, pure replacement and a qubit channel with $0<κ<h$. No computability of $κ$ or efficient circuit synthesis is claimed. △ Less

This mission is the statement-level formalization of Bath dimension and initial entropy for closed repeated use of a quantum channel (arXiv:2609.18267v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: uniform collision gain (Theorem 3.1, PDF p. 6). 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

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

• Theorem 2.1 (seed paper result): exact bath-dimension/initial-entropy rate region: Closed all-horizon causal device and complete adaptive process metric, actual rate-limit region, counted padding/internal-purification transformations (hard)
• Theorem 2.2: same-spectrum converse: Same actual initializer in two complete adaptive tester experiments and all-integer liminf resource rates (hard)
• Theorem 5.1: causal balancing for any fixed finite exact witness: Causal block compiler with actual flat initializer, repeated-unitary semantics and separately converging seed/data rates (hard)
• Proposition 7.1: unitary channels: Complete all-horizon memory rate c_seq and bath-free repeated-unitary realization (hard)
• Proposition 7.2: qubit dephasing and exact streaming corner: Counted exact streaming process from independent Pauli generators, ordered history words and one clocked unitary (hard)
• Proposition 7.3: pure replacement: Pure-replacer complete operating memory rate and counted preallocated-cell/clock process (hard)
• Proposition 8.1: shared-seed marginal/complete separation: Shared-bit repeated controlled-Z process, product-marginal repeatability and supremum complete adaptive error (hard)
• Section 8, unnumbered: zero memory rate iff unitary: Zero complete operating memory rate as an asymptotic repeated-service property (hard)
• Lemma A.1: fixed adaptive spectral concentration projector: Reachable states of adaptive controllers with fresh comparison channels and untouched spent Lambda outputs (hard)
• Lemma A.2: simultaneous bath/exterior/source support and spectral-cap cuts: Exact comparison block and pure complete exterior, including future-accessed spectators and their purifiers (hard)
• Lemma A.4: exact integer wires and reversible flat-stock preparation: Reversible flat-stock preparation and permanent wire/tranche allocation with immediate collision service (hard)
• Proposition A.5: joint recycling, every prefix, and one repeated unitary: Joint comparison boundary invariant, actual block composition, every prefix and counted repeated-unitary clock (hard)
• Proposition A.6: exact actual spectrum and every-horizon limits: Every-integer-horizon compiled family with actual flat spectrum, exact physical counts and separate seed/data limits (hard)

Selected references

• Bath dimension and initial entropy for closed repeated use of a quantum channel, arXiv:2609.18267v1, https://arxiv.org/abs/2609.18267v1

Motivation

In this paper we fill the gap in previous works by proving the formula for entanglement-assisted capacity of quantum channel with additive constraint (such as bosonic Gaussian channel). The main tools are the coding theorem for classical-quantum constrained channels and a finite dimensional approximation of the input density operators for entanglement-assisted capacity. The new version contains improved formulation of sufficient conditions under which suprema in the capacity formulas are attained.

This mission is the statement-level formalization of Entanglement-assisted capacity of constrained quantum channel (arXiv:quant-ph/0211170v2). 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 Trace-norm compactness of an energy sublevel (§3, unnumbered Lemma (proof on PDF p.11), PDF p. 10). 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:

• §1, Proposition 1: An operational constrained c-q coding model on arbitrary input alphabets and general trace-class output states, with genuine product outputs, bounded POVMs, maximal message error, and a liminf achievable-rate capacity. (hard)
• §1, Proposition 2 (conclusion on p.3): Borel-probability barycenters and integrated entropy for trace-norm state-valued maps, coupled to a genuine bounded-below unbounded selfadjoint observable with Gibbs trace. (hard)
• §2, Proposition 3, (19)--(20): Parallel general trace-class CPTP channel powers, constrained block codes and two separately defined information optimizations with different feasible sets. (hard)
• §3, Proposition 4, (30): Energy-constrained operational entanglement-assisted block capacity on arbitrary Hilbert spaces, plus actual purification/reference extension and the finite-entropy mutual-information interface. (hard)
• §3, (31)--(32): The special locally encoded common-resource assisted ensemble class and its block Holevo optimum, distinct from operational assisted codes. (hard)
• §3, assertion before (33): Constrained channel mutual information for arbitrary entangled block states, with actual reference purifications and additive energy expectation. (hard)
• §3, finite-rank approximation and (35) on p.10: Constructed positive-eigenvalue spectral truncations, their normalized purifications, and channel mutual information in one compatible operator model. (hard)
• §3, Proposition 5, (37): Actual dual-channel domination for bounded-below unbounded output observables, Gibbs trace, and an operational assisted capacity attaining state. (hard)
• Closing paragraph; (30) with (36): Extended-valued relative-entropy channel mutual information coupled to operational assisted capacity without either entropy restriction. (hard)

Selected references

• Entanglement-assisted capacity of constrained quantum channel, arXiv:quant-ph/0211170v2, https://arxiv.org/abs/quant-ph/0211170v2

Motivation

The Schur transform, which block-diagonalizes the tensor representation $U^{\otimes n}$ of the unitary group $\mathbf{U}_d$ on $n$ qudits, is an important primitive in quantum information and theoretical physics. We give a generalization of its quantum circuit implementation due to Bacon, Chuang, and Harrow (SODA 2007) to the case of mixed tensor $U^{\otimes n} \otimes \bar{U}^{\otimes m}$, where $\bar{U}$ is the dual representation. This representation is the symmetry of unitary-equivariant channels, which find various applications in quantum majority vote, multiport-based teleportation, asymmetric state cloning, black-box unitary transformations, etc. The "mixed" Schur transform contains several natural extensions of the representation theory used in the Schur transform, in which the main ingredient is a duality between the mixed tensor representations and the walled Brauer algebra. Another element is an efficient implementation of a "dual" Clebsch-Gordan transform for $\bar{U}$. The overall circuit has complexity $\widetilde{O} ((n+m)d^4)$. Finally, we show how the mixed Schur transform enables efficient implementation of unitary-equivariant channels in various settings and discuss other potential applications, including an extension of permutational quantum computing that includes partial transposes.

This mission is the statement-level formalization of The mixed Schur transform: efficient quantum circuit and applications (arXiv:2310.01613v1). 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 Two-input conclusive teleportation: exact success and corrected output (Section 5.1.1: two-input conclusive teleportation success, PDF p. 29). 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:

• Main result / Corollary 4.12: efficient mixed Schur isometry: Concrete signed-staircase rational irreps with orthonormal GT and dimension-truncated path coordinates, their fixed mixed Schur isometry, and its binary channel/resource semantics. (hard)
• Section 3.3 and Remark 3.1: cascade correctness and factor-order flexibility: Ordinary and dual CG maps on the concrete signed GT sectors, path extension/reindexing and canonical permutations for factor type words. (hard)
• Theorem 4.5: multiplicity-free dual Wigner–Eckart: Concrete rational-irrep actions in GT bases and the actual multiplicity-free dual CG matrix. (hard)
• Proposition 4.6: dual CG coefficient tensor operators: The source dual CG coefficient blocks and their concrete irrep actions. (hard)
• Lemma 4.7: restriction of the coefficient tensor operators: Compatible GT restriction inclusions between U(d) and U(d-1) and actual coefficient tensor blocks. (hard)
• Proposition 4.8: reduced Wigner coefficient recursion: The constructed restriction blocks and reduced coefficients relative to the lower-dimensional source dual CG transform. (hard)
• Section 4.3 Eqs.(69)–(71): recursive factorization: The modified lower dual transform and reduced Wigner rotation on valid dependent label sectors. (hard)
• Remark 4.10: coherent reduced Wigner operator synthesis: A concrete reduced-Wigner target in the source GT conventions and its uniform reversible finite-precision coefficient/synthesis computation. (hard)
• Corollary 4.11: efficient dual Clebsch–Gordan transform: The actual coherent dual CG transform over bounded staircase labels and its encoded circuit/workspace interface. (hard)
• Remark 4.13: extensions to elementary and symmetric-power input irreps: Remark 4.13: extensions to elementary and symmetric-power input irreps (source-ambiguity)
• Proposition 5.2: deterministic one-input teleportation implementation: Proposition 5.2: deterministic one-input teleportation implementation (source-ambiguity)
• Section 5.1.1: random symmetric unitaries and random equivariant channels: Section 5.1.1: random symmetric unitaries and random equivariant channels (source-ambiguity)
• Proposition 5.5: Choi-only average-case observable prediction: A Choi-measurement training law, actual learned estimator function and cost-bearing classical learner implementing the HCP adaptation. (hard)
• Lemma 5.10: Schur-sparse Choi and square-root block encodings: Valid Schur-label encodings of the actual fixed transform and two-sided sparse row/column/value oracle programs with gate/query accounting. (hard)
• Proposition 5.11: output expectation estimation from a Choi square root: Proposition 5.11: output expectation estimation from a Choi square root (source-ambiguity)
• Section 5.1.3: combined diagonal/sparse estimation bounds: Section 5.1.3: combined diagonal/sparse estimation bounds (source-ambiguity)
• Section 5.1.3: composition by square-root Choi block encodings: Section 5.1.3: composition by square-root Choi block encodings (source-ambiguity)
• Section 5.2: partially transposed permutational quantum computing: Section 5.2: partially transposed permutational quantum computing (source-ambiguity)

Selected references

• The mixed Schur transform: efficient quantum circuit and applications, arXiv:2310.01613v1, https://arxiv.org/abs/2310.01613v1

Motivation

The maximum rates for reliably transmitting classical information over Bosonic multiple-access channels (MACs) are derived when the transmitters are restricted to coherent-state encodings. Inner and outer bounds for the ultimate capacity region of the Bosonic MAC are also presented. It is shown that the sum-rate upper bound is achievable with a coherent-state encoding and that the entire region is asymptotically achievable in the limit of large mean input photon numbers.

This mission is the statement-level formalization of Multiple-Access Bosonic Communications (arXiv:quant-ph/0506171v2). 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 Operational homodyne and heterodyne coherent-state MAC regions (§II.B, (5)–(8): single-mode homodyne/heterodyne capacity regions, 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

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

• §II.B,(9)–(11): Normalized coherent-state Fock ensembles and collective-receiver product-code MAC capacity (hard)
• §II.B,(12): Additive random-displacement Fock channel and operational product-code capacity (hard)
• §II.C,(23)–(27): Collective-receiver wideband bosonic coding and Gaussian ensemble entropy (hard)
• §III.A,(35)–(40),(50)–(58): Physical Gaussian displaced-state mixtures, raw second moments, and infinite-dimensional entropy (hard)
• §III.A,(48)–(49): Individual Holevo maximization over physical displacement laws (hard)
• §III.A,(57)–(58): Joint Holevo sum functional for independent physical displacement laws (hard)
• §III.A,(31)–(34),(59): Operational HSH two-sender capacity with physical Gaussian seed (hard)
• §III.B,(60)–(65): Fixed-seed Gaussian beam-splitter MAC and photon-budget accounting (hard)
• §III.B,(66),Fig.5: Operational fixed-seed Gaussian region realizing the explicit strict extension (hard)
• §IV,Theorem 1,(67)–(74): Anisotropic attenuator, thermal entropy conjecture, squeeze whitening, and ordinary classical capacity (hard)
• §IV,(75)–(76): Physical displaced squeezed-seed coding and unconditional anisotropic-channel capacity lower bound (hard)
• §IV,(77): Thermal attenuator capacity and conditional specialization (hard)
• §IV,(78)–(79): Pure squeezed-environment attenuator capacity and equal-energy thermal comparison (hard)
• §V,(80) and individual bounds: Ultimate independent-sender bosonic capacity allowing across-use entanglement (hard)
• §V, coherent-state sum achievement: Physical coherent encoding attaining the ultimate MAC sum capacity (hard)
• §V, Gaussian sum achievement: Pure one-port Gaussian seed output and above-threshold physical sum code (hard)
• Appendix,(A.1): Photon-support-constrained operational quantum MAC regions and their closed limit (hard)
• Abstract; §V,PDF pp.9–10: Unspecified whole-region high-energy convergence notion (source-ambiguity)

Selected references

• Multiple-Access Bosonic Communications, arXiv:quant-ph/0506171v2, https://arxiv.org/abs/quant-ph/0506171v2

Why this game matters

An optimal stopping game asks two players to choose when to stop a shared process. The first player receives one payoff if they stop first and another if the second player stops first. Such a game changes when one player knows a parameter that the other can only infer from observations. The informed player can reveal information through the timing of a stop, and can conceal it by randomising. De Angelis, Ekström and Glover study this interaction for a diffusion with one of two possible drifts. Their preprint gives a verification theorem for general payoffs and solves a linear geometric Brownian example explicitly. This mission targets the latter result, Theorem 6.10. The result is proved in the paper; the work here is to express its model, strategy classes, supporting results and conclusion in Lean.

The game and its information

The asset value starts at $x>0$ and evolves as a geometric Brownian motion $X_t=x\exp((\mu_\theta-\sigma^2/2)t+\sigma W_t)$, where $\sigma>0$, $\mu_0<0<\mu_1$, and the hidden type $\theta\in\{0,1\}$ selects the drift. Initially $\mathbb P(\theta=1)=\pi\in(0,1)$; write $\phi=\pi/(1-\pi)$ for the initial odds. Player 1 sees the history of $X$ and chooses an almost surely finite stopping time $\tau$ for its augmented observation filtration $\mathcal F^X$. Player 2 also knows $\theta$ and chooses an adapted, nondecreasing control $\Gamma$ for the augmented filtration $\mathcal F^{X,\theta}$. An independent uniform variable $U$ turns this control into the randomised stopping time $\gamma=\inf\{t\ge0:\Gamma_t>U\}$. The initial value $\Gamma_0$ may be positive, representing a jump at time zero.

If $\tau<\gamma$, Player 1 receives $f(X_\tau)$; if $\gamma\le\tau$, Player 1 receives $g(X_\gamma)$. Thus a finite tie pays $g$. The expected payoff is $J(\tau,\Gamma)$. Player 1 maximises it and Player 2 minimises it. A saddle point $(\tau^*,\Gamma^*)$ satisfies $J(\tau,\Gamma^*)\le J(\tau^*,\Gamma^*)\le J(\tau^*,\Gamma)$ for every admissible pair $(\tau,\Gamma)$. In the linear example $f(y)=y$ and $g(y)=(1+\varepsilon)y$, where $\varepsilon>0$.

The uninformed player's posterior probability $\Pi_t=\mathbb P(\theta=1\mid\mathcal F^X_t)$ is expressed through the posterior odds $\Phi_t=\Pi_t/(1-\Pi_t)$. The informed strategy is a pair $(\Gamma^0,\Gamma^1)$, one control for each type. Conditional laws $P^i=P(\cdot\mid\theta=i)$ define the interim payoffs $J^0,J^1$. The scaled ex-ante payoff is $\widehat J=(1+\phi)J$. These quantities permit both an ex-ante saddle-point statement and the agent-form equilibrium statement of Proposition 3.6.

Formalization targets

The supporting targets begin with the filtering and payoff identities of Section 3, the quasi-variational verification result of Theorem 5.1, and the reflected-likelihood and boundary-value facts of Section 6. They culminate in the explicit linear-game equilibrium. Two real numbers $0<A<B$ are determined by equations (90) and (93); piecewise power functions $V_1,V$ are defined by (89) and (91), extended by (94)–(97), and $V_0(\phi)=V(\phi)-\phi V_1(\phi)$. The type-one control $\Gamma^B$ keeps the adjusted odds $\Phi^B=\Phi(1-\Gamma^B)$ below $B$, while Player 1 stops at $\tau_A=\inf\{t:\Phi^B_t\le A\}$.

The goal is Theorem 6.10: $(\tau_A,(0,\Gamma^B))$ is a saddle point, and for every $x,\phi>0$,

$$\widehat J_{x,\phi}(\tau_A,(0,\Gamma^B))=xV(\phi),\qquad J^0_{x,\phi}(\tau_A,0)=xV_0(\phi),\qquad J^1_{x,\phi}(\tau_A,\Gamma^B)=xV_1(\phi).$$

The mission's milestone list follows the paper's stated results. It includes the payoff reductions, Theorem 5.1, reflection at $B$, the ODE bounds, the unique ratio $A/B$, and the verification of the explicit value functions.

What the result establishes

The theorem identifies actual strategies for both players, rather than only showing that the game's upper and lower values coincide. It specifies how the informed player's randomisation depends on the unobserved type and how the uninformed player responds to the adjusted odds. It also gives the ex-ante and both type-conditional payoffs. Without the saddle inequalities over the full strategy classes, the formulas would describe candidate strategies rather than an equilibrium.

A Lean development must capture the paper's information restrictions and time-zero behaviour before the analytical proof can be meaningful. Reusable components include a model-independent two-filtration randomised Dynkin frame, the augmented observation filtrations, randomised stopping times, nonnegative extended payoffs, conditional-law decomposition, and Stieltjes integration with an initial jump. The paper has a written proof; the statements here are open Lean goals, not machine-checked proofs.

Main difficulty

The verification theorem couples a partial differential inequality to a singular control and a stopping time. The adjusted odds can jump when the control jumps, so ordinary continuous-path differential conditions do not by themselves describe the admissible action. The support conditions and transversality limits in Theorem 5.1 are needed to connect the analytic candidate values to payoffs for strategies that can stop at any time. In the linear example, obtaining the power-function candidates is only one part of the target: their free boundaries must be valid, the reflected control must be admissible, and the saddle inequalities must hold against all admissible alternatives.

Formalization scope and conventions

The Lean model uses the explicit strong solution of the §6 GBM on a complete probability space carrying a Brownian motion and independent uniform devices $U,\Theta$. It sets $\theta^\pi=\mathbf1_{\{\Theta<\pi\}}$. Paths of the chosen Brownian modification are continuous. Player 1's filtration is generated by $X$ plus null sets; Player 2's also contains $\theta$; neither contains $U$. Stopping times live in $[0,\infty]$, with Player 1 required to stop almost surely. Payoffs are nonnegative extended integrals and equal zero if both stopping times are infinite. The Stieltjes convention counts $\Gamma_0$.

The posterior odds $\Phi$ use the GBM closed form. The running-maximum formula defines $\Gamma^B$ and permits its initial jump. The tilted law used in Lemma 6.5 is represented by an equivalent likelihood-path law. Theorem 5.1 is stated for the GBM instance with general continuous $0\le f\le g$ and relative closures inside $(0,\infty)^2$. Its localisation integral retains the factor printed in the preprint. The explicit boundaries, controls and values in the goal are definitions, never free variables or hypotheses; the saddle inequalities quantify over the full player strategy classes.

There is a normalization slip in the paper's (23): it prints $\Phi_t=dP^1/dP^0$ on $\mathcal F^X_t$, although $\Phi_0=\phi$ and a Radon–Nikodym derivative at time zero equals one. Equations (20)–(21) give $dP^1/dP^0=\Phi_t/\phi$. The formal filtering item uses that corrected identity. Equation (50) similarly identifies the ex-ante value with the scaled payoff; the formal target records $\widehat J=(1+\phi)J$ and states the payoff identities without confusing the two. The source's domain $\mathbb R_+^2$ in Theorem 6.10 is read as $x,\phi>0$, as required by the model. These readings are documented in the local moderation notes.

Selected references

• T. De Angelis, E. Ekström and K. Glover, Dynkin Games with Incomplete and Asymmetric Information, arXiv preprint 1810.07674v5, 2020. Preprint.

Motivation

Large manufacturers procure components by competitive bidding, and many of them also run cost-reduction investigations: the buyer's engineers visit a supplier's plant and look for process changes that lower the cost of the contracted part. The savings are passed to the buyer as a lower contract price. In practice such investigations usually happen after the contract is awarded, on the winner only. Chen, Beil and Duenyas (Operations Research 70(6), 2022) compare that convention with a mechanism in which the buyer investigates before the award, possibly several suppliers, and then awards the contract on the investigated prices.

Investigating before the award obviously helps the buyer for fixed bids: she sees more cost reductions before choosing. The question is whether suppliers lose. The buyer keeps every identified saving, and investigations of competitors make their prices more aggressive, so suppliers seem to have reason to resist. The paper shows that, when suppliers are ex ante symmetric, they do not: every supplier's ex ante expected profit is at least as high when investigations come before the award. This mission formalizes that result.

Setting

A buyer procures one contract from suppliers $\mathcal N=\{1,\dots,N\}$ and must transact with one of them. Supplier $i$ has a private cost $c_i=\Delta^c_i+\epsilon^c_i$, where $\Delta^c_i\ge0$ is public and $\epsilon^c_i$ has density $f$ on $[\underline c,\bar c]$ with mean $0$; so $c_i$ has density $f_i(c)=f(c-\Delta^c_i)$, c.d.f. $F_i$, and support $C_i=[\underline c_i,\bar c_i]$. Costs are independent.

An investigation of supplier $i$ costs the buyer $d\ge0$ and reveals a cost reduction $t_i=\Delta^t_i+\epsilon^t_i\ge0$, where $\epsilon^t_i$ has density $g$ on $[\underline t,\bar t]$ with mean $0$, independently of everything else. At most $\hat N\in\{1,\dots,N\}$ suppliers can be investigated, and costs always exceed reductions: $\Delta^t_i+\bar t<\Delta^c_i+\underline c$. Each supplier submits a sealed bid $b_i\in B_i=[0,\bar c_i]$. If an investigated supplier wins, he is paid his updated bid $b_i-t_i$ and his cost becomes $c_i-t_i$, so his margin is $b_i-c_i$ in every case.

• BAI (bid, award, investigate). The buyer awards the contract to the lowest $\lambda_i=b_i-r_i$, where $r_i=\max\{0,\Delta^t_i-d\}$ is the expected saving from investigating the winner afterwards. Ties are broken at random.
• BIA (bid, investigate, award). The buyer investigates sequentially. Each round she uses the bids and the reductions revealed so far to stop or to investigate one more supplier, and stopping is final. She then awards the contract to the lowest updated bid. Her policy minimizes the expected payment plus investigation cost, problem (1). Theorem 1 solves (1) by an index policy: with $\tau$ the root of $d=\int_\tau^\infty(\epsilon^t-\tau)\,dG(\epsilon^t)$, each supplier gets the index $\mu_i(b_i)=b_i-\max\{0,\tau+\Delta^t_i\}$. The buyer investigates in increasing order of index while the current lowest updated bid is at least the next index, up to a cap $\bar N\le\hat N$.

Supplier $i$'s winning probability at bids $b$ is $W_i(b)$, over $t$ and the tie-break. With the others bidding $\beta_{-i}(c_{-i})$, his expected profit from bidding $b$ at cost $c$ is $u_i(b;c)=(b-c)\,\mathbf E_{c_{-i}}[W_i(b,\beta_{-i}(c_{-i}))]$, equation (5). A Bayesian Nash equilibrium is a profile of strategies $\beta_i:C_i\to B_i$ that are best replies at every type. Supplier $i$'s ex ante expected profit is $\mathbf E_{c_i}[u_i(\beta_i(c_i);c_i)]$.

Formalization targets

Goal: Theorem 2 (weak form)

Suppose that suppliers are ex ante symmetric ($\Delta^c_i=\Delta^c$, $\Delta^t_i=\Delta^t$), that $F_i/f_i$ is nondecreasing (Assumption 1), and that $d<\max_i\Delta^t_i$ (Assumption 2). Let $\beta^{\mathrm{BIA}}$ be a symmetric equilibrium of BIA, and $\beta^{\mathrm{BAI}}$ a symmetric nondecreasing equilibrium of BAI. Then for every supplier $i$,

$$\mathbf E_{c_i}\big[u^{\mathrm{BAI}}_i(\beta^{\mathrm{BAI}}_i(c_i);c_i)\big]\;\le\;\mathbf E_{c_i}\big[u^{\mathrm{BIA}}_i(\beta^{\mathrm{BIA}}_i(c_i);c_i)\big].$$

Milestones

1. Proposition 1. There exists an equilibrium $\check\beta$ of the first-price auction with costs $c_i-r_i$ whose shifted strategy $\tilde\beta_i(c_i)=\check\beta_i(c_i-r_i)+r_i$ is a BAI equilibrium.
2. Theorem 1(a). The index policy (3) minimizes the buyer's expected cost (1) over all admissible sequential policies, for every bid vector.
3. Zero profit at the top. $U^{\mathcal M}_i(\bar c_i)=0$ for $\mathcal M\in\{\mathrm{BIA},\mathrm{BAI}\}$.
4. Envelope formula (A.2). $U^{\mathcal M}_i(c_i)=U^{\mathcal M}_i(\bar c_i)+\int_{c_i}^{\bar c_i}\phi^{\mathcal M}_i(y)\,dy$.
5. Ex ante identity. $\mathbf E_{c_i}[U^{\mathcal M}_i(c_i)]=U^{\mathcal M}_i(\bar c_i)+\mathbf E_{c}\big[A^{\mathcal M}_i(c)\,F_i(c_i)/f_i(c_i)\big]$.
6. Pointwise comparison. At cost vector $c$ and realized reduction vector $t$, $\sum_i A^{\mathrm{BAI}}_i(c) F_1(c_i)/f_1(c_i)=\min_i F_1(c_i)/f_1(c_i)\le\sum_i A^{\mathrm{BIA}}_i(c,t) F_1(c_i)/f_1(c_i)$ almost everywhere, with $\sum_iA^{\mathcal M}_i=1$.

Significance

The theorem identifies a win-win procurement design. With symmetric suppliers, a buyer who chooses the cheaper of BAI and BIA weakly lowers her own cost, and this choice never lowers any supplier's ex ante profit. The gain does not come from sharing savings, since the buyer keeps all identified savings. It comes from strategic bidding: under BIA a supplier need not submit the lowest initial bid to win, so price competition at the bid stage softens. The paper's Figure 1 shows the higher BIA bid curves. Theorem 1 is of independent interest: it is an index solution of a capped sequential search problem in which an uninvestigated bid may still win.

The paper proves the result on paper. To our knowledge none of it is machine-checked. A formalization adds three things. It makes the mechanisms precise, including the tie-breaking and the stopping rule that the text leaves partly implicit. It pins down the right inequality: the printed "higher" is not strict, and with a single supplier both mechanisms give the same profit. It also produces reusable components: an envelope-theorem layer for bidding games with an indirect mechanism, and a capped-search index theorem.

Difficulty

The proof of Theorem 2 needs the BIA winning probability only through its total, $\sum_i A^{\mathrm{BIA}}_i=1$. Everything else rests on three technical steps. The first is the envelope formula (A.2) for an indirect mechanism whose allocation $W_i$ has no closed form and need not be continuous in the bid. The usual argument assumes a differentiable direct mechanism and does not apply as stated. The second is the claim that in BAI the lowest-cost supplier wins almost surely. That needs a symmetric equilibrium that is not merely nondecreasing but free of pooling, and this must be derived from the equilibrium conditions. The third is the "by symmetry" step that equates each supplier's ex ante profit with the average over suppliers. It needs both the equilibria and the mechanisms to be invariant under relabelling the suppliers.

Theorem 1(a) is a dynamic program over adaptive policies with a cap and an outside option. A Weitzman-style argument must handle a cap $\bar N$ and suppliers whose index makes investigation worthless ($\tau_i=0$). It cannot simply be imported from Pandora's-box results.

Formalization scope

Suppliers are Fin N with $N\ge1$; all values are real numbers. A single definitions module PreAwardInvest.WinWin.Model contains the following.

• Parameters and assumptions. The parameters, and the standing assumptions of §3.1 (densities with mean zero, nonnegative costs and reductions, footnote 6, $1\le\hat N\le N$, $d\ge0$), with $f>0$ on $(\underline c,\bar c)$ added. Assumptions 1 and 2 are separate predicates.
• Laws. The cost and reduction laws are densities with respect to Lebesgue measure, and their vectors have product laws.
• Policies. A policy reads the bids, the investigated set and the revealed reductions. An admissible policy is nonanticipative and measurable in the reductions, and stopping is final.
• Index policy. It takes $\tau$ as any root of its equation. Ties in the ranking and in both awards are broken by one uniformly random priority order, so that BIA and BAI are symmetric under relabelling. Theorem 1(a) compares policies for bids in $B_i=[0,\bar c_i]$.
• Profits and equilibria. Profits follow (5), with the expectation over $c_{-i}$ taken over the whole cost vector with coordinate $i$ overwritten. Equilibria require measurable strategies into $B_i=[0,\bar c_i]$. Ex ante profit is the expectation of the equilibrium profit, not the Myerson virtual-cost expression.

Several conventions are disclosed hypotheses or corrections. The goal uses $\le$ in place of the printed "higher". The equilibria in the goal are assumed symmetric, and the BAI one nondecreasing (Lemma 1's class). Strict monotonicity is not assumed, because with one supplier the equilibrium bid is the constant $\bar c_1$.

The goal is not trivialized. BAI awards on bids through $\lambda_i=b_i-r_i$ and BIA runs the index policy on bids and revealed reductions. Neither mechanism has "lowest cost wins" built in, which is milestone 6. Ex ante profit is defined from (5), so milestones 4–5 are not definitional. A sorry-free check exhibits a one-supplier instance that satisfies every hypothesis of the goal. In it both ex ante profits equal $1/2$.

Not formalized: Theorem 1(b)–(c), Lemma 1 (existence via Athey 2001), the closed form (4) of $W_i$, the asymmetric results (Propositions 2–4), the buyer-cost comparison (Theorem 3), the optimal mechanism (Theorem 4), and the extensions of §9. Contributions welcome: the envelope theorem for monotone-selection bidding games, measurability of the winning probabilities, and the index policy's optimality.

Selected references

• Q. Chen, D. R. Beil, I. Duenyas, Procurement mechanisms with post-auction pre-award cost-reduction investigations, Operations Research 70(6):3054–3075, 2022. https://doi.org/10.1287/opre.2022.2349 (accepted manuscript: LBS Research Online eprint 2544).
• S. Athey, Single crossing properties and the existence of pure strategy equilibria in games of incomplete information, Econometrica 69(4):861–889, 2001. https://doi.org/10.1111/1468-0262.00223
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• P. Milgrom, I. Segal, Envelope theorems for arbitrary choice sets, Econometrica 70(2):583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• M. L. Weitzman, Optimal search for the best alternative, Econometrica 47(3):641–654, 1979. https://doi.org/10.2307/1910412
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009. https://doi.org/10.1016/C2009-0-22474-3

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