All missions

Motivation

Open Markovian quantum systems with fast and full Hamiltonian control can be reduced to an equivalent control system on the standard simplex modelling the dynamics of the eigenvalues of the density matrix describing the quantum state. We explore this reduced control system for answering questions on reachability and stabilizability with immediate applications to the cooling of Markovian quantum systems. We show that for certain tasks of interest, the control Hamiltonian can be chosen time-independent. -- The reduction picture is an example of dissipative interconversion between equivalence classes of states, where the classes are induced by fast controls.

This mission is the statement-level formalization of Reachability, Coolability, and Stabilizability of Open Markovian Quantum Systems with Fast Unitary Control (arXiv:2308.00561v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

61 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.7: Asymptotic cooling equals constant-Hamiltonian pure-state global attraction (Theorem 4.7: Asymptotic cooling equals constant-Hamiltonian pure-state global attraction, PDF p. 17). 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

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

• Theorem 2.4: Equivalence Theorem: A consistent full statement of Theorem 2.4: Equivalence Theorem (source-ambiguity)
• Proposition 2.6: Lie saturate of the full system: A consistent full statement of Proposition 2.6: Lie saturate of the full system (source-ambiguity)
• Proposition 3.2: Strong stabilization and compensating Hamiltonian: A consistent full statement of Proposition 3.2: Strong stabilization and compensating Hamiltonian (source-ambiguity)
• Proposition 3.5: Eight criteria for viability of a face: A consistent full statement of Proposition 3.5: Eight criteria for viability of a face (source-ambiguity)
• Lemma 4.11: Rank-d global attraction and non-enclosing lazy subspaces: A consistent full statement of Lemma 4.11: Rank-d global attraction and non-enclosing lazy subspaces (source-ambiguity)
• Corollary 4.13: Non-enclosing lazy subspace criterion for direct reachability: A consistent full statement of Corollary 4.13: Non-enclosing lazy subspace criterion for direct reachability (source-ambiguity)
• Proposition 4.19: Direct versus indirect face reachability: A consistent full statement of Proposition 4.19: Direct versus indirect face reachability (source-ambiguity)
• Lemma C.3: Freedom of CP-generator representation: A consistent full statement of Lemma C.3: Freedom of CP-generator representation (source-ambiguity)
• Lemma C.19: Attractive support via Hamiltonian control: A consistent full statement of Lemma C.19: Attractive support via Hamiltonian control (source-ambiguity)
• Unnumbered reduced/full Lie-saturate relations: A consistent full statement of Unnumbered reduced/full Lie-saturate relations (source-ambiguity)
• Unnumbered uniqueness of the Hamiltonian part: A consistent full statement of Unnumbered uniqueness of the Hamiltonian part (source-ambiguity)

Selected references

• Reachability, Coolability, and Stabilizability of Open Markovian Quantum Systems with Fast Unitary Control, arXiv:2308.00561v1, https://arxiv.org/abs/2308.00561v1

Motivation

Operator-sum or Kraus representations for single-mode Bosonic Gaussian channels are developed, and several of their consequences explored. Kraus operators are employed to bring out the manner in which the unphysical matrix transposition map when accompanied by injection of a threshold classical noise becomes a physical channel. The action of the quantum-limited attenuator and amplifier channels as simply scaling maps on suitable quasi-probabilities in phase space is examined in the Kraus picture. Consideration of cumulants is used to examine the issue of fixed points. In the cases of entanglement-breaking channels a description in terms of rank one Kraus operators is shown to emerge quite simply. In contradistinction, it is shown that there is not even one finite rank operator in the entire linear span of Kraus operators of the quantum-limited amplifier or attenuator families, an assertion far stronger than the statement that these are not entanglement breaking channels. A characterization of extremality in terms of Kraus operators, originally due to Choi, is employed to show that all quantum-limited Gaussian channels are extremal. The fact that every noisy Gaussian channel can be realised as product of a pair of quantum-limited channels is used to construct a discrete set of linearly independent Kraus operators for noisy Gaussian channels, including the classical noise channel, and these Kraus operators have a particularly simple structure.

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

What is formalized

34 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §III Eq.(3.11): explicit phase-conjugation Kraus family (§III Eq.(3.11): explicit phase-conjugation Kraus family, 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

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

• Paper headline / §II Eqs.(2.1)–(2.4): vacuum-dilation Kraus construction: vacuum dilation, infinite tensor embedding and nuclear partial trace (hard)
• §II Eqs.(2.5)–(2.10): Hermite generating-function evaluation: normalized Hermite Fock–Schroedinger transform and canonical metaplectic matrix elements (hard)
• §II Eq.(2.7): unrestricted nonsingular M reading: §II Eq.(2.7): unrestricted nonsingular M reading (source-ambiguity)
• Theorem 4: invariant thermal state and attraction: Theorem 4: invariant thermal state and attraction (source-ambiguity)
• Eqs.(3.30)–(3.35): phase-conjugator action on thermal states: thermal density, its exact parameter iteration, and local logarithmic characteristic derivatives (hard)
• Theorem 6: attenuation scales the diagonal weight: distributional diagonal P weight and its connection to the actual B channel and Weyl law (hard)
• §IV finite-support non-invariance sentence: §IV finite-support non-invariance sentence (source-ambiguity)
• Interrupted attenuation: printed large-N coefficient: Interrupted attenuation: printed large-N coefficient (source-ambiguity)
• Eqs.(6.7)–(6.10): A2 generalized measure-and-prepare representation: position spectral measure, normalized Hermite transport and A2 measure-and-prepare map (hard)
• Theorem 12: A2 breaks nonclassicality and entanglement: concrete A2 spectral measure-and-prepare channel (hard)
• §VI fixed-point remark: A2 has no invariant density: concrete A2 channel on all densities with its characteristic law (hard)
• Eqs.(7.1),(7.8): random-displacement representation for B1: actual Weyl displacement Gaussian mixture and its normal-channel convex structure (hard)
• Theorem 13: quantum-limited channels are extremal: convex set of all normal CPTP maps and Gaussian/metaplectic equivalence (hard)
• §VIII remark: D(1) is bistochastic but not random unitary: all probability-measure random-unitary mixtures and a bounded-observable normal extension (hard)
• §I/§VIII: only quantum-limited Gaussian channels are extremal: normal-CPTP convex decompositions and independent Gaussian quantum-limit predicate (hard)
• Table I: full canonical composition table: all sixteen canonical composition classes, including singular A2 and metaplectic equivalence (hard)
• Theorem 14: noisy decomposition and independent discrete Kraus families: noisy canonical Gaussian channels and exact two-factor identification (hard)
• §IX: noisy A2 as a quantum-limited composite: noisy A2 canonical class and mixed continuous/discrete Kraus kernel (hard)
• §IX: apparent B1 factorization obstruction: §IX: apparent B1 factorization obstruction (source-ambiguity)
• Theorem 15: simultaneous diagonality of Kraus effects: Theorem 15: simultaneous diagonality of Kraus effects (source-ambiguity)
• §IX error-correction remark: §IX error-correction remark (source-ambiguity)
• Appendix: general pair composition including Gaussian unitary representatives: Gaussian characteristic action and exact metaplectic representative substitution (hard)
• Appendix Table II: full noncanonical-pair classification: Appendix Table II: full noncanonical-pair classification (source-ambiguity)
• Appendix: effect of noncanonical squeezing on noise: Appendix: effect of noncanonical squeezing on noise (source-ambiguity)
• Gaussian dilation, CP conditions and Holevo classification [11,12,17–21,26,27]: Gaussian dilation, CP conditions and Holevo classification [11,12,17–21,26,27] (source-ambiguity)
• Kraus representation and Stinespring dilation [28–31]: Kraus representation and Stinespring dilation [28–31] (source-ambiguity)
• Entanglement breaking versus rank-one representations [35–37]: Entanglement breaking versus rank-one representations [35–37] (source-ambiguity)
• Ordered quasiprobabilities, Laguerre identities, coherent-state representations [44–49]: Ordered quasiprobabilities, Laguerre identities, coherent-state representations [44–49] (source-ambiguity)
• Amplification destroys Gaussian nonclassicality at κ≥√2 [41–43,57]: Amplification destroys Gaussian nonclassicality at κ≥√2 [41–43,57] (source-ambiguity)
• Choi extremality criterion and proposed infinite-dimensional extension [30,62]: Choi extremality criterion and proposed infinite-dimensional extension [30,62] (source-ambiguity)
• Bistochastic/random-unitary distinction [38,52,64]: Bistochastic/random-unitary distinction [38,52,64] (source-ambiguity)
• Kraus-assisted classical error correction [39,40]: Kraus-assisted classical error correction [39,40] (source-ambiguity)
• Mentioned classical/quantum capacity results [8–16]: Mentioned classical/quantum capacity results [8–16] (source-ambiguity)
• Previously known EB/non-EB Gaussian facts [36,37]: Previously known EB/non-EB Gaussian facts [36,37] (source-ambiguity)
• Mixed-basis Hermite integral evaluations [58,61]: Mixed-basis Hermite integral evaluations [58,61] (source-ambiguity)
• Quantum Zeno effect [55]: Quantum Zeno effect [55] (source-ambiguity)

Selected references

• Operator-sum Representation for Bosonic Gaussian Channels, arXiv:1012.4266v1, https://arxiv.org/abs/1012.4266v1

Motivation

The relative entropy of entanglement $E_R$ is defined as the distance of a multi-partite quantum state from the set of separable states as measured by the quantum relative entropy. We show that this optimisation is always achieved, i.e. any state admits a closest separable state, even in infinite dimensions; also, $E_R$ is everywhere lower semi-continuous. We use this to derive a dual variational expression for $E_R$ in terms of an external supremum instead of infimum. These results, which seem to have gone unnoticed so far, hold not only for the relative entropy of entanglement and its multi-partite generalisations, but also for many other similar resource quantifiers, such as the relative entropy of non-Gaussianity, of non-classicality, of Wigner negativity $\unicode{8212}$ more generally, all relative entropy distances from the sets of states with non-negative $\lambda$-quasi-probability distribution. The crucial hypothesis underpinning all these applications is the weak*-closedness of the cone generated by free states, and for this reason the techniques we develop involve a bouquet of classical results from functional analysis. We complement our analysis by giving explicit and asymptotically tight continuity estimates for $E_R$ and closely related quantities in the presence of an energy constraint.

This mission is the statement-level formalization of Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the theme (arXiv:2105.08091v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness (Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness, PDF p. 7). 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

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

• Theorem 9: dual variational formula for resource relative entropy: support-compressed exponential and log-partition (hard)
• Lemma 11: Gibbs variational formula without faithfulness: log-partition at singular and zero positive trace-class operators (hard)
• Lemma 13: duality for a weak*-compact convex subnormalised set: support-compressed log-partition and extended inner supremum (hard)
• Remark 14: Petz dual formula without faithfulness: nonfaithful Petz log-partition functional (hard)
• Corollary 20: bipartite relative entropy of entanglement: completed bipartite state space, closed-hull separability and log-partition (hard)
• Corollary 22: weak*-closed cones for partition separability: partition-indexed completed tensor products and closed-hull pi-separability (hard)
• Corollary 23: multipartite relative entropy of partition entanglement: multipartite pi-separable distance and log-partition (hard)
• Lemma 24: weak*-closed PPT cone: partial transposition T(H_A tensor H_B) to B(H_A tensor H_B) (hard)
• Corollary 25: relative entropy of NPT entanglement: PPT state space, extended distance and log-partition (hard)
• Lemma 30: photon-number attenuation preserves lambda positivity: concrete Weyl representation, lambda-positive states and number attenuation (hard)
• Corollary 31: weak*-closed lambda-positive cone: lambda-positive cone on the actual m-mode Hilbert space (hard)
• Corollary 32: relative entropy of lambda negativity: lambda-positive distance and support-compressed dual formula (hard)
• Lemma 33 (cited): quantum Darmois–Skitovich characterisation as printed: a corrected quantum Darmois-Skitovich statement and unitary beam splitter (source-ambiguity)
• Lemma 34: weak*-closed cone of Gaussian states: all displaced m-mode Gaussian states as actual trace-class states (hard)
• Corollary 35: attainability and lower semicontinuity of non-Gaussianity: Gaussian-state set, Gaussification and moment-defined entropy identity (hard)
• Unnumbered consequence after Corollary 35: entropy of Gaussification: actual Gaussification on the finite-number-energy state set (hard)
• Unnumbered result (124): finite-local-dimension continuity bounds: six bipartite entanglement measures and tensor-power regularizations (hard)
• Proposition 36: bipartite energy continuity estimates (125),(127): all six resource measures, energy moduli and oscillator specialization (hard)
• Proposition 36: generic-G asymptotic-tightness clause: a valid hypothesis set for generic-G asymptotic tightness (source-ambiguity)
• Remark 37: faithfulness of the bipartite continuity modulus: the source-admissible G and actual generalized-inverse continuity modulus (hard)
• Corollary 38: uniform and asymptotic continuity of six bipartite measures: six bipartite measures on correlated n-copy states and additive energy (hard)
• Unnumbered multipartite entropy upper bounds (149),(150), proved in Appendix C: multipartite marginals and extended local entropy upper bounds (hard)
• Unnumbered result (151): finite-dimensional multipartite continuity: partition separability, one unrestricted final factor and singleton-only regularization (hard)
• Proposition 39: multipartite energy continuity estimates (155)–(157): multipartite energy budgets and the complete three continuity moduli (hard)
• Proposition 39: asymptotic-tightness clause for m=2: partition-restricted large-energy tightness (source-ambiguity)
• Remark 40: faithfulness of multipartite continuity moduli: the actual H[s] entropy capacity and multipartite moduli (hard)
• Corollary 41: uniform and asymptotic multipartite continuity: grouped multipartite copies, additive local energies and partition measures (hard)
• Lemma 43: infinite-dimensional Lieb three-operator inequality: support-compressed exponential of log A+log B-log C (hard)
• Lemma 44: countably decomposable separable approximation to a pure state: actual countable pure-product mixture with all prescribed marginals (hard)

Selected references

• Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the theme, arXiv:2105.08091v3, https://arxiv.org/abs/2105.08091v3

Motivation

We extend the definition of the conditional min-entropy from bipartite quantum states to bipartite quantum channels. We show that many of the properties of the conditional min-entropy carry over to the extended version, including an operational interpretation as a guessing probability when one of the subsystems is classical. We then show that the extended conditional min-entropy can be used to fully characterize when two bipartite quantum channels are related to each other via a superchannel (also known as supermap or a comb) that is acting on one of the subsystems. This relation is a pre-order that extends the definition of "quantum majorization" from bipartite states to bipartite channels, and can also be characterized with semidefinite programming. As a special case, our characterization provides necessary and sufficient conditions for when a set of quantum channels is related to another set of channels via a single superchannel. We discuss the applications of our results to channel discrimination, and to resource theories of quantum processes. Along the way we study channel divergences, entropy functions of quantum channels, and noise models of superchannels, including random unitary superchannels, and doubly-stochastic superchannels. For the latter we give a physical meaning as being completely-uniformity preserving.

This mission is the statement-level formalization of Comparison of Quantum Channels by Superchannels (arXiv:1808.02607v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majorization of channels by all paired entropy tests (Theorem 7, continued p.19, PDF p. 18). 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

• Comparison of Quantum Channels by Superchannels, arXiv:1808.02607v3, https://arxiv.org/abs/1808.02607v3

Motivation

Sharing-economy platforms (ride-sharing, car-sharing, peer-to-peer lending) sit between two groups. They charge consumers a price and pay self-scheduling workers a wage, and they compete with rival platforms on both sides at once. How a platform pays its workers is a design choice that varies across the industry: some announce a fixed wage per job, some a fixed commission rate on the consumer price, and some, as Uber did in its "upfront pricing" experiments, set prices and wages job by job. Drivers and regulators have argued over these schemes, and whether the choice matters for the platforms' own profits is a question in its own right.

Zhang, Chen and Raghunathan (SSRN 3555993, published in Management Science, 2022) answer it in a parsimonious duopoly model with linear demand and supply. Their main comparison, Proposition 3, shows that every scheme can be the most profitable one. Which one wins depends on whether consumers or workers switch more readily between the platforms. Many two-sided platform models, for example ones in which supply does not respond to the rival's wage, find no such reversal.

Setting

Two platforms $i \in \{1,2\}$, with $\bar i = 3-i$, charge consumer prices $p_i$ and pay wages $w_i$ per transaction. Six parameters $a, b, c, k, l, m > 0$ define

$$d_i = a - b(p_i - p_{\bar i}) - c\,p_i, \qquad s_i = -k + l(w_i - w_{\bar i}) + m\,w_i,$$

the demand and the worker supply of platform $i$. Here $b$ measures how readily consumers switch platforms, $c$ the price sensitivity of loyal consumers, $l$ how readily workers switch, and $m$ the wage sensitivity of loyal workers. A transaction needs both a consumer and a worker, so the transaction volume is $\max\{0,\min\{d_i,s_i\}\}$ and the profit is

$$\pi_i = (p_i - w_i)\,\max\{0,\min\{d_i, s_i\}\}.$$

The standing assumptions are Assumption 1, $a/c > k/m$, and Assumption 2, $l \le 2c + c^2/b$.

Three wage schemes define three games:

1. DCR (dynamic commission rate). The platforms simultaneously choose a price $p_i$ and a commission rate $\alpha_i$. The wage is $w_i = (1-\alpha_i)p_i$, so profit is $\alpha_i p_i \max\{0,\min\{d_i,s_i\}\}$.
2. FCR (fixed commission rate). The platforms first announce commission rates $\alpha_i$, then, having observed both, set prices.
3. FW (fixed wage). The platforms first announce wages $w_i$, then set prices.

DCR is solved by Nash equilibrium. FCR and FW are solved by subgame-perfect equilibrium: a stage-2 price rule must give a Nash equilibrium of the pricing game after every pair of stage-1 announcements, and no stage-1 announcement may be improved on. The paper studies symmetric equilibria with positive demand and supply. Write $\pi^{D*}, \pi^{F*}, \pi^{W*}$ for the resulting platform profits.

Formalization targets

Goal: Proposition 3

Write $\alpha^{D*}$ for the DCR equilibrium commission rate and

$$Q = \frac{b+c+l+m}{(b+c)(l+m)\alpha^{D*}} - \frac{b + (1-\alpha^{D*})l}{(1-\alpha^{D*})(cl-bm)}$$

for the left side of the paper's Inequality (13). For every symmetric equilibrium of each game with positive demand and supply:

$$\begin{aligned} &\text{(a)}\ \ \tfrac{b}{c} > \tfrac{l}{m} &&\Longrightarrow\ \pi^{W*} > \pi^{F*} > \pi^{D*},\\ &\text{(b)}\ \ \tfrac{b}{c} < \tfrac{l}{m},\ Q > 0 &&\Longrightarrow\ \pi^{F*} > \pi^{D*} > \pi^{W*},\\ &\text{(c)}\ \ \tfrac{b}{c} < \tfrac{l}{m},\ Q < 0 &&\Longrightarrow\ \pi^{D*} > \pi^{F*} > \pi^{W*}. \end{aligned}$$

The goal is stated about the equilibria of the three games, not about the closed-form prices.

Milestones

• Lemma 1 (p. 10): the DCR game has exactly one symmetric equilibrium with positive demand and supply, given by the closed forms (4) and (5), and $0 < \alpha^{D*} < 1$.
• Lemma 2 (p. 11): the FCR equilibrium commission rate is the unique zero in $(\bar\alpha, 1)$ of the quadratic $f$ of (44), equivalently the solution of (6). The price is $(a+k)/(c + m(1-\alpha^*))$, (7).
• Lemma 3 (p. 12): the FW equilibrium wage and price are (8) and (9).
• Profit increases in price (A.8, p. 52): with demand equal to supply, profit is a concave quadratic in the equilibrium price. All three equilibrium prices lie on its increasing branch.
• Three price comparisons (A.8, pp. 52–53):
  • $p^{W*} - p^{D*}$ has the sign of $bm - cl$;
  • $\alpha^{D*} < \alpha^{F*}$ if and only if (13) holds;
  • $\alpha^{W*} < \alpha^{F*}$ if and only if $cl > bm$.

Significance

Proposition 3 makes the choice of wage scheme a substantive strategic variable. The fixed-wage scheme is either the best or the worst for the platforms, and the fixed-commission scheme is never the worst. The ranking of profits equals the ranking of equilibrium prices and reverses that of wages. The paper's welfare results (Propositions 4 and 5) build on it, since consumer and worker surplus orderings are read off the same price ranking.

Formalizing it adds three things:

• A checked equilibrium analysis. The appendix's equilibrium analysis is partly written out and partly asserted ("we can verify that neither platform has incentive to deviate").
• Corrected statements. The printed comparisons contain slips; see Formalization scope.
• A model for later work. The definitions give a reusable formal model of two-stage price competition with endogenous two-sided supply.

The result is proved in the paper; nothing in it has been machine-checked.

Difficulty

The comparison itself, once the equilibria are known, is rational-function algebra. The difficulty is the equilibrium characterizations.

• The payoff is kinked. Profit is a product of a margin and a minimum of demand and supply, so each best response must be analysed region by region: supply exceeding demand, matching it, or falling short.
• FCR and FW need the whole subgame. Their stage-2 pricing games must be solved after every pair of announcements, including off-path pairs in which a rival's supply is non-positive.
• Local optimality is not enough. The obvious argument, setting the derivative of the stage-1 profit to zero along the matched-supply branch, gives only a necessary condition. Existence needs global deviations ruled out, in particular a platform raising its wage enough that its own supply exceeds demand. That is exactly where Assumption 2 enters.

Formalization scope

• Parameters. All six parameters are reals and strictly positive ($\mathbb R^+$ read as $>0$). Assumptions 1 and 2 are bundled in Params.Standing.
• Strategies.
  • Actions range over all of $\mathbb R$: prices, commission rates and wages alike. No bound such as $0 \le \alpha \le 1$ is imposed.
  • DCR actions are pairs (price, commission rate).
  • A two-stage profile is a pair of stage-1 actions together with stage-2 price rules $P_i : \mathbb R^2 \to \mathbb R$. "Symmetric" means equal stage-1 actions and equal on-path prices; off-path play is unrestricted.
• Truncated volume. The paper writes the volume as $\min\{d_i,s_i\}$. With negative values allowed, the profit is unbounded above and no equilibrium exists, so the formalization uses $\max\{0,\min\{d_i,s_i\}\}$.
• Non-trivial equilibria. Equilibria are required to have positive demand and supply on the path (p. 9). Zero-volume symmetric equilibria exist and are excluded.
• Continuity on the path. Two-stage equilibria are required to have stage-2 price rules continuous at the equilibrium stage-1 pair. The appendix presupposes this when it differentiates the subgame prices in the stage-1 actions. It is necessary: without it, zero-profit equilibria of nearby pricing subgames can punish every deviation, and other FCR commission rates become subgame-perfect outcomes.
• Corrections to the printed statements.
  • Case (c). It is stated with "$Q < 0$" where the paper says "(13) does not hold". At $Q = 0$ the DCR and FCR outcomes coincide and the strict ranking fails.
  • $\alpha^{W*}$. It is defined as $1 - w^{W*}/p^{W*}$, because the appendix's displayed closed form has the sign of $k$ reversed.
  • Denominators. Real divisions occur in (6) and (13), and their denominators are carried or proved nonzero.

A formalization that compares only the closed-form prices, or uses the literal untruncated payoff (which makes every statement about equilibria vacuous), is not this mission.

• Contributions welcome:
  • best-response lemmas for the kinked profit;
  • existence of pricing equilibria in every subgame;
  • the global no-deviation arguments behind Lemmas 2 and 3;
  • the algebra of the price comparisons.

Selected references

• C. Zhang, J. Chen, S. Raghunathan, Two-Sided Platform Competition in a Sharing Economy, SSRN working paper 3555993; published in Management Science, 2022. https://ssrn.com/abstract=3555993, https://doi.org/10.1287/mnsc.2022.4302
• D. M. Kreps, J. A. Scheinkman, Quantity Precommitment and Bertrand Competition Yield Cournot Outcomes, Bell Journal of Economics 14(2), 1983. https://doi.org/10.2307/3003636
• S. C. Choi, Price Competition in a Channel Structure with a Common Retailer, Marketing Science 10(4), 271–296, 1991, the source the paper cites for its linear demand model (p. 7). https://doi.org/10.1287/mksc.10.4.271

Why decoding good quantum LDPC codes matters

Quantum computers must correct errors faster than they accumulate, and quantum low-density parity-check (LDPC) codes are the leading candidates for doing so with little overhead: every check involves a bounded number of qubits, so syndromes can be measured by local circuits. In 2021–2022 the first asymptotically good quantum LDPC codes appeared, with dimension and minimum distance both linear in the code length $n$: the expander lifted product codes of Panteleev and Kalachev (arXiv:2111.03654) and the quantum Tanner codes of Leverrier and Zémor (arXiv:2202.13641). A code is only useful if errors can be corrected efficiently. Leverrier and Zémor (arXiv:2208.05537) give two decoders for quantum Tanner codes that correct every error of weight up to a constant fraction of $n$: a sequential one running in linear time, and a parallel decoder running in a logarithmic number of rounds of local updates. This mission is about the parallel decoder.

Timeline:

• 2021, Panteleev–Kalachev: asymptotically good quantum LDPC codes and locally testable classical codes (arXiv:2111.03654).
• 2022, Leverrier–Zémor: quantum Tanner codes, a simpler construction on left-right Cayley complexes (arXiv:2202.13641).
• 2022, Gu–Pattison–Tang, Leverrier–Zémor and Dinur–Hsieh–Lin–Vidick: efficient decoders for linear-distance quantum LDPC codes (arXiv:2206.06557, arXiv:2206.07571, arXiv:2206.07750).
• 2022, Leverrier–Zémor, Decoding quantum Tanner codes: sequential and parallel decoders up to a constant fraction of $n$, with a revised parallel analysis in v3 (arXiv:2208.05537v3).

The code and the decoder

Let $G$ be a finite group and $A=A^{-1}$, $B=B^{-1}\subseteq G$ with $|A|=|B|=\Delta$. The quadripartite left-right Cayley complex has four copies of $G$ as vertices, $V_{ij}=G\times\{ij\}$, and one square $\{(g,00),(ag,01),(gb,10),(agb,11)\}$ for every $(g,a,b)\in G\times A\times B$. The set of squares $Q$ has $n=|G|\Delta^2$ elements, and every vertex $v$ sees its $Q$-neighbourhood $Q(v)$ as an $A\times B$ array: columns are indexed by $b$, rows by $a$. The left Cayley graph $\mathrm{Cay}(G,A)$ and the right Cayley graph $\mathrm{Cay}(G,B)$ are assumed to be non-bipartite Ramanujan graphs: every adjacency eigenvalue other than $\pm\Delta$ has absolute value at most $2\sqrt{\Delta-1}$.

Two local codes $C_A\subseteq\mathbb F_2^A$, $C_B\subseteq\mathbb F_2^B$ with $\dim C_A+\dim C_B=\Delta$ are fixed. Write $V_0=V_{00}\cup V_{11}$ and $V_1=V_{01}\cup V_{10}$. The code $\mathcal C_1\subseteq\mathbb F_2^Q$ consists of the vectors whose view on every $Q(v)$, $v\in V_1$, lies in the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$: every local view is a sum of a word whose columns are in $C_A$ and a word whose rows are in $C_B$. $\mathcal C_0$ is defined in the same way on $V_0$ with $C_A^\perp$, $C_B^\perp$. The local codes and their duals have distance at least $\delta\Delta$. Both dual tensor codes are $\kappa$-product-expanding: every codeword $x$ splits as $x=c+r$ with $|x|\ge\kappa\Delta(\|c\|+\|r\|)$, where $\|c\|$ counts non-zero columns and $\|r\|$ non-zero rows.

A $\sigma_x$-type error $e\in\mathbb F_2^Q$ is decoded in three phases. In the preprocessing phase every $v\in V_1$ chooses a minimum-weight local error $\varepsilon_v$ with the local syndrome of $e$; the mismatch is $Z=\sum_{v\in V_1}\varepsilon_v$. The mismatch decomposition writes $Z=\hat C_0+\hat R_0+\hat C_1+\hat R_1$, with $\hat C_j$ a sum of $C_A$-columns and $\hat R_i$ a sum of $C_B$-rows. Postprocessing outputs $\hat e=\sum_{v\in V_{10}}\varepsilon_v+\hat C_0+\hat R_1$. The parallel decoder (Algorithm 3) runs rounds of four substeps, one for each of $V_{00},V_{01},V_{10},V_{11}$. In a substep, every vertex $v$ of the current class simultaneously looks for a non-zero local dual tensor codeword $x_v$ on $Q(v)$ with $|\hat Z|-|\hat Z+x_v|\ge|x_v|/2$, picks one of maximum weight, splits it as $c_v+r_v$ with $\|c_v\|+\|r_v\|$ minimal, and updates $\hat C_j$, $\hat R_i$ and $\hat Z$.

Formalization targets

Goal: Theorem 20 (= Theorem 3)

Fix $\varepsilon\in(0,1/6)$ and $\delta,\kappa>0$. For all $\Delta$ large enough, every error with

$$|e|<\frac1{2^{12}}\min\Big(\frac{\varepsilon^3}{16},\frac\kappa4\Big)\delta^2\kappa^2\frac n\Delta$$

is corrected by every run of the parallel decoder. With $\theta=\frac14\big(\frac14-\frac32\varepsilon\big)$, each round satisfies $|\hat Z_{k+1}|\le(1-\theta)|\hat Z_k|$, so $\hat Z_k=0$ once $(1-\theta)^k\cdot4|e|<1$, and then $e+\hat e$ lies in the span $\mathcal C_0^\perp$ of the $\sigma_x$-generators.

Milestones

• Lemma 4 (expander mixing) and Lemma 5: $\lambda(\mathcal G^\square_0),\lambda(\mathcal G^\square_1)\le4\Delta$.
• Lemmas 7, 10, 11, 8 and Theorem 9: the minimum distance, $d_{\min}\ge\delta^2\kappa^2n/(1024\Delta)$.
• Lemmas 14, 15, 16 and Theorem 12: if a minimum decomposition of a non-zero mismatch has few active vertices, some local codeword lowers $|Z|$ by $(1-\varepsilon)|x_v|$.
• Lemma 17: $|Z|\le4|e|$ and $\|Z\|\le4|e|/(\kappa\Delta)$.
• Lemma 19: below $2^{-16}\varepsilon^3\kappa^2\delta^2n/\Delta$, sequential decoding with parameter $1/2$ never stalls, and switching to $\varepsilon$ still converges.
• Lemma 18: if the $\varepsilon$-sequential decoder converges, one parallel round removes at least $\theta|Z|$.

Significance

The theorem shows that asymptotically good quantum LDPC codes can be decoded against adversarial errors of linear weight by $O(\log n)$ rounds of local computation, each vertex acting only on its own $Q$-neighbourhood. This matters for fault tolerance, where decoding latency is a bottleneck. The milestones carry independent value. Theorem 9 is a linear minimum distance bound for quantum Tanner codes in the quadripartite setting. Theorem 12 is the local-to-global "weight reduction" principle on which both decoders rest. Lemmas 4–5 are spectral facts about Cayley graphs and square complexes that are reusable for any expander-based code.

The paper's results are proved, not open; none has been machine-checked. The sequential decoder's correctness (Theorem 13) is posed separately on the platform as an open goal in the mission Decoding quantum Tanner codes (Leverrier, Zemor), which shares this mission's published definitions; this mission does not restate it. Formalizing the present chain would give a complete, checked proof that a parallel decoder exists for good quantum LDPC codes, and would expose the constants. Two printed constants are corrected here (see the scope section), and sharper constants or simpler arguments are welcome.

Difficulty

The obvious argument is to bound the mismatch and its norm, apply Theorem 12 repeatedly, and let all vertices of a class flip at once. That argument fails because parallel flips are not sequential flips. A vertex's best local move against the mismatch at its turn need not be the move a converging sequential run would make, and a round could stall even though a sequential run never does. Lemma 18 resolves this with a virtual sequential run, a partition of its increments into "good" and "bad" ones (Claim 1), and the maximum-weight rule at every vertex. Without that rule the lemma is false. Theorem 12 itself is a counting contradiction. It uses robustness, the expander mixing lemma twice, and two notions of "exceptional" vertices, and it needs $\Delta$ large. Theorem 9 needs the coset-minimization of Lemma 7 before the same counting can start.

Formalization scope

The development builds on the published layers QAlgorithms_Defs_TensorCode and QAlgorithms_Defs_TannerDecoder. These define the complex, $\varphi_v$, $\mathcal C_0$, $\mathcal C_1$, the $\sigma_x$ span, minimum local corrections, the mismatch, Algorithm 2 and the output $\hat e$. The conventions are:

• A vertex $(g,ij)$ is (g, (i, j)) : G × (Bool × Bool), squares are G × A × B, and weights are hammingNorm cast to ℝ.
• One new definitions file holds Algorithm 3 (admissible move, parallel choice, substep, round, run), decompositions and their norm, active, exceptional and ordinary vertices, the clustering sets $T$, stalled and converging sequential decoders, $\mathcal C_1^\perp$, and the square graphs $\mathcal G^\square_k$.
• "$\Delta$ large enough" is $\exists\Delta_0\,\forall\Delta\ge\Delta_0$, with $\Delta_0$ depending only on the constants fixed before it.
• Only $\sigma_x$-type errors are treated; the $\sigma_z$ case is symmetric.
• Non-bipartiteness of the Cayley graphs (the standing choice of p. 10) is assumed wherever spectral bounds are used.
• Theorem 12 assumes $Z\ne0$ and asks for a non-zero $x_v$.

Corrected constants. Theorem 9 is stated with $1024$ instead of the printed $256$, because Lemma 8 and the proof's $|x|\ge\frac{\kappa\Delta}2\|x\|$ give $1024$. The goal's error bound uses $\min(\varepsilon^3/16,\kappa/4)$ instead of $\min(\varepsilon^3/16,\kappa)$, which is what the corrected distance supports. Both corrected statements are weaker than the printed ones.

No trivialization. Every vertex must flip a maximum-weight admissible move whenever one exists, and runs range over all such choices. "Logarithmic time" is the per-round contraction factor, not mere eventual termination. Validity is membership of $e+\hat e$ in the $\sigma_x$-generator span, with $\hat e$ the paper's postprocessing output. A formalization that lets vertices idle, drops the maximum-weight rule, or proves only eventual termination does not prove this theorem.

Needed and reusable infrastructure:

• spectral graph theory for regular multigraphs (expander mixing, eigenvalues of commuting Cayley adjacencies);
• product expansion and local minimality of decompositions;
• the combinatorics of the left-right complex (shared rows and columns).

Contributions proving the graph lemmas or Lemma 18, whose proof is pure counting, are especially welcome.

Selected references

• A. Leverrier, G. Zémor, Decoding quantum Tanner codes, IEEE Transactions on Information Theory; arXiv:2208.05537v3, 2022. https://arxiv.org/abs/2208.05537
• A. Leverrier, G. Zémor, Quantum Tanner codes, FOCS 2022; arXiv:2202.13641. https://arxiv.org/abs/2202.13641
• P. Panteleev, G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022; arXiv:2111.03654. https://arxiv.org/abs/2111.03654
• S. Gu, C. A. Pattison, E. Tang, An efficient decoder for a linear distance quantum LDPC code, STOC 2023; arXiv:2206.06557. https://arxiv.org/abs/2206.06557
• A. Leverrier, G. Zémor, Efficient decoding up to a constant fraction of the code length for asymptotically good quantum codes, SODA 2023; arXiv:2206.07571. https://arxiv.org/abs/2206.07571
• I. Dinur, M.-H. Hsieh, T.-C. Lin, T. Vidick, Good quantum LDPC codes with linear time decoders, arXiv:2206.07750, 2022. https://arxiv.org/abs/2206.07750
• G. Kalachev, P. Panteleev, Two-sided robustly testable codes, arXiv:2206.09973, 2022. https://arxiv.org/abs/2206.09973

Motivation

High-dimensional statistical learning (HDSL) fits a model with $p$ parameters from $n$ samples when $p$ may far exceed $n$. The standard guarantees for sparse estimators, such as the Lasso, rest on restricted strong convexity (RSC) or restricted eigenvalue conditions on the empirical risk (Negahban et al., 2012; Loh & Wainwright, 2015). These conditions fail or are hard to verify for many losses that matter in operations research and machine learning: nonsmooth losses, losses of neural networks, and M-estimation problems whose population risk is not strongly convex near any sparse vector.

Liu, Ye and Lee (arXiv:1903.00616v2; Operations Research, 2022) remove RSC entirely. They regularize the empirical risk with a folded concave penalty, the minimax concave penalty (MCP) of Zhang (2010), and analyse not a global minimizer (intractable, since the problem is nonconvex) but any point satisfying a weak second-order stationarity condition. They also replace exact sparsity by approximate sparsity: the best sparse vector need only be $\varepsilon_A$-optimal for the population risk. Their main result, Theorem 1, gives an excess-risk bound whose sample complexity is poly-logarithmic in $p$.

Setting

Observations $Z_1, \dots, Z_n$ are i.i.d. copies of a random element $Z$ of a measurable space $\mathcal W$. A loss $L(\beta, z)$, with parameter $\beta \in \mathbb R^p$, defines the population risk $\mathbb L(\beta) = \mathbb E[L(\beta, Z)]$, assumed finite for every $\beta$ and bounded below, the empirical risk $\mathcal L_n(\beta) = \frac1n\sum_i L(\beta, Z_i)$, and the regularized objective

$$\mathcal L_{n,\lambda}(\beta) = \mathcal L_n(\beta) + \sum_{j=1}^p P_\lambda(|\beta_j|), \qquad P_\lambda(\theta) = \int_0^\theta \frac{[a\lambda - t]_+}{a}\,dt,$$

with tuning parameters $a, \lambda > 0$. Norms: $\|\cdot\|$ is Euclidean, $|\cdot|$ is $\ell_1$, $\|\cdot\|_\infty$ is the max norm and $\|\cdot\|_0$ counts nonzero entries.

The standing assumptions are:

• smoothness (11): each partial derivative $\partial L/\partial\beta_j$ is $U_L$-Lipschitz along coordinate $j$, for almost every $z$;
• Assumption 3: the centred losses $L(\beta, Z_i) - \mathbb E L(\beta, Z_i)$ are sub-exponential with $\psi_1$-norm at most $\sigma \ge 1$ on the box $\|\beta\|_\infty \le R$;
• Assumption 4: $L(\cdot, z)$ is $\mathcal C(z)$-Lipschitz on the box, where $\mathcal C(Z_i)$ is sub-exponential around its mean ($\psi_1$-norm at most $\sigma_L \ge 1$) and $\mathbb E\,\mathcal C(Z_i) \le \mathcal C_\mu$, $\mathcal C_\mu \ge 1$;
• Assumption 1 (A-sparsity): some $\beta^*_{\varepsilon_A}$ with $\|\beta^*_{\varepsilon_A}\|_\infty \le R$, $R \ge 1$, and $s = \|\beta^*_{\varepsilon_A}\|_0 > 1$ nonzero entries satisfies $\mathbb L(\beta^*_{\varepsilon_A}) - \inf_\beta \mathbb L(\beta) \le \varepsilon_A$. Assumption 2 replaces $\inf_\beta \mathbb L$ by any lower bound $L^*_g$.

A vector $\hat\beta$ satisfies the S³ONC (significant subspace second-order necessary conditions, Definition 1) at a sample if it is a KKT point of $\mathcal L_{n,\lambda}$, with subgradients $\kappa_j \in \partial|\hat\beta_j|$, and $U_L + P''_\lambda(|\hat\beta_j|) \ge 0$ whenever $|\hat\beta_j| \in (0, a\lambda)$. With $\tilde\zeta = \ln(3eR(\sigma_L + \mathcal C_\mu))$, Theorem 1 fixes $\lambda = \sqrt{8\sigma/(c a n^{2/3})\,[\ln(n^{2/3}p) + \tilde\zeta]}$, where $c \in (0, 1/2]$ is the constant of the Bernstein inequality (12).

Formalization targets

Goal: Theorem 1 (p. 18)

For $a < \min\{1/U_L, 1\}$ and any random $\hat\beta$ with $\|\hat\beta\|_\infty \le R$ satisfying the S³ONC almost surely:

(i) if $\mathcal L_{n,\lambda}(\hat\beta) \le \mathcal L_{n,\lambda}(\beta^*_{\varepsilon_A}) + \Gamma$ almost surely and $n > C_3[((\Gamma + \varepsilon_A)/\sigma)^3 + s(\ln(np) + \tilde\zeta)]$, then with probability at least $1 - 2(p+1)e^{-n/C_3} - 6e^{-n^{1/3}/C_3}$,

$$\mathbb L(\hat\beta) - \inf_\beta \mathbb L(\beta) \le C_3\sigma\Big[\frac{s(\ln(np)+\tilde\zeta)}{n^{2/3}} + \sqrt{\frac{s(\ln(np)+\tilde\zeta)}{n}} + \frac{1}{n^{1/3}}\Big] + C_3\sqrt{\frac{\sigma(\Gamma+\varepsilon_A)}{n^{1/3}}} + \Gamma + \varepsilon_A;$$

(ii) if $\hat\beta$ is no worse in $\mathcal L_{n,\lambda}$ than a Lasso solution $\hat\beta^{\ell_1}$, the $\Gamma$-free bound (22) holds under (21).

$C_3, C_4$ are universal constants. The goal fixes the polynomial rate $n^{-1/3}$; the general-rate result is Proposition 1.

Milestones (the paper's proof chain)

1. Proposition 2: the S³ONC forces $|\hat\beta_j| \notin (0, a\lambda)$ almost surely.
2. Lemma EC.1: the empirical risk is $(2\sigma_L + \mathcal C_\mu)$-Lipschitz on the box with high probability.
3. Proposition 3: uniform deviation of $\mathcal L_n$ from $\mathbb L$ over $\{\|\beta\|_\infty \le R, \|\beta\|_0 \le p'\}$.
4. Proposition 4: $\|\hat\beta\|_0 \le p'_u - 1$ with high probability.
5. Lemma EC.2: comparison of the Lasso solution with $\beta^*_{\varepsilon_A}$ in $\mathcal L_{n,\lambda}$.
6. Proposition 5: the joint sparsity and excess-risk events for general $\varrho \in (0, 1/2)$.
7. Proposition 1: the excess-risk bounds (16), (18) at S³ONC solutions for general $\varrho$.

Significance

The theorem shows that second-order stationarity, which first- and second-order methods can certify (the paper's Theorem 2 gives a pseudo-polynomial algorithm), suffices for poly-logarithmic sample complexity in $p$ without convexity or RSC. The paper builds on it for nonsmooth losses through smoothing (Theorem 3) and for regularized neural networks (Theorem 4). The same definitions layer (MCP, S³ONC, A-sparsity) serves those results.

The result is proved on paper, in the electronic companion of the cited preprint. Nothing of it is formalized: the platform has no folded concave penalty, no S³ONC and no excess-risk bound for sparse M-estimation without RSC. This mission provides the definitions, the goal and the proof chain as stated by the authors, with two disclosed adjustments (see Formalization scope).

Difficulty

The obvious argument bounds $\mathcal L_n(\hat\beta) - \mathbb L(\hat\beta)$ uniformly over the box $\|\beta\|_\infty \le R$ and then compares $\hat\beta$ with $\beta^*_{\varepsilon_A}$. It fails: a covering of a $p$-dimensional box costs a factor $p$, not $\ln p$, in the sample size. The usual repair, RSC, which localizes the estimator near a sparse target, is exactly what the paper does without. $\hat\beta$ is moreover only a stationary point of a nonconvex objective, not a minimizer, so no optimality inequality over the whole space is available. The probabilistic part requires keeping the constants consistent across several union bounds and two Bernstein inequalities, with failure probabilities that must stay summable in the sparsity level. In Lean, an additional obstacle is that suprema over uncountable sparse sets are not obviously measurable.

Formalization scope

• Data: an abstract measurable space $\mathcal W$ (its embedding in $\mathbb R^q$ plays no role), independent $Z_i$ with common law $\mu$. $L(\beta, \cdot)$ is measurable and $\mu$-integrable for every $\beta$, and $\mathbb L$ is bounded below, so $\inf_\beta \mathbb L(\beta)$ is a genuine infimum.
• Norms: the Euclidean norm is written out (Mathlib's norm on Fin p → ℝ is the sup norm). $\|\cdot\|_{\psi_1}$ is the published Orlicz norm HighDimProb.Concentration.subexponentialNorm, always together with an explicit witness of sub-exponentiality. The paper cites the equivalent moment form; the difference is absorbed by the universal constants.
• Bernstein constant: (12) and the analogous bound for $\mathcal C(Z_i)$ used in Lemma EC.1 are hypotheses with their constant $c$, quantified first. Every universal constant ($C_1$–$C_4$, $\tilde c$) comes after $c$ and before every problem object: $p$, $n$, the distribution, $L$, $\hat\beta$, $\Gamma$. Remark 1 asserts that such a $c \in (0, 1/2]$ exists; the platform's proved bernstein_weighted supplies one.
• Derivatives: the gradient enters through coordinate partial derivatives, which is all (11), (13), (14) use. $P'_\lambda, P''_\lambda$ are derivatives of the literal integral (4).
• Probabilities: "with probability at least $1-\delta$" is an upper bound $\delta$ on the outer measure of the failure set.
• Random vectors: $\hat\beta$ and $\hat\beta^{\ell_1}$ are arbitrary measurable maps with the stated almost-sure properties; no statement constructs them.
• Corrections: $a < 1$ is added to Theorem 1 and Proposition 1. It is Proposition 5's hypothesis, which their printed proofs invoke. Proposition 4's $\zeta_1(\epsilon)$ prints $\sigma_C$, and $\sigma_L$ is meant. Theorem 1's $\lambda$ is kept as printed ($\ln(n^{2/3}p)$), although Proposition 1 at $\varrho = 1/3$ uses $\ln(n^{1/3}p)$.

The trivializing formalizations are ruled out explicitly: constants chosen after the instance, junk values of non-integrable expectations, empty infima or undefined derivatives, the sup norm in place of the Euclidean norm, and an estimator chosen by the theorem.

Welcome contributions: proofs of the milestones in order; a Lean proof that Assumption 3 implies (12), via the published Bernstein inequality; a measurable-selection or outer-measure lemma for suprema over sparse boxes, which is reusable across high-dimensional statistics.

Selected references

• H. Liu, Y. Ye, H. Y. Lee, High-dimensional learning under approximate sparsity with applications to nonsmooth estimation and regularized neural networks, Operations Research, 2022; preprint arXiv:1903.00616v2, 2021. https://arxiv.org/abs/1903.00616
• C.-H. Zhang, Nearly unbiased variable selection under minimax concave penalty, Annals of Statistics 38(2), 2010. https://arxiv.org/abs/1002.4734
• J. Fan, R. Li, Variable selection via nonconcave penalized likelihood and its oracle properties, Journal of the American Statistical Association 96, 2001. https://doi.org/10.1198/016214501753382273
• S. N. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, Statistical Science 27(4), 2012. https://arxiv.org/abs/1010.2731
• P.-L. Loh, M. J. Wainwright, Regularized M-estimators with nonconvexity: statistical and algorithmic theory for local optima, Journal of Machine Learning Research 16, 2015. https://arxiv.org/abs/1305.2436
• R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027

Motivation

Call centers, hospital wards and other service systems with many agents serve several customer classes, and customers who wait too long hang up or leave. The standard model is the multiclass many-server queue with reneging: $N$ identical servers, $J$ classes, class-dependent service-time and patience-time distributions, and a control policy that decides when an idle server takes a customer and from which class. Exact analysis is out of reach once service and patience times are not exponential, so performance is studied through fluid limits: the limit of the system scaled by $1/N$ as $N\to\infty$.

A. L. Puha and A. R. Ward (MOR 2022, doi:10.1287/moor.2021.1166) prove such a limit theorem for general service and patience distributions, batch arrivals and an arbitrary admissible head-of-the-line policy, including policies that idle or randomize. Earlier results covered one class without reneging (Kaspi and Ramanan, Ann. Appl. Probab. 2011), one class with reneging and unit arrivals (Kang and Ramanan, Ann. Appl. Probab. 2010), and static priority policies (Atar, Kaspi and Shimkin, Math. Oper. Res. 2014).

Setting

Fix $J\ge1$ classes. Class $j$ has a service-time distribution $G^s_j$ on $\mathbb R_+$ with density $g^s_j$, and a patience-time distribution $G^r_j$ on $[0,\infty]$ with density $g^r_j$ on $\mathbb R_+$, so a customer may never abandon. For a distribution $G$ with density $g$, $H=\sup\{x:G(x)<1\}$ is the right edge of its support and $h=g/(1-G)$ on $[0,H)$ is its hazard function.

In the $N$-th queue, class-$j$ customers arrive by a counting process $E^N_j$ that may jump by more than one. The state is $(\alpha^N,X^N,\nu^N,\eta^N)$: $X^N_j$ counts class-$j$ customers in system; $\nu^N_j$ is the age-in-service measure, a unit atom at the service age of each class-$j$ customer in service; and $\eta^N_j$ is the potential-queue measure, a unit atom at the time in system of each class-$j$ customer whose patience has not run out. The control enters only through the entry-into-service times. A head-of-the-line (HL) policy serves each class in order of arrival. It is admissible when the entry-into-service process $K^N$ is adapted to the filtration generated by the state history and the policy's own independent uniform random variables.

The fluid model works on the state space $\mathbb X=\mathbb R^J_+\times\prod_j\mathbf M[0,H^s_j)\times\prod_j\mathbf M[0,H^r_j)$ of finite measures with the weak topology. Given an arrival function $E$ (nondecreasing, rcll, $E(0)=0$), a path $(X,\nu,\eta)$ defines the auxiliary functions $B_j=\langle1,\nu_j\rangle$, $Q_j=X_j-B_j$, $D_j(t)=\int_0^t\langle h^s_j,\nu_j(u)\rangle du$, $K_j=B_j+D_j-B_j(0)$, $I=1-\sum_jB_j$, and the reneging function

$$R_j(t)=\int_0^t\int_0^{Q_j(u)}h^r_j\big((F_{j,u})^{-1}(y)\big)\,dy\,du,\qquad F_{j,u}(x)=\langle1_{[0,x]},\eta_j(u)\rangle .$$

A fluid model solution for $E$ satisfies the constraints (35)–(37), the monotonicity of $K$, the balance law $X_j=X_j(0)+E_j-R_j-D_j$, and the transport equations (46)–(47) for $\nu_j$ and $\eta_j$ driven by $dK_j$ and $dE_j$.

Formalization targets

Goal: Theorem 1 (p. 17)

Under Assumptions 4 and 5, for every sequence of admissible HL policies:

$$\{(\bar X^N,\bar\nu^N,\bar\eta^N)\}_{N}\ \text{is tight in }\mathbf D(\mathbb X),$$

and every distributional limit point $(X,\nu,\eta)$ is, almost surely, a continuous fluid model solution for $E$ started from $(X^0,\nu^0,\eta^0)$, with continuous auxiliary functions and each $\eta_j(t)$ charging no points. Assumptions 1–3 ask that the scaled arrivals and initial states converge. Assumption 4 asks that the hazards be bounded or lower semicontinuous near the right edges $H^s_j,H^r_j$. Assumption 5 adds continuity of $E$, an atomless $\eta^0$, and control of $\bar K^N$ by C-tightness or by inequality (55).

Milestones

1. Lemma 1, (24) and (26): the prelimit dynamic equations for $\langle f,\nu^N_j\rangle$ and $\langle\varsigma,\eta^N_j\rangle$.
2. Lemma 6, (61): $\langle1_{[0,x]}h^r_j,\eta^N_j(t)\rangle=\int_0^{F^N_{j,t}(x)}h^r_j((F^N_{j,t})^{-1}(y))\,dy$.
3. Lemma 7: the compensator bounds $|\mathcal A^N_{s,j}(\varphi,t)|\le\|\varphi\|_\infty(X^N_j(0)+E^N_j(t))\int_0^mh^s_j$ and the reneging analogue.
4. Lemma 8: relative compactness in $\mathbf D(\mathbb R_+)$ of the fluid-scaled real processes, and their C-tightness under Assumption 5.
5. Lemma 2 (i) and (iii): continuity and the absence of atoms propagate along fluid model solutions.

Significance

Theorem 1 characterizes fluid limits for every admissible HL policy at once. To get the fluid limit of a specific policy, one adds the equations that policy imposes and proves uniqueness for the resulting system; the paper does this for weighted random buffer selection (its Theorems 3–5). The reneging equation (40) is the main new feature: abandonment depends on the whole distribution of waiting times in queue, not only on the queue length. Allowing batch arrivals means the reneging count can only be sandwiched between two compensators, which is why Lemma 6 is needed.

The results are proved in the paper, with parts of the tightness argument delegated to Kang–Ramanan and Kaspi–Ramanan. None of them is formalized. The mission defines from scratch a measure-valued queue with abandonment, the Skorokhod space $\mathbf D(\mathbb X)$ with $J_1$ convergence, and the fluid model of §3. These definitions are reusable for the single-class models of Kaspi–Ramanan and Kang–Ramanan, for the WRBS and static-priority policies, and for other measure-valued fluid limits.

Difficulty

Each milestone is a known argument, but the obvious route to the goal breaks at the reneging term. A naive limit passage in the prelimit reneging count $R^N_j$ fails: with batch arrivals, $R^N_j$ is not a functional of $\eta^N_j$ and $Q^N_j$ alone, because customers with equal waiting times may be split between queue and service. Identifying the limit as the nonlinear function (40) requires bounds from above and below by marked point processes. It also requires showing that the compensators of these processes converge to a common limit, which uses that $\eta$ charges no points along the limit. The tightness part needs Kurtz–Jakubowski criteria for measure-valued processes on spaces $[0,H)$ whose right end may carry escaping mass. Lemma 6 is a pathwise identity for finite counting measures, and Lemma 7 is a pathwise bound.

Formalization scope

Classes are Fin J with $J\ge1$. Time is ℝ≥0. Customers are indexed by integers as in the paper. Event times are extended reals: a patience of $\infty$ keeps a customer in the potential queue forever, and an entry time of $\infty$ means the customer is never served. $\mathbf M[0,H)$ is FiniteMeasure on the subtype $[0,H)$ of ℝ≥0. $J_1$ convergence uses one time change for all coordinates, with the maximum of the sup-norm and Lévy–Prokhorov distances on $\mathbb X$. Convergence in distribution, distributional limit points, relative compactness and C-tightness are stated in coupling form; on the Polish space $\mathbf D(\mathbb X)$ these are equivalent to the usual notions. Hazards take values in $[0,\infty]$ and are $0$ off $[0,H)$. The integrals in (37), (40), (41), Lemma 6 and Lemma 7 are integrals of nonnegative functions. The derivative indicators that define the departure, reneging and marked processes are written as explicit counts.

Four readings are disclosed in the items. The goal's initial condition is stated through a coupling carrying $(E,X^0,\nu^0,\eta^0)$ jointly, because the limit point lives on its own probability space. $G^s,G^r$ in (46)–(47) are read as $G^s_j,G^r_j$. In Lemma 8, the (K.2) branch of Assumption 2 is read as relative compactness of $\bar K^N_j$, because the printed (K.2) does not imply it. The goal encodes Assumption 2 as printed. The head-of-the-line order is the HL condition stated in words on pp. 8–9 rather than inequality (10) alone, which would let a policy skip a waiting customer for good and serve younger ones.

The statement admits trivializing formalizations, and they are excluded here. The HL predicate contains only the defining constraints of Definitions 1–3: entry no earlier than arrival and before abandonment (9), the head-of-the-line order (the HL condition of pp. 8–9, which contains (10): a customer can enter service only after every earlier customer of its class has entered or abandoned), the state constraints (S.1), (S.2), (15) and (16), and rcll paths. The identities (18)–(26) are not in it. All standing independence and distributional hypotheses and the adaptedness of $K^N$ are explicit. The auxiliary functions $R,D,B,Q,K,I$ are computed from the path, never chosen. The policy is not specialized: idling and randomization are allowed.

Not posed: Lemmas 3–5, 9 and 10, Theorem 2, and Lemma 2 (ii) and (iv). Lemma 4 needs a server-assignment filtration, Lemma 5 needs predictable quadratic variations, and Theorem 2, Lemma 9 and Lemma 10 need measure-valued marked point processes on $[0,H)\times\mathbb R_+$. Formalizing these, or a sorry-free construction of an admissible system satisfying Assumptions 1–5, is welcome.

Selected references

• A. L. Puha, A. R. Ward, Fluid limits for multiclass many-server queues with general reneging distributions and head-of-the-line scheduling, Mathematics of Operations Research, Articles in Advance, 2021 (2022). https://doi.org/10.1287/moor.2021.1166
• H. Kaspi, K. Ramanan, Law of large numbers limits for many-server queues, Annals of Applied Probability 21 (2011) 33–114. https://doi.org/10.1214/10-AAP681
• W. Kang, K. Ramanan, Fluid limits of many-server queues with reneging, Annals of Applied Probability 20 (2010) 2204–2260. https://doi.org/10.1214/10-AAP683
• R. Atar, H. Kaspi, N. Shimkin, Fluid limits for many-server systems with reneging under a priority policy, Mathematics of Operations Research 39 (2014) 672–696. https://doi.org/10.1287/moor.2013.0632
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

A fork-join queue splits every incoming job into tasks, sends one task to each of $N$ parallel servers, and declares the job complete only when all tasks are done. The model describes assembly systems in which a manufacturer orders parts from $N$ suppliers and can only start production when every part has arrived, as well as parallel computing and storage systems in which a request is answered only after all sub-requests return. Because a job waits for its slowest task, the performance of the system is governed by the maximum queue length over the $N$ servers, and the question of interest is how this maximum behaves when $N$ is large and the system is heavily loaded.

Schol, Vlasiou and Zwart (arXiv:1912.11661, Mathematics of Operations Research 47(2), 2022) study this question in a nearly deterministic regime: arrivals and services happen in almost every time slot, and the traffic intensity of each server tends to $1$ at rate $N^{-2}$. Even in the empty-start case the queue lengths of different servers are dependent, because every server sees the same arrival process; the maximum of $N$ dependent random walks has to be analysed directly.

Timeline. Early work treats two service stations and obtains exact asymptotics (Flatto and Hahn, 1984; Baccelli, 1985; Wright, 1992). For more stations the literature turned to approximations and bounds: Nelson and Tantawi (1988) and Baccelli and Makowski (1989) bound the mean response time, and Ko and Serfozo (2004) approximate the response-time distribution in M/M/s fork-join queues. Heavy-traffic process limits for a fixed number of stations were obtained by Varma (1990) and Nguyen (1993, 1994), with reflected Brownian motion limits, and by Lu and Pang (2015–2017) for many-server stations. Sigman and Whitt (2011) analysed nearly deterministic G/G/1 and G/D/N queues. The paper of this mission gives a process-level (fluid) limit for the largest queue when the number of servers $N$ itself grows, in the nearly deterministic regime and with a non-zero initial condition.

Setting

Fix $\alpha,\beta>0$. For each $N$ the system runs in discrete time slots $j=1,2,\dots$. In slot $j$ a task arrives at all $N$ servers with probability $p^{(N)}=1-\alpha/N-\beta/N^2$ (indicator $X^{(N)}(j)$), and server $i$ completes a task with probability $q^{(N)}=1-\alpha/N$ (indicator $Y_i^{(N)}(j)$), all indicators being independent. The arrival process is $A^{(N)}(n)=\sum_{j=1}^{n}X^{(N)}(j)$ and the service process of server $i$ is $S_i^{(N)}(n)=\sum_{j=1}^{n}Y_i^{(N)}(j)$.

Server $i$ starts with $Q_i^{(N)}(0)=\lfloor r_NU_i\rfloor$ tasks, where $U_1,U_2,\dots$ are i.i.d. random variables, the initial queue lengths are non-negative, and $r_N\ge0$ is a scaling sequence. By Lindley's recursion the maximum queue length at time $n$ is

$$Q^{(N)}_{(\alpha,\beta)}(n)=\max_{i\le N}\max\Big(\sup_{0\le k\le n}\big[(A^{(N)}(n)-A^{(N)}(k))-(S_i^{(N)}(n)-S_i^{(N)}(k))\big],\;Q_i^{(N)}(0)+A^{(N)}(n)-S_i^{(N)}(n)\Big).$$

The first term alone is the maximum queue length of the system started empty. The initial condition is assumed to satisfy $Q^{(N)}_{(\alpha,\beta)}(0)/(N\log N)\to q(0)\ge0$ in probability (Assumption 2.3), and either $U_i$ has a finite right endpoint (Assumption 2.4) or $U_i$ is continuous with $-\log\mathbb P(U_i>vt)/-\log\mathbb P(U_i>t)\to h(v)$ as $t\to\infty$ for all $v\in[0,1]$ (Assumption 2.5, the Gumbel-domain case).

The fluid limit is

$$q(t)=\max\Big(\big(\sqrt{2\alpha t}-\beta t\big)\mathbb 1\big(t<\tfrac{\alpha}{2\beta^2}\big)+\tfrac{\alpha}{2\beta}\mathbb 1\big(t\ge\tfrac{\alpha}{2\beta^2}\big),\;g(t,q(0))-\beta t\Big),$$

with $g(t,q(0))=q(0)+\sqrt{2\alpha t}$ under Assumption 2.4 and $g(t,q(0))=\sup\{\sqrt{2\alpha t}\,u+q(0)v : u^2+h(v)\le1,\ 0\le u,v\le1\}$ under Assumption 2.5. In Lean these are fluid, fluidEmpty, gFinite and gGumbel; the queue is maxQueue and the empty-start queue maxQueueEmpty.

Formalization targets

Goal: Theorem 2.1 (fluid limit)

For every $T>0$ and $\epsilon>0$,

$$\mathbb P\left(\sup_{0\le t\le T}\left|\frac{Q^{(N)}_{(\alpha,\beta)}(tN^3\log N)}{N\log N}-q(t)\right|>\epsilon\right)\xrightarrow{N\to\infty}0,$$

under Assumptions 2.1–2.3 and either Assumption 2.4 or Assumption 2.5 (one conjunct per case).

Milestones

1. Section 4.2 tools. The pathwise oscillation bound of Lemma 4.1; the non-uniform Berry–Esseen rate of Lemma 4.2 for the standardized service process; the moment bound of Lemma 4.3; the extreme-value Lemma B.1 for sums of independent relatively stable variables and its consequence Lemma 4.4 for the Gaussian surrogate of the initial condition.
2. Pointwise convergence (Section 4.3). Lemmas 4.6 and 4.8 (bounds for the empty-start system), Lemma 4.5 (its pointwise limit), Lemma 4.9 (the initial-condition part) and Theorem 4.1: $Q^{(N)}_{(\alpha,\beta)}(tN^3\log N)/(N\log N)\to q(t)$ in probability for each $t>0$.
3. Tightness (Section 4.4). Lemma 4.10 (maxima preserve uniform convergence), Lemmas 4.11–4.12 (moduli of continuity of the two parts) and Corollary 4.1 (tightness of the scaled process on $[0,T]$).

Significance

The result. Theorem 2.1 identifies the scaling under which the maximum queue length of a large, heavily loaded fork-join system follows a deterministic curve: time of order $N^3\log N$ and space of order $N\log N$. The limit separates the contribution of the empty-start dynamics, which saturate at the steady-state level $\alpha/(2\beta)$ after time $\alpha/(2\beta^2)$, from the contribution of the initial backlog, which is governed by the extreme-value class of the initial condition. For instance, with $h(v)=v$ and $q(0)=\alpha/(2\beta)$ the system "starts and stays in steady state" on an initial interval (p. 12). The theorem gives the transient behaviour needed to judge how long a backlog at the slowest supplier persists.

Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission produces a formal statement of the model and of the fluid limit, and the intermediate results of Section 4. The proof combines a non-uniform Berry–Esseen inequality, extreme-value theory for maxima of sums, Doob's maximal inequality and a tightness criterion; formalizing it would give reusable Lean versions of several of these tools.

Difficulty

The obvious argument treats the $N$ queues as independent reflected random walks and applies extreme-value theory to their maximum. It fails because all servers share the arrival process, so the queues are dependent. The paper handles this by splitting each queue into a common arrival term and an individual service term, but the individual terms are maxima of $N$ centred random walks evaluated at a time of order $N^3\log N$, and their Gaussian approximation must be accurate at the scale of the maximum: a uniform Berry–Esseen bound is too weak, and a non-uniform bound with the right rate in $N$ is needed (Lemma 4.2). Upgrading pointwise convergence to uniform convergence on $[0,T]$ requires a modulus-of-continuity estimate for a maximum of $N$ processes (Lemmas 4.11–4.12), where the number of processes grows with $N$. The initial-condition term requires an extreme-value result for maxima of sums of two independent coordinates with different tails (Lemma B.1).

Formalization scope

All objects are defined in one module, LargeForkJoin.FluidLimit.Model. Times are natural numbers, and $Q(tN^3\log N)$ is evaluated at $\lfloor tN^3\log N\rfloor$, which is the paper's own convention $Q(n)=Q(\lfloor n\rfloor)$. Servers are indexed $0,\dots,N-1$. All variables live on one probability space; the Bernoulli laws are imposed for $N\ge N_0$ (for small $N$, $p^{(N)}$ can be negative), and within each $N\ge N_0$ the arrival indicators, service indicators and initial-condition variables $U_i$ used by that system are mutually independent. The independence of $(U_i)$ from arrivals and services is an added assumption: the paper uses it in its proofs but does not state it. Initial queue lengths are non-negative almost surely. Assumption 2.5 adds $\mathbb P(U_i>t)>0$ for all $t$, without which its ratio is undefined; "continuous" means "no atoms". Convergence in probability to a constant is written with $\epsilon$-events, and $\sup_{0\le t\le T}|\cdot|>\epsilon$ as "some $t\in[0,T]$ has $|\cdot|>\epsilon$", the same event. Lemmas 4.4 and 4.9 speak of Gaussian variables outside the model; they are stated for the law of $N$ independent pairs (standard normal, law of $U_1$).

The goal is stated about the maximum queue length built from the Bernoulli indicators through (2.3), uniformly on $[0,T]$. A statement about a Gaussian or reflected-Brownian surrogate (the heuristics of Sections 2.2–2.3), or a pointwise statement (Theorem 4.1), would not be Theorem 2.1.

Not included: Propositions 2.1–2.3 (other scalings and the steady state), the variant of Theorem 2.1 under Assumption 2.6, Theorem 4.2 (finite-dimensional distributions, a generic fact), and Lemma 4.7, whose statement includes the stationary case $t=\infty$ and needs a stationary-queue object. Contributions of general tools are welcome: a non-uniform Berry–Esseen inequality for Bernoulli sums, extreme-value results for maxima of i.i.d. sequences (relative stability, Gumbel-domain tails), and the tightness criterion of Billingsley's Theorem 7.3.

Selected references

• D. Schol, M. Vlasiou, B. Zwart, Large fork-join queues with nearly deterministic arrival and service times, Mathematics of Operations Research 47(2), 2022; arXiv:1912.11661v3. https://arxiv.org/abs/1912.11661v3
• L. Flatto, S. Hahn, Two parallel queues created by arrivals with two demands I, SIAM Journal on Applied Mathematics 44(5), 1984. https://doi.org/10.1137/0144072
• F. Baccelli, A. M. Makowski, Queueing models for systems with synchronization constraints, Proceedings of the IEEE 77(1), 1989. https://doi.org/10.1109/5.21076
• R. Nelson, A. N. Tantawi, Approximate analysis of fork/join synchronization in parallel queues, IEEE Transactions on Computers 37(6), 1988. https://doi.org/10.1109/12.2212
• K. Sigman, W. Whitt, Heavy-traffic limits for nearly deterministic queues, Journal of Applied Probability 48(3), 2011. https://doi.org/10.1239/jap/1316796905
• S.-S. Ko, R. F. Serfozo, Response times in M/M/s fork-join networks, Advances in Applied Probability 36(3), 2004. https://doi.org/10.1239/aap/1093962240
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

Why periodic dividends matter

A firm can return cash to shareholders by paying dividends, but a payment reduces the reserves available to survive future losses. If cash can be distributed only at scheduled dates while equity can be raised between those dates, the firm must coordinate a discrete dividend decision with a continuous-time financing decision. Keppo, Reppen and Soner study this combination for a firm whose cash flow is a Brownian motion with drift. Their preprint identifies the firm's optimal value through an operator that first solves the financing problem between dividend dates and then chooses the next dividend. The mission concerns that characterization, Theorem 3.4, together with the regularity results on which it depends.

The cash reserve model

Let $x\ge0$ be the initial reserve and let $C_t=\mu t+\sigma W_t$, where $W$ is a one-dimensional Brownian motion, $\mu>0$ is profitability, and $\sigma>0$ is volatility. Dividends of amounts $\ell_n\ge0$ may be paid at dates $nT$, with $T>0$. Equity issues have sizes $\zeta_k\ge0$ and occur at stopping times $\tau_k$; the issue times are locally finite. A positive issue costs

$$c(\zeta)=\lambda_f+(1+\lambda_p)\zeta,\qquad \lambda_f,\lambda_p>0,$$

while no issue costs zero. The cash reserve after actions at time $t$ is $X_t=x+C_t-L_t+I_t$. The ruin time $\theta$ is the first strictly positive time that $X_t<0$. A dividend cannot exceed the reserve immediately before its date, and no action is taken after ruin. These conditions define the admissible controls $\mathcal A_x$.

The firm's value function is the supremum, over admissible controls, of expected discounted dividends less expected discounted issue costs:

$$V(x)=\sup_{(L,I)\in\mathcal A_x}\mathbb E_x\left[\sum_{n\ge0}e^{-\rho nT}\ell_n-\sum_k e^{-\rho\tau_k}c(\zeta_k)\right],\qquad \rho>0.$$

The first sum includes a possible dividend at time zero, following the displayed objective in §3.1 of the preprint. An issue at time $T$ belongs to the next period. Thus the one-period financing operator $\mathcal L\phi$ charges issues on $[0,T)$ and evaluates its continuation reward $\phi$ at the reserve immediately before $T$. The dividend operator is

$$\mathcal D\phi(x)=\sup_{0\le\ell\le x}\{\phi(x-\ell)+\ell\},\qquad \mathcal T=\mathcal D\circ\mathcal L.$$

The continuation class $\mathcal C_A$ consists of the continuous, nondecreasing functions $\phi:[0,\infty)\to[0,\infty)$ that satisfy the issuance boundary condition of Definition 3.2, are bounded above by $x+A$, and have $\phi(x)-x$ nondecreasing and bounded in absolute value by $A$. Its larger class $\widehat{\mathcal C}_A$ omits the last condition. The intervention value in the boundary condition is $\mathcal I\phi(x)=\sup_{\zeta>0}\{\phi(x+\zeta)-c(\zeta)\}$.

Formalization targets

The first target is the mapping statement in Theorem 3.3: $\mathcal D:\widehat{\mathcal C}_A\to\mathcal C_A$ for $A\ge0$. With

$$A^*=\frac{\mu T}{e^{\rho T}-1},$$

the next targets are the one-period bound $0\le\mathcal L\phi(x)\le e^{-\rho T}x+A$ for $A\ge A^*$, the classical one-period characterization of Theorem 3.6, and the remaining mapping and contraction assertions of Theorem 3.3. In particular, $\mathcal T$ contracts the uniform distance between functions in $\mathcal C_A$ by the factor $e^{-\rho T}$.

The goal is Theorem 3.4:

$$V\in\mathcal C_{A^*},\qquad \mathcal T V=V,\qquad \phi\in\mathcal C_{A^*}\ \text{and}\ \mathcal T\phi=\phi\ \Longrightarrow\ \phi=V.$$

This identifies the fixed point with the value defined from admissible controls. It also asserts that the value is finite at every nonnegative initial reserve.

What the characterization gives

Theorem 3.4 turns an infinite-horizon control problem into repeated one-period calculations. Since Theorem 3.3 makes $\mathcal T$ a strict contraction on $\mathcal C_{A^*}$, iterating it determines the value in that class. The source connects this characterization to a numerical method when the one-period financing problem can be computed efficiently. A proof in Lean would also provide reusable statements about locally finite impulse controls, periodic actions, ruin, and discounted extended-real objectives. The preprint proves the mathematical results; this mission records their statements as open Lean theorems for machine-checked proofs.

Where the difficulty lies

The dividend operator is an elementary supremum over one payment, but the financing operator ranges over adapted impulses before ruin. Its regularity is central: the paper invokes Theorem 3.6 to show that $\mathcal L\phi$ is continuous and satisfies the issuance boundary condition. That theorem characterizes the arbitrary-maturity issuance value as the unique classical solution of a parabolic equation with a nonlocal boundary condition. The fixed-point conclusion alone would leave an additional gap: Theorem 3.4 must identify that fixed point with the original control supremum, including the limit over dividend periods and its terminal reward.

Formalization scope

Lean represents nonnegative reserves by $\mathbb R_{\ge0}$ and the discount, costs and function values by real numbers. Control values and one-period rewards are suprema in extended real numbers, with dividends and issue costs integrated separately as nonnegative quantities. The $\mathcal L$ bound proves the finiteness needed before converting to real values. An expression with both expected dividends and expected costs infinite takes the extended-real value $-\infty$ and cannot improve a supremum with a finite admissible alternative.

The paper's cumulative processes are represented by nonnegative dividend amounts and a locally finite impulse sequence of nonnegative issues. This makes explicit that equity cannot be supplied by an uncharged continuous component. Simultaneous impulses are allowed; merging them cannot increase the cost. The Brownian cash flow uses the published AtaBarjesteh23.Workload.IsDriftBM definition. The model requires a probability measure, adaptation to a filtration, and positive $\rho,\mu,\sigma,\lambda_f,\lambda_p,T$. The filtration is right-continuous and its initial σ-algebra contains all subsets of ambient null measurable sets, as required by the usual conditions. A dividend at time zero follows the objective's sum. In $\mathcal L$, the continuation value uses $X_{T-}$, resolving the free-issue-at-$T$ ambiguity in the printed formula. The arbitrary-maturity problem retains its separately printed non-strict survival indicator.

The value $V$ is defined solely from admissible controls, never from $\mathcal T$ or its iterates. Theorem 3.6 uses time to maturity and states smoothness only on the interior rectangle; uniqueness is restricted to the closed nonnegative time-state rectangle. Reusable work includes stopping-time measurability, impulse summation and parabolic regularity. Contributions proving the goal or the four listed milestones are within scope; §4's random-profitability model and §3.4's numerical experiments are outside this mission.

Selected references

• J. Keppo, A. M. Reppen and H. M. Soner, Discrete Dividend Payments in Continuous Time, Mathematics of Operations Research, 2021; preprint arXiv:1805.05077v2, 2019. https://arxiv.org/abs/1805.05077v2