All missions

Motivation

The applications of the general formulae of channel capacity developed in the quantum information theory to evaluation of information transmission capacity of optical channel are interesting subjects. In this review paper, we will point out that the formulation based on only classical-quantum channel mapping model may be inadequate when one takes into account a power constraint for noisy channel. To define the power constraint well, we should explicitly consider how quantum states are conveyed through a transmission channel. Basing on such consideration, we calculate a capacity formula for an attenuated noisy optical channel with genreral Gaussian state input; this gives certain progress beyond the example in our former paper.

This mission is the statement-level formalization of Information capacity formula of quantum optical channels (arXiv:quant-ph/0105042v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lossless number-state entropy maximum and capacity (Eqs.(58)-(59), PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Main result: transmitter-constrained squeezed-state optical capacity, original (53) and (56): A constructed fixed pure squeezed seed and its noisy attenuated displacement alphabet, with measurable modulation mixtures, raw transmitter photon accounting, and operational product-code capacity linked to both Gaussian covariance branches. (hard)
• Physical Gaussian reduction and attained covariance maximum, (47)–(49): The paper-specific measurable displaced-Gaussian family and raw-moment/covariance interface connecting arbitrary modulation laws to the attained output-covariance optimization in (48)-(49). (hard)
• Coherent-state specialization of the attenuated noisy capacity, (54): The constructed displaced thermal output family for coherent transmission through attenuation plus classical noise, and its transmitter-constrained operational classical coding capacity. (hard)
• Squeezing penalty within regime [A]: Physical fixed-seed capacities for the squeezed and coherent displacement alphabets with a common transmitter budget and the regime-(50) comparison. (hard)
• Photon-loss Holevo bounds in high/low photon regimes, (64)–(65): A quantitatively specified source assertion: Photon-loss Holevo bounds in high/low photon regimes, (64)–(65) (source-ambiguity)
• Approximate optimum binary single-symbol prior and amplitudes, (79)–(80): A quantitatively specified source assertion: Approximate optimum binary single-symbol prior and amplitudes, (79)–(80) (source-ambiguity)
• Single-symbol versus collective weak-energy comparison, (81): A quantitatively specified source assertion: Single-symbol versus collective weak-energy comparison, (81) (source-ambiguity)
• Three equal-angle qubit letters: numerical one-use capacity claim: A quantitatively specified source assertion: Three equal-angle qubit letters: numerical one-use capacity claim (source-ambiguity)
• Claim that no discrete channel simulates the classical continuous channel: A quantitatively specified source assertion: Claim that no discrete channel simulates the classical continuous channel (source-ambiguity)

Selected references

• Information capacity formula of quantum optical channels, arXiv:quant-ph/0105042v1, https://arxiv.org/abs/quant-ph/0105042v1

Motivation

We give two integrability criteria for representations of Banach--Lie algebras as skew-symmetric unbounded operators on a dense domain of a Hilbert space.

This mission is the statement-level formalization of Integrating representations of Banach--Lie algebras (arXiv:1003.0999v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Product rule for a strongly continuous operator path (Lemma 4, 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

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

• Theorem 1: Actual tangent Banach--Lie algebra identification for the given simply connected G, its exponential curves, smooth orbit maps on the SAME H, and the predicate D subset H-infinity with derived action exactly alpha on D. (hard)
• Corollary 2: Actual tangent Banach--Lie algebra identification for the given simply connected G, its exponential curves, smooth orbit maps on the SAME H, and the predicate D subset H-infinity with derived action exactly alpha on D. (hard)
• Corollary 3: Actual tangent Banach--Lie algebra identification for the given simply connected G, its exponential curves, smooth orbit maps on the SAME H, and the predicate D subset H-infinity with derived action exactly alpha on D. (hard)
• Corollary 8 and equation (3): Canonical intersection of FULL finite-composition domains of the closed operators, and alpha-prime computed from the unique ordered decomposition. (hard)
• Lemma 11: The actual locally convergent Dynkin BCH product on a symmetric starlike zero-neighbourhood, its chart-domain guards, and delta defined from the inverse differential of the actual right translation. (hard)
• Lemma 12: The actual locally convergent Dynkin BCH product on a symmetric starlike zero-neighbourhood, its chart-domain guards, and delta defined from the inverse differential of the actual right translation. (hard)
• Lemma 13: The actual locally convergent Dynkin BCH product on a symmetric starlike zero-neighbourhood, its chart-domain guards, and delta defined from the inverse differential of the actual right translation. (hard)
• Proposition 14: The actual locally convergent Dynkin BCH product on a symmetric starlike zero-neighbourhood, its chart-domain guards, and delta defined from the inverse differential of the actual right translation. Also the ordered local diffeomorphism F and its computed inverse components x_j(t). (hard)

Selected references

• Integrating representations of Banach--Lie algebras, arXiv:1003.0999v3, https://arxiv.org/abs/1003.0999v3

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