All missions

Motivation

We establish a quantum version of the classical isoperimetric inequality relating the Fisher information and the entropy power of a quantum state. The key tool is a Fisher information inequality for a state which results from a certain convolution operation: the latter maps a classical probability distribution on phase space and a quantum state to a quantum state. We show that this inequality also gives rise to several related inequalities whose counterparts are well-known in the classical setting: in particular, it implies an entropy power inequality for the mentioned convolution operation as well as the isoperimetric inequality, and establishes concavity of the entropy power along trajectories of the quantum heat diffusion semigroup. As an application, we derive a Log-Sobolev inequality for the quantum Ornstein-Uhlenbeck semigroup, and argue that it implies fast convergence towards the fixed point for a large class of initial states.

This mission is the statement-level formalization of Geometric inequalities from phase space translations (arXiv:1606.08603v2). 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 Lemma 1: convolution data processing (Lemma 1, (30), PDF p. 11). 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, (35)–(36): quantum Stam inequality; abstract seed: Canonical extended displacement family with output finite second derivatives established from local input C2 (hard)
• Lemma 3, (40): inverse-Fisher sensitivity: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Theorem 2: entropy-power concavity: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Theorem 3, (44): hybrid entropy power inequality: Source-pinned general-state entropy/Fisher analytic domain; differential-entropy and heat-asymptotic moment domain for arbitrary classical densities (source-ambiguity)
• Theorem 4, (51): entropy isoperimetry: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Theorem 5: energy-constrained attenuator optimum: Extended right entropy derivative convention on the full finite-mean state/law domain, and energy-constrained attainment with that convention (source-ambiguity)
• Theorem 6: constrained quantum/classical correspondence: Extended right entropy derivative convention on the full finite-mean state/law domain, and energy-constrained attainment with that convention (source-ambiguity)
• Theorem 8: geometric pure-death optimum: Extended right entropy derivative convention on the full finite-mean state/law domain, and energy-constrained attainment with that convention (source-ambiguity)
• Lemma 8, (62): relative entropy production identity: Source-pinned general-state entropy/Fisher analytic domain; well-defined rate/energy identities without infinity cancellations (source-ambiguity)
• Example 1: large-entropy OU convergence: Exact threshold together with a source-pinned domain for entropy/relative-entropy rates (source-ambiguity)
• Unnumbered (65): entropy/Fisher log-Sobolev inequality: Source-pinned general-state entropy/Fisher analytic domain (source-ambiguity)
• Lemma 9, (66)–(67): qOU log-Sobolev inequality: Source-pinned general-state entropy/Fisher analytic domain; well-defined rate/energy identities without infinity cancellations (source-ambiguity)
• Example 2: low-energy OU convergence: Exact threshold together with a source-pinned domain for entropy/relative-entropy rates (source-ambiguity)
• Lemma 10, (72): classical OU entropy derivative: Initial-density domain justifying entropy differentiation, integrability and vanishing boundary terms for the classical OU process (source-ambiguity)

Selected references

• Geometric inequalities from phase space translations, arXiv:1606.08603v2, https://arxiv.org/abs/1606.08603v2

Motivation

Let {\rho} the density matrix of a mixed Gaussian state. Assuming that one of the Robertson--Schr"odinger uncertainty inequalities is saturated by {\rho}, e.g. ({\Delta}^{{\rho}}X_1)^2({\Delta}^{{\rho}}P_1)^2={\Delta}^{{\rho}}(X_1,P_1)^2+(1/4)\hbar^2, we show that there exists a unique pure Gaussian state whose Wigner distribution is dominated by that of {\rho} and having the same variances and covariance {\Delta}^{{\rho}}X_1,{\Delta}^{{\rho}}P_1, and {\Delta}^{{\rho}}(X_1,P_1) as {\rho}. This property can be viewed as an analytic version of Gromov's non-squeezing theorem in the linear case, which implies that the intersection of a symplectic ball by a single plane of conjugate coordinates determines the radius of this ball.

This mission is the statement-level formalization of The Unique Pure Gaussian State Determined by the Partial Saturation of the Uncertainty Relations of a Mixed Gaussian State (arXiv:1205.5222v1). 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 Saturation of one Robertson–Schrödinger inequality gives minimal symplectic capacity (Section 4, First step (continued on p.8), 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

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

• Theorem 1 (both clauses): A corrected uniqueness and domination statement for normalized Gaussian physical states (source-ambiguity)
• Section 4, Second step: A valid uniqueness criterion for a quantum blob contained in a minimal-capacity ellipsoid (source-ambiguity)
• Proposition 2: A valid replacement for the claimed fixed conjugate-coordinate plane section-area identity (source-ambiguity)

Selected references

• The Unique Pure Gaussian State Determined by the Partial Saturation of the Uncertainty Relations of a Mixed Gaussian State, arXiv:1205.5222v1, https://arxiv.org/abs/1205.5222v1

Motivation

We show that Araki and Masuda's weighted non-commutative vector valued $L_p$-spaces [Araki & Masuda, Publ. Res. Inst. Math. Sci., 18:339 (1982)] correspond to an algebraic generalization of the sandwiched R'enyi divergences with parameter $\alpha = \frac{p}{2}$. Using complex interpolation theory, we prove various fundamental properties of these divergences in the setup of von Neumann algebras, including a data-processing inequality and monotonicity in $\alpha$. We thereby also give new proofs for the corresponding finite-dimensional properties. We discuss the limiting cases $\alpha\to \{\frac{1}{2},1,\infty\}$ leading to minus the logarithm of Uhlmann's fidelity, Umegaki's relative entropy, and the max-relative entropy, respectively. As a contribution that might be of independent interest, we derive a Riesz-Thorin theorem for Araki-Masuda $L_p$-spaces and an Araki-Lieb-Thirring inequality for states on von Neumann algebras.

This mission is the statement-level formalization of R'enyi divergences as weighted non-commutative vector valued Lₚ-spaces (arXiv:1608.05317v2). 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-dimensional identification of Araki–Masuda and sandwiched Rényi divergences (§4.1 Eq.(39); Definition 2 and Eq.(10), p.5; Definition 7, p.8, PDF p. 9). 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:

• Lemma 1: interpolation for products of spatial derivatives: Supported spatial derivative and its domain-sensitive complex powers in arbitrary normal representations (hard)
• Lemma 3: representation independence: Representation-indexed extended Araki–Masuda vector norms and GNS implementers (hard)
• Proposition 4: norm interpolation: General Araki–Masuda norms at reciprocal exponents, including infinity (hard)
• Corollary 5: convexity of log of the p-th power: Extended logarithm of the p-th power of the general Araki–Masuda norm (hard)
• Theorem 6: Riesz–Thorin for Araki–Masuda spaces: Extended induced operator norm between general Araki–Masuda spaces (hard)
• Lemma 8, monotonicity clause: General Araki–Masuda divergence with an infinity-order endpoint (hard)
• Lemma 8, full-range continuity clause: A valid finite-domain boundary hypothesis for the printed continuity assertion (source-ambiguity)
• Lemma 9: fidelity and max-relative entropy endpoints: General AM divergence, squared intertwiner fidelity, and domination infimum (hard)
• Proposition 11: three Petz-divergence properties: Petz spectral moments, Umegaki entropy, and endpoint extensions on arbitrary W*-algebras (hard)
• Theorem 12, Eq.(57): algebraic ALT divergence comparison: Distinct general AM and Petz divergences in the common order domain (hard)
• Theorem 12, Eq.(58): vector ALT assertion as printed: Support and representative restrictions missing from Eq.(58) (source-ambiguity)
• Theorem 13: Umegaki entropy as the alpha=1 limit: General AM divergence and extended spectral Umegaki entropy (hard)
• Theorem 14, Eq.(72): data processing: Normal unital completely positive observable maps and general AM divergences (hard)
• Theorem 14, Eq.(73): Stinespring vector inequalities: A consistent p=2 definition or a corrected reversed endpoint in Eq.(73) (source-ambiguity)
• §5 Eq.(81): tensor-product additivity: Spatial von Neumann tensor powers and product normal states with AM divergences (hard)
• §5 Eq.(84): lower bound on the strong converse exponent: General tensor-product testing exponent with extended limsup/liminf and AM variational bound (hard)
• Lemma 16: general interpolation for unbounded positive operators: Supported unbounded positive self-adjoint operators with genuine complex-power domains (hard)
• Lemma 20: Jensen for unbounded operators: Domain-sensitive closed quadratic-form compression, including potentially nondense form domains, and fractional powers (hard)

Selected references

• R'enyi divergences as weighted non-commutative vector valued Lₚ-spaces, arXiv:1608.05317v2, https://arxiv.org/abs/1608.05317v2

Motivation

The Littlewood-Richardson coefficients $c^{\lambda}_{\mu\nu}$ give the multiplicity of an irreducible polynomial ${\rm GL}_n$-representation $F^{\lambda}_n$ in the tensor product of polynomial representations $F^{\mu}_n\otimes F^{\nu}_n$. In this paper, we generalize these coefficients to an $r$-fold tensor product of rational representations, and give a new method for computing them using an analogue of statistical contingency tables. We demonstrate special cases in which our method reduces to counting statistical contingency tables with prescribed margins. Finally, we extend our result from the general linear group to both the orthogonal and symplectic groups.

This mission is the statement-level formalization of Contingency tables and the generalized Littlewood-Richardson coefficients (arXiv:2012.06928v1). 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 Stable rational GL multiplicities as weighted hollow LR tables (Theorem 3, 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.

Selected references

• Contingency tables and the generalized Littlewood-Richardson coefficients, arXiv:2012.06928v1, https://arxiv.org/abs/2012.06928v1

Motivation

This article provides an elementary introduction to Gaussian channels and their capacities. We review results on the classical, quantum, and entanglement assisted capacities and discuss related entropic quantities as well as additivity issues. Some of the known results are extended. In particular, it is shown that the quantum conditional entropy is maximized by Gaussian states and that some implications for additivity problems can be extended to the Gaussian setting.

This mission is the statement-level formalization of Gaussian quantum channels (arXiv:quant-ph/0505151v1). 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 Gaussian states maximize quantum conditional entropy at fixed moments (§3.3, Eq. (23): Gaussian conditional-entropy extremality (abstract seed), 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

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

• Section 3.3, Eqs. (24)--(25): Operational distillable entanglement on arbitrary finite-mode bipartite trace-class states, with genuine LOCC protocols on tensor powers and asymptotic EPR yield in nats. (hard)
• Section 5.4, Eqs. (54)--(55); independent capacity definition on p.15: A Gaussian-displacement ensemble interface in the accepted full trace-class model: centered Gaussian trace-class realization for every physical covariance, finite-dimensional Gaussian probability laws including singular laws, measurable displaced-state preparation in trace norm, its trace-norm barycenter, and the independently optimized Gaussian Holevo objective with exact average-state constraints. (hard)
• Section 5.4, Eq. (58) implies (I)--(IV); proof continues p.17: A Gaussian-displacement ensemble interface in the accepted full trace-class model: centered Gaussian trace-class realization for every physical covariance, finite-dimensional Gaussian probability laws including singular laws, measurable displaced-state preparation in trace norm, its trace-norm barycenter, and the independently optimized Gaussian Holevo objective with exact average-state constraints. Also needed: compatible tensor-product channels and marginal constraint sets for the capacity-additivity clause. (hard)
• Section 5.4, final consequence after Eq. (61): An unrestricted infinite-dimensional entanglement-of-formation functional and its global tensor-additivity property, with the ensemble convention and finite-marginal-entropy domain needed by the background implications. (hard)

Selected references

• Gaussian quantum channels, arXiv:quant-ph/0505151v1, https://arxiv.org/abs/quant-ph/0505151v1

Motivation

We prove that it is impossible to distill more entanglement from a single copy of a two-mode bipartite entangled Gaussian state via LOCC Gaussian operations. More generally, we show that any hypothetical distillation protocol for Gaussian states involving only Gaussian operations would be a deterministic protocol. Finally, we argue that the protocol considered by Eisert et al. [quant-ph/0204052] is the optimum Gaussian distillation protocol for two copies of entangled Gaussian states.

This mission is the statement-level formalization of Gaussian transformations and distillation of entangled Gaussian states (arXiv:quant-ph/0204069v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite Gaussian contraction and normalized covariance update (Eqs.(1),(3)–(7), 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

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

• Single-copy nondistillation paragraph: Full Gaussian LOCC instruments and deterministic-LOCC entanglement monotonicity on actual conditional states (hard)
• Eq.(8), Bell measurement and Fig.1: Trace-preserving Bell quadrature spectral instrument and outcome-dependent local displacement feedback (hard)
• Fixed-input deterministic realization, continued pp.2–3: Universal fixed-input deterministic Gaussian LOCC replacement including ideal homodyne operations (hard)
• Finite-squeezing sentence continued on p.3: Topology and domain of the claimed approximation to an infinitely squeezed resource/transformation (source-ambiguity)
• Eqs.(9),(10): Actual Gaussian separability-to-product-resource decomposition and normalized possibly degenerate posterior displacement law (hard)
• Pure-resource optimum paragraph: Operational pure-resource protocol family including ideal resources and deterministic displacement-mixture degradation (hard)
• Fig.2 and optimum protocol paragraph: Full operational Fig.2 family and entanglement-dominating reduction from arbitrary Gaussian LOCC protocols (hard)

Selected references

• Gaussian transformations and distillation of entangled Gaussian states, arXiv:quant-ph/0204069v2, https://arxiv.org/abs/quant-ph/0204069v2

Motivation

We develop an approximation approach to infinite dimensional quantum channels based on detailed investigation of the continuity properties of entropic characteristics of quantum channels and operations (trace-nonincreasing completely positive maps) as functions of a pair ``channel, input state''. The obtained results are then applied to the following problems: continuity of the $\chi$-capacity as function of a channel; strong additivity of the $\chi$-capacity for infinite dimensional channels; the analytical expression for the convex closure of the output entropy of arbitrary quantum channel.

This mission is the statement-level formalization of On approximation of quantum channels (arXiv:0711.2245v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Strong topology of quantum operations is metrizable (§3, unnumbered: metrizability of the operation topology, 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:

• §2, Proposition 1: entropy functionals of measures: Bochner barycenter and spectral entropy/relative entropy functionals for arbitrary Borel state measures (hard)
• §2, Corollary 1: continuity on entropy-continuous barycenters: Finite-valued entropy continuity on barycenter images and the three measure functionals (hard)
• §2, Proposition 2(A–C): convex closures and attainment: Genuine real locally convex trace-class domain, two spectral entropies, closed convex envelopes and pure measure attainment (hard)
• §2, equation (7): finite versus general-measure χ optimization: Finite-ensemble and general-measure Holevo optimization on fixed Bochner barycenter fibers (hard)
• §2, equation (8): finite-output-entropy χ identity: Unnormalized spectral S and both convex envelopes in the finite-output-entropy Holevo identity (hard)
• §3, Remark 1: compact-uniform versus strong topology: Genuine bounded complex-linear trace-class maps with their Banach operator norm and compact-uniform topology (hard)
• §3, Proposition 3: generalized Choi–Jamiolkowski isomorphism: Source-ambiguity / missing hypothesis: full rank of TrH |Ω⟩⟨Ω| does not imply full rank of TrK |Ω⟩⟨Ω|. With H=C², K=C, Ω=e0⊗1, identity and dephasing channels on C² have identical Y images. The proof assumes a complete Schmidt basis of H. Faithful input marginal or restriction to its support is required. (source-ambiguity)
• §3, proof of Proposition 3: faithful canonical purification: Canonical faithful purification and typed tensor amplification Choi homeomorphisms (hard)
• §3, unnumbered: channels with two fixed marginals: Canonical Choi map in input-reference/output order for channels with two fixed marginals (hard)
• §3, Corollary 2(1–2): compactness criterion as printed: Printed (1) is false without strong closedness of F0. On C² with σ=I/2, the unitary conjugations diag(1,e^{it}) for 0<t<1 have singleton evaluation image {σ}, yet the channel set is nonclosed and noncompact. The proof establishes relative compactness, not compactness of every subset. (source-ambiguity)
• §3, Example 1: negative compactness observations: Unpinned hypotheses: finite-dimensional operation fibers are uniformly compact, and for faithful σ and A=0 the positive-map fiber is just the zero map, compact in both topologies. The source’s universal-sounding negative claims require an existential example or restrictions it does not specify. (source-ambiguity)
• §4, Proposition 4: joint lower semicontinuity: Joint extended Holevo function and closed convex output-entropy envelope (hard)
• §4, Lemma 1: joint lower semicontinuity for measures: Joint extended H-integral on operations times weak Borel probability measures (hard)
• §4, Corollary 3: convexity/concavity in the operation: Extended convexity and concavity in operations of chi and closed convex output entropy (hard)
• §4, unnumbered: entropy minimum at an extreme channel: Closed convex output entropy, convex operation sets and their actual extreme points (hard)
• §4, unnumbered: minimal-noise channel with fixed input/output: CCoOE and canonical inverse-Choi extreme coupling minimizers (hard)
• §4, Proposition 5: entropy-controlled convergence of characteristics: Joint spectral H convergence and three extended characteristic limits (hard)
• §4, application after Proposition 5: energy-constrained joint continuity: Finite real-valued spectral entropy and characteristic functions on the energy-bounded product (hard)
• §4, Proposition 6(A–B): approximation without finite output entropy: Both extended entropy envelopes and chi under compression or domination approximation (hard)
• §4, Lemma 2: order bound for finite-ensemble Holevo quantities: Subnormalized infinite-dimensional relative entropy and its finite-ensemble order comparison (hard)
• §4, Remark 3: continuous bounded approximation of χ and CCoOE: Spectral chi and CCoOE plus increasing bounded continuous concave/convex function approximations (hard)
• §5.1, unnumbered equation (18): lower semicontinuity of constrained χ-capacity: Constrained single-use chi-capacity on arbitrary state subsets (hard)
• §5.1, equations (19) and postprocessing example: Extended constrained capacity and typed postprocessing composition (hard)
• §5.1, Proposition 7: capacity continuity on compact constraints: Spectral H continuous convergence on compact input constraints and chi-capacity (hard)
• §5.1, Corollary 4: energy-constrained capacity continuity: Finite real constrained capacity and output partition-function condition (hard)
• §5.1, Proposition 8: stability of output optimal average: Uniquely specified output optimal average as a capacity-approaching-ensemble limit (hard)
• §5.2, Proposition 9: strong χ-capacity additivity for complementary-EB channels: Actual Stinespring complementary channels, tensor products and extended chi-capacity (hard)
• §5.2, Example 3: the externally defined Φap channel: The named channel Φap is specified only by a reference to the example in [18] (quant-ph/0608090); the allowed local paper does not define its action, input/output spaces or full a,p domain. The claimed operational classical capacity also needs the external constrained coding model. Proposition 9 itself is retained without this unresolved example. (source-ambiguity)
• §5.3, unnumbered: atomic roof equality iff lower semicontinuity: Separate countable-pure and general-measure entropy roofs on trace-norm states (hard)
• §5.3, Proposition 10: increasing continuous bounded convex approximation of CCoOE: Ordered output eigenvalues with zero padding, unnormalized truncated spectral entropy and countable pure roofs (hard)
• §5.3, Corollary 5: uniform convergence on entropy-continuous compact sets: Spectral truncated pure roofs and real uniform convergence on entropy-continuous compact sets (hard)
• §5.3, unnumbered Gaussian energy application: Unpinned source interface: the Gaussian-channel and energy convention are delegated to [8]; this paper supplies no number of modes, canonical Hamiltonian, or parameter/access specification for that application. Corollary 5 and the explicit partition-function energy results remain state targets. (source-ambiguity)
• §5.3, unnumbered EoF limit representation: Actual partial-trace entropy channel, general-measure EoF and truncated atomic pure roofs (hard)
• §5.3, unnumbered EoF class-membership conclusion: The function class hat P is not defined in the supplied paper; [17] is referenced for its definition. A precise class-membership proposition cannot be invented merely from the letter P. The actual displayed EoF approximation theorem is separately retained. (source-ambiguity)
• §5.3, unnumbered uniform EoF approximation under energy bound: Missing energy assumptions: no composite Hamiltonian or spectral/partition-function hypothesis is specified for this sentence. Bounded mean energy alone need not give compactness or entropy continuity. Supplying an arbitrary Hamiltonian would make the claim false; the precise sufficient conditions are preserved in Corollary 5. (source-ambiguity)
• §6, unnumbered Corollary: two-marginal compactness as printed: Printed necessity is false: on l²(N), A={|n⟩⟨n|:n∈N} is noncompact and B={0} is compact. Every joint positive operator has equal traces of its two marginals, so A⊗B is empty and compact. Nonempty counterexamples also arise from unused trace sectors. Continuous partial traces only prove compactness of their actual images, not arbitrary supersets A,B. (source-ambiguity)

Selected references

• On approximation of quantum channels, arXiv:0711.2245v1, https://arxiv.org/abs/0711.2245v1

Motivation

We address the problem of learning an unknown unitary transformation from a finite number of examples. The problem consists in finding the learning machine that optimally emulates the examples, thus reproducing the unknown unitary maximum fidelity. Learning a unitary is equivalent to storing it in the state of a quantum memory (the memory of the learning machine), and subsequently retrieving it. We prove that, whenever the unknown unitary is drawn from a group, the optimal strategy consists in a parallel call of the available uses followed by a "measure-and-rotate" retrieving. Differing from the case of quantum cloning, where the incoherent "measure-and-prepare" strategies are typically suboptimal, in the case of learning the "measure-and-rotate" strategy is optimal even when the learning machine is asked to reproduce a single copy of the unknown unitary. We finally address the problem of the optimal inversion of an unknown unitary evolution, showing also in this case the optimality of the "measure-and-rotate" strategies and applying our result to the optimal approximate realignment of reference frames for quantum communication.

This mission is the statement-level formalization of Optimal quantum learning of a unitary transformation (arXiv:0903.0543v2). 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 Covariance without loss for a delayed learning comb (§III A, Eq.(9): covariance without loss for a learning comb, 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

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

• Abstract and §III A: optimal N-to-1 unitary learning: Canonical memory, its normalized covariant POVM and the actual integral measure-and-rotate retrieval channel. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• Lemma 2 (Optimal states for storage): Canonical irrep memory and an isometric embedding into H_o tensor H_i tied to the actual U^N decomposition. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III A, Eq.(14): covariance without loss for retrieval: Two independent group actions on the actual reduced irrep memory. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III A, Eqs.(19)-(25): sharp fixed-storage retrieval bound: Common-irrep coupling maps for U tensor conjugate(U_j), actual m_K^(j), occurrence sets P_KL, and transported retrieval blocks. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• Theorem 1 (Optimal retrieving strategy): Actual eta_h memory coordinates and their integrated retrieval Choi matrix. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III B.1: multiple outputs with optimal single-copy fidelities: Canonical measure-and-rotate optimum plus local input insertion and output marginal maps for arbitrary joint Sigma. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §III B.2: optimal N-to-M learning for global fidelity: Canonical storage and an integral conditional tensor-target retrieval with M-dependent optimized weights. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• Remark: generalization to nonidentical group representations: Heterogeneous example/target tensor representations with actual based decomposition and common coupling data. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §IV: optimal inversion learning: Canonical integral estimator/conditional inverse channel and the normalized inverse global objective. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §IV: optimal approximate reference-frame realignment: Canonical token orbit and decoder on the Haar-correlated token/message state. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)
• §IV: fidelity-optimal versus maximum-likelihood token states: Actual SU(2) and U(1) tensor-power irrep families and their optimized-token versus likelihood-token fidelity sequences. Shared prerequisite: A finite, continuous, unitary, based irreducible decomposition of the actual example tensor representation, with positive multiplicities, pairwise inequivalent irreps, an exhaustive unitary intertwiner, and the induced canonical-memory embedding. (hard)

Selected references

• Optimal quantum learning of a unitary transformation, arXiv:0903.0543v2, https://arxiv.org/abs/0903.0543v2

Motivation

The coding theorem for the entanglement-assisted communication via infinite-dimensional quantum channel with linear constraint is extended to a natural degree of generality. Relations between the entanglement-assisted classical capacity and the $\chi$-capacity of constrained channels are obtained and conditions for their coincidence are given. Sufficient conditions for continuity of the entanglement-assisted classical capacity as a function of a channel are obtained. Some applications of the obtained results to analysis of Gaussian channels are considered. A general (continuous) version of the fundamental relation between the coherent information and the measure of privacy of classical information transmission by infinite-dimensional quantum channel is proved.

This mission is the statement-level formalization of On the entanglement-assisted classical capacity of infinite-dimensional quantum channels (arXiv:1210.6926v2). 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 Theorem 1, (14): general constrained entanglement-assisted coding theorem (Theorem 1, (14): general constrained entanglement-assisted coding theorem, 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

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

• Proposition 2 [7]: existence of a generalized optimal ensemble (cited): Nonempty feasible set and finite-valued entropy continuity (source-ambiguity)
• Corollary 1, both sufficient alternatives: Meaning of nontrivial subchannel and non-pure optimal support in alternative 2 (source-ambiguity)
• Unnumbered Gaussian strictness application, both alternatives: Energy above the pure ground-state boundary in the full-row-rank alternative (source-ambiguity)
• Section 5 Gaussian continuity application: Many-mode regular irreducible Weyl system, canonical unbounded quadratures, oscillator closed form, and actual Gaussian channel action compatible with the trace-class channel (hard)
• Appendix Proposition 5(1): Gaussian c-q characterization: Many-mode Gaussian dual action on bounded Weyl observables, full normal dual, and general commuting-range c-q predicate (hard)
• Appendix Proposition 5(2): full-rank Gaussian subchannel claim: Many-mode Gaussian interface and subspace restriction compatible with the full-rank Weyl action (hard)

Selected references

• On the entanglement-assisted classical capacity of infinite-dimensional quantum channels, arXiv:1210.6926v2, https://arxiv.org/abs/1210.6926v2

Why returns risk matters

A buyback contract lets a retailer return unsold goods to a manufacturer at an agreed returns price. The promise changes the retailer's willingness to order before demand is known. If the manufacturer may fail to honor it, the retailer must also judge how credible the promise is. Wang, Gurnani, and Subramanian study what the contract's wholesale and returns prices reveal about that credibility in a supply chain with one manufacturer and one retailer (Wang et al., 2020, §3–4). Their returns-risk result gives a precise case in which a more reliable manufacturer signals through lower prices. The direction is economically consequential because lower orders and less leftover stock accompany the signal.

This mission follows the authors' revised SSRN version, whose main-body page numbers and Electronic Companion result numbers fix the statements below. The result is a known theorem in that paper; the open work here is its Lean formalization.

Model and notation

The manufacturer offers a pair $(w,r)$: a nonnegative wholesale price $w$ per unit ordered and a nonnegative returns price $r$ per unit the manufacturer accepts back. Her marginal production cost is zero. The retailer orders stock $s\ge0$ before observing demand. After demand's baseline is realized, he sets a retail price $p_i\in[0,\alpha_i/\beta]$. Demand is $\alpha_i-\beta p_i$, where the baseline is high, $\alpha_h$, with probability $\lambda$, or low, $\alpha_l<\alpha_h$, with probability $\lambda^c=1-\lambda$. Write $\Delta\alpha=\alpha_h-\alpha_l$ and $\alpha=\lambda\alpha_h+\lambda^c\alpha_l$.

The manufacturer's type is the probability $\theta$ that she honors the returns promise. The less risky type has probability $\bar\theta$ and the riskier type has probability $\underline\theta<\bar\theta$. The retailer does not know the type when he sees the contract, so his perceived probability is $\hat\theta(w,r)$. Demand potential $\lambda$ is common knowledge in this mission. With $x^+=\max(x,0)$, the retailer's order formula from Lemma 1, at perceived demand probability $\hat\lambda$, is

$$s^R(w,r,\hat\theta,\hat\lambda) =\tfrac12(\hat\lambda\alpha_h+(1-\hat\lambda)\alpha_l-\beta w) +\tfrac{1-\hat\lambda}{2} \left[\Delta\alpha-\frac{\beta}{\hat\lambda}(w-\hat\theta r)\right]^+.$$

The low-demand unsold quantity is half the positive-part term. The manufacturer's expected profit, with actual return probability $\theta$, is equation (2):

$$\Pi(w,r\mid\hat\theta,\theta) =w\,s^R(w,r,\hat\theta,\lambda) -\lambda^c\theta r\, \frac{\left[\Delta\alpha-(\beta/\lambda)(w-\hat\theta r)\right]^+}{2}.$$

The retailer's price-stage and ordering objectives are defined separately, so Lemma 1 connects this formula to actual optimization rather than merely repeating a definition (SSRN version, pp. 9–11 and EC p. 1).

With the type known, Lemma 2 gives the symmetric-information benchmark:

$$w^\circ=\frac{\alpha}{2\beta},\quad r^\circ(\theta)=\frac{\alpha_l}{2\beta\theta},\quad \pi^\circ=\frac{\lambda^c\lambda(\Delta\alpha)^2+\alpha^2}{8\beta}, \quad s^\circ=\frac{\alpha_h}{4},\quad q^\circ=\frac{\Delta\alpha}{4}.$$

The two types earn the same $\pi^\circ$. Their actual returns prices differ because the expected payment depends on $\theta r$.

Formalization targets

The main target is Proposition 1. A separating equilibrium has the riskier type offer $(w^\circ,r^\circ(\underline\theta))$ and the less risky type offer a solution $(\bar w^\star,\bar r^\star)$ of problem (4). The retailer believes $\bar\theta$ at the latter contract and $\underline\theta$ at every other contract. Problem (4) maximizes $\Pi(\bar w,\bar r\mid\bar\theta,\bar\theta)$ over $\bar w\ge\bar\theta\bar r\ge0$, subject to the riskier type's non-mimicry constraint and the less risky type's participation constraint. A solution must actually attain that maximum; existence is part of the goal. The target comparison is

$$\bar w^\star<w^\circ,\qquad \bar r^\star<r^\circ(\bar\theta)<r^\circ(\underline\theta),\qquad \bar s^\star<s^\circ,\qquad \bar q^\star<q^\circ,$$

and no stock remains after high demand. The Lean goal also verifies both types' no-deviation clauses under the stated beliefs (SSRN version, p. 13, Proposition 1; EC p. 15).

The milestone list follows the paper's retailer-response and benchmark lemmas, then the Appendix B bounds on the transformed optimizer and the less risky type's off-path deviations. The transformed coordinates are $\tilde w=\bar w-w^\circ$ and $\tilde u=\bar w-\bar\theta\bar r-\lambda\Delta\alpha/(2\beta)$. They encode the constraints and quadratic objective in (B.4)–(B.7), rather than defining the original profit by that quadratic outside its valid region.

What the result gives

Under the authors' model, signaling greater reliability reduces both contract prices and the retailer's volume of trade. The comparison distinguishes the effects of information about returns risk from the symmetric-information benchmark. The paper also studies signals about demand potential and joint private information, but those are distinct results (Wang et al., 2020, §§5–6).

A complete Lean development would make the demand-stage optimization, two-type incentive constraints, existence of a maximizer, and the directional inequalities independently checkable and reusable in related contract models. The present mission states those targets; it does not claim they already have machine-checked proofs. The authors prove them in the cited paper. The objective here is to formalize that known argument or another proof of the same statements.

Where the proof is difficult

The less risky type chooses two continuous prices under a non-mimicry constraint that is nonlinear and changes form when the retailer stops carrying safety stock. A direct appeal to an unconstrained quadratic optimum misses the boundary and can violate the riskier type's incentive constraint. Existence also requires an attained maximum of problem (4), rather than a supremum or an assumed optimizer. The Appendix B characterization shows that the optimal transformed coordinates satisfy specific equations and strict inequalities; the no-deviation check then ranges over off-path contracts, not only local perturbations (SSRN version, EC pp. 4–15).

Formalization scope

Lean uses real parameters for the two demand baselines, $\beta$, $\lambda$, $\bar\theta$, and $\underline\theta$, and pairs of reals for contracts. The standing assumptions include $0<\alpha_l<\alpha_h$, $\beta>0$, $0<\lambda<1$, and $0<\underline\theta<\bar\theta\le1$. The strict lower bounds on $\alpha_l$ and $\underline\theta$ are disclosed additions: the printed model allows zero, but its returns-price benchmark divides by $\theta$ and Proposition 1's strict lower-price claim fails at $\alpha_l=0$.

The admissible action set for a type $\theta$ is $w\ge\theta r\ge0$, as in the paper's optimization problems; a deviation is checked when $w-\hat\theta(w,r)r\ge0$, following the retailer-response convention on p. 10. Beliefs range over $[\underline\theta,\bar\theta]$ and are pessimistic away from the less risky type's equilibrium contract. This is the paper's operational most-efficient profile from problem (4). Maximality over all possible separating equilibria and refinement by the intuitive criterion are outside this target.

For the retailer-price value, Lean takes a real supremum over the compact nonempty interval $[0,\alpha_i/\beta]$; the objective is continuous there under the standing assumptions. Lemma 1 makes its printed order formula an optimizer only when that formula is nonnegative, correcting the negative-order edge case; it states the unsold stock as the realized leftover at every optimal retail price, and claims the low-demand amount only under the price cap $\beta\hat\theta r\le\alpha_l$ of Lemma A.1, without which the printed amount can exceed the stock. Manufacturer profit remains the paper's equation (2); defining it as the Appendix B quadratic would make the target easier by changing the model. The first-stage solution predicate quantifies over every feasible contract and carries no desired sign condition. Reusable contributions include the price-stage analysis, the symmetric-information benchmark, and optimization facts for the transformed feasible set.

Selected references

• S. Wang, H. Gurnani, and U. Subramanian, The Informational Role of Buyback Contracts, Management Science, 2020. DOI; authors' revised SSRN version, abstract 3166462. The formal statements use the latter version's pp. 7–13 and Electronic Companion pp. 1–15.

Motivation

Financial constraints, the gap between what a firm could produce and what it can raise from outside investors, are a central object of corporate finance. In moral-hazard models of financing, an entrepreneur must be paid an agency rent to exert unobservable effort, and the investor can only be repaid out of what is left; the agency rent therefore fixes the entrepreneur's pledgeable income and the degree to which the entrepreneur is financially constrained (Tirole, The Theory of Corporate Finance, 2006).

J. Starmans, Technological Determinants of Financial Constraints (manuscript, February 4, 2022; published in Management Science, 2022, doi:10.1287/mnsc.2022.4421), asks how an entrepreneur's production technology, meaning which part of the cash-flow distribution the entrepreneur's effort improves, determines the agency rent, and hence which entrepreneur an investor with limited capital prefers to finance. The answer links technology, the form of the optimal security (debt, equity or a combination), and financial constraints in one model. The mission formalizes the paper's general comparison of entrepreneurs (its Proposition 6) together with the closed-form solution of the contracting problem on which it rests.

Setting

There are states $\Omega=\{0,\dots,n\}$ with $n>1$, and a project pays the cash flow $x_i$ in state $i$, where $0=x_0<x_1<\dots<x_n$. If the entrepreneur shirks, the state is drawn from a baseline distribution $q$ with $q_i>0$ for every state. An entrepreneur's type $p$ is the distribution of the state under effort. Write $\mathbb E_w[f]=\sum_i w_if_i$.

The likelihood ratio of a type is $\varphi_i(p)=(p_i-q_i)/q_i$. The type set $\mathscr P$ consists of the distributions $p$ such that (Assumption 1) every type creates the same expected value of effort $\pi>0$, $\mathbb E_p[x]-\mathbb E_q[x]=\pi$; (Assumption 2) $p$ first-order stochastically dominates $q$, with at least one strict tail inequality; and (Assumption 3) $\varphi(p)$ is single-peaked in the state. The cumulative likelihood ratio is

$$\Phi_j(p)=\frac{\sum_{i=j}^n(p_i-q_i)}{\sum_{i=j}^n q_i},\qquad \Phi^*(p)=\max_{j\in\Omega}\Phi_j(p),$$

and $\bar\iota(p)$ denotes the highest state with $p_i>q_i$: the upper end of the region the entrepreneur improves.

A contract $s=(s_i)_{i\in\Omega}$ pays the entrepreneur $s_i$ in state $i$. Given the entrepreneur's disutility of effort $c$, an optimal contract solves problem (1): maximize the investor's expected payoff $\mathbb E_p[x-s]$ subject to the incentive constraint $\mathbb E_p[s]-c\ge\mathbb E_q[s]$, the participation constraint $\mathbb E_p[s]-c\ge0$, limited liability $s_i\ge0$, and monotonicity of both payoffs, $s_i\ge s_{i-1}$ and $x_i-s_i\ge x_{i-1}-s_{i-1}$. The agency rent of an optimal contract is $\mathbb E_q[s]$. The tranches $\bar s^k_i=\mathbb 1\{i\ge k\}(x_k-x_{k-1})$, $k=1,\dots,n$, partition the cash flow.

Formalization targets

Goal: Proposition 6

Let $p',p''\in\mathscr P$ with $\bar\iota(p')=1<\bar\iota(p'')$. For every $c\in(0,\pi]$ both have optimal contracts, and, writing $s'_c,s''_c$ for any optimal contracts at $c$:

$$\Phi^*(p')<\Phi^*(p'')\ \Longrightarrow\ \exists\,\bar c\in(0,\pi):\ \mathbb E_q[s''_c]<\mathbb E_q[s'_c]\ \text{on }(0,\bar c),\quad \mathbb E_q[s'_c]<\mathbb E_q[s''_c]\ \text{on }(\bar c,\pi];$$ $$\Phi^*(p')>\Phi^*(p'')\ \Longrightarrow\ \mathbb E_q[s'_c]<\mathbb E_q[s''_c]\ \text{on }(0,\pi].$$

The threshold $\bar c$ is existential; no constant is fixed.

Milestones

In attack order: the sign facts $p_0<q_0$, $p_n\ge q_n$ (Lemma A.1); the sign pattern of $\varphi(p)$ (Lemma 2) and of $\Phi(p)$ (Lemma 3); the greedy optimal contract $\sum_{j<m}\bar s^{\sigma(j)}+\lambda_{\sigma(m)}\bar s^{\sigma(m)}$ with thresholds $0=\bar c_0<\bar c_1\le\dots\le\bar c_n=\pi$ (Proposition 1); the closed-form agency rent, continuous, increasing, piecewise linear and convex in $c$ (Proposition 2); the bounds $s\le\min\{x,x_{\bar\iota(p)}\}$ and $\mathbb E_q[s]\le\mathbb E_q[\min\{x,x_{\bar\iota(p)}\}]$ with equality iff $c=\pi$ (Corollaries 2 and 3); and the two facts of the proof of Proposition 6 (p. 47): the agency rent is $c/\Phi^*(p)$ on $[0,\pi]$ when $\bar\iota(p)=1$, and on an initial interval for every $p$.

Significance

Proposition 6 says that the peak cumulative likelihood ratio, the informativeness of the most informative tranche, decides which entrepreneur is cheaper to incentivize when effort is cheap, while at high disutility of effort the entrepreneur who improves only the left tail of the distribution (whose optimal contract is equity-like) is cheaper. Its instance with the optimal equity-financed and the optimal debt-financed entrepreneurs is the paper's Proposition 5, which underlies its predictions about which firms are more financially constrained. The milestones give a complete closed-form solution of a linear contracting problem with limited liability and two-sided monotonicity under a single-peaked likelihood ratio, a setting that generalizes the monotone likelihood ratio property.

The results are proved in the paper (Appendix A). As far as a search of the Prove2Me catalog shows, none of them, and no model of security design with tranches, has a machine-checked proof. The mission produces formal proofs of the paper's results; the agency-rent formula of Proposition 2 is a reusable description of a fractional knapsack's value function.

Difficulty

The comparison is not a pointwise statement about two formulas: the agency rent is the value of an optimization problem over all contracts, and only the solution of that problem (Proposition 1) turns it into a piecewise-linear function. The step that does not follow from slopes alone is the comparison at $c=\pi$: it needs the identification of the optimal contract at $c=\pi$ with $\min\{x,x_{\bar\iota(p)}\}$ (Corollaries 2 and 3), which rests on the sign structure of Lemmas 2 and 3 and therefore on Assumptions 2 and 3 together. The monotonicity constraint on the investor's payoff, $x_i-s_i\ge x_{i-1}-s_{i-1}$, is what caps each tranche at weight one; without it (the paper's Appendix C) the agency rent is $c/\Phi^*(p)$ for every $c$ and the crossing in case (i) disappears.

Formalization scope

States are Fin (n + 1); types, contracts and cash flows are vectors Fin (n + 1) → ℝ, and all expectations are finite sums. The standing assumptions $n>1$, $0=x_0<\dots<x_n$, $q_i>0$, $\sum_iq_i=1$, $\pi>0$ are bundled in Economy.Standing; $\mathscr P$ is InP, which keeps Assumption 2's strict clause as written. Tranches and positions of the ordering $\sigma$ are indexed by Fin n, standing for the paper's indices $1,\dots,n$ shifted by one. $\Phi^*$ is the maximum over all of $\Omega$, including $j=0$. $\bar\iota(p)$ is defined as the highest state with $p_i>q_i$; Lemma 2 shows it is the paper's $\bar\iota(p)$. The agency rent function is the infimum of $\mathbb E_q[s]$ over optimal contracts, and Proposition 2 states that every optimal contract attains it on $[0,\pi]$.

Conventions disclosed in the statements: "an optimal contract from Proposition 1" in Corollaries 2–3 and in the goal is read as every optimal contract of problem (1) (all optimal contracts share one agency rent, footnote 7, p. 11); existence of optimal contracts is stated explicitly wherever a statement quantifies over them; the investor's capital $I$ and the condition $\mathbb E_q[x]+\pi-c\ge I\ge\mathbb E_q[x]$ (p. 8) are omitted because problem (1) drops the investor's participation constraint. Each statement carries its own range of $c$ as on its page.

The agency rent is defined through problem (1) over all feasible contracts, never by the formula of Proposition 2 or the construction of Proposition 1; a formalization that defined it by the formula, or that dropped the monotonicity constraint (1f), would make the goal arithmetic or false, and is ruled out.

A complete development needs only finite sums and elementary real analysis (one-sided slopes, convexity on an interval); Mathlib suffices. Contributions welcome: proofs of the milestones, a general lemma on fractional knapsack problems (reusable beyond this mission), and the paper's remaining results (Propositions 3–5 and 7).

Selected references

• J. Starmans, Technological Determinants of Financial Constraints, manuscript, February 4, 2022; Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4421
• J. Tirole, The Theory of Corporate Finance, Princeton University Press, 2006.
• R. D. Innes, Limited liability and incentive contracting with ex-ante action choices, Journal of Economic Theory 52(1), 1990, 45–67. https://doi.org/10.1016/0022-0531(90)90066-S
• J. Poblete and D. Spulber, The form of incentive contracts: agency with moral hazard, risk neutrality, and limited liability, RAND Journal of Economics 43(2), 2012, 215–234. https://doi.org/10.1111/j.1756-2171.2012.00164.x

Motivation

A series system works only if every one of its components works. Deciding whether it works by inspecting components one at a time, in the order that minimizes the expected inspection cost, is the classic sequential testing problem for series systems (Mitten 1960; Butterworth 1972; Simon & Kadane 1975). It is solved by sorting the components by the ratio $c_i/(1-p_i)$. In medical diagnosis, quality control and software testing, tests are often run in batches: a laboratory charges a fixed shipping-and-handling fee per batch on top of the per-test fees. Daldal, Gamzu, Segev & Ünlüyurt (Naval Research Logistics, 2016) introduced this sequential batch testing problem and gave a $(6.829+\epsilon)$-approximation. Segev and Shaposhnik (SSRN 3277805, 2018; Operations Research) settled its approximability up to $1+\epsilon$ with a polynomial-time approximation scheme (PTAS).

Timeline:

• 1960–1975: the single-test problem is solved by a ratio rule (Mitten; Butterworth; Simon–Kadane).
• 2016: batch testing with a set-up cost; a $6.829+\epsilon$ approximation (Daldal et al.).
• 2018: a quasi-PTAS and then a PTAS (Segev & Shaposhnik), the results of this mission.

Setting

Let $X_1,\dots,X_n$ be independent Bernoulli variables with $\Pr[X_i=1]=p_i$. Testing $X_i$ costs $c_i>0$, and each batch also costs a set-up cost $\beta\ge0$. A testing scheme is an ordered partition $S=(S_1,\dots,S_T)$ of $[n]$. Batch $S_t$ is inspected only if every earlier batch found no zero, which happens with probability $\varphi(S,t)=\prod_{\tau<t}\prod_{i\in S_\tau}p_i$. The expected cost is

$$E(S)=\sum_{t=1}^{T}\varphi(S,t)\Big(\beta+\sum_{i\in S_t}c_i\Big),$$

and the problem is to minimize $E(S)$ over all testing schemes.

The algorithm first scales the costs by $c_{\min}=\min_i c_i$ and rounds each $c_i/c_{\min}$ up to a power $(1+\epsilon)^r$. The variables then fall into cost classes $C_0,\dots,C_R$ of equal rounded cost. A state is a vector $N=(N_0,\dots,N_R)$ in $F=\prod_r\{0,\dots,|C_r|\}$: it records that the $N_r$ lowest-probability variables of each class $C_r$ have been tested. $P_0(N)$ is the product of their $p_i$. An action $\Delta\gneq0$ costs $C(\Delta)=\beta+\sum_r\Delta_r(1+\epsilon)^r$, in normalized units. For a set of states $G$, a $G$-path runs $0\to\cdots\to N^{(\mathrm{all})}=(|C_0|,\dots,|C_R|)$ through $G$ with strictly increasing states, and costs $\sum_t P_0(N^{(t-1)})\,C(N^{(t)}-N^{(t-1)})$. $\mathrm{OPT}_G$ is the least such cost.

Let $\psi(N)$ be the largest class with $N_r\ge1$, and let $\kappa=\lceil\log_{1+\epsilon}(n/\epsilon)\rceil$. A state is nice-looking if every class $r\le\psi(N)-\kappa$ is exhausted. It is great-looking if, in addition, on each of the $\kappa$ middle classes $\psi(N)-\kappa<r\le\psi(N)$ it holds

$$N_r=\min\Big\{\Big\lfloor\mu_r\cdot\tfrac{\epsilon^2}{\kappa}\cdot P_2[(1+\epsilon)^\rho]\,/\,(1+\epsilon)^r\Big\rfloor,\ |C_r|\Big\}$$

for some integer $0\le\rho\le R+\lceil\log_{1+\epsilon}n\rceil$ and non-negative integers $\mu_r$ with $\sum_r\mu_r\le3\kappa/\epsilon^2$. Here $P_2[x]$ rounds $x$ down to a power of 2. $F_{\mathrm{nice}}$ and $F_{\mathrm{great}}$ denote these sets.

Formalization targets

Goal: Theorem 1 (p. 6), in algorithm-output form

For $0<\epsilon\le1$: the dynamic program over $F_{\mathrm{great}}$ has an optimal path. The testing scheme $S_\pi$ of any optimal path $\pi$ satisfies, with the original costs,

$$E(S_\pi)\le(1+\epsilon)\,K(\epsilon)\,E(S)\ \text{ for every testing scheme }S,\qquad K(\epsilon)=(1+3\epsilon)(1+\epsilon)^2+2\epsilon(1+\epsilon)^4,$$

and $|F_{\mathrm{great}}|\le(n+1)\,(R+\lceil\log_{1+\epsilon}n\rceil+1)\binom{\lfloor3\kappa/\epsilon^2\rfloor+\kappa}{\kappa}$.

Milestones, in proof order

• Rounding: $E_c(S)\le E_{\hat c}(S)\le(1+\epsilon)E_c(S)$ (§2.1, p. 8).
• Greedy-within-class: every scheme is matched by an $F$-path (pp. 8–10). Path cost equals the expected cost of the path's scheme (eqs. (1), (3)).
• Lemmas 1–2 and Theorem 2: $\mathrm{OPT}_{F_{\mathrm{nice}}}\le(1+\epsilon)\,\mathrm{OPT}_F$ (pp. 12–14).
• Lemmas 3–4, on the bucketing by powers of $1+\epsilon$ in probability (p. 18).
• Lemma 5 and Properties A–C, on the great-looking construction (pp. 19–24).
• Theorem 3: $\mathrm{OPT}_F\le\mathrm{OPT}_{F_{\mathrm{great}}}\le K(\epsilon)\,\mathrm{OPT}_F$ (p. 17).
• The explicit count of $|F_{\mathrm{great}}|$ (pp. 16–17).

Significance

The PTAS shows that batch testing of series systems can be approximated to within any factor $1+\epsilon$ in polynomial time for fixed $\epsilon$, improving the earlier constant factor $6.829+\epsilon$. Its ingredients are general tools of approximate dynamic programming: a structural ordering that turns schemes into count vectors, a collapse of the state space by exhausting cheap classes, and a rounding of the middle classes onto a coarse power-of-two grid. Local charging arguments control the error of the last two. These tools apply beyond this problem.

The result is proved on paper; nothing in it has a machine-checked proof that we know of. A formalization produces a checked chain from the testing model to the approximation guarantee, including the delicate parts: the rounding interplay in Lemma 5, the double-sum exchange in the proof of Theorem 3, and the case analysis of inequalities (8)–(12). It also makes explicit what the paper leaves as $1+O(\epsilon)$ and $O(n)$. The resulting library of testing schemes, count-vector dynamic programs and restricted state spaces can be reused for other sequential testing models.

Difficulty

Restricting the dynamic program to a small set of states can only make it worse. The work is showing it is not much worse, and the obvious charging fails. Exhausting all cheap classes at once (Theorem 2) costs only a factor $1+\epsilon$, but it leaves $n^{O(\kappa)}$ states, which is quasi-polynomial. Rounding the middle classes onto a grid shrinks the state space to polynomial size, but a per-step rounding error is not small compared with that step's own cost. It must be charged to the cost of all earlier steps. That charge is affordable only because the bucketing makes the probabilities of successive steps decrease geometrically (Lemma 4). The grid must also be nested from step to step so that rounding never forces a count to decrease (Lemma 5, which relies on the power-of-two operator $P_2$). Any single per-step argument loses a factor that does not tend to $1$.

Formalization scope

All objects are defined from scratch in one file in BatchTesting.PTAS. The model and its conventions:

• Instance. An instance is $(p,c,\beta)$ on Fin n, with standing assumptions $n\ge1$, $p_i\in[0,1]$, $c_i>0$ and $\beta\ge0$. Of these, $c_i>0$ is the paper's own (p. 8); the other three are added. Every statement also assumes $0<\epsilon\le1$; $\epsilon\le1$ is used in the proofs of Property A and inequality (12).
• Normalization. The normalization $\min_i c_i=1$ is carried out by the definitions, never assumed. The goal compares expected costs of the original instance.
• Testing schemes and paths. Testing schemes are lists of Finsets, and may contain empty batches. Paths are lists of states with strictly increasing steps. Every DP statement is in path form ("for every path there is a path with cost at most …"), not as an infimum over paths.
• Classes. Class arithmetic ($\psi$, $\kappa$, the middle range) is in $\mathbb Z$, and $\psi(0)=-\infty$ is encoded as $-1$. Ties within a class are broken by index.
• Constructions. The constructions of §3.4, §4.3 and §4.5 are definitions, so Lemmas 1–5 and Properties A–C are about the page's objects. Steps with $P_0=0$ form one extra last bucket. The §4.5 action is integer-valued, so Lemma 5 has content.

The paper's "$1+O(\epsilon)$" is the explicit $K(\epsilon)$ of its own chain on pp. 19–20. Its "within factor $1+\epsilon$" is the factor $(1+\epsilon)K(\epsilon)$, which reaches $1+\epsilon'$ after rescaling $\epsilon$. The running time is not formalized: the inputs are real numbers and the exponent is $O(1/\epsilon^3)$. The explicit bound on $|F_{\mathrm{great}}|$ stands in for it.

The statement "some testing scheme is within $1+\epsilon$ of optimal" is trivially true, because an optimal scheme exists. The goal therefore concerns the scheme read off an optimal path over $F_{\mathrm{great}}$, and it carries the state count.

A complete development needs finite products over nested Finsets, an exchange argument for the greedy order, and list manipulations of paths (removing zero actions, subsequences). The counting milestone needs a stars-and-bars bound. The testing-scheme and path layer can be reused for other sequential testing problems. Proofs of any milestone, and alternative arguments with better constants, are welcome.

Selected references

• D. Segev, Y. Shaposhnik, A Polynomial-Time Approximation Scheme for Sequential Batch Testing of Series Systems, SSRN preprint 3277805, 2018; published in Operations Research. https://ssrn.com/abstract=3277805, https://doi.org/10.1287/opre.2019.1967
• R. Daldal, I. Gamzu, D. Segev, T. Ünlüyurt, Approximation algorithms for sequential batch-testing of series systems, Naval Research Logistics 63(4):275–286, 2016.
• L. Mitten, An analytic solution to the least cost testing sequence problem, Journal of Industrial Engineering 11(1):17, 1960.
• R. Butterworth, Some reliability fault-testing models, Operations Research 20(2):335–343, 1972.
• H. A. Simon, J. B. Kadane, Optimal problem-solving search: All-or-none solutions, Artificial Intelligence 6(3):235–247, 1975.

Motivation

Consumer electronics firms receive a steady stream of defective product returns (DPRs): units that fail shortly after purchase and are exchanged for a new unit. Many of these returns are repaired and resold as refurbished products at a discount. Refurbishing is usually studied as a cost-recovery or environmental question. Singh, Ramachandran and Subramanian ask a different question: how do defective returns interact with the firm's pricing over time when consumers are strategic, that is, when they anticipate future prices and may wait?

The relevant background is the time-inconsistency problem of a durable-goods monopolist. Coase (1972) argued that a monopolist selling a durable good over time competes with its own future sales; Bulow (1982, 1986) made this precise in a two-period model and showed that a firm that cannot commit to its second-period price earns strictly less than one that can. The paper embeds defective returns in Bulow's two-period model. Returns from the first period become the supply of a cheaper refurbished product in the second, which competes with the firm's own new product in that period. The paper finds that a higher defect rate can then raise the firm's profit.

Setting

A monopolist sells over two periods to a continuum of consumers of total mass one. A consumer's quality valuation $\theta$ is uniformly distributed on $[0,1]$; each consumer buys at most one unit.

• The new product has perceived quality $v_n$ and marginal cost $c_n$. The refurbished product has quality $v_r$, with $0<v_r<v_n$, and refurbishing cost $c_r$, with $0\le c_r<c_n$.
• The defect rate $\alpha>0$ is the expected number of replacement units per unit sold, so selling $q$ new units costs $(1+\alpha)c_nq$. A refurbished unit has defect rate $k_r\alpha$ with $0\le k_r<1$ and costs $(1+k_r\alpha)c_r$ per unit sold. Each return costs the consumer a hassle $h\ge 0$.
• Firm and consumers discount the second period by $\rho\in(0,1)$.

A type-$\theta$ consumer's discounted utilities are

$$U^\theta_1=v_n\theta-h\alpha-p_1,\quad U^\theta_2=\rho(v_n\theta-h\alpha-p_2),\quad U^\theta_r=\rho(v_r\theta-hk_r\alpha-p_r),\quad U^\theta_0=0,$$

for buying new in period 1, new in period 2, refurbished in period 2, or nothing. Write $\mu_n=v_n-(1+\alpha)c_n-h\alpha$ and $\mu_r=v_r-(1+k_r\alpha)c_r-hk_r\alpha$.

Without commitment. The firm sets $p_1$; consumers buy in period 1 if $U^\theta_1\ge\max\{U^\theta_2,U^\theta_r,0\}$ at the second-period prices they anticipate. After observing first-period sales $q_1$, the firm chooses $(p_2,p_r)$ to maximize second-period profit subject to the returns constraint $(1+k_r\alpha)q_r\le\alpha q_1$, since refurbished units come only from first-period returns. In a subgame-perfect outcome the anticipated prices are the optimal ones. $\Pi^*(\alpha)$ is the firm's optimal discounted two-period profit.

With commitment. The firm announces $(p_1,p_2,p_r)$ at the start; each consumer picks the best of the four options, and the firm maximizes subject to the same returns constraint. $\Pi^C(\alpha)$ is the optimal profit.

Formalization targets

Goal: Proposition 3

For every parameter vector satisfying the standing assumptions:

$$\text{(i)}\quad \Pi^C \text{ is strictly decreasing on } \{\alpha>0:\Pi^C(\alpha)>0\};$$ $$\text{(ii)}\quad \Pi^*(\alpha)\le\Pi^C(\alpha)\quad(\alpha>0);$$ $$\text{(ii)(a)}\quad \Pi^*(\alpha)=\Pi^C(\alpha)\quad\text{for } \alpha\ge\alpha_c=\frac{v_n-c_n}{c_n+h}.$$

At the parameters of the paper's Figure 3 ($c_n=0.7$, $c_r=0.1$, $v_n=1$, $\rho=0.9$, $k_r=0.25$, $h=0.05$):

$$\text{(ii)(b)}\quad \exists\,\hat v_r<1\ \ \forall v_r\in(\hat v_r,1):\ \alpha\mapsto\Pi^*(\alpha)\ \text{is neither nondecreasing nor nonincreasing on }(0,\infty).$$

Milestones

In attack order:

• Proposition 1, the second-period product strategy (None, New Only, Refurbished Only, Product Line) with explicit thresholds $\bar\alpha$, $\underline q_1$, $\bar q_1$.
• Lemma 2, which excludes two candidate equilibrium strategies.
• Proposition 7, the commitment benchmark: no new units in period 2, and refurbishing none, some or all returns according to $\bar\alpha$ and an explicit $\bar v_r$.
• The three general parts (i), (ii), (ii)(a) of Proposition 3.

Significance

The result. Under commitment, defects only add friction: replacement production, refurbishing cost and hassle all lower profit, so $\Pi^C$ falls with $\alpha$. Without commitment, the firm's temptation to sell new units again in period 2 is what lowers its profit, as in Bulow's model. Refurbished returns compete with that second-period new product, and above $\alpha_c$ the firm stops offering it. The defect rate then acts as a commitment device, and on part of the parameter space profit increases with $\alpha$. Without the commitment benchmark, this effect could not be separated from the direct cost of defects.

Formalizing it. Proposition 3 is proved on paper through closed forms for each candidate strategy (Tables 2, 4 and 8 of the paper) and signs of derivatives. No part of it has a machine-checked proof. The mission adds a two-period durable-goods monopoly with strategic consumers to the platform, with both its subgame-perfect and its commitment profit defined from the consumers' purchase rules. Part (ii)(b) appears here in a corrected form: as printed it is vacuous (see Formalization scope), and the mission states a non-vacuous version at the paper's own numerical parameters.

Difficulty

$\Pi^*$ is defined through an equilibrium, not a formula. Evaluating it requires three steps:

• the second-period optimum for every $q_1$, which is a strictly concave quadratic program over a polygon whose active constraints change with $q_1$ and $\alpha$ (Proposition 1);
• consumers' rational anticipation of those prices in the first period;
• a one-dimensional maximization over $q_1$ of a piecewise-quadratic profit.

The obvious route to part (ii)(b) is to differentiate a closed form in $\alpha$. It fails at the step that matters: the increase happens at the boundary between strategies $NNR_A$ and $N\emptyset R_A$, where the equilibrium strategy switches. There the profit is not given by a single formula, and the sign must be controlled uniformly in $v_r$ near $v_n$. Part (i) needs the commitment optimum, its regime boundaries ($\bar\alpha$, $\bar v_r$), and a strictly negative derivative inside each regime, glued across regime changes.

Formalization scope

The Lean development lives in the namespace RefurbCommit.DefectProfit. All quantities are real.

• Demands are Lebesgue measures of buyer sets defined by the purchase rules, not the closed forms (4.2), (4.4), (B.19). The closed forms omit the clipping of $\theta$ to $[0,1]$. A consumer indifferent between two options counts in both buyer sets; the overlaps have measure zero.

• Second period. The remaining types are $[0,1-q_1]$. Prices are optimal if they satisfy the returns constraint and maximize $\Pi_2$ among all prices that satisfy it.

• $\Pi^*$ is the supremum of (4.5) over subgame-perfect outcomes $(p_1,q_1,p_2,p_r)$. In such an outcome, $q_1$ is the first-period demand at $p_1$ under the anticipation $(p_2,p_r)$, and $(p_2,p_r)$ is optimal given $q_1$. $\Pi^C$ is the supremum of (B.20) over feasible committed prices. Both suprema are taken in $\mathbb R$; the commitment set always contains $0$.

• Added hypotheses, each disclosed in the item concerned:

  • $v_r>0$;
  • $v_r(c_n+h)-v_n(c_r+h)k_r>0$ wherever $\bar\alpha$ is used;
  • in Proposition 1, $\mu_r>0$ for the ordering $\underline q_1<\bar q_1$, and $q_1>0$ in the two cases that sell refurbished units;
  • $\Pi^*>0$ or $\Pi^C>0$ where the paper's positive-profit restriction is used.

  The paper's bound $h<\bar h$ (p. 8) is not imposed.

• Part (ii)(b) is pinned to the Figure 3 parameters, and $\hat v_r<v_n$ is required. As printed, "there exists $\hat v_r$ such that $\Pi^*$ is non-monotonic when $\hat v_r<v_r<v_n$" holds vacuously with $\hat v_r=v_n$. A formalization that lets $\hat v_r=v_n$, lets $\hat v_r$ depend on $v_r$, reads "non-monotonic" as "not nonincreasing" only, or defines $\Pi^*$ or $\Pi^C$ by the paper's closed-form tables is trivial and does not capture the result.

A complete development needs the following:

• the second-period quadratic program;
• a measure-theoretic computation of interval buyer sets;
• the rational-expectations reduction of the first period to a choice of $q_1$;
• continuity of the equilibrium profit in $\alpha$.

The buyer-set and second-period lemmas apply to other two-period vertical-differentiation models. Contributions of any of these lemmas, of exact profit formulas proved from the definitions, and of the closed-form strategy tables as theorems are welcome.

Selected references

• N. Singh, K. Ramachandran, R. Subramanian, Intertemporal product management with strategic consumers: the value of defective product returns, Manufacturing & Service Operations Management, 2021. Accepted manuscript (Dec. 2020): https://ssrn.com/abstract=2511424; journal version https://doi.org/10.1287/msom.2021.0972
• R. H. Coase, Durability and monopoly, Journal of Law and Economics 15(1), 1972. https://doi.org/10.1086/466731
• J. I. Bulow, Durable-goods monopolists, Journal of Political Economy 90(2), 1982. https://doi.org/10.1086/261063
• J. Bulow, An economic theory of planned obsolescence, Quarterly Journal of Economics 101(4), 1986. https://doi.org/10.2307/1884182

Why capacity scaling with predictions matters

A data center can save energy by running fewer servers when demand is low, but restarting servers costs energy and queued work delays users. A controller must choose capacity while demand arrives, with limited knowledge of future traffic. Forecasts can help, yet an inaccurate forecast can make a controller perform worse than one that ignores it. Rutten and Mukherjee study this tension in a continuous-time fluid model and give a controller whose cost improves with prediction quality while retaining a bound for arbitrary predictions (arXiv:2101.12160v2, §§2–4).

The paper’s Adaptive Balanced Capacity Scaling controller, or ABCS, joins an online controller to Adapt to the Prediction, or AP. AP starts with an offline capacity plan for predicted arrivals and reacts to arrivals missed by the forecast. ABCS uses AP as advice while changing its own response rates according to the current queue and capacity. Theorem 4.11 gives an explicit bound for both accurate and inaccurate forecasts (Rutten–Mukherjee, p. 16).

The fluid model

Time ranges over a known finite interval $[0,T]$, with $T>0$. An arrival rate $\lambda(t)\geq0$ brings divisible work into a queue. A server schedule $m(t)\geq0$ supplies processing capacity, with $m(0)=0$. The workload $q(t)$ is the work waiting at time $t$. It increases when arrivals exceed service and decreases under spare service only while work is waiting. The defining equation is

$$q(t)=\int_0^t(\lambda(s)-m(s))\mathbf 1\{q(s)>0\text{ or }\lambda(s)\geq m(s)\}\,ds.$$

The objective combines three costs. With waiting weight $\omega>0$, activation price $\beta>0$, and operating rate $\theta\geq0$, the cost $\operatorname{Cost}^{\lambda}(m,t)$ is $\omega\int_0^t q$, plus $\beta$ times the limiting sum of positive capacity increases, plus $\theta\int_0^t m$. The offline optimum $\operatorname{Opt}$ is the infimum of total cost over feasible schedules for the actual arrivals. The infimum is attained according to Proposition 2.2 (pp. 7–8, equations (2.1)–(2.3)).

A prediction $\tilde\lambda$ covers the same horizon. Its mean absolute error is $\|\tilde\lambda-\lambda\|_{\mathrm{MAE}}=T^{-1}\int_0^T|\tilde\lambda-\lambda|$. It is $\eta$-accurate when $\eta>0$ and $\int_0^T|\tilde\lambda-\lambda|\leq\eta\operatorname{Opt}$. An algorithm has competitive ratio at most $C$ if its cost is at most $C\operatorname{Opt}$ for every instance and applicable prediction. These are Definitions 3.1–3.3 (pp. 10–11).

AP adds to an offline optimum for $\tilde\lambda$ an online response to positive underprediction $\Delta\lambda=(\lambda-\tilde\lambda)^+$. ABCS receives AP’s server schedule $\tilde m$ and the workload $\tilde q$ that schedule would produce under actual arrivals. It chooses its own schedule $m$ by an integrated form of the differential rule $m'=(\hat r_1\omega q-\hat r_2\theta m)/\beta$. The coefficients switch between $r_1,R_1$ and $r_2,R_2$ by comparing $(m,q)$ with $(\tilde m,\tilde q)$, as specified in Algorithm 3 (pp. 13–15).

Formalization targets

Theorem 4.11: an adaptive competitive bound

For every $\eta$-accurate prediction, the goal is

$$\operatorname{Cost}^{\lambda}(m,T)\leq \min\{[1+(\sqrt{2\omega\beta}+\theta)\eta]\,\mathrm{OCR},\ \mathrm{PCR}\} \operatorname{Opt}.$$

The constants $\mathrm{OCR}$ and $\mathrm{PCR}$ are exactly the rate-dependent formulas in equation (4.14), with $c_1$ through $c_6$ defined there. The first term approaches $\mathrm{OCR}$ as prediction error shrinks; the second is a uniform bound over predictions. The goal quantifies over every admissible instance, forecast, AP advice, and ABCS trajectory. It is the pointwise cost form of the paper’s competitive-ratio statement, Definition 3.3 (p. 16, Theorem 4.11).

Results leading to the goal

The milestone list includes the offline minimizer, the pessimistic bound $\operatorname{Cost}(\mathrm{ABCS})\leq\mathrm{PCR}\operatorname{Opt}$, the advice comparison $\operatorname{Cost}(\mathrm{ABCS})\leq\mathrm{OCR}\operatorname{Cost}(\mathrm{AP})$, and AP’s additive prediction-error bound. It also records equations (A.32), (A.34), and (A.30), which express the cost decomposition and online-correction estimate used for AP (pp. 8, 14, 22–23, 35).

What the result gives

The theorem puts the quality of a forecast into the same cost units as waiting, server activation, and operation. A good forecast yields the OCR term; a poor one cannot push the bound above PCR. The constants expose how the four ABCS response rates trade closeness to advice against protection from bad advice. In the zero-confidence setting $R_1=r_1$, $R_2=r_2$ the paper reports both ratios equal to five; for instance $R_1=r_1=2$, $R_2=r_2=1$ gives $\mathrm{OCR}=\mathrm{PCR}=5$ from (4.14) (p. 16, Remark 4.14).

The paper proves the mathematical result. The present formalization supplies precise Lean statements for the model, controller rules, intermediate claims, and final bound; their proofs remain to be machine checked. A complete proof would also make the reflection workload, limiting switching cost, and potential-function inequalities reusable in continuous-time online optimization.

Where the proof is difficult

The comparison bounds require potential functions whose derivatives balance queueing cost, capacity increases, and power cost across several switching cases. The case analysis in Appendices A.9–A.10 depends on regularity of the trajectories and of the advice. Simply integrating a differential inequality is insufficient until absolute continuity and the behavior at switching times are established. The existence of an ABCS trajectory for general arrival processes is not proved in the paper, so it is a separate analytical issue (pp. 37–45).

The offline existence result has a different obstacle: the capacity activation term is a limsup of positive mesh increments and does not vary continuously with the schedule in an elementary function norm. The paper uses a selection argument. The AP estimate also needs the one-sided queue reflection to behave appropriately when predicted arrivals and underprediction are separated (pp. 29–30, 34–36).

Formalization scope

Lean represents time and rates by real numbers and costs and the offline infimum by extended nonnegative reals $\mathbb R_{\geq0}\cup\{\infty\}$. The workload is an implicit integral-equation predicate. Offline optimization ranges over feasible schedule–workload pairs. AP and ABCS are trajectory predicates, with the latter expressing the integrated differential equation; the statements concern every trajectory satisfying it. They do not assert general existence. The zero-arrival instance has explicit AP and ABCS trajectories in a separate sanity check.

The source assumes nonnegative arrivals and predictions, $T>0$, $\omega,\beta>0$, $\theta\geq0$, and $R_i\geq r_i\geq0$. Lean additionally requires integrability of arrival rates and relevant integrands. It uses $r_1,r_2>0$ because real division by zero would turn the paper’s infinite constants into finite Lean values. The AP correction starts at zero, as required by the server schedule’s initial value. The mesh activation sum clips its last interval at $t$ so that cost through $t$ depends only on $m$ through $t$. These choices are recorded with the item statements.

The cost keeps $q$ explicit because ABCS reads queue values. The accuracy condition uses extended nonnegative arithmetic and expresses $\|\tilde\lambda-\lambda\|_{\mathrm{MAE}}\leq\eta\operatorname{Opt}/T$ without dividing by a possibly infinite optimum. The formalization rules out zero-denominator constants, default values from nonintegrable Bochner integrals, dependence on schedules after the horizon, and a vacuous zero-instance controller. Contributions on workload reflection, switching-cost limits, offline attainment, controller existence, and the stated milestones are welcome.

Selected references

• Debankur Mukherjee and Daniel Rutten, Online Capacity Scaling Augmented With Unreliable Machine Learning Predictions, arXiv:2101.12160v2, 2022; published as A New Approach to Capacity Scaling Augmented with Unreliable Machine Learning Predictions, Mathematics of Operations Research, 2024. arXiv

Motivation

Most equity markets trade through a continuous limit order book (CLOB): any market order is matched immediately against the resting limit orders. Budish, Cramton and Shim (QJE 2015) argued that continuous matching creates mechanical arbitrage and a race in speed between high-frequency market makers, and proposed frequent batch auctions instead, with a lower bound of about 100 milliseconds on the auction period. Earlier work, notably Madhavan (J. Finance 1992), compared auctions and continuous markets through the quality of price formation. What neither line of work gives is a quantitative answer to the question an exchange designing a periodic auction has to settle: how long should an auction last? A longer auction gathers more liquidity before the price is fixed, but the information on which that liquidity was posted grows stale.

Jusselin, Mastrolia and Rosenbaum (arXiv:1906.01713, published in Operations Research, 2021, doi:10.1287/opre.2021.2113) model a market organized in sequential call auctions triggered by market orders, measure the quality of price formation by the mean squared distance between the clearing price and the efficient price, and give this error in semi-explicit form as a function of the auction duration $h$ (their Theorem 2.1). Minimizing the formula on Euronext data gives optimal durations of a few minutes. This mission formalizes that formula and the lemmas of its proof.

Setting

Fix constants $\nu>0$, $\mu>0$, $\sigma_f>0$, $\sigma\ge0$, $K>0$, $P_0\in\mathbb R$ and an auction duration $h\ge0$. On a probability space $(\Omega,\mathcal F,\mathbb P)$:

• the efficient price is $P_t=P_0+\sigma_fW_t$, with $W$ a standard Brownian motion;
• market makers arrive at the epochs $\tau^{mm}_1<\tau^{mm}_2<\cdots$ of a Poisson process $N^{mm}$ of intensity $\mu$;
• the auction opens at the first market order, at a time $\tau^{op}_1\sim\mathrm{Exp}(\nu)$, and clears at $\tau^{cl}_1=\tau^{op}_1+h$;
• the $k$-th market maker posts the linear supply $S_k(p)=K(p-\tilde P_k)$ around its view $\tilde P_k=P_{\tau^{mm}_k}+g_k$, where the estimation noises $g_k$ are i.i.d., centred, with variance $\sigma^2$;
• the market takers' imbalance at the clearing is a square-integrable random variable $I_{\tau^{cl}_1}$;
• $W$, $N^{mm}$, $\tau^{op}_1$, $(g_k)$ and $I_{\tau^{cl}_1}$ are mutually independent.

With $N=N^{mm}_{\tau^{cl}_1}$ market makers present, the clearing price solves $\sum_{k=1}^N S_k(p)=I_{\tau^{cl}_1}$, and the mid-price ignores the market orders:

$$P^{cl}_{\tau^{cl}_1}=\frac1N\sum_{k=1}^N\tilde P_k+\frac1K\frac{I_{\tau^{cl}_1}}N,\qquad P^{mid}_{\tau^{cl}_1}=\frac1N\sum_{k=1}^N\tilde P_k .$$

On $\tilde\Omega=\{N^{mm}_{\tau^{cl}_1}>0\}$ these are defined, and the two quality criteria are

$$E(h)=\mathbb E\big[(P^{cl}_{\tau^{cl}_1}-P_{\tau^{cl}_1})^2\,\big|\,\tilde\Omega\big],\qquad E^{mid}(h)=\mathbb E\big[(P^{mid}_{\tau^{cl}_1}-P_{\tau^{cl}_1})^2\,\big|\,\tilde\Omega\big].$$

In Lean these are E p P X h and Emid p P X h, built from Pcl, Pmid, Peff and OmegaT in AuctionDuration.ClearingError.Model.

Formalization targets

Goal: Theorem 2.1 (p. 10)

With $c(h)=\big(1-e^{-\mu h}\tfrac{\nu}{\nu+\mu}\big)^{-1}e^{\nu h}$,

$$E^{mid}(h)=c(h)\int_h^{+\infty}\nu e^{-\nu t}\Big(\big(\sigma_f^2\tfrac t6+\sigma^2\big)e^{-\mu t}\int_0^{\mu t}\frac{e^s-1}{s}ds+\sigma_f^2\tfrac t3\big(1-e^{-\mu t}\big)\Big)dt,$$ $$E(h)=E^{mid}(h)+\frac{\mathbb E[I^2_{\tau^{cl}_1}]}{K^2}\,c(h)\int_h^{+\infty}\nu e^{-\nu t}e^{-\mu t}\int_0^{\mu t}\frac1s\int_0^s\frac{e^u-1}{u}du\,ds\,dt,$$

together with the integrability of both squared errors.

Milestones (Appendix A, pp. 20–22)

1. (9): $\mathbb P(N^{mm}_{\tau^{cl}_1}>0)=1-e^{-\mu h}\nu/(\nu+\mu)$.
2. Lemma A.2 (11): for $N_t\sim\mathrm{Poisson}(m_t)$, $\mathbb E[\mathbf 1_{N_t>0}/N_t]=e^{-m_t}\int_0^{m_t}\frac{e^s-1}s ds$ and the analogous double integral for $\mathbb E[\mathbf 1_{N_t>0}/N_t^2]$.
3. Lemma A.2 (12): closed forms of $\mathbb E[(1+N_t)^{-2}]$ and $\mathbb E[(2+N_t)^{-2}]$, for $m_t>0$.
4. Lemma A.1 (10): $g(t)=\sigma_f^2\frac{t^2}2\mu\,\mathbb E[(N^{mm}_t+1)^{-2}]+\sigma_f^2\frac{t^3}3\mu^2\,\mathbb E[(N^{mm}_t+2)^{-2}]$, where $g(t)$ is the expected squared average price move between the market makers' arrivals and a deterministic time $t$.
5. (8): $E(h)=\mathbb P(\tilde\Omega)^{-1}e^{\nu h}\int_h^{+\infty}\nu e^{-\nu t}\big(g(t)+\sigma^2f(t)+\ell(t)/K^2\big)dt$, with $f(t)=\mathbb E[\mathbf 1_{N^{mm}_t>0}/N^{mm}_t]$ and $\ell(t)=\mathbb E[I^2_{\tau^{cl}_1}]\,\mathbb E[\mathbf 1_{N^{mm}_t>0}/(N^{mm}_t)^2]$.

Significance

The result. Theorem 2.1 turns the design question into a one-dimensional minimization: every quantity in the formula is a model parameter that can be estimated from order-book data ($\nu$, $\mu$, $\sigma_f$, $\sigma$, $K$, $\mathbb E[I^2]$). It shows that $E(h)>E^{mid}(h)$ for $h>0$, quantifies the cost of market orders through $\mathbb E[I^2]/K^2$, and contains the continuous order book as the case $h=0$, so that the auction and the CLOB can be compared in one metric. The paper's Lemma 2.1 identifies $E(h)$ with the almost-sure long-run average squared error over the sequence of auctions, and Section 3 feeds the formula with the imbalance produced by strategic market takers.

Formalizing it. The result is proved on paper; no part of it is machine-checked. The mission produces a formal model of a call auction with Poisson liquidity and a Brownian efficient price, a checked derivation of the error formula, and, as separable by-products, closed forms for inverse moments of a Poisson variable (Lemma A.2) and a Palm-type computation for Brownian increments sampled at Poisson points (Lemma A.1). The proof in Appendix A is a short sketch: the passage from the random clearing time to deterministic times in (8), the vanishing of cross terms, and the Palm formula step of Lemma A.1 are asserted rather than carried out.

Difficulty

The obvious argument conditions on everything and expands the square. The random clearing time is the obstacle: the number of market makers, their arrival epochs and the Brownian value at the clearing all depend on $\tau^{op}_1$, and the conditioning on $\tilde\Omega$ couples the Poisson process with the opening time, so neither can be treated as having its unconditional law. Turning (8) into a rigorous statement needs a disintegration over $\tau^{op}_1$ and measurability of Brownian motion evaluated at random times. Lemma A.1 needs the conditional uniformity of Poisson arrival epochs given their number (or the Mecke–Palm formula) combined with independence from $W$; neither is available off the shelf. The Lemma A.2 identities are series manipulations, but they require exchanging sums and integrals of $(e^s-1)/s$ near $s=0$.

Formalization scope

AuctionDuration.ClearingError.Model defines Params (with Standing: $\nu,\mu,\sigma_f,K>0$, $\sigma\ge0$), the random objects Auction (W, interarrival times A, opening time T, noises g, imbalance J), the hypothesis bundle IsModel, and Nmm, tauCl, Peff, view, Pmid, Pcl, OmegaT, E, Emid, gFun, fFun, ellFun. Market-maker arrivals use the published definition QueueingFundamentals.Foundations.ArrivalProcess (IsExpInterarrivals, arrivalTime, countingProcess); the Brownian motion is Mathlib's IsBrownianReal.

Conventions the formalization commits to:

• One auction, the first one; the regenerative multi-auction structure is not modelled.
• Appendix A's reading of Assumption 2: the Poisson process and the $\mathrm{Exp}(\nu)$ opening time are independent and are conditioned jointly on $\tilde\Omega$. Assumption 2 read literally (opening time unconditioned) gives a different value, under which Theorem 2.1 does not hold.
• Added hypotheses, disclosed in every item: $\mathbb E[g_k]=0$; independence of $I_{\tau^{cl}_1}$ from the other families; every Brownian path continuous (a version choice); $m_t>0$ in (12).
• Lean's g k and arrivalTime A (k+1) are the paper's $g_{k+1}$ and $\tau^{mm}_{k+1}$. $W$ is indexed by $\mathbb R_{\ge0}$ and evaluated at t.toNNReal.
• $1/0=0$ in Lean; $E$, $E^{mid}$ are integrals under P[|OmegaT X h], and $f$, $\ell$, $g$ carry the indicator $\mathbf 1_{N_t>0}$ as on the page. Inner integrands $(e^s-1)/s$ are $0$ at $s=0$, a null set.
• Lemma A.2 is stated for a Poisson random variable, the time-$t$ marginal of the paper's inhomogeneous process; only that law enters.

$E$, $E^{mid}$, $g$, $f$ and $\ell$ are expectations over the model, not their closed forms: defining any of them by the formulas of Theorem 2.1 or Lemmas A.1–A.2 would make the goal or a milestone true by definition, and is ruled out. Integrability conjuncts in the goal, (8) and Lemma A.1 prevent a junk Bochner value from satisfying an identity.

Useful published facts: QueueingFundamentals.Foundations.poisson_count_cdf (Proved) gives the Poisson law of countingProcess for exponential interarrival times, which reduces Lemmas A.1–A.2 at fixed $t$ to Poisson-distribution computations. Contributions of general value are welcome: conditional uniformity of Poisson epochs, a Mecke formula for the published arrival process, measurability of Brownian motion at random times, and inverse-moment identities for the Poisson law.

Selected references

• P. Jusselin, T. Mastrolia, M. Rosenbaum, Optimal auction duration: a price formation viewpoint, arXiv:1906.01713v3, 2020 (Operations Research, 2021). https://arxiv.org/abs/1906.01713v3 ; https://doi.org/10.1287/opre.2021.2113
• E. Budish, P. Cramton, J. Shim, The high-frequency trading arms race: frequent batch auctions as a market design response, The Quarterly Journal of Economics 130(4), 1547–1621, 2015. https://doi.org/10.1093/qje/qjv027
• A. Madhavan, Trading mechanisms in securities markets, The Journal of Finance 47(2), 607–641, 1992. https://doi.org/10.1111/j.1540-6261.1992.tb04403.x
• J.-F. Coeurjolly, J. Møller, R. Waagepetersen, A tutorial on Palm distributions for spatial point processes, International Statistical Review 85(3), 404–420, 2017 (the Palm formula used for Lemma A.1). https://doi.org/10.1111/insr.12205