All missions

Motivation

We extend the mathematical theory of quantum hypothesis testing to the general $W^*$-algebraic setting and explore its relation with recent developments in non-equilibrium quantum statistical mechanics. In particular, we relate the large deviation principle for the full counting statistics of entropy flow to quantum hypothesis testing of the arrow of time.

This mission is the statement-level formalization of Quantum Hypothesis Testing and Non-Equilibrium Statistical Mechanics (arXiv:1109.3804v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 1.1 (Proposition 1.1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 3.7: Translation-covariant lattice interactions and canonical tensor inclusions (hard)
• Theorem 3.8: Translation-covariant lattice interactions and canonical tensor inclusions (hard)
• Theorem 3.9: Actual CAR quasi-free states, compressions and Fourier symbols (hard)
• Theorem 4.2: Two-index testing exponents with genuine iterated limits (hard)
• Theorem 5.1: Genuine W*-standard form and normal positive predual (hard)
• Proposition 5.2: Unbounded relative Tomita/modular operators and spectral calculus (hard)
• Proposition 5.3: Extended Araki entropy on normal positive W*-functionals (hard)
• Proposition 5.4: Source-corrected scope/formula for Proposition 5.4 (source-ambiguity)
• Proposition 5.5: Unbounded relative Tomita/modular operators and spectral calculus (hard)
• Lemma 5.6: Unbounded relative Tomita/modular operators and spectral calculus (hard)
• Lemma 5.7: Unbounded relative Tomita/modular operators and spectral calculus (hard)
• Theorem 6.1: Unbounded relative Tomita/modular operators and spectral calculus (hard)
• Proposition 6.2: W*-projection/effect testing and general-index exponent construction (hard)
• Proposition 6.3: W*-projection/effect testing and general-index exponent construction (hard)
• Proposition 6.4: Extended Araki entropy on normal positive W*-functionals (hard)
• Theorem 6.5: W*-projection/effect testing and general-index exponent construction (hard)
• Theorem 6.6: W*-projection/effect testing and general-index exponent construction (hard)
• Proposition 6.7: Reversed modular characteristic functions and W*-Stein families (hard)
• Theorem 6.8: Reversed modular characteristic functions and W*-Stein families (hard)
• Proposition 7.1: W*-dynamics, relative Hamiltonians and normal-state FCS (hard)
• Theorem 7.2: quantum hypothesis testing of the arrow of time: W*-dynamics, relative Hamiltonians and normal-state FCS (hard)
• Theorem 8.1: Spin--fermion model with SF1--SF3 and finite approximants (hard)
• Theorem 8.2: EBB CAR dynamics, wave operators and on-shell scattering matrix (hard)
• Theorem 8.3: Source-corrected scope/formula for Theorem 8.3 (source-ambiguity)
• Generalized tests have the same testing results: W*-projection/effect testing and general-index exponent construction (hard)
• Section 3.4.1: quantum i.i.d. reduction: Source-corrected scope/formula for Section 3.4.1: quantum i.i.d. reduction (source-ambiguity)
• Pressure and its convexity: Translation-covariant lattice interactions and canonical tensor inclusions (hard)
• Open-system multi-parameter FCS: Open-system tensor embeddings and joint spectral FCS (hard)
• TD FCS local large deviation principle: Source-corrected scope/formula for TD FCS local large deviation principle (source-ambiguity)
• TD analytic cumulants and central limit theorem: Source-corrected scope/formula for TD analytic cumulants and central limit theorem (source-ambiguity)
• Scaled spectral lower bounds (6.5)–(6.6): Unbounded relative Tomita/modular operators and spectral calculus (hard)
• Sufficient analytic moment condition for Stein: Reversed modular characteristic functions and W*-Stein families (hard)
• W*-open-system entropy production currents: W*-dynamics, relative Hamiltonians and normal-state FCS (hard)
• W*-FCS transient Evans–Searles symmetry: W*-dynamics, relative Hamiltonians and normal-state FCS (hard)
• W*-FCS long-time law and local deviations: Source-corrected scope/formula for W*-FCS long-time law and local deviations (source-ambiguity)
• Finite approximation yields physical FCS: W*-dynamics, relative Hamiltonians and normal-state FCS (hard)
• Explicit arrow-of-time concentration after Theorem 7.2: Source-corrected scope/formula for Explicit arrow-of-time concentration after Theorem 7.2 (source-ambiguity)
• Attainment interpretation of the Hoeffding bound: Source-corrected scope/formula for Attainment interpretation of the Hoeffding bound (source-ambiguity)
• Landauer–Buttiker energy and charge current limits (8.4): EBB CAR dynamics, wave operators and on-shell scattering matrix (hard)
• Theorem 8.3(1) independently valid thermodynamic conclusion: XY-chain finite-volume Hamiltonian, product Gibbs preparation and FCS cumulants (hard)

Selected references

• Quantum Hypothesis Testing and Non-Equilibrium Statistical Mechanics, arXiv:1109.3804v2, https://arxiv.org/abs/1109.3804v2

Motivation

In most communication schemes information is transmitted via travelling modes of electromagnetic radiation. These modes are unavoidably subject to environmental noise along any physical transmission medium and the quality of the communication channel strongly depends on the minimum noise achievable at the output. For classical signals such noise can be rigorously quantified in terms of the associated Shannon entropy and it is subject to a fundamental lower bound called entropy power inequality. Electromagnetic fields are however quantum mechanical systems and then, especially in low intensity signals, the quantum nature of the information carrier cannot be neglected and many important results derived within classical information theory require non-trivial extensions to the quantum regime. Here we prove one possible generalization of the Entropy Power Inequality to quantum bosonic systems. The impact of this inequality in quantum information theory is potentially large and some relevant implications are considered in this work.

This mission is the statement-level formalization of A generalization of the Entropy Power Inequality to Bosonic Quantum Systems (arXiv:1402.0404v2). 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 Three scalar thermal-entropy asymptotics (§IV.B Eq. (86); §VI.B Eqs. (103), (104), PDF p. 17). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §II Eqs. (3)–(5): Concrete arbitrary-n two-input beam-splitter output on full Fock coefficient densities; extended coefficient entropy is already available. (hard)
• §II Eqs. (6), (7): Full two-input n-mode squeezing channel on general density operators, including phase conjugation. (hard)
• §II observation following Eq. (5): n-mode Gaussian predicate and finite covariance on the same full-density mixing model. (hard)
• §II.A Eq. (9): Summed divergence-based displacement Fisher information with genuine derivative/extended-limit semantics. (hard)
• §II.A Eqs. (12), (13); §IV.A (38), (83); §VI.A (97): Weighted total divergence-based Fisher information on the physical beam-splitter and amplifier outputs. (hard)
• §II.B Eq. (19), proof §IV.B p.17: An unrestricted every-state entropy asymptotic, without adding a finite-covariance domain. (source-ambiguity)
• §II.B Eq. (22); §IV.A.1 Eq. (53), p.13: Full additive Gaussian noise map and both full-density mixing channels, characterized beyond moments. (hard)
• §II.C Eq. (33); §VI.A Eq. (90), p.22: Full squeezing output and its extended total n-mode entropy. (hard)
• §II.C Eq. (35); §VI.B Eqs. (101), (111), (112): Entropy photon number of the actual arbitrary-input beam-splitter output with infinite entropy allowed. (hard)
• §II.D observation and Fig. 2, p.11: An exact numerical bound and a specified decay domain for the plotted thermal-candidate gap. (source-ambiguity)
• §IV.A.2 Eqs. (64), (68), (69): n-mode quadrature displacement orbits and their actual relative-entropy second derivatives. (hard)
• §IV.A.3 Eqs. (70), (71), completed p.16: Full-density mixing and multimode Weyl displacements with the amplifier B-direction time reversal. (hard)
• §IV.A.3 Eqs. (81), (82), completed p.17: Directional, rather than merely summed, divergence-Fisher information for both physical output families. (hard)
• §IV.B Eqs. (85), (87): Finite quadrature moment/covariance interface and normalized heat-channel output in the accepted spectral state model. (hard)
• §IV.C Eq. (89), Fig. 3 p.19: Independent ordinary classical broadcast code region with full Fock block inputs and an unconditional per-use mean photon constraint. (hard)

Selected references

• A generalization of the Entropy Power Inequality to Bosonic Quantum Systems, arXiv:1402.0404v2, https://arxiv.org/abs/1402.0404v2

Motivation

We show that the cross Wigner function can be written in the form $W(\psi, \phi)= \hat S (\psi \otimes \overline{\hat\phi})$ where ${\hat\phi}$ is the Fourier transform of $\phi$ and $\hat S$ is a metaplectic operator that projects onto a linear symplectomorphism $S$ consisting of a rotation along an ellipse in phase space (or in the time-frequency space). This formulation can be extended to generic Weyl symbols and yields an interesting fractional generalization of the Weyl-Wigner formalism. It also provides a suitable approach to study the Bopp phase space representation of quantum mechanics, familiar from deformation quantization. Using the "metaplectic formulation" of the Wigner transform we construct a complete set of intertwiners relating the Weyl and the Bopp pseudo-differential operators. This is an important result that allows us to prove the spectral and dynamical equivalence of the Schr"odinger and the Bopp representations of quantum mechanics.

This mission is the statement-level formalization of Metaplectic formulation of the Wigner transform and applications (arXiv:1401.3388v1). 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 Periodicity, two elliptic invariants, and coordinate-pair rotations (Remark 5: periodicity and elliptic invariants, PDF p. 5). 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

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

• Theorem 7 / introductory main result: metaplectic Wigner formula: Independent cross-Wigner L2 extension, exterior L2 product, and canonical metaplectic evolution (hard)
• Theorem 4: special symplectic flow and metaplectic projection: Genuine metaplectic double cover, its projection, and the identity-based lift of the fixed Hamiltonian flow (hard)
• Lemma 6: Fourier-pullback formula for the unitary evolution: Canonical self-adjoint graph closure of the Schwartz quadratic realization and its spectral/Stone evolution (hard)
• Theorem 8: metaplectic formula for general Weyl symbols: Schwartz-kernel correspondence and independent distributional Weyl symbol (18) (hard)
• Unnumbered: periodic fractional family and its distinguished members: Printed 2theta0 endpoint conflicts with the fixed quadratic evolution; compatible all-L2 family is also unconstructed (source-ambiguity)
• Theorem 10: regularity of fractional cross Wigner functions: Jointly continuous distribution exterior product on strong duals and compatible S/L2/S-prime Wigner actions (hard)
• Unnumbered: fractional Moyal identity and window isometry: Printed order of the two window factors in the Moyal identity, plus the all-L2 fractional window (source-ambiguity)
• Unnumbered: fractional symbol of a rank-one operator: Rank-one Schwartz-to-distribution map for arbitrary L2 vectors and its computed fractional symbol (hard)
• Theorem 12: inversion, range projection, and distributional adjoint: Distributional transpose used by the printed extension (26) (source-ambiguity)
• Theorem 12, explicit Hilbert-space clauses (i),(ii) and adjoint (25): Actual fractional L2 window map, its bounded adjoint contraction, and projection onto its independently defined closed range (hard)
• Theorem 13: fractional kernel formula: Computed formal-adjoint kernel, fractional distributional symbols, and Schwartz-valued fractional Wigner test (hard)
• Unnumbered equations (31): transport between standard and fractional calculi: Compatible generic distributional symbol and all-L2 Wigner actions of U (hard)
• Theorem 14: fractional symbol of composition: Partially defined distributional Moyal composition on compatible operator-symbol pairs (hard)
• Unnumbered equation (33): algebraic properties of the fractional product: Composable domains for both associations and both distributive laws of the fractional product (hard)
• Unnumbered equations (34),(35): fractional adjoint and reflected-angle kernel formula: Printed parameter-reflection identity (34) is incompatible with conjugation of the fixed generator; generic symbol/kernel actions are also missing (source-ambiguity)
• Corollary 15: fractional observable expectation formula: Formal-self-adjoint generic operator, fractional distribution symbol, and its evaluation on a Schwartz Wigner function (hard)
• Unnumbered: standard and fractional position marginals: Printed inverse-U coefficient in the fractional marginal is not the required conjugate transformed symbol; delta-product and Wigner actions are also missing (source-ambiguity)
• Unnumbered equation (37): conjugation reflects the fractional parameter: Printed reflected-angle equality (37) fails for the actual quadratic evolution; compatible all-L2 family is also missing (source-ambiguity)
• Theorem 16: Weyl symbol of the phase-space extension: Distributional phase-space extension from the operator kernel and its computed double-phase Weyl symbol (hard)
• Theorem 20: exact Bopp Weyl symbol: Generic distributional Bopp operator and submersion pullback of an arbitrary tempered Weyl symbol (hard)
• Unnumbered main result: Weyl–Bopp intertwining relations: Compatible generic distributional Bopp operator, fixed-window isometries, transpose adjoints, and totality over windows (hard)
• Unnumbered final result: transfer of all spectral clauses of Theorem 17: Specified L2 realizations and eigenfunction domains for the generic operator and its Bopp counterpart (source-ambiguity)
• Unnumbered final result: transfer of both dynamical clauses of Theorem 18: Generic Bopp and window maps on S/S-prime, with the correctly extended adjoint for reverse solution transfer (hard)

Selected references

• Metaplectic formulation of the Wigner transform and applications, arXiv:1401.3388v1, https://arxiv.org/abs/1401.3388v1

Motivation

We consider a quantum generalization of the classical heat equation, and study contractivity properties of its associated semigroup. We prove a Nash inequality and a logarithmic Sobolev inequality. The former leads to an ultracontractivity result. This in turn implies that the largest eigenvalue and the purity of a state with positive Wigner function, evolving under the action of the semigroup, decrease at least inverse polynomially in time, while its entropy increases at least logarithmically in time.

This mission is the statement-level formalization of Contractivity properties of a quantum diffusion semigroup (arXiv:1607.04242v6). 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 Order comparison of second derivatives at a common zero minimum (Lemma 3 (Appendix C), PDF p. 29). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 1: Unbounded spectral functional calculus and state-weighted L2 space (hard)
• Theorem 3: Canonical n-mode trace-class diffusion and Hilbert-Schmidt generator domain (hard)
• Theorem 5: Schwartz densities, Wigner transform, and trace-class generator membership (hard)
• Theorem 6: Diffusion on Schwartz states and extended von Neumann entropy (hard)
• Theorem 7: Finite local Fisher derivatives for faithful Gaussian densities (hard)
• Theorem 8: Fisher information at nonfaithful Gaussian states (source-ambiguity)
• Theorem 9: Displacement Fisher information with output differentiability (hard)
• Theorem 10: Half-line second differentiability of Gaussian entropy power (hard)
• Lemma 2: Unbounded logarithms, double commutators and trace-class extensions (hard)
• Section 5, equations (5.2),(5.7)-(5.9): Operator/Fourier interface with the paper Wigner normalization (hard)
• Section 5, proof of Theorem 6: Purity curve of the actual canonical diffusion and its Dirichlet energy (hard)
• Appendix C, equation (C.1): Extended relative entropy of the fixed hybrid Weyl convolution (hard)
• Appendix C, equations (C.2),(C.6): Weakly measurable essentially bounded operator fields and normal product states (hard)

Selected references

• Contractivity properties of a quantum diffusion semigroup, arXiv:1607.04242v6, https://arxiv.org/abs/1607.04242v6

Motivation

We consider energy-constrained infinite-dimensional quantum channels from a given system (satisfying a certain condition) to any other systems. We show that dealing with basic capacities of these channels we may assume (accepting arbitrarily small error $\varepsilon$) that all channels have the same finite-dimensional input space -- the subspace corresponding to the $m(\varepsilon)$ minimal eigenvalues of the input Hamiltonian. We also show that for the class of energy-limited channels (mapping energy-bounded states to energy-bounded states) the above result is valid with substantially smaller dimension $m(\varepsilon)$. The uniform finite-dimensional approximation allows to prove the uniform continuity of the basic capacities on the set of all quantum channels with respect to the strong (pointwise) convergence topology. For all the capacities we obtain continuity bounds depending only on the input energy bound and the energy-constrained-diamond-norm distance between quantum channels (generating the strong convergence on the set of quantum channels).

This mission is the statement-level formalization of Uniform finite-dimensional approximation of basic capacities of energy-constrained channels (arXiv:1707.05641v2). 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 Monotonicity of the perspective of a nonnegative concave function (Lemma 1, 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

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

• Theorem 1: Actual Cchi, Cea, Qbar, Cpbar and regularized C,Q,Cp from Section 4.1: discrete ensembles constrained in average energy, genuine complementary channel/purification, all positive block lengths, additive Hamiltonians and tensor-power input-subspace restrictions. Finiteness must be established on the stated energy domain before taking real differences. (hard)
• Theorem 2: Actual Cchi, Cea, Qbar, Cpbar and regularized C,Q,Cp from Section 4.1: discrete ensembles constrained in average energy, genuine complementary channel/purification, all positive block lengths, additive Hamiltonians and tensor-power input-subspace restrictions. Finiteness must be established on the stated energy domain before taking real differences. Energy-constrained diamond distance as the supremum of the actual ancilla-amplified channel-difference trace norm over all normalized inputs of energy <= E; the induced metric uniformity and its strong-topology compatibility. (hard)
• Theorem 3: Actual Cchi, Cea, Qbar, Cpbar and regularized C,Q,Cp from Section 4.1: discrete ensembles constrained in average energy, genuine complementary channel/purification, all positive block lengths, additive Hamiltonians and tensor-power input-subspace restrictions. Finiteness must be established on the stated energy domain before taking real differences. Energy-constrained diamond distance as the supremum of the actual ancilla-amplified channel-difference trace norm over all normalized inputs of energy <= E; the induced metric uniformity and its strong-topology compatibility. (hard)
• Lemma 2: Actual extended QCMI on arbitrary complete separable tripartite spaces, using the finite-rank-compression supremum with homogeneous evaluation on subnormalized operators, and its compatibility with the trace-class state/channel model. Support-restricted extended mean energy on a common closed subspace of AD. (hard)
• Lemma 3: Actual relative-entropy mutual information on arbitrary block outputs and references, compatible tensor powers and the energy truncation map. (hard)
• Lemma 6: Actual block mutual information and energy-constrained diamond distance for energy-limited channels on arbitrary output/reference systems. (hard)
• Appendix Lemma 7: Actual extended QCMI on arbitrary complete separable tripartite spaces, using the finite-rank-compression supremum with homogeneous evaluation on subnormalized operators, and its compatibility with the trace-class state/channel model. Energy-constrained diamond distance as the supremum of the actual ancilla-amplified channel-difference trace norm over all normalized inputs of energy <= E; the induced metric uniformity and its strong-topology compatibility. (hard)
• Remark 1: Actual extended QCMI on arbitrary complete separable tripartite spaces, using the finite-rank-compression supremum with homogeneous evaluation on subnormalized operators, and its compatibility with the trace-class state/channel model. Arbitrary block channels and reference/conditioning systems with the input marginal-energy constraints of Lemma 3. (hard)

Selected references

• Uniform finite-dimensional approximation of basic capacities of energy-constrained channels, arXiv:1707.05641v2, https://arxiv.org/abs/1707.05641v2

Motivation

Unitary equivariance is a natural symmetry that occurs in many contexts in physics and mathematics. Optimization problems with such symmetry can often be formulated as semidefinite programs for a $d^{p+q}$-dimensional matrix variable that commutes with $U^{\otimes p} \otimes \bar{U}^{\otimes q}$, for all $U \in \mathrm{U}(d)$. Solving such problems naively can be prohibitively expensive even if $p+q$ is small but the local dimension $d$ is large. We show that, under additional symmetry assumptions, this problem reduces to a linear program that can be solved in time that does not scale in $d$, and we provide a general framework to execute this reduction under different types of symmetries. The key ingredient of our method is a compact parametrization of the solution space by linear combinations of walled Brauer algebra diagrams. This parametrization requires the idempotents of a Gelfand-Tsetlin basis, which we obtain by adapting a general method arXiv:1606.08900 inspired by the Okounkov-Vershik approach. To illustrate potential applications, we use several examples from quantum information: deciding the principal eigenvalue of a quantum state, quantum majority vote, asymmetric cloning and transformation of a black-box unitary. We also outline a possible route for extending our method to general unitary-equivariant semidefinite programs.

This mission is the statement-level formalization of Linear programming with unitary-equivariant constraints (arXiv:2207.05713v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2.2: equivariance characterized by the Choi commutator (Proposition 2.2: equivariance characterized by the Choi commutator, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 6.4 (seed p.1 abstract, formal statement pp.34–37): Unrestricted permutation-symmetry LP claim in Theorem 6.4 (source-ambiguity)
• Lemma 5.2: total JM eigenvalue on a canonical path idempotent: Shape-labelled physical isotypic projectors at every mixed-tower level (hard)
• Corollary 5.3: individual JM eigenvalues equal edge contents: Independent physical canonical path projectors (hard)
• §5.6, unnumbered: diagrammatic primitive central and canonical idempotents: Diagram multiplication/polynomial evaluation and independently labelled physical projectors (hard)
• §6.1.1, unnumbered: full Brauer symmetry gives scalar blocks: Mixed physical central-idempotent parametrization and admissible irrep count (hard)
• §6.1.2, unnumbered: GT symmetry gives the diagonal path ansatz: Canonical physical GT projector basis and dimensions (hard)
• §6.1.3, unnumbered: residual permutation-symmetry blocks and multiplicity-free regimes: Actual restriction modules and simultaneous unitary block intertwiner (hard)
• Proposition 6.2: q=1 symmetry makes coefficients depend only on the last edge: Last-edge-labelled canonical physical projectors for q=1 (hard)
• §6.3 proof, unnumbered explicit result: conversion with a constructed diagonal ansatz: Constructed diagrammatic idempotents, sparse syntax and counted source-model algorithm (hard)
• Remark 6.7: scalar variables and weighted partial-trace constraints: Constructed diagonal ansatz and exact weighted partial-trace constraint transport (hard)
• §7.1, unnumbered: threshold testing reduces to a central-idempotent LP: General induced spectrum law with a fixed-basis minimax model and central-weight objective transport (hard)
• Lemma B.1: permutation restriction is multiplicity-free for min(p,q)≤2: Physical mixed simple modules and their actual S_p×S_q restriction multiplicities (hard)
• Lemma B.2: permutation restriction is multiplicity-free for d=2: Actual restriction multiplicity for arbitrary p,q at d=2 (hard)
• Table 2: new numerical transposition values beyond previous work: Certified values or intervals for the new qutrit transposition SDP optima (source-ambiguity)
• Appendix D, unnumbered proposal: diagrammatic off-diagonal blocks: Correct off-diagonal diagram matrix units with nonzero pivots and consistent phases (source-ambiguity)

Selected references

• Linear programming with unitary-equivariant constraints, arXiv:2207.05713v2, https://arxiv.org/abs/2207.05713v2

Motivation

A nonprofit choosing how to serve people with different needs may have two ways to use an additional dollar: offer more product variants, or deliver a larger fraction of each product. Beneficiaries can sometimes finish an incomplete product themselves, but doing so takes effort. Zhang, Atasu and Ramachandran study this choice for services such as incremental housing and temporary shelter. The question is how a limited budget changes the optimal combination of variety and completion.

The paper’s main text first models the beneficiaries’ needs and the nonprofit’s costs, then derives the allocation pattern in Lemmas 1–2 and Proposition 3. This mission targets those results in the authors’ SSRN version. The optimization is over a continuous variety level, as the paper explicitly assumes in §4.2; the integer case has a different comparative static for completion at footnote 5 on p. 13.

Setting

A variety level $n\ge1$ describes how many equally spaced variants the nonprofit offers to a unit mass of beneficiaries with uniformly distributed ideal locations. The analysis treats $n$ as a real decision variable. A completion level $\alpha\in[0,1]$ is the fraction of each variant the nonprofit provides. Heterogeneity $\theta\in(0,2]$ reduces the utility of a complete variant with distance from a beneficiary’s ideal. Aggregating the closest variant’s utility gives $\alpha(1-\theta/(4n))$ §3, pp. 7–8.

Each beneficiary may complete at most $1-\alpha$ of the product. With quadratic effort cost $\beta e^2$, where $\beta>0$, optimal self-completion effort is $e^*(\alpha)=\min\{1/(2\beta),1-\alpha\}$. The nonprofit’s expenditure is $\alpha g(n)$, where $g(1)>0$, $g'(n)>0$, and $g''(n)\ge0$ for $n\ge1$. Its total net benefit is

$$W(n,\alpha)=\alpha\left(1-\frac{\theta}{4n}\right)-\alpha g(n)+e^*(\alpha)-\beta e^*(\alpha)^2.$$

At a budget $B\ge0$, a decision is feasible when $n\ge1$, $0\le\alpha\le1$, and $\alpha g(n)\le B$. An optimal decision is a feasible decision whose value of $W$ is at least that of every other feasible decision. Without the budget constraint, the same domain $n\ge1$, $\alpha\in[0,1]$ defines the unconstrained problem §3, p. 10 and §4.2, pp. 12–13.

The standing assumption that provision is worthwhile says some $n\ge1$ satisfies $g(n)<1-\theta/(4n)$. Let $n^*_{NB}$ be the unconstrained optimal variety: it is $1$ when $\theta/4\le g'(1)$; otherwise it is the solution above $1$ of $\theta/(4n^2)=g'(n)$. Write $\alpha^*_{NB}=\max\{1-[\theta/(4n^*_{NB})+g(n^*_{NB})]/(2\beta),0\}$ and $B_2=\alpha^*_{NB}g(n^*_{NB})$. These are the unconstrained completion level and the budget needed to afford that pair Lemma 1, p. 12.

Formalization targets

Lemma 1 asserts that $(n^*_{NB},\alpha^*_{NB})$ maximizes $W$ without a budget constraint. Lemma 2 says every optimal decision exhausts its budget below $B_2$:

$$0\le B<B_2\quad\Longrightarrow\quad\alpha^*g(n^*)=B.$$

Proposition 3 is the goal. It asserts thresholds $0\le B_1\le B_2$, a small-budget variety $n_0\ge1$, and middle-regime decisions such that an optimal pair can be selected as

$$(n^*,\alpha^*)= \begin{cases} (n_0,B/g(n_0)), & 0\le B<B_1,\\ (n_1(B),B/g(n_1(B))), & B_1\le B<B_2,\\ (n^*_{NB},\alpha^*_{NB}), & B\ge B_2. \end{cases}$$

Both $n_1(B)$ and $B/g(n_1(B))$ are nondecreasing on the middle interval, using the paper’s weak meaning of “increasing.” The goal characterizes $n_0$ using the appendix’s function $\Lambda_1(n)=-n(4n-\theta)g'(n)+\theta g(n)$: $n_0=1$ if $\Lambda_1(1)\le0$, and otherwise $n_0>1$ is its zero. It also requires $B_1\ge(1-1/(2\beta))g(n_0)$. These conditions retain the paper’s small-budget regime and prevent an arbitrary threshold from making it empty Proposition 3, p. 13; proof, Online Appendix p. 2.

Significance

The three regimes identify when a nonprofit should spend an increment of budget solely on completion, when variety and completion should rise together, and when additional budget no longer changes its choice. Lemma 1 also says that, even with ample funds, completing the entire product need not be optimal because beneficiaries can add value through their own effort §4.2, pp. 12–14.

The paper proves these claims analytically. This mission asks for machine-checked proofs of the continuous model’s optimization statements, including the attainment and feasibility of each claimed optimum. The reusable part is a compact interface for a two-variable budget-constrained optimization problem with a beneficiary best response. There is no existing machine-checked proof of these particular claims in the platform catalog at drafting time.

Difficulty

The binding-budget curve $\alpha=B/g(n)$ crosses the point $\alpha=1-1/(2\beta)$, where beneficiary effort changes formula. Thus optimizing a single smooth expression over all variety levels does not cover the problem. A stationary point calculated in one region also must be checked against feasible points in the other. The argument needs to establish global optimality and preserve the bounds $0\le\alpha\le1$ as the budget changes Online Appendix pp. 2–3.

The appendix’s candidate threshold in one case can exceed $B_2$ when the unconstrained variety is $1$. Proposition 3 itself asks only for a threshold $B_1\le B_2$, so the formal goal retains that existential form. The proof’s candidate must be capped at $B_2$ in that case; the middle interval can then be empty. This discrepancy is recorded for solvers, who should establish the proposition as stated rather than assume the appendix’s candidate always satisfies the bound Online Appendix p. 3.

Formalization scope

All quantities are real. The Lean model stores $g$, $g'$, and $g''$ as separate functions and requires the two derivative identities, positive $g'$ and nonnegative $g''$ for $n\ge1$. It uses the closed formula for $W$ and the minimum formula for effort. The hypotheses $\theta>0$, $\beta>0$, and $B\ge0$ make explicit the economic parameter and budget domains; $\theta>0$ is needed for the stated variety characterization, and $\beta>0$ is implicit in the paper’s increasing quadratic effort cost. The paper’s $g(1)>0$, $\theta\le2$, and worthwhile-provision assumption are retained.

Optimality always includes membership in the feasible set. This rules out an out-of-domain maximizer. The upper regime asserts that the displayed pair is an optimum, allowing other optima when $\alpha^*_{NB}=0$. Division by $n$ and $g(n)$ is used only at varieties $n\ge1$; the standing assumptions imply $g(n)>0$ there. The goal fixes $B_2$ by the paper’s formula and pins down $n_0$, so it cannot be discharged by choosing arbitrary empty budget ranges. Proofs of the two appendix monotonicity claims, the binding-budget lemma, and the global small-budget optimum are welcome along with the goal.

Selected references

• C. Zhang, A. Atasu and K. Ramachandran, Partial Completion as a Nonprofit Strategy, SSRN preprint 3684891, forthcoming in Manufacturing & Service Operations Management, 2021. SSRN.

Motivation

Electric vehicle adoption depends on both the number of drivers willing to buy a vehicle and the availability of places to charge it. These decisions reinforce one another: an additional charging pile reduces expected search cost, while an additional vehicle increases demand for charging. A city may subsidize the vehicle purchase, each charging session, or the construction of a pile. The instruments can have different effects even when the public spending they require is equal. Zhang and Dou study these tradeoffs in a two location market with different pile costs and charging inconvenience. Their 2021 paper gives conditions under which one subsidy has a greater marginal effect on gross social surplus than another.

The target here is the paper's Theorem 3. It addresses a local comparison of policy instruments at a given policy mix. It does not claim that a policy satisfying a condition is globally optimal or that the same ranking holds after a large change in subsidy.

Setting

There are two locations, A and B. A fraction $\eta$ of potential drivers resides at A and the remainder at B. Driver type $z\geq 0$ measures the annual benefit of using an electric vehicle. In the base model it has distribution $H(z)=1-e^{-az}$ for $z\geq 0$, with $a>0$. A vehicle costs $p$ per year, and each driver needs one charging session every $T$ years. A session occupies a pile for time $\tau$.

At location $i$, a session has regulated fee $f$, waiting cost $c_i\tau$, and expected search cost $s_i/(1-\rho_i)$ when expected pile utilization is $\rho_i$. Drivers at A charge at A. Drivers at B choose between the locations using the paper's logit probabilities $\phi_A(\rho)$ and $\phi_B(\rho)$; their expected cost is a log sum of the two location costs. The purchase threshold is $z_i^*(\rho)=p-\gamma+u_i^e(\rho)/T$, where $\gamma$ is the vehicle purchase subsidy. These thresholds, the purchase probabilities $1-H(z_i^*)$, and the choice probabilities determine the arrival rates $\lambda_A$ and $\lambda_B$.

Charging service providers choose piles $m_A,m_B$ per provider to maximize annual profit, taking expected utilization as fixed. The number of providers is $n$; a pile at $i$ costs $k_i$ annually. A policy $\omega=(\alpha_A,\alpha_B,\beta,\gamma)$ pays $\alpha_i$ per pile and $\beta$ per session, in addition to $\gamma$ per vehicle purchase. A rational expectations equilibrium matches each expected utilization $\xi_i$ with the actual ratio $\tau\lambda_i/(nm_i)$, while the provider's pile choices maximize profit. The mission uses the positive pile regime of the paper's equilibrium analysis. In it, Theorem 1 determines $\xi_i=(k_i-\alpha_i)\tau/(\beta+f)$.

Gross social surplus, denoted $GSS$, has three components in equation (8): the external benefit $\theta T(\lambda_A+\lambda_B)$, the integral of driver surplus above each purchase threshold, and provider surplus. The total subsidy value $S(\omega)$ and the government's objective $U_G=GSS-(1+\delta)S$ are represented separately. The goal compares derivatives of $GSS$ per equal increment in subsidy value, following the normalization in the proof of Theorem 3.

Formalization targets

Equilibrium and surplus identities

Theorem 1 asserts existence and uniqueness of the positive pile equilibrium. The proof of Theorem 3 also states that provider break even makes its gross social surplus equal to

$$GSS(\omega)=\left(\theta T+\frac{T}{a}\right)(\lambda_A+\lambda_B).$$

This is a theorem about the surplus defined by equation (8), not its definition. The milestone list also records the purchase subsidy derivative and bounds on the usage and pile subsidy derivatives given in the paper's technical proof.

Marginal subsidy comparison

The goal is Theorem 3. Write $k_As_A\geq k_Bs_B$. For a pile subsidy mix $(\alpha_A,\alpha_B,\gamma)$, a sufficient condition for the purchase subsidy to yield at least as much additional gross social surplus as the paper's pile subsidy direction at equal marginal spending, when the pair is balanced and the subsidies are nonnegative, is

$$\max_{i\in\{A,B\}} \frac{(k_i-\alpha_i)^2s_i\tau} {k_i[f-(k_i-\alpha_i)\tau]^2}\leq\mu.$$

For a nonnegative usage subsidy mix $(\beta,\gamma)$, a sufficient condition for usage subsidy to yield at least as much is

$$\frac{k_Bs_B\tau}{(\beta+f-k_B\tau)^2}\geq\mu.$$

Here $\mu$ is the efficiency of the vehicle purchase subsidy relative to subsidies paid to providers. The inequalities are local sufficient conditions; they make no claim about large policy changes.

Significance

The two conditions connect the subsidy ranking to pile cost, search cost, charging time, and subsidy efficiency. They identify parameter regimes in which a city can increase gross social surplus more through charging side support, or more through vehicle purchase support, at equal marginal subsidy value. This gives a precise comparison within the paper's model, complementing its separate results on spatial mismatch and policy optima. The source result and its proof are published in the authors' version; this mission asks for a machine checked formalization of that known result.

A complete development would also supply reusable results on the exponential tail integral, derivatives of logit choice probabilities, and the relationship between a profit maximizing provider choice and equilibrium utilization. Those statements are useful for other two sided adoption and infrastructure models that combine provider investment with consumer choice.

Difficulty

Changing a subsidy changes more than the direct transfer. It changes utilization, search costs, the logit split of B's charging sessions, vehicle purchase thresholds, and both arrival rates. A comparison that looks only at the direct increase in purchases misses the displacement of charging activity between A and B. The pile subsidy comparison is especially sensitive to the direction in which the two pile subsidies change: equal changes in $\alpha_A$ and $\alpha_B$ do not have equal marginal effects or equal costs. The equilibrium quantities must also be connected to the derivatives of the actual surplus expression rather than to an assumed closed form.

Formalization scope

The Lean model uses real valued parameters, policies, utilizations, arrival rates, and pile counts, with two explicit locations. It fixes $f_A=f_B=f$, as the base model does. The standing assumptions are $0<\eta<1$, $a,T,\tau,f,n>0$, $0<s_A\leq s_B$, $0\leq c_A\leq c_B$, $0<k_B<k_A$, $0<\mu\leq1$, and $\delta\geq0$. It also requires $\theta\geq0$: the externality is described as a benefit, and the derivative comparisons use its nonnegative contribution. The interior regime is $\alpha_i<k_i$ and $(k_i-\alpha_i)\tau<\beta+f$ at both locations. Positive purchase thresholds are required at derivative evaluation points because the exponential distribution has a boundary at zero.

Equation (10) is expressed by $\xi_i nm_i=\tau\lambda_i$, with utilization constrained below one. This excludes a division by zero that would otherwise create a false zero pile equilibrium in Lean. The distribution function is zero below zero. The subsidy value is $S=\sum_i\alpha_i nm_i+(\beta+T\gamma/\mu)\sum_i\lambda_i$, read from the proof's displayed derivatives on p. S10 and its treatment of pile subsidies on p. S9. The goal quantifies over every equilibrium selection on the interior regime and asserts such a selection exists. Its marginal comparisons use $d\gamma/d\beta=\mu/T$ and the pile subsidy direction $d\alpha_i=(k_i-\alpha_i)^2/(fk_i)\,dC$. A pile subsidy pair is balanced if no feasible nonnegative pair with the same equilibrium subsidy value yields higher gross social surplus. The goal requires this condition for the pile subsidy comparison and requires nonnegative subsidies at each policy mix.

The formalization must retain equation (8)'s driver surplus integral and provider surplus. Defining $GSS$ by the break even closed form would make the goal circular. Contributions on the source's integral, equilibrium existence, derivative bounds, and the connection to the selected equilibrium are within scope.

Selected references

• W. Zhang and Y. Dou, Coping with Spatial Mismatch: Subsidy Design for Electric Vehicle and Charging Markets, authors' SSRN version, 2021, pp. 7–19 and Online Supplement pp. S5–S11. SSRN 3336398.
• W. Zhang and Y. Dou, Coping with Spatial Mismatch: Subsidy Design for Electric Vehicle and Charging Markets, Manufacturing & Service Operations Management, 2021. DOI:10.1287/msom.2021.1017.

Motivation

Manufacturers of durable products — airlines' aircraft, consumer electronics, cars — increasingly hand the after-sales product service (help desks, repair, field maintenance) to a third-party provider. The provider is often more cost-efficient, and the brand can concentrate on its core product. The price of outsourcing is visibility: once the service is run by someone else, the brand no longer observes the service environment that drives the cost of serving customers, and it pays the provider on the basis of a belief that drifts away from reality as unobserved shocks accumulate.

Y. Wang, M. Li, N. Ma and H. Zhang (MSOM 2024, doi:10.1287/msom.2022.0222) model this trade-off with a martingale model of forecast evolution (MMFE, in the sense of Heath and Jackson 1994): the environment evolves by multiplicative mean-one lognormal shocks, and after outsourcing the brand stops seeing them. Their Proposition 4 shows that this loss of visibility alone — with no switching cost, a cheaper provider and a product-value gain — can make outsourcing unprofitable. The question belongs to the operations literature on service outsourcing under information asymmetry (e.g. Hasija, Pinker and Shumsky 2008; Feng, Ren and Zhang 2019).

Setting

A single service period is described by the following data.

• A resource level $k\ge 0$ yields expected customer satisfaction $\theta(k)=1-e^{-\lambda k}$, with $\lambda>0$.
• Maintaining level $k$ in-house in environment $d$ costs $c(k,d)=C\,k(1+\beta d)$, with base unit cost $C>0$ and environment sensitivity $\beta$. The provider's cost is $c^S(k,d)=\alpha\,c(k,d)$, with cost efficiency $0<\alpha\le 1$.
• The brand's revenue is $R(k)=v-\pi(1-\theta(k))$ under direct service and $R^o(k)=v^o-\pi(1-\theta(k))$ under outsourcing, where $\pi\ge 0$ is the expected penalty of an unsatisfied encounter and $v^o\ge v$ is the improved product value.
• Period profits: $G(k,d)=R(k)-c(k,d)$ (direct service) and $G^o(k,w)=R^o(k)-w$ (outsourced, with payment $w$).
• The brand fixes a target resource level $\bar k>0$ (a service level agreement).

Partial observability. The brand holds a belief $d^b>0$ about the environment. The true environment is $d=\xi\,d^b$, where the unobserved shock $\xi$ is lognormal with mean $1$ and variance parameter $s^2$ (the variance of $\ln\xi$). Equivalently, $\xi=\xi_s(Z)=\exp(sZ-s^2/2)$ with $Z\sim N(0,1)$.

Payment. Without reporting, learning or monitoring, the brand pays $w=c^S(\bar k,d^b)$; when the true environment exceeds the belief, the provider's participation constraint forces the payment up to $c^S(\bar k,d)$. With full observability the payment would be $c^S(\bar k,d)$ always.

Value of outsourcing. $\Delta(s)=\mathbb E\big[G^o(\bar k,w)-G(\bar k,d)\big]$, and $\Delta_{\mathrm{full}}(s)$ is the same expectation with the full-observability payment. The error function is $\operatorname{erf}(x)=\frac{2}{\sqrt\pi}\int_0^x e^{-t^2}dt$.

Formalization targets

Goal: Proposition 4

For all parameters satisfying the standing assumptions:

$$\Delta(s)=\Delta_{\mathrm{full}}(s)-\mathbb E\Big[\mathbf 1\{d\le d^b\}\big(c^S(\bar k,d^b)-c^S(\bar k,d)\big)\Big]\quad(s>0),$$

with a pointwise nonnegative loss term (part (a): only an upward drift of the belief matters);

$$s\mapsto \Delta(s)\ \text{is strictly decreasing on }(0,\infty)$$

(part (b)); and (part (c)) there exist admissible parameters with $\alpha<1$, $v<v^o$ and some $s>0$ such that $\Delta(s)<0$.

Milestones

1. Lemma 3(a): $\mathbb E[d]=d^b$, the belief is unbiased.
2. Lemma 3(b), eq. (10): $\mathbb P(d^b-d\ge X)=\tfrac12\big(1+\operatorname{erf}\big((\ln(1-X/d^b)+s^2/2)/(\sqrt2 s)\big)\big)$ for $X<d^b$.
3. Lemma 3(c): this probability is nondecreasing in $s$ for $X\ge 0$.
4. $\mathbb E[c^S(\bar k,d)]=c^S(\bar k,d^b)$ (proof of Proposition 4(a)).
5. $\mathbb E[c^S(\bar k,d^b)-c^S(\bar k,d)\mid d\le d^b]=\alpha C\beta\bar k d^b\Big(1-\frac{1-\operatorname{erf}(s/2\sqrt2)}{1-\operatorname{erf}(-s/2\sqrt2)}\Big)$ (proof of Proposition 4(c)).
6. That conditional loss tends to $\alpha C\beta\bar k d^b$ as $s\to\infty$.

Significance

The result. Proposition 4 separates two effects that are usually conflated in the outsourcing literature: environment uncertainty, which makes outsourcing more attractive (the provider absorbs a growing cost), and partial observability, which erodes its value. It shows that the second can dominate on its own: the value lost when the belief overshoots the true environment grows with the accumulated variance, and with a long enough relationship it wipes out both the provider's cost advantage and the product-value gain. This underpins the paper's later analysis of learning and monitoring (§5.1–§5.2), which are evaluated by how much of this loss they recover.

Formalizing it. The result is proved in the paper; nothing in it is machine-checked. The mission produces a checked version of the benchmark analysis with every hidden convention made explicit: the representation of the lognormal shock, the payment rule at the boundary, and the per-period reading of $\Delta$. Along the way it produces reusable facts about mean-one lognormals — the mean identity, the closed form of their lower tail and of their truncated first moment in terms of erf, and the monotonicity of the tail in the volatility — which recur wherever MMFE-type forecast evolution is used.

Difficulty

The model-level algebra is short; the work is in the probability. The parts of the argument that are not routine are:

• Eq. (10) and its derivative. The tail probability must be identified with the standard normal distribution function and rewritten through erf, and then differentiated in $s$ through a parametric integral whose integration bound moves with $s$. Mathlib has the Gaussian measure but no erf, so the connection must be built.
• The truncated moment. The conditional loss requires $\mathbb E[\xi_s\mathbf 1\{\xi_s\le 1\}]$ in closed form, a change-of-measure computation for the Gaussian density.
• Integrability bookkeeping. Every expectation in the statement is a Bochner integral, which is $0$ for a non-integrable integrand; each step must carry integrability of $\xi_s$ and of the piecewise payment.

The obvious shortcut — replacing $\Delta$ by an erf formula and proving monotonicity of erf — is exactly what the mission excludes: the closed form of $\Delta$ is not stated in the paper and must be derived from the model.

Formalization scope

All objects live in the namespace PSOutsourcing.PartialObs in one definitions file. Conventions committed to:

• All quantities are real numbers. Expectations are integrals against gaussianReal 0 1; the shock is xi s z = exp(s z − s²/2) and the true environment is xi s z * db.
• Standing assumptions: $C>0$, $\beta>0$, $0<\alpha\le1$, $\lambda>0$, $\pi\ge0$, $v\le v^o$, $\bar k>0$, $d^b>0$. The paper allows $\beta\ge0$; $\beta>0$ and $\bar k>0$ are added because otherwise nothing depends on the environment and part (b) fails.
• $\Delta$ is the expected per-period value of outsourcing in the §5 benchmark with fixed $\bar k$. The paper's $\Delta_i=V^{TS}_i(d^b_i,s_i)-V^{DS}_i(d_i)$ is not pinned down as a function of $s_i$, and its proof argues period by period; with $\bar k$ fixed no decision remains in a period.
• The tie $d=d^b$ (probability $0$) is assigned to the belief-payment side.
• Lemma 3(b) is stated for $X<d^b$ (Lean's Real.log 0 = 0 cannot express the paper's $\ln 0=-\infty$); Lemma 3(c) adds $X\ge 0$, which its proof uses; derivatives are stated with HasDerivAt.
• Part (b) is strict decrease in $s$ on $(0,\infty)$, equivalent to strict decrease in $s^2$.
• In part (c) the witness must have $\alpha<1$ and $v<v^o$; without these the claim would hold for an uninteresting reason (a provider no cheaper than in-house service).

A formalization in which $\Delta$ is defined by its closed form, or in which the payment ignores the participation constraint, trivializes the goal and is ruled out: $\Delta$ is the expectation of the period-profit difference under the stated payment rule.

Infrastructure needed: erf and its relation to the standard normal distribution function, the Gaussian moment generating function (Mathlib's mgf_gaussianReal), truncated lognormal moments, and differentiation of Gaussian tail probabilities in a parameter. These lemmas are reusable well beyond this mission, and contributions of them as standalone theorems are welcome.

Selected references

• Y. Wang, M. Li, N. Ma, H. Zhang, Product service outsourcing: impact of environment uncertainty and partial observability, Manufacturing & Service Operations Management, 2024. https://doi.org/10.1287/msom.2022.0222
• D. C. Heath, P. L. Jackson, Modeling the evolution of demand forecasts with application to safety stock analysis in production/distribution systems, IIE Transactions 26(3), 17–30, 1994. https://doi.org/10.1080/07408179408966604
• S. Hasija, E. J. Pinker, R. A. Shumsky, Call center outsourcing contracts under information asymmetry, Management Science 54(4), 793–807, 2008. https://doi.org/10.1287/mnsc.1070.0804
• T. Feng, Z. J. Ren, F. Zhang, Service outsourcing: capacity, quality and correlated costs, Production and Operations Management 28(3), 682–699, 2019. https://doi.org/10.1111/poms.12949

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.