A Practical Quantum Algorithm for the Schur TransformResearch Paper
Motivation
We describe an efficient quantum algorithm for the quantum Schur transform. The Schur transform is an operation on a quantum computer that maps the standard computational basis to a basis composed of irreducible representations of the unitary and symmetric groups. We simplify and extend the algorithm of Bacon, Chuang, and Harrow, and provide a new practical construction as well as sharp theoretical and practical analyses. Our algorithm decomposes the Schur transform on n qubits into O(n4log(ϵn)) operators in the Clifford+T fault-tolerant gate set and uses exactly 2⌊log2(n)⌋−1 ancillary qubits. We extend our qubit algorithm to decompose the Schur transform on n qudits of dimension d into O(nd2+2logp(ϵnd2+1)) primitive operators from any universal gate set, for p≈3.97.
This mission is the statement-level formalization of A Practical Quantum Algorithm for the Schur Transform (arXiv:1709.07119v6). 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 Exact three-register Schur encoding space (§3.3 Eqs.(24)–(27), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
7 results of the paper are not stated yet, because the library lacks an interface they need:
Abstract; §4 Eqs.(35)–(36): A concrete source-compatible padded recursive Schur family together with a fixed-wire nuclear-norm H,T,CNOT compiler. (hard)
Erratum: The source recursive synthesis/analysis maps on fixed padded coordinates to which reversal can be attached. (hard)
§§3.1–3.3: Complete bodies for source spin-CG blocks, ancillary insertion and a compatible routing permutation including ghost coordinates at every stage. (hard)
§3 Eq.(19); §4 Eqs.(31)–(34): An exact shared-block program with matrix semantics tied to the source CG/routing construction. (hard)
§4 Eq.(34): A corrected source-endorsed refined polynomial in Eq.(34). (source-ambiguity)
§5 Eqs.(38)–(39); §6 item 3: A source-compatible general-d add-a-box encoding and exact shared CG-plus-routing program. (hard)
Abstract; §5 Eq.(40): The intended quantified class of qudit primitive alphabets and its synthesis/error convention. (source-ambiguity)
On the relation between states and maps in infinite dimensionsResearch Paper
Motivation
Relations between states and maps, which are known for quantum systems in finite-dimensional Hilbert spaces, are formulated rigorously in geometrical terms with no use of coordinate (matrix) interpretation. In a tensor product realization they are represented simply by a permutation of factors. This leads to natural generalizations for infinite-dimensional Hilbert spaces and a simple proof of a generalized Choi Theorem. The natural framework is based on spaces of Hilbert-Schmidt operators L2(H2,H1) and the corresponding tensor products H1⊗H2∗ of Hilbert spaces. It is proved that the corresponding isomorphisms cannot be naturally extended to compact (or bounded) operators, nor reduced to the trace-class operators. On the other hand, it is proven that there is a natural continuous map C:L1(L2(H2,H1))→L∞(L(H2),L1(H1)) from trace-class operators on L2(H2,H1) (with the nuclear norm) into compact operators mapping the space of all bounded operators on H2 into trace class operators on H1 (with the operator-norm). Also in the infinite-dimensional context, the Schmidt measure of entanglement and multipartite generalizations of state-maps relations are considered in the paper.
This mission is the statement-level formalization of On the relation between states and maps in infinite dimensions (arXiv:0706.2617v1). 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 Finite-dimensional Jamiolkowski permutations are unitary and equivariant (Theorem 1; equations (12)–(17), PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
15 results of the paper are not stated yet, because the library lacks an interface they need:
§3, unnumbered construction (18)–(19): Complete Hilbert–Schmidt operator Hilbert space with bounded-operator realization and canonical conjugate-dual tensor equivalence (hard)
Proposition 1, (20)–(23): Matrix-element and four-factor pairing characterization with uniqueness for both completed B2 permutations (hard)
Example 1, (24)–(28): Hilbert–Schmidt sandwich superoperators and their rank-one J images (hard)
Proposition 2; examples on pp.9–10: Operator-norm compact extensions and failure of trace-class restriction for J and its inverse (hard)
Theorem 2, (29): Trace-norm Banach space of nuclear operators on B2 and the compact bounded-to-trace-class Choi operator (hard)
§3, state-to-Kraus conclusion: Density operators on B2 and nuclear-norm convergent Kraus sums under C (hard)
Theorem 3: Adjoint on the realized B2 Hilbert space and J Hermiticity criterion (hard)
Theorem 4; proof p.14: Positive cone on B2 inputs, countably separable density ensembles, and trace tests of J (hard)
Theorem 5; proof (33)–(35): Positivity of finite identity amplifications and fixed injective positive Hilbert–Schmidt Kraus amplifications (hard)
Squashed entanglement for multipartite states and entanglement measures based on the mixed convex roofResearch Paper
Motivation
New measures of multipartite entanglement are constructed based on two definitions of multipartite information and different methods of optimizing over extensions of the states. One is a generalization of the squashed entanglement where one takes the mutual information of parties conditioned on the state's extension and takes the infimum over such extensions. Additivity of the multipartite squashed entanglement is proved for both versions of the multipartite information which turn out to be related. The second one is based on taking classical extensions. This scheme is generalized, which enables to construct measures of entanglement based on the {\it mixed convex roof} of a quantity, which in contrast to the standard convex roof method involves optimization over all decompositions of a density matrix rather than just the decompositions into pure states. As one of the possible applications of these results we prove that any multipartite monotone is an upper bound on the amount of multipartite distillable key. The findings are finally related to analogous results in classical key agreement.
This mission is the statement-level formalization of Squashed entanglement for multipartite states and entanglement measures based on the mixed convex roof (arXiv:0704.2236v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
19 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 4 / abstract: additivity of both multipartite q-squashed entanglements (Proposition 4 / abstract: additivity of both multipartite q-squashed entanglements, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
12 results of the paper are not stated yet, because the library lacks an interface they need:
Theorem 2: axiomatic quantum upper bound on distillable key: Unrestricted multipartite pdit distillation protocols, operational key capacity, and communication accounting (hard)
Example 1 / equation (75): normalized q-squashed key upper bound: Unrestricted multipartite pdit distillation protocols, operational key capacity, and communication accounting (hard)
Theorem 3 [13]: multipartite Devetak–Winter protocol (cited/background): Classicalization and preprocessing assumptions absent from the printed Devetak–Winter rate (source-ambiguity)
Lemma 3 and Remarks 1–2: communication and output support bounds: Correct support-space dimension and uniform dependence of the communication constant (source-ambiguity)
§V.C: unrestricted key-rate supremum equals linear-communication supremum: Unrestricted multipartite pdit distillation protocols, operational key capacity, and communication accounting (hard)
Theorem 4: axiomatic classical upper bound on distillable key: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
§V.D: linear-communication classical protocols suffice: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
Example 2 / equations (89)–(90): total intrinsic information bounds classical key: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
Example 3 / equations (91)–(92): dual intrinsic information bounds classical key: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
§VI: arbitrary convex extension-set claim (source ambiguity): Admissibility and local-operation/flag closure of an arbitrary convex extension family (source-ambiguity)
§VI: regularized mixed roof of I_c upper-bounds key: Multipartite I_c and private-state normalization of its regularized mixed roof (source-ambiguity)
Selected references
Squashed entanglement for multipartite states and entanglement measures based on the mixed convex roof, arXiv:0704.2236v3, https://arxiv.org/abs/0704.2236v3
Ramp-up of Hawking radiation in Bose-Einstein condensate analogue black holesResearch Paper
Motivation
Inspired by a recent experiment by Steinhauer and co-workers, we present a simple model which describes the formation of an acoustic black hole in a Bose-Einstein condensate, allowing an analytical computation of the evolution in time of the corresponding density-density correlator. We show the emergence of analog Hawking radiation out of a "quantum atmosphere" region significantly displaced from the horizon. This is quantitatively studied both at T=0 and even in the presence of an initial temperature T, as is always the case experimentally.
This mission is the statement-level formalization of Ramp-up of Hawking radiation in Bose-Einstein condensate analogue black holes (arXiv:2005.04443v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Sonic horizon and the two flow regions (Following (4), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
8 results of the paper are not stated yet, because the library lacks an interface they need:
Abstract and conclusion: Spatial origin in a significantly displaced quantum atmosphere (source-ambiguity)
Figures 2--4 and accompanying discussion: Vacuum ramp-up and finite-distance valley location (source-ambiguity)
Text following Figure 4: Length of the observed peak (source-ambiguity)
Comparison at T=TH following (20): Noticeable difference between T=TH and vacuum evolution (source-ambiguity)
Figure 5 and accompanying text: Finite-time appearance and thermal ramp-up delay (source-ambiguity)
Prose after incoming stationary-limit discussion: Positive thermal incoming contribution and smaller-than-outgoing comparison (source-ambiguity)
Example x=-xp=10 and following sentence: Smallness and one-order-of-magnitude thermal comparison (source-ambiguity)
Conclusion, reported onset scales: Observed onset times and atmosphere distance (source-ambiguity)
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOLResearch Paper
Motivation
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.
This mission is the statement-level formalization of A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL (arXiv:2209.10978v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The coefficient-sum conversion equals the canonical univariate conversion (§3.3: lemma multivar_as_univar, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Deferred results
10 results of the paper are not stated yet, because the library lacks an interface they need:
The Real Symplectic Groups in Quantum Mechanics and OpticsResearch Paper
Motivation
text of abstract (We present a utilitarian review of the family of matrix groups Sp(2n,ℜ), in a form suited to various applications both in optics and quantum mechanics. We contrast these groups and their geometry with the much more familiar Euclidean and unitary geometries. Both the properties of finite group elements and of the Lie algebra are studied, and special attention is paid to the so-called unitary metaplectic representation of Sp(2n,ℜ). Global decomposition theorems, interesting subgroups and their generators are described. Turning to n-mode quantum systems, we define and study their variance matrices in general states, the implications of the Heisenberg uncertainty principles, and develop a U(n)-invariant squeezing criterion. The particular properties of Wigner distributions and Gaussian pure state wavefunctions under Sp(2n,ℜ) action are delineated.)
This mission is the statement-level formalization of The Real Symplectic Groups in Quantum Mechanics and Optics (arXiv:quant-ph/9509002v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
What is formalized
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §IV (4.20): Euler decomposition (seed paper result) (§IV (4.20): Euler decomposition (seed paper result), PDF p. 16). 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:
§II and VIII: canonical translations and first moments: Finite-second-moment domain and trace pairing for arbitrary mixed densities on concrete L2 (hard)
§IV (4.1)(i): dimension of Sp: Compatible smooth real Lie-group charts on the actual symplectic matrix subgroup (hard)
§V (5.6)–(5.8): split brackets and subgroup generators: Intrinsic subgroup Lie algebras and images of their generators in arbitrary representations (hard)
§V: finite-dimensional nonunitarity and compact adaptation: Continuous finite-dimensional group representations and a derived Cartan-adapted positive Hermitian form (hard)
§VI (6.2)–(6.4): quadratic generators and photon number: Self-adjoint closures of quadratic oscillator generators and the total photon-number operator (hard)
§XII: Gaussian pure-state rays as Sp/U(n): Descended Sp/K conjugation action on concrete Gaussian rank-one L2 projectors (hard)
§XII (12.8)–(12.11): exactly which Gaussians are Wigner distributions: Positive trace-class density realizing an arbitrary normalized Gaussian Wigner function (hard)
We introduce a Gaussian version of the entanglement of formation adapted to bipartite Gaussian states by considering decompositions into pure Gaussian states only. We show that this quantity is an entanglement monotone under Gaussian operations and provide a simplified computation for states of arbitrary many modes. For the case of one mode per site the remaining variational problem can be solved analytically. If the considered state is in addition symmetric with respect to interchanging the two modes, we prove additivity of the considered entanglement measure. Moreover, in this case and considering only a single copy, our entanglement measure coincides with the true entanglement of formation.
This mission is the statement-level formalization of Gaussian Entanglement of Formation (arXiv:quant-ph/0306177v2). 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 Parametrization of pure Gaussian covariance matrices (Lemma 1, Eq.(16), 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
13 results of the paper are not stated yet, because the library lacks an interface they need:
Prop. 1: Gaussian ensemble roof equals pure covariance optimization: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. (hard)
Lemma 2: a real pure Gaussian optimizer exists: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. (hard)
Prop. 2: symmetric two-mode formula, with explicit convention correction: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. (hard)
Prop. 3: additivity for finite products of symmetric states: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. The joint roof must permit correlated decompositions of arbitrary finite products, rather than being defined as the sum of factor roofs. (hard)
§IV: monotonicity under Gaussian LOCC: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. Operational GLOCC also requires local Gaussian instruments and classical communication; it cannot be defined as the class of maps that decrease E_G. (hard)
Section II, Eq.(4) and preparation paragraph: CM/mean-normalized actual multimode Gaussian densities and tensor-local bounded Weyl displacements with measurable integrable operator barycentres. (hard)
§V, Eqs.(26)–(30): attained determinant optimization: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. The headline includes the value of the actual ensemble roof, attainment, and existence of a common-boundary optimizer; the matrix minimum alone would be incomplete. (hard)
§§I,VI,IX: E_G upper-bounds E_F: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. The unrestricted pure-state roof must be independent as well, and must retain non-Gaussian continuous ensembles. (hard)
§VI: no loss of negativity in the symmetric optimum: An integrated full finite-mode Gaussian-density realization, actual normalized reduction, trace-norm measurable pure-Gaussian ensembles, and independently defined von Neumann ensemble roof in bits. (hard)
§VI: claimed strict negativity gap for nonsymmetric states: A precise valid quantitative domain and conclusion for the printed qualitative or strict claim. (source-ambiguity)
§VIII: optical distribution comparison at zero temperature: A precise valid quantitative domain and conclusion for the printed qualitative or strict claim. (source-ambiguity)
§VIII: qualitative finite-temperature crossover: A precise valid quantitative domain and conclusion for the printed qualitative or strict claim. (source-ambiguity)
§VIII: qualitative diminishing return of initial squeezing: A precise valid quantitative domain and conclusion for the printed qualitative or strict claim. (source-ambiguity)
Information capacity formula of quantum optical channelsResearch Paper
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)
Integrating representations of Banach--Lie algebrasResearch Paper
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)
Quantum Hypothesis Testing and Non-Equilibrium Statistical MechanicsResearch Paper
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)
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)
A generalization of the Entropy Power Inequality to Bosonic Quantum SystemsResearch Paper
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)
Metaplectic formulation of the Wigner transform and applicationsResearch Paper
Motivation
We show that the cross Wigner function can be written in the form W(ψ,ϕ)=S^(ψ⊗ϕ^) where ϕ^ is the Fourier transform of ϕ and 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 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)
Contractivity properties of a quantum diffusion semigroupResearch Paper
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)
Uniform finite-dimensional approximation of basic capacities of energy-constrained channelsResearch Paper
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 ε) that all channels have the same finite-dimensional input space -- the subspace corresponding to the m(ε) 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(ε). 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
Linear programming with unitary-equivariant constraintsResearch Paper
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 dp+q-dimensional matrix variable that commutes with U⊗p⊗Uˉ⊗q, for all U∈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:
§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)
Partial Completion as a Nonprofit Strategy: Under a Budget Constraint, the Optimal Variety and Completion Levels Follow Three Budget Regimes and Both Rise With the BudgetResearch Paper
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 leveln≥1 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α∈[0,1] is the fraction of each variant the nonprofit provides. Heterogeneity θ∈(0,2] reduces the utility of a complete variant with distance from a beneficiary’s ideal. Aggregating the closest variant’s utility gives α(1−θ/(4n))§3, pp. 7–8.
Each beneficiary may complete at most 1−α of the product. With quadratic effort cost βe2, where β>0, optimal self-completion effort is e∗(α)=min{1/(2β),1−α}. The nonprofit’s expenditure is αg(n), where g(1)>0, g′(n)>0, and g′′(n)≥0 for n≥1. Its total net benefit is
W(n,α)=α(1−4nθ)−αg(n)+e∗(α)−βe∗(α)2.
At a budget B≥0, a decision is feasible when n≥1, 0≤α≤1, and αg(n)≤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≥1, α∈[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≥1 satisfies g(n)<1−θ/(4n). Let nNB∗ be the unconstrained optimal variety: it is 1 when θ/4≤g′(1); otherwise it is the solution above 1 of θ/(4n2)=g′(n). Write αNB∗=max{1−[θ/(4nNB∗)+g(nNB∗)]/(2β),0} and B2=αNB∗g(nNB∗). These are the unconstrained completion level and the budget needed to afford that pair Lemma 1, p. 12.
Formalization targets
Lemma 1 asserts that (nNB∗,αNB∗) maximizes W without a budget constraint. Lemma 2 says every optimal decision exhausts its budget below B2:
0≤B<B2⟹α∗g(n∗)=B.
Proposition 3 is the goal. It asserts thresholds 0≤B1≤B2, a small-budget variety n0≥1, and middle-regime decisions such that an optimal pair can be selected as
Both n1(B) and B/g(n1(B)) are nondecreasing on the middle interval, using the paper’s weak meaning of “increasing.” The goal characterizes n0 using the appendix’s function Λ1(n)=−n(4n−θ)g′(n)+θg(n): n0=1 if Λ1(1)≤0, and otherwise n0>1 is its zero. It also requires B1≥(1−1/(2β))g(n0). 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 α=B/g(n) crosses the point α=1−1/(2β), 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≤α≤1 as the budget changes Online Appendix pp. 2–3.
The appendix’s candidate threshold in one case can exceed B2 when the unconstrained variety is 1. Proposition 3 itself asks only for a threshold B1≤B2, so the formal goal retains that existential form. The proof’s candidate must be capped at B2 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≥1. It uses the closed formula for W and the minimum formula for effort. The hypotheses θ>0, β>0, and B≥0 make explicit the economic parameter and budget domains; θ>0 is needed for the stated variety characterization, and β>0 is implicit in the paper’s increasing quadratic effort cost. The paper’s g(1)>0, θ≤2, 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 αNB∗=0. Division by n and g(n) is used only at varieties n≥1; the standing assumptions imply g(n)>0 there. The goal fixes B2 by the paper’s formula and pins down n0, 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.
Coping with Spatial Mismatch: Subsidy Design for Electric Vehicle and Charging Markets: Charging-Cost Conditions Under Which EV-Purchase or Charging-Side Subsidies Are Marginally More EffectiveResearch Paper
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 η of potential drivers resides at A and the remainder at B. Driver type z≥0 measures the annual benefit of using an electric vehicle. In the base model it has distribution H(z)=1−e−az for z≥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 τ.
At location i, a session has regulated fee f, waiting cost ciτ, and expected search cost si/(1−ρi) when expected pile utilization is ρi. Drivers at A charge at A. Drivers at B choose between the locations using the paper's logit probabilities ϕA(ρ) and ϕB(ρ); their expected cost is a log sum of the two location costs. The purchase threshold is zi∗(ρ)=p−γ+uie(ρ)/T, where γ is the vehicle purchase subsidy. These thresholds, the purchase probabilities 1−H(zi∗), and the choice probabilities determine the arrival rates λA and λB.
Charging service providers choose piles mA,mB per provider to maximize annual profit, taking expected utilization as fixed. The number of providers is n; a pile at i costs ki annually. A policyω=(αA,αB,β,γ) pays αi per pile and β per session, in addition to γ per vehicle purchase. A rational expectations equilibrium matches each expected utilization ξi with the actual ratio τλi/(nmi), 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 ξi=(ki−αi)τ/(β+f).
Gross social surplus, denoted GSS, has three components in equation (8): the external benefit θT(λA+λB), the integral of driver surplus above each purchase threshold, and provider surplus. The total subsidy value S(ω) and the government's objective UG=GSS−(1+δ)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(ω)=(θT+aT)(λA+λ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 kAsA≥kBsB. For a pile subsidy mix (αA,αB,γ), 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
i∈{A,B}maxki[f−(ki−αi)τ]2(ki−αi)2siτ≤μ.
For a nonnegative usage subsidy mix (β,γ), a sufficient condition for usage subsidy to yield at least as much is
(β+f−kBτ)2kBsBτ≥μ.
Here μ 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 αA and α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 fA=fB=f, as the base model does. The standing assumptions are 0<η<1, a,T,τ,f,n>0, 0<sA≤sB, 0≤cA≤cB, 0<kB<kA, 0<μ≤1, and δ≥0. It also requires θ≥0: the externality is described as a benefit, and the derivative comparisons use its nonnegative contribution. The interior regime is αi<ki and (ki−αi)τ<β+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 ξinmi=τλ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=∑iαinmi+(β+Tγ/μ)∑iλ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γ/dβ=μ/T and the pile subsidy direction dαi=(ki−αi)2/(fki)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.
Product Service Outsourcing: Impact of Environment Uncertainty and Partial Observability: The Value of Outsourcing Strictly Declines in the Partial-Observability Variance and Can Be Strictly NegativeResearch Paper
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≥0 yields expected customer satisfaction θ(k)=1−e−λk, with λ>0.
Maintaining level k in-house in environment d costs c(k,d)=Ck(1+βd), with base unit cost C>0 and environment sensitivity β. The provider's cost is cS(k,d)=αc(k,d), with cost efficiency0<α≤1.
The brand's revenue is R(k)=v−π(1−θ(k)) under direct service and Ro(k)=vo−π(1−θ(k)) under outsourcing, where π≥0 is the expected penalty of an unsatisfied encounter and vo≥v is the improved product value.
Period profits: G(k,d)=R(k)−c(k,d) (direct service) and Go(k,w)=Ro(k)−w (outsourced, with payment w).
The brand fixes a target resource levelkˉ>0 (a service level agreement).
Partial observability. The brand holds a belief db>0 about the environment. The true environment is d=ξdb, where the unobserved shock ξ is lognormal with mean 1 and variance parameters2 (the variance of lnξ). Equivalently, ξ=ξs(Z)=exp(sZ−s2/2) with Z∼N(0,1).
Payment. Without reporting, learning or monitoring, the brand pays w=cS(kˉ,db); when the true environment exceeds the belief, the provider's participation constraint forces the payment up to cS(kˉ,d). With full observability the payment would be cS(kˉ,d) always.
Value of outsourcing.Δ(s)=E[Go(kˉ,w)−G(kˉ,d)], and Δfull(s) is the same expectation with the full-observability payment. The error function is erf(x)=π2∫0xe−t2dt.
Formalization targets
Goal: Proposition 4
For all parameters satisfying the standing assumptions:
with a pointwise nonnegative loss term (part (a): only an upward drift of the belief matters);
s↦Δ(s)is strictly decreasing on (0,∞)
(part (b)); and (part (c)) there exist admissible parameters with α<1, v<vo and some s>0 such that Δ(s)<0.
Milestones
Lemma 3(a): E[d]=db, the belief is unbiased.
Lemma 3(b), eq. (10): P(db−d≥X)=21(1+erf((ln(1−X/db)+s2/2)/(2s))) for X<db.
Lemma 3(c): this probability is nondecreasing in s for X≥0.
E[cS(kˉ,d)]=cS(kˉ,db) (proof of Proposition 4(a)).
E[cS(kˉ,db)−cS(kˉ,d)∣d≤db]=αCβkˉdb(1−1−erf(−s/22)1−erf(s/22)) (proof of Proposition 4(c)).
That conditional loss tends to αCβkˉdb as s→∞.
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 Δ. 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 E[ξs1{ξs≤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 ξs and of the piecewise payment.
The obvious shortcut — replacing Δ by an erf formula and proving monotonicity of erf — is exactly what the mission excludes: the closed form of Δ 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, β>0, 0<α≤1, λ>0, π≥0, v≤vo, kˉ>0, db>0. The paper allows β≥0; β>0 and kˉ>0 are added because otherwise nothing depends on the environment and part (b) fails.
Δ is the expected per-period value of outsourcing in the §5 benchmark with fixed kˉ. The paper's Δi=ViTS(dib,si)−ViDS(di) is not pinned down as a function of si, and its proof argues period by period; with kˉ fixed no decision remains in a period.
The tie d=db (probability 0) is assigned to the belief-payment side.
Lemma 3(b) is stated for X<db (Lean's Real.log 0 = 0 cannot express the paper's ln0=−∞); Lemma 3(c) adds X≥0, which its proof uses; derivatives are stated with HasDerivAt.
Part (b) is strict decrease in s on (0,∞), equivalent to strict decrease in s2.
In part (c) the witness must have α<1 and v<vo; without these the claim would hold for an uninteresting reason (a provider no cheaper than in-house service).
A formalization in which Δ is defined by its closed form, or in which the payment ignores the participation constraint, trivializes the goal and is ruled out: Δ 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
A Class of Dissimilarity Semimetrics for Preference Relations: Axiomatic Characterization of the µ-Top-Difference Semimetrics on Acyclic OrdersResearch Paper
Motivation
How far apart are two preferences? Distance functions on preference relations are used to deduce a consensus ranking from a collection of individual preferences. The classical answer is the Kemeny–Snell metric (Kemeny and Snell 1962), proposed axiomatically for linear orders and extended by Bogart (1973) to partial orders. It counts rank reversals between two orders and weighs all of them equally: swapping the two best alternatives costs as much as swapping the two worst.
For a decision maker who chooses from menus, these swaps are not equivalent. A disagreement at the top of the ranking changes what is chosen from many menus; one at the bottom changes almost nothing. Weighted Kendall-type metrics on linear orders (Can 2014; Hassanzadeh and Milenkovic 2014) were proposed for this reason, but they live only on linear orders. Nishimura and Ok (2022) instead compare two preferences by the sets of maximal elements they select in every menu. Their domain is the set of acyclic orders, which contains linear orders, partial orders, preorders and the non-transitive acyclic relations that arise as revealed preferences. Their main result, Theorem 3.1, is an axiomatic characterization of this family of semimetrics.
Setting
Let X be a nonempty finite set of alternatives. For a binary relation R on X, the asymmetric partR> is defined by xR>y iff xRy and not yRx, and the symmetric part is R∖R>. R is an acyclic order if it is reflexive and there is no cycle z1R>z2R>⋯R>zkR>z1 of pairwise distinct elements. The set of all acyclic orders is A(X). A generic acyclic order is written ≿, with strict part ≻ and symmetric part ∼; a second one is ⊵, with strict part ⊳. For S⊆X, the set of maximal elements is
M(S,≿)={x∈S:y≻xfor noy∈S}.
For a positive (possibly zero) measure μ on 2X, the μ-top-difference semimetric is
Dμ(≿,⊵)=S⊆X∑μ(M(S,≿)△M(S,⊵)).
The axioms use elementary perturbations. For distinct a,b not comparable by ≻, the single addition≿⊕(a,b) makes a strictly better than b. It is ≿⊔{(a,b)} when a,b are ≿-incomparable and ≿∖{(b,a)} when a∼b, and it is admitted only when the result is acyclic. For a≻b, the single deletion is ≿⊖(a,b)=≿∖{(a,b)}. An acyclic ≿0 is a one-step perturbation of ≿ toward ⊵, written ≿→≿0↠⊵, in either of two cases:
(i) ≿0=≿⊖(a,b) for some a≻b with not a⊳b, and consistency condition (2) holds: every x with x⊳b already has x≻b;
(ii) ≿0=≿⊕(a,b) for some a,b not ≻-comparable with a⊳b.
An order is in-between≿ and ⊵ if it is reached from ≿ by a finite nonempty chain of one-step perturbations toward ⊵.
For distinct a,b, the partial order ≿ab ranks every alternative other than a,b strictly above both a and b and makes no other comparisons, and ≿ab+ adds a≻b. Put N(b,≿)=∣{x∈X∖{b}:not x≻b}∣. For a semimetric d on A(X) with values in [0,∞):
Axiom 1: if ≿0 is in-between ≿ and ⊵, then d(≿,⊵)=d(≿,≿0)+d(≿0,⊵).
Axiom 3: if a,b are not ≻-comparable, d(≿,≿⊕(a,b))=2N(b,≿)−1d(≿ab,≿ab+); if a≻b, d(≿,≿⊖(a,b))=2N(b,≿)d(≿ab,≿ab+).
Axiom 4: if ≻=⊳, then d(≿,⊵)=0.
Formalization targets
Goal: Theorem 3.1 (p. 15)
For every nonempty finite X and every semimetric d on A(X),
d satisfies Axioms 1, 3, 4⟺∃μ≥0 on 2X:d=Dμ on A(X)×A(X).
Milestones
The "if" direction:
Dμ is a semimetric (§3.1, p. 12);
Lemma 3.3 (p. 16): along ≿→≿0↠⊵, the sets M(S,≿)△M(S,≿0) and M(S,≿0)△M(S,⊵) are disjoint, with union M(S,≿)△M(S,⊵);
Theorem 2.2 (p. 11): distinct acyclic orders with equal symmetric parts are joined by finitely many one-step perturbations;
Lemma 3.4 (p. 17): under Axioms 1 and 3, d(≿ab,≿ab+) does not depend on a;
with μ{b}=d(≿ab,≿ab+): d=Dμ on single additions and deletions (p. 17), and on pairs with equal symmetric parts (pp. 17–18).
Significance
Theorem 3.1 gives a complete description of a family of preference distances that is sensitive to where in a ranking two preferences disagree. The weight 2N(b,≿) in Axiom 3 is the number of menus in which a change at b is visible. Taking μ to be the counting measure gives the top-difference semimetricD (Theorem 3.2, with the normalization Axiom 2). The paper then uses Dμ to compute diameters of classes of orders, to find best transitive approximations of acyclic preferences, and to compare with weighted Kendall metrics. All of these rest on the additivity (Axiom 1) and on the perturbation calculus of §2.3.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. The mission formalizes the definitions and the proof's structure: the reachability theorem for acyclic orders (Theorem 2.2), the menu-wise decomposition (Lemma 3.3), the counting identity behind Axiom 3, and the reconstruction of μ from d. The perturbation calculus and the reachability theorem are reusable for other order-theoretic distances.
Difficulty
The "if" direction rests on Lemma 3.3. The obvious generalization fails: for the literature's notion of betweenness (R∗∩R∗⊆R⊆R∗∪R∗), Example 2.1 (p. 10) shows that maximal sets can move away from the target, and additivity breaks. Condition (2) is exactly what restores it, so it must be kept.
The "only if" direction has two hard points. First, Theorem 2.2: arbitrary additions and deletions need not lead from ≿ to ⊵. A deletion may violate (2), and an addition may create a cycle in a non-transitive relation. The perturbations must be chosen in a particular order. Second, the count 2N(b,≿)−1 of the menus affected by a single addition, and its interaction with acyclicity, must be established exactly, since Axiom 3 fixes these constants.
Formalization scope
Everything sits in the namespace PrefSemimetric.TopDiff, with one definitions module Model. The conventions are:
Relations. Relations are X → X → Prop over [Fintype X] [DecidableEq X]. The goal assumes [Nonempty X], as in "nonempty finite set".
Acyclic orders and d.A(X) is not a subtype. A candidate d is a real function on all relations, but every axiom, the semimetric property and the conclusion quantify only over relations satisfying IsAcyclicOrder. Acyclicity is reflexivity plus irreflexivity of the transitive closure of the strict part, which is equivalent to the page's absence of cycles of distinct elements.
Semimetric. The paper does not define the word. It is read as a pseudometric on A(X) with values in [0,∞) (IsSemimetric): nonnegative, zero on the diagonal, symmetric, and satisfying the triangle inequality.
The measure.μ is given by point weights w≥0 with μ(T)=∑x∈Tw(x); every positive measure on 2X has this form, and the zero measure is included (footnote 14). The sum over S⊆X runs over all subsets, and those with ∣S∣≤1 contribute 0.
Single addition.≿⊕(a,b) is the single formula "add (a,b), remove (b,a)", which agrees with both cases of p. 8. Axiom 3's ⊕ clause and case (ii) apply only when the result is acyclic, as the page's "provided that it is acyclic" requires.
The exponent.Nb b R - 1 is natural-number subtraction; it is exact in its clause, because a itself is counted.
The measure in the "only if" milestones. These take the weights as a hypothesis w(b)=d(≿ab,≿ab+) for all a=b, which is the page's definition μ{b}=mb.
Two trivializing readings are ruled out. "In-between" keeps consistency condition (2); with the literature's weaker betweenness, the "if" direction is false. Axiom 3 keeps its acyclicity provisos, and dropping them would constrain d on cyclic relations. A sorry-free sanity file confirms that the axioms are satisfiable (by d≡0), that a genuine one-step perturbation exists, and that display (8) holds for the counting measure on a two-element set.
Not formalized: Theorem 3.2, Lemma 2.1, Examples 3.1–3.2 and §§3.4–6 (weighted Kendall metrics, computational formulas, diameters, best transitive approximations, non-embeddability). Contributions are welcome on any milestone. Theorem 2.2 and Lemma 3.3 are the natural entry points.
Selected references
Bibliographic data as cited in the paper's reference list (arXiv:2203.04418v1, p. 29).
H. Nishimura and E. A. Ok, A Class of Dissimilarity Semimetrics for Preference Relations, arXiv:2203.04418v1, 2022; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2203.04418
J. Kemeny and J. Snell, Preference ranking: An axiomatic approach, in Mathematical Models in the Social Sciences, Ginn, New York, 1962, pp. 9–23.
K. Bogart, Preference structures I: Distances between transitive preference relations, J. Math. Soc. 3 (1973), 49–67.
B. Can, Weighted distances between preferences, J. Math. Econ. 51 (2014), 109–115.
F. Hassanzadeh and O. Milenkovic, An axiomatic approach to constructing distances for rank comparisons and aggregation, IEEE Trans. Inf. Theory 60 (2014), 6417–6439.
Proportional Volume Sampling and Approximation Algorithms for A-Optimal Design: Sampling with an α-Approximate (d−1, d)-Wise Independent Measure Gives an α-ApproximationResearch Paper
Motivation
In linear regression with a budget, an experimenter holds n candidate experiments, each described by a vector vi∈Rd, and may run only k of them. If the experiments in S⊆[n] are run and the unknown parameter is estimated by least squares, the covariance of the estimate is proportional to (∑i∈Svivi⊤)−1. A-optimal design chooses S to minimise the trace of that matrix, which is the mean squared error of the estimator. The criterion is one of the classical optimality criteria of experimental design (Pukelsheim, Optimal Design of Experiments, SIAM 2006) and appears in feature selection, sensor placement and matrix sparsification.
Selecting the best k-set exactly is NP-hard (the paper proves this in its Theorem 1.7), so the question is approximation. Avron and Boutsidis (SIAM J. Matrix Anal. Appl. 2013) connected A-optimal design to volume sampling (Deshpande–Rademacher, FOCS 2010), which samples a set with probability proportional to det(VSVS⊤), and obtained the approximation ratio k−d+1n−d+1. Nikolov, Singh and Tantipongpipat (arXiv:1802.08318; Mathematics of Operations Research, 2022) reweight volume sampling by a second measure μ that can depend on a solution of the natural convex relaxation. Their first result, Theorem 1.3, shows that the approximation ratio of this scheme is controlled by a single combinatorial property of μ, approximate (d−1,d)-wise independence. Their later theorems obtain ratios d (when k=d) and 1+ϵ (when k is large) by exhibiting such measures.
Setting
Let V=[v1,…,vn] be a real d×n matrix and d≤k≤n. For S⊆[n], VS is the d×∣S∣ submatrix of the columns indexed by S, so VSVS⊤=∑i∈Svivi⊤. The A-optimal design problem is
OPT=S⊆[n],∣S∣=kmintr(VSVS⊤)−1,
with the value +∞ for sets whose Gram matrix is singular.
The convex relaxation (1)–(3) replaces the indicator of S by x∈Rn:
Write VS(x) for the matrix with columns xivi, i∈S, so that V(x)V(x)⊤=∑ixivivi⊤, and xL=∏i∈Lxi.
Let Uk (U≤k) be the subsets of [n] of size exactly (at most) k, and μ a probability measure on them. Proportional volume sampling with measure μ (Definition 1.1) is the distribution μ′ with
The measure μ is α-approximate (d−1,d)-wise independent with respect to a feasible x (Definition 1.2) if for all T,R⊆[n] with ∣T∣=d−1 and ∣R∣=d,
PrS∼μ[R⊆S]PrS∼μ[T⊆S]≤αxRxT.
For a square matrix M with eigenvalues λ1,…,λm, Ek(M) is the k-th elementary symmetric polynomial ek(λ1,…,λm); Em(M)=detM.
Algorithm 1 (p. 8) solves the relaxation for x, samples S∼μ′, and pads S with arbitrary indices to size k if it is smaller.
Formalization targets
Goal: Theorem 1.3
If x is an optimal solution of (1)–(3) and μ is α-approximate (d−1,d)-wise independent with respect to x, then the output pad(S) of Algorithm 1 satisfies, for every k-set Sopt,
so the algorithm is an α-approximation in expectation, and some k-set has objective at most αCP (the integrality gap is at most α). The constant α is a parameter: the goal fixes no value of it, so later constructions of better measures plug into it unchanged.
Milestones
Lemma 2.1: det(VT(x)⊤VT(x))=xTdet(VT⊤VT) for ∣T∣≤d.
Padding a set with further vectors does not increase tr(VSVS⊤)−1 (p. 8).
Significance
Theorem 1.3 turns an approximation question about a continuous, spectral objective into a question about the marginals of a distribution on sets: any measure with approximately independent (d−1)- and d-marginals relative to the relaxation's solution yields an approximation algorithm with the same ratio, and simultaneously bounds the integrality gap of the relaxation. The paper's Theorems 1.4 and 1.5 are proved by applying it to hard-core distributions, giving a d-approximation for k=d and a (1+ϵ)-approximation for k=Ω(ϵd+ϵ2log(1/ϵ)).
The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The formalization produces, beyond the theorem itself, a reusable linear-algebra layer that the pinned Mathlib lacks: the Cauchy–Binet formula for Gram matrices, its extension (4) to all elementary symmetric functions of the spectrum, and the identity trM−1=Ed−1(M)/detM. These are standard tools for determinantal point processes and volume sampling, and a later formalization of the hard-core constructions (Theorems 1.4, 1.5) would build directly on this mission's goal.
Difficulty
The reduction itself is a short calculation once both sides of (5) are written as ratios of sums over (d−1)- and d-subsets; the difficulty is in the linear algebra that produces those ratios. Identity (4) needs Cauchy–Binet for non-square matrices together with the relation between the coefficients of the characteristic polynomial, its roots and sums of principal minors; none of this is in Mathlib in the required form, and the eigenvalue side requires that the characteristic polynomial of a real symmetric matrix splits over R. Applying (4) to every VS separately and exchanging the order of summation is bookkeeping between index sets of different sizes, which is where informal proofs are quietest. The expectation also has to be handled honestly at sets S with singular VSVS⊤: they are never sampled, but the paper's displayed equality on p. 9 counts them, so the first display holds only as an inequality.
Formalization scope
Everything is over R, with index sets Finset (Fin n) and V a Matrix (Fin d) (Fin n) ℝ. A probability measure on U≤k is a nonnegative function on subsets of [n] with total mass 1 vanishing on sets larger than k; this covers Uk as a special case. Ek is the elementary symmetric function of the real roots of the characteristic polynomial, applied only to symmetric matrices. Lean's matrix inverse is 0 on singular matrices, so every comparison of objectives assumes positive definiteness of the inverted matrix, and OPT is expressed by quantifying over k-sets with positive definite Gram matrix rather than by an infimum.
The statements add the following, each disclosed in the item's Formalization Note: 1≤d (for the natural-number subtraction d−1); a positive normaliser ∑Sμ(S)det(VSVS⊤)>0, which Definition 1.1 presupposes; positive definiteness of ∑ixivivi⊤, which is what a finite CP means; Definition 1.2 in cross-multiplied form; and "≤" in place of the printed "=" in the first display of p. 9. Theorem 1.3 assumes a suitable μ only for the optimal x, as the remark after the theorem says; this implies the printed form. The padding of Algorithm 1 is an arbitrary map pad with S⊆pad(S) and ∣pad(S)∣=k on the support of μ.
The goal is not inequality (5) alone and Ek is not defined as a sum of minors, and the expectation is not defined as the ratio of p. 9; any of those would make milestones true by definition. A sorry-free sanity file shows that all hypotheses of the goal are simultaneously satisfiable (d=k=n=2, V=I, x=(1,1), μ the point mass at [2], α=1).
Contributions are welcome at every milestone; the Cauchy–Binet layer (milestones 2 and 3) is reusable well beyond this mission and is the natural place to start.
Selected references
A. Nikolov, M. Singh, U. Tantipongpipat, Proportional Volume Sampling and Approximation Algorithms for A-Optimal Design, arXiv:1802.08318v5, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1802.08318
H. Avron, C. Boutsidis, Faster Subset Selection for Matrices and Applications, SIAM Journal on Matrix Analysis and Applications 34(4):1464–1499, 2013. https://arxiv.org/abs/1201.0127
A. Deshpande, L. Rademacher, Efficient Volume Sampling for Row/Column Subset Selection, FOCS 2010, 329–338. https://doi.org/10.1109/FOCS.2010.38
Z. Mariet, S. Sra, Elementary Symmetric Polynomials for Optimal Experimental Design, NeurIPS 2017. https://arxiv.org/abs/1705.09677
Report-Dependent Utility and Strategy-Proofness: The True Ranking Is Optimal for Every Decreasing Report-Dependent Utility If and Only If No Ranking Raises the Probability of a Top-r MatchResearch Paper
Why truthful reports fail in strategy-proof mechanisms
Deferred acceptance and top trading cycles are strategy-proof: submitting one's true preference ranking is optimal whatever the other participants do (Roth, 1982). School-choice and residency-match systems around the world use them for this reason. Yet laboratory and field data show participants misreporting systematically, most often by leaving popular options out of their list or by ranking options with high admission chances above options they prefer (Chen and Sönmez, 2006; Hassidim, Marciano, Romm and Shorrer, 2017; Chen and Pereyra, 2019; survey by Hakimov and Kübler, 2021). One line of explanation treats these reports as mistakes; another looks for preferences under which they are optimal, such as expectation-based loss aversion (Dreyfuss, Heffetz and Rabin, 2022).
V. Meisner's paper Report-dependent utility and strategy-proofness proposes report-dependent utility: on top of the value of the option she is assigned, a participant cares about where that option sits in the list she submitted, enjoying acceptance by her reported top choice and disliking acceptance only at the bottom. The paper's Proposition 2 says exactly when truth-telling survives such preferences, for every strength of the report-dependent component. This mission formalizes Proposition 2 and the steps of its proof.
Setting
A participant ranks n options, labelled 1,…,n. She gets a report-independent payoffvs from being matched with option s, and the options are labelled so that
v1≥v2≥⋯≥vn.
A rank-ordered list (ROL) is a bijection R from options to ranks [[1,n]]={1,…,n}; its r-th ranked option is r=R−1(r). The true ROLR=(1,2,…,n) ranks options by v. She also receives a report-dependent payoffρ(r) when matched with her r-th ranked option, where ρ:[[1,n]]→R is decreasing.
The other participants' reports are fixed. An option s is attainable (As=1) if the participant would be matched with it by ranking it first. The attainability distributionP is a probability distribution on the 2n states (A1,…,An)∈{0,1}n; the As may be correlated in any way. In a strategy-proof mechanism she is matched with the highest-ranked attainable option of her list, so her match probability at rank r under R is
fr=P(Ar=1,At=0∀t<r),
and her expected payoff is
U(v∣R)=r=1∑nfr(vr+ρ(r)).(1)
Under the truth these are fr and U(v∣R). The true ROL is optimal if U(v∣R)≥U(v∣R) for every R=R.
In Lean, options and ranks are Fin n, a ROL is Rt : Equiv.Perm (Fin n) (option ↦ rank), the truth is 1, P is a function (Fin n → Bool) → ℝ, and fr, U(v∣R) are matchProb P Rt r, payoff v ρ P Rt.
Formalization targets
Goal: Proposition 2 (p. 7)
For every non-truthful ROL R: U(v∣R)≥U(v∣R) for all decreasing ρ if and only if
r=1∑rˉ(fr−fr)≥0∀rˉ∈[[1,n]].(3)
Hence the true ROL is optimal for every decreasing ρ if and only if (3) holds against all non-truthful ROLs.
Milestones (steps of the proof, pp. 12–13)
First-order stochastic dominance: ∑s≤kfR(s)≤∑s≤kfs for every k.
Δv≥0 for decreasing v.
If (3) fails at some rˉ, some strictly decreasing ρ gives U(v∣R)<U(v∣R).
If (3) holds, U(v∣R)≥U(v∣R) for every decreasing ρ.
Supporting statements (the displays of the proof)
The decomposition U(v∣R)−U(v∣R)=Δv+Δρ with Δv=∑svs(fs−fR(s)) and Δρ=∑rρ(r)(fr−fr).
All ROLs have the same total match probability ∑rfr.
Δρ=∑r=1n−1(ρ(r)−ρ(r+1))(∑i≤rfi−∑i≤rfi).
Significance
Proposition 2 gives a testable condition, stated only in terms of beliefs about admission, under which no report-dependent taste of any size can break truth-telling: no alternative list may raise the probability of being matched with one of the top rˉ ranked options, for any rˉ. Conversely, when an alternative list does raise such a probability, as ranking a safe option first does, a strong enough report-dependent payoff makes that list strictly better than the truth even though the mechanism is strategy-proof. The paper uses this to separate settings in which truthful reports are predicted from those in which self-selection is predicted, and contrasts it with Proposition 1, under which every list is optimal for some beliefs.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission provides one, together with a reusable finite model of matching under correlated attainability (match probabilities of the highest-ranked attainable option, the expected payoff (1)) and the stochastic-dominance property of the truthful lottery, which other results about rank-ordered lists in strategy-proof mechanisms can import.
Difficulty
The two directions are elementary in spirit but need care. The "only if" direction in the paper takes a limit of decreasing functions ρ; a formal proof has to exhibit an actual strictly decreasing ρ and control the report-independent term Δv uniformly. The "if" direction rests on two facts the paper asserts briefly: that the true lottery stochastically dominates every other (which is a statement about the match rule under arbitrarily correlated attainability, not an assumption), and a summation-by-parts rewriting of Δρ that uses the equality of total match probabilities across lists. The paper's inequalities "Δv>0" and the final ">0" are strict as printed but hold only weakly, so the formal statements use ≥.
Formalization scope
Model. Options and ranks are Fin n, 0-indexed (Lean index i is the page's i+1). A ROL is Equiv.Perm (Fin n) mapping options to ranks; the r-th ranked option is R.symm r; the truth is 1. States are Fin n → Bool; P is a real weight function and IsAttainabilityDist P says it is nonnegative with total mass one. Probabilities are finite sums; there is no measure theory.
Match rule.matchProb P R r is the weight of the states in which the rank-r option is attainable and every option ranked above it is not: the highest-ranked attainable option is matched, as on p. 5. The distribution P does not depend on the submitted list.
Conventions in the goal. "Decreasing ρ" is StrictAnti ρ, the model's standing assumption; the equivalence also holds for weakly decreasing ρ. The order v1≥⋯≥vn is a hypothesis (Antitone v). The normalizations vn=0 and ρ(1)>0>ρ(n) are not imposed: all lists have the same total match probability, so adding a constant to v or ρ leaves U(v∣R)−U(v∣R) unchanged, and the statement with them is equivalent. "Non-truthful" is Rt ≠ 1. Condition (3) is Condition3 P Rt, with rbar : Fin n the page's rˉ shifted by one and Iic rbar the ranks 1,…,rˉ.
Not trivial.P is an arbitrary correlated distribution and the match probability is the highest-ranked-attainable rule, so neither side of the equivalence can hold by a degenerate model: for two options with independent fair-coin attainability both sides hold, and for a point mass on "only option 2 attainable" both fail against the swapped list.
Infrastructure. Only finite sums over Fin n and Fin n → Bool, permutations of Fin n and Mathlib's summation by parts. Proofs of any milestone are welcome, as are alternative proofs of the goal that bypass the decomposition.
Selected references
V. Meisner, Report-dependent utility and strategy-proofness, CRC TRR 190 Discussion Paper No. 289, 2021; Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4504
A. E. Roth, The economics of matching: stability and incentives, Mathematics of Operations Research 7(4), 1982. https://doi.org/10.1287/moor.7.4.617
A. Hassidim, D. Marciano, A. Romm, R. I. Shorrer, The mechanism is truthful, why aren't you?, American Economic Review 107(5), 2017. https://doi.org/10.1257/aer.p20171027
R. Hakimov, D. Kübler, Experiments on centralized school choice and college admissions: a survey, Experimental Economics 24(2), 2021. https://doi.org/10.1007/s10683-020-09667-7
B. Dreyfuss, O. Heffetz, M. Rabin, Expectations-based loss aversion may help explain seemingly dominated choices in strategy-proof mechanisms, American Economic Journal: Microeconomics, 2022. https://doi.org/10.1257/mic.20200259
Agricultural Supply Chains in Emerging Markets: Competition and Cooperation Under Correlated Yields: The Minimum Guaranteed Price Selects Under-, Full- or Over-Production Land Allocation EquilibriaResearch Paper
Motivation
In many emerging economies, smallholder farmers decide each season how much of their land to give to an export crop, sold through a local processor at a price linked to the world market, and how much to keep for a traditional alternative crop. Yields are uncertain and often correlated across neighbouring regions because they share weather. Governments and development agencies frequently protect farmers with a minimum guaranteed price: no processor may pay less than po per unit of harvest. Whether such a floor encourages too little, enough, or too much planting relative to the processing capacity of the region is a policy question with direct consequences for farm income and processor utilization.
Li, Kouvelis and Dada (SSRN 3531158; published in Manufacturing & Service Operations Management 26(2), 2024, doi:10.1287/msom.2022.0076) model this as a two-stage game between two farmers and two capacity-constrained processors, and characterize the land-allocation equilibria in closed form for all-or-nothing yields. This mission formalizes that characterization, together with the second-stage pricing results it is built on.
Setting
There are two regions i∈{1,2}, each with one farmer and one processor. The processed crop sells at the world price pe. Processor i has unit processing cost ci and capacity Ki>0, with c1≤c2, and the minimum guaranteed price satisfies 0≤po≤pe−c2.
Second stage. Farmer i has planted xi units of land and harvests yi=xiYie, where Yie is the random yield. Both farmers sell first to the winning processor (Processor 1 on ties); a winner who cannot absorb the whole harvest first takes the harvest of its own region's farmer, and the residual goes to the losing processor up to its capacity (Theorem 1 of the paper). Processor i's profit gi(p1,p2) is its margin pe−ci−pi times the amount it procures. Its willingness to paypˉi is the highest price p∈[po,pe−ci] at which winning at p is no worse than losing at po (conditions (7)–(8)). The processors then settle as in a second-price auction (Theorem 3): if pˉ1≥pˉ2, Processor 1 wins and the final prices are (p1∗,p2∗)=(pˉ2,po); otherwise Processor 2 wins and they are (po,pˉ1). Farmer i's revenue fi is the sum of her sales to the two processors at the final prices.
First stage. Farmer i's expected profit is
Fi(x1,x2)=E[fi(x1Y1e,x2Y2e)]−xiUi+Ai,
where Ui is the per-unit cost of export-crop land, including the forgone alternative crop, and Ai is a constant. An equilibrium is a pair (x1∗,x2∗)∈[0,L1]×[0,L2] in which each xi∗ maximizes Fi given the other farmer's choice.
All-or-nothing (AON) yields. Each Yie takes the value H>0 or 0. In the symmetric IID chain the processors are identical (c1=c2=c, K1=K2=K), the farmers are identical (U1=U2=U, A1=A2=A), and the yields are independent with P(Yie=H)=h∈(0,1).
Formalization targets
Goal: Theorem 6, parts 1, 3, 4 (p. 20)
In the symmetric IID chain with U>0, Li≥2K/H and the participation condition pe−c>U/(hH):
po<h2HU−h1−h(pe−c)⟹all equilibria satisfy x1∗+x2∗=HK,and a nondegenerate segment of that line consists of equilibria;2h2h−1(pe−c)+2h2HU≤po<21[(pe−c)+h(1−h)HU]⟹(HK,HK)is the unique equilibrium;po>21[(pe−c)+h(1−h)HU]⟹(H2K,H2K)is the unique equilibrium.
Milestones
Theorem 2 (p. 14): the WTPs equal the closed forms (9)–(10) whenever the total harvest is positive.
Lemma 1 (p. 14): pˉ1−pˉ2 depends on the total harvest only, is continuous, and changes sign at most once, from + to −.
Theorem 4, part 1 (p. 15): if (pe−c1−po)/K1≥(pe−c2−po)/K2, Processor 1 wins at every harvest.
§3.1 (p. 19): in the symmetric chain pˉ1=pˉ2, and Processor 1 wins at prices (pˉ2,po).
§3 (p. 18): under AON yields, F1=hanf1(x1H,0)+haaf1(x1H,x2H)−x1U1+A1, and similarly for F2.
§3.1 (p. 19): Fi decreases at rate U beyond 2K/H, so every equilibrium has xi∗≤2K/H.
Lemma 2 (p. 19): if pe−c<U/(hH), then (0,0) is the unique equilibrium. This is the no-production region, the complement of the goal's participation condition.
Significance
The theorem shows that the price floor is the decisive policy lever. A low floor leaves farmers with thin margins and produces under-planting together with a whole continuum of equilibria, so total production is pinned down but its split between regions is not. Intermediate floors coordinate both farmers on filling exactly the processing capacity. A high floor makes planting so attractive that both farmers plant enough to fill both processors on their own, and part of the harvest goes unsold whenever both crops succeed. These regimes underlie the paper's later comparisons of ownership structures and yield correlations (§4–§5).
The result is proved on paper; it has no machine-checked proof. Formalization adds a precise model of a second-stage protocol that is described partly in prose, and it pins down the boundary cases. Checking the printed statement already corrected three points: part 2 of Theorem 6 is false as printed, the participation condition must be strict for part 1, and the threshold of part 4 must be strict.
Difficulty
The profits Fi are piecewise linear in (x1,x2), but the pieces come from nested min and (⋅)+ operations in the allocation rule, multiplied by a WTP that is itself a ratio of such terms. Each farmer's best response is therefore discontinuous and has to be found region by region. The two farmers are not symmetric even in the symmetric chain, because Processor 1 wins every tie and so farmer 1's harvest is served first. Equilibrium claims are global: "unique equilibrium" requires excluding every other point of [0,L1]×[0,L2], including allocations above 2K/H and corners where a farmer plants nothing. The WTPs are defined as suprema, so identifying them with (9)–(10) is a separate optimization over all competing prices.
Formalization scope
All quantities are real numbers. The model is one definition, AgriChain.LandAlloc.Model: the chain, the allocation of Theorem 1 indexed by the winning processor, the profits (5)–(6), the WTP sets defined by (7)–(8) and the WTPs as their suprema, the final prices of Theorem 3 with ties going to Processor 1, the revenues (11)–(12), AON yield laws, the expected profits (13)–(14) as finite sums over the four yield outcomes, and the equilibrium. The equilibrium is the published generic pure-Nash predicate CarbonDoubleCount.Planner.IsPureNash, with feasible sets [0,Li]. Ui and Ai are real parameters, as in the paper from (13) on.
Hypotheses added to the goal: 0<h<1, H>0, K>0 and U>0 (the thresholds divide by h, H and h(1−h), and the bound xi∗≤2K/H needs U>0); Li≥2K/H (the over-production equilibrium plants 2K/H); the participation condition pe−c≥U/(hH) of p. 19, made strict; and part 4's threshold, made strict. "Unique equilibrium" is an "if and only if", asserting existence. Part 2 of Theorem 6 is not posed: at h=1/2, H=K=U=1, pe−c=5, po=0 its hypotheses hold, but the unique equilibrium is (4/5,3/5), whose total 7/5 is below 3K/(2H). Theorem 5 (p. 18) and part 2 of Theorem 4 are not posed either.
The goal is about the equilibria of the full model. Defining the WTPs by (9)–(10), defining Fi by the two-term AON form, or stating Theorem 6 for a hand-simplified symmetric profit would make the milestones definitional and is ruled out. Contributions are welcome on every milestone. The WTP computation and the AON reduction are reusable for the paper's other correlation structures (§4–§5).
Selected references
J. Li, P. Kouvelis, M. Dada, Agricultural Supply Chains in Emerging Markets: Competition and Cooperation under Correlated Yields, SSRN working paper 3531158, version of 2023-01-03. https://ssrn.com/abstract=3531158
Contracting for Product Support Under Information Asymmetry: Under Countervailing Incentives the First-Best Menu Solves the Performance-Based Screening Problem with Zero Information RentResearch Paper
Why product-support contracts matter
A repair supplier can invest in capacity before a service contract begins, while the customer may know more about how often her equipment fails. The supplier must choose both an incentive to maintain uptime and a menu that gives customers reason to reveal their failure rates. Li, Mishra, and Netessine study this interaction for maintenance, repair, and overhaul services. Their model compares a price per repair with a performance-based contract (PBC), under which the supplier is paid for the product's uptime. The latter ties revenue to the outcome the customer values. The paper asks when that arrangement can preserve the full-information outcome despite asymmetric information about product reliability. Li, Mishra, and Netessine, SSRN author version, §§1, 3, 5.
The specific result targeted here is Proposition 5(i). The two customer types differ both in failure rate and in the value of their outside options. This creates countervailing incentives: the customer with the less reliable product need not always be the one seeking a better contract. The paper identifies a range of outside-option ratios in which a single separating PBC menu gives each type the same contract she would receive if the supplier knew her type. Li, Mishra, and Netessine, Proposition 5(i), p. 18.
The contracting setting
A contract period has length one. A product has failures at a rate λ, and the supplier sets a repair rate μ by investing in capacity. Each repair requires a random lead time. The product's uptimeA is one minus total downtime. The paper's expected-uptime expression is E[A∣λ,μ]=1−λ/μ. It uses this expression to turn the stochastic model into the closed-form payoffs of its supplementary equation (B.39). Li, Mishra, and Netessine, §3, pp. 7–10, and supplement (B.39), p. 9.
There are two types, L and H, with 0<λL<λH. The probability of the low-failure type is β∈(0,1). Type τ can decline the contract and obtain her reservation payoffMτ; the setting has 0<MH<ML. The supplier receives vτ per unit uptime from a customer choosing contract τ and incurs a capacity cost cμτ plus expected material cost crλτ. The customer's payoff, evaluated at her actual failure rate λ, is (r−vτ)(1−λ/μτ), where r is revenue per unit uptime. The supplier's corresponding payoff is vτ(1−λ/μτ)−crλ−cμτ. Li, Mishra, and Netessine, §§3–4 and supplement (B.39).
A menu contains one positive-price, positive-rate contract for each type. Individual rationality (IR) requires that each type's payoff from her designated contract reach her reservation payoff. Incentive compatibility (IC) requires that neither type prefer the other contract. In problem (9), the supplier maximizes her prior-weighted payoff over all menus satisfying both IR and both IC constraints. Under full information, the two types can be optimized separately; Proposition 1(ii) gives the first-best PBC repair rate μτ0=rλτ/c and the price vτ0=r−Mτμτ0/(μτ0−λτ). Li, Mishra, and Netessine, Proposition 1, p. 12; problem (9), p. 18.
Formalization targets
The goal formalizes Proposition 5(i). Define the first-best menu by offering (vL0,μL0) to type L and (vH0,μH0) to type H. Condition (10) is
μH0−λHμH0−λL≤MHML≤μL0−λHμL0−λL.
When this condition holds and both first-best prices are positive, the first-best menu is feasible for problem (9) and achieves at least the supplier payoff of every feasible menu. Both IR constraints bind, so each customer's information rent is zero; the two repair rates differ, so the menu separates the types. Li, Mishra, and Netessine, Proposition 5(i), p. 18.
The milestones follow the paper's stated calculations: the binding-IR price and reduced objective from (B.6)–(B.7); the PBC part of Proposition 1(ii)–(iii); the two IC slack formulas (B.41) and (B.42); and the first-best payoff bound used at the end of the proof of Proposition 5(i). The joint-profit benchmark is Πτ0=r−2crλτ−crλτ. Li, Mishra, and Netessine, supplement pp. 3–4 and 9.
What the result provides
The result identifies a parameter region in which screening does not reduce productive efficiency or leave an information rent to either customer type. The supplier can offer the same repair capacities and prices as in the full-information problem while satisfying each type's participation and truthful-choice requirements. This makes the full-information outcome a concrete benchmark for the other regions of Proposition 5, where one or more constraints bind differently. Li, Mishra, and Netessine, Proposition 5, pp. 18–19.
The mathematical result is proved in the paper. This mission asks for machine-checked proofs of the model identities and the first region of its screening theorem. The reusable artifacts are the explicit PBC menu, the four feasibility constraints, the separation between supplier and joint profit, and a uniform upper bound over every feasible menu. No existing platform theorem found in the local prior-art index has this paper's contract space and payoffs.
Where the difficulty lies
The first-best solution optimizes a contract separately for each known type. With private failure rates, a customer can choose the contract intended for the other type; solving the two full-information problems alone therefore does not establish a feasible screening menu. The signs of both IC slacks must agree with the ratio interval in condition (10), and every denominator in the ratio and in the first-best prices must be nonzero. Feasibility still is not enough for the conclusion: optimality compares the candidate with all positive-price, positive-rate menus satisfying the four constraints, including menus with slack IR constraints. Li, Mishra, and Netessine, problem (9), p. 18, and supplement (B.39)–(B.43), p. 9.
Formalization scope
The Lean development uses real-valued prices, rates, costs, payoffs, and prior weights. It represents expected uptime and expected payoffs by the paper's closed form (B.39), 1−λ/μ; it does not encode the underlying Poisson failure process or random repair times in this first mission. The model keeps a separate customer payoff, supplier payoff, and joint-profit function, so πsP is never confused with Π0. The menu's feasibility predicate contains exactly the four constraints of problem (9), plus the strict positivity of both prices and both repair rates written under its maximization sign. The objective uses the prior weights β and 1−β. Li, Mishra, and Netessine, §§3–5.2 and supplement (B.39).
The standing predicate makes the parameter domain explicit: r,c>0, cr≥0, 0<λL<λH, 0<β<1, and 0<MH<ML. The order of the two outside options is stated in the paper's setting; MH>0 is needed for the ratio ML/MH in (10). The goal also assumes vL0,vH0>0, because a first-best menu with a nonpositive price is not in problem (9)'s admissible set. The algebraic IC milestones explicitly exclude zero denominators, and the goal's ratio condition with the standing order rules out its degenerate denominator cases.
The candidate's optimality is stated against every feasible menu. Restricting competitors to first-best-form or binding-IR menus would make the main theorem weaker. Useful contributions include proofs of the source's algebraic identities, the first-best profit properties, the global upper bound, and Proposition 5(i) itself. The omitted stochastic expected-uptime identity and the remaining cases of Proposition 5 are separate formalization work; the present goal uses the closed form printed by the paper.
Selected references
Li, D., N. Mishra, and S. Netessine, Contracting for Product Support under Information Asymmetry, Management Science, 2022, author version SSRN 2881356, doi:10.1287/mnsc.2022.4606.
Contagious Bank Runs and Committed Liquidity Support: A Unique Break-Even Committed Asset Price Between the Two Market Prices Minimizes the Risk of Systemic Bank FailuresResearch Paper
Motivation
When a bank run forces asset sales, the sale price can reflect buyers’ beliefs about the condition of other banks as well as the assets being sold. In the two-bank model of Li and Ma, observing two runs makes buyers more pessimistic about the aggregate state than observing one. That change in beliefs lowers the market price precisely when both banks need liquidity. The paper studies whether a regulator can commit in advance to a purchase price that reduces joint failures while recovering its expected expenditure. Its Proposition 3 gives a specific break-even policy in a limiting version of the model.
The paper proves the policy result in its accepted manuscript, dated 28 October 2021, and was published in Management Science in 2022. The result is mathematically known. The work here is to state its price, payoff, and risk claims as machine-checkable theorems with the paper’s parameter restrictions visible.
Setting
There are two banks and two aggregate states, good G and bad B. In state s, each bank’s asset portfolio produces a cash flow uniformly distributed between a state-dependent lower bound θs and a common upper bound θˉ. The good state has the higher lower bound: 0<θB<θG. Conditional on the state, the banks’ cash flows are independent. The prior probability of G is α∈(0,1); the probability of B is 1−α. These are the primitives of §2.1 of Li and Ma.
Each bank finances a unit portfolio using equity E, retail deposits F, and positive wholesale debt 1−E−F. A wholesale creditor who withdraws early receives a gross factor qrD, while one who waits receives rD, where rD>1 and q<1. The debt obligations used throughout are
D1=(1−E−F)qrD,D2=(1−E−F)rD+F.
Assumptions (1)–(3) say D2>θs in both states, F>D1, and q>21+θG/(2D2). The candidate market-price interval begins at P=(θB+D2)/2 and ends below qD2. The upper-cash-flow condition in footnote 29 is θˉ>F/(1−D1/P). It keeps the uniform probabilities within their intended range on this interval. Footnotes 25 and 27 explain why the interval is nonempty and P>D1; see pp. 13 and 15 of the accepted manuscript.
Buyers who observe M∈{1,2} bank runs use a posterior probability ωMB of state B, with ωMG=1−ωMB. Their expected profit from buying one unit at price P is ΠM(P). A market break-even pricePM∗ solves ΠM(PM∗)=0 in [P,qD2). The two prices differ because the number of runs changes buyers’ posterior. In the paper’s ϵ,η→0 regime, a committed regulator price PA gives the critical cash flow
θ∗(PA)=1−qD1/PAD2−D1.
The regulator’s expected payoffVA(PA) averages purchase gains over the two states and the possibilities of one or two runs, exactly as in equation (22). The systemic-failure probabilitySYS(PA) is the prior-weighted probability that both banks’ cash flows fall below θ∗(PA), using the closed uniform formula on p. 26 of Li and Ma.
Formalization targets
The milestone path establishes the existence of the two market prices, their ordering, the payoff identity (23), the signs of VA at those prices, and the monotonicity of payoff and systemic risk. The main target is Proposition 3: a unique regulator price lies strictly between the market prices,
P2∗<PA∗<P1∗,VA(PA∗)=0.
Both VA and SYS decrease strictly as the committed price rises through [P,qD2). Among all prices in the regulator’s program (20)–(21),
PA≥P2∗,VA(PA)≥0,θ∗(PA)≥D2,
the price PA∗ minimizes SYS and satisfies SYS(PA∗)<SYS(P2∗). This is the limit interpretation of the comparison printed at the end of Proposition 3.
Significance
The theorem identifies a precommitted price at which the regulator breaks even across possible numbers of runs, while a buyer who acts after observing the run count must break even conditional on that count. The resulting interval between P2∗ and P1∗ is where liquidity support can lower joint failures without an expected transfer. The program also excludes saving banks whose cash flow is below D2; the policy result meets that solvency restriction.
A checked formalization would make the paper’s assumptions and the links among posterior prices, regulator payoff, and systemic risk explicit. Proposition 3 is proved in the paper; its Lean proof and the supporting results in this mission remain to be completed. The definitions of the uniform two-state model, posterior weights, and payoff sums can support later formal work on related liquidity policies, while the paper-specific financial parameters remain tied to this model.
Difficulty
The regulator cannot choose a price from the simple interval between two fixed asset values. Each price changes the cash-flow threshold at which runs lead to failure, which changes the posterior beliefs used in ΠM and the probabilities weighting VA. A direct comparison of PA with either market price therefore does not determine the sign of the regulator’s total payoff. The proof must control both market-contingent profits and their state and run-count weights before the break-even price and its risk effect can be certified.
Formalization scope
Lean represents the aggregate state by a two-constructor type and the primitive bank data by one parameter structure. The standing predicate includes assumptions (1)–(3), rD>1, q<1, 0<θB<θG, 0<α<1, footnote 29, and positive wholesale debt. The last condition makes the model’s financing convention explicit. The formulation uses the paper’s closed forms in the ϵ,η→0 limit; it does not encode creditor signals or the full global game.
Uniform probabilities are not clipped, because the relevant threshold lies inside the cash-flow support on the stated price interval. The market prices are characterized by their break-even equations rather than chosen from a prior existence assumption: a milestone establishes their existence. VA is defined by equation (22), not the later identity (23), and the policy goal asserts existence and uniqueness of its zero. The feasible set is exactly program (20)–(21). Strict decrease means strict antitonicity on [P,qD2). Lean’s real division is total at zero, so the critical-threshold formula has junk values at singular inputs; every claim uses the economically valid interval. Useful contributions include proofs of the market-price milestones, the payoff identity and signs, and the two monotonicity results.
Selected references
Z. Li and K. Ma, Contagious Bank Runs and Committed Liquidity Support, author’s accepted manuscript, 28 October 2021, WRAP 165968; published in Management Science, 2022, doi:10.1287/mnsc.2021.4258.
Disclosing Delivery Performance Information When Consumers Are Sensitive to Promised Delivery Time, Delivery Reliability, and Price: Full or No Information-Quality Effort Is OptimalResearch Paper
Motivation
Online retailers and service providers quote a promised delivery time and are judged on how often they meet it. Platforms increasingly publish delivery-performance information, such as on-time ratings or conformance scores, so that consumers can weigh a quoted time against the firm's record. Producing accurate information is costly: the firm must track deliveries, audit ratings and present them clearly. Whether a firm should pay for precise information, or let consumers infer its reliability from noisy signals, is a question for operations management (capacity, lead-time quotation) and for marketing (pricing, information disclosure) at once.
Leng, Becerril-Arreola, Parlar and Ferguson (MSOM 2024; the mission follows the authors' preprint of April 2nd, 2023) model a firm that jointly sets a price, a promised delivery time and an effort toward the quality of its conformance information, facing consumers who care about all three. Their central analytical result, Theorem 1, says the firm should never invest partially: the optimal effort is either none or full.
The model joins two lines of work. The first is joint price and delivery-time decisions with congestion, as in So (2000), Liu, Parlar and Zhu (2007) and Boyaci and Ray (2006), where delivery reliability enters demand. The second is logit demand from discrete-choice theory (Anderson, de Palma and Thisse 1992), where the scale parameter measures how dispersed consumers' valuations are.
Setting
A firm serves consumers at service rateμ. It sets a pricep, a promised delivery timet, and an information-quality effortϕ∈[0,1]. The market has size Λ. Each consumer compares the firm with an outside option of deterministic utility Ve.
If consumers arrive at rate l, the firm operates as an M/M/1 queue, and an order is delivered within the promised time with probability
q=1−e−(μ−l)t(eq. (1)).
The deterministic utility of buying is
V=α−p+βrρq−βtt(eq. (4)),
where α is the base value, βr and βt are the sensitivities to the conformance score and to the promised time, and ρ scales the score. Effort narrows the dispersion of consumers' inferences: the utility shock has scale
ωθ(ϕ)=βr2(1−ϕ2)+ωY2(eq. (6)),
decreasing from βr2+ωY2 at ϕ=0 to ωY at ϕ=1.
The demand rateλ(p,t,ϕ) is the logit share times the market size (eqs. (8)–(9)):
λ=1+exp[−(V−Ve)/ωθ]Λ.
Since V depends on λ through q, this is a fixed-point equation in λ. The firm earns
Π(p,t,ϕ)=λ(p,t,ϕ)(p−bϕ−c)(eq. (11)),
with unit cost c and unit effort cost b. A plan (p,t) is feasible when p≥c, t≥0 and (μ−λ)t≥1. The optimal profitΠ∗(ϕ) is the supremum of Π over feasible plans, λ∗(ϕ) and V∗(ϕ) are the demand and utility at the optimal plan, and the gap
h(ϕ)=βr2ϕbωθ−ωθV∗(ϕ)−Ve
measures by how much Lemma 2's condition (19) holds. With Sˉ(ϕ) the largest attainable market share (eq. (10)), the capacity condition (16) is μ≥SˉΛ+(βt/(βrρ))e.
Formalization targets
Goal: Theorem 1 (p. 15)
Let V1=V∗(1). If
βr2bωY2≥V1−Ve(23),
then Π∗ is strictly decreasing on [0,1] and ϕ∗=0 is the unique optimum. Otherwise Π∗ strictly decreases and then strictly increases, with the turn at some ϕ0∈(0,1). In both cases
Π∗(ϕ)<max{Π∗(0),Π∗(1)}for all ϕ∈(0,1).
Milestones
Eq. (10): λ(p,t,ϕ)≤Sˉ(ϕ)Λ.
Lemma 1, item 2: the optimal plan exists, is unique, and solves the first-order equations (13)–(14).
Lemma 2, item 1 (profit part): if (19) holds at ϕ, then Π∗ has non-positive derivative there.
Lemma 2, item 2 (demand and profit parts): if (19) fails at ϕ, then λ∗ and Π∗ have positive derivatives there.
h(ϕ)→+∞ as ϕ→0+ (p. OA-7).
Eq. (35): h′(ϕ0)<0 wherever h(ϕ0)<0 (p. OA-8).
Single crossing: h(ϕ0)<0 implies h<0 on [ϕ0,1) (pp. OA-8 – OA-9).
h(1−)=bωY/βr2−(V1−Ve)/ωY, so (23) holds exactly when h(1−)≥0 (p. OA-9).
Three supporting items have no counterpart in the paper. They state that the demand fixed point is well posed, that Π∗ is continuous on [0,1], and the envelope identity dΠ∗/dϕ=−(λ∗βr2ϕ/ωθ)h(ϕ).
Significance
Theorem 1 is a bang-bang result. A firm choosing how much to spend on delivery-performance information should consider only two options, no effort and full effort, and condition (23) gives a closed-form test for when no effort is optimal. The paper's sensitivity results (Corollaries 1–4) and its numerical study are all built on this reduction, since they compare the two endpoint regimes using the closed forms in Table 1.
The result has an analytical proof in the paper's online appendix, but no machine-checked proof. The formalization adds a precise statement of the model's well-posedness: the demand is a fixed point, and the optimal plan exists and is unique. It also makes the comparative statics explicit. Parts of Lemma 2 as printed are false, namely the directions of t∗ and λ∗ in item 1 and of p∗ and V in item 2, and the mission states only the parts that hold. A complete development would certify which of the paper's conclusions survive and by which argument.
Difficulty
The optimal profit Π∗(ϕ) is the value of a two-dimensional optimization whose objective is defined through an implicit equation, since demand appears on both sides of the logit formula. Differentiating Π∗ in ϕ requires an envelope argument over a constrained problem. That in turn requires knowing that the optimum is interior, unique and a smooth function of ϕ, and that the queue constraint (μ−λ)t≥1 does not bind.
The single-crossing step is the delicate one. The paper reaches it through a derivative of λ∗ with respect to ωθ (eqs. (30)–(34)) whose sign claims are partly wrong. The tempting shortcut, to read the sign of Π∗′ off the sign of λ∗′, is unsound: when (19) holds, λ∗ can rise while Π∗ falls.
Formalization scope
Everything is real-valued and lives in the namespace DeliveryDisclosure.InfoEffort. A structure Params holds Λ,α,βr,βt,ρ,Ve,ωY,μ,c,b, and the predicate Standing bundles the standing assumptions. The paper writes βr,βt≥0 but divides by them, so Standing requires Λ,βr,βt,ρ,ωY,b>0, together with c≥0 and condition (16) for every ϕ∈[0,1].
The logit demand (8)–(9) with scale (6) is the primitive. The paper derives it from a Gumbel-plus-C(ϕ) decomposition of the utility shock that holds only when ωY=ϕβr. Every result from (8) on uses only the logit formula, so neither Claim 1 nor the C(ϕ) distribution is formalized.
Demand is the supremum of the l∈[0,Λ] below the logit right-hand side, which is the unique fixed point for t≥0. The function Real.sigmoid gives the logit share.
The shortest delivery time is t=0, so Vˉ=α−c+βrρ.
Effort ranges over the closed interval [0,1]. The paper's 0+ and 1− are its endpoints, and V1 is V at the ϕ=1 optimum.
Π∗ is the supremum over all feasible plans, not a closed form or a solution of (13)–(14).
h divides by ϕ, so it is used only on (0,1].
Π∗ is defined as a supremum over all feasible plans and h uses V at the optimum, which rules out a trivializing formalization: Π∗ cannot be replaced by Table 1's closed forms, by profit at a fixed plan, or by a demand with the conformance frozen. Lemma 1's corner case (item 1), Claim 1, Remarks 1–5, Table 1 and Corollaries 1–4 are not formalized.
A complete development needs implicit differentiation of a fixed point, an envelope theorem for a two-variable constrained maximization, and existence of maximizers on a non-compact feasible set. These ingredients apply to other congestion-pricing and logit-demand models. Contributions toward any milestone are welcome, as are proofs of the supporting items.
Selected references
M. Leng, R. Becerril-Arreola, M. Parlar, M. Ferguson, Disclosing Delivery Performance Information When Consumers Are Sensitive to Promised Delivery Time, Delivery Reliability, and Price, Manufacturing & Service Operations Management, 2024 (authors' preprint, April 2nd, 2023). https://doi.org/10.1287/msom.2023.0223
K. C. So, Price and time competition for service delivery, Manufacturing & Service Operations Management 2(4):392–409, 2000.
L. Liu, M. Parlar, S. X. Zhu, Pricing and lead time decisions in decentralized supply chains, Management Science 53(5):713–725, 2007.
T. Boyaci, S. Ray, The impact of capacity costs on product differentiation in delivery time, delivery reliability, and price, Production and Operations Management 15(2):179–197, 2006.
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
N. S. Cardell, Variance components structures for the extreme-value and logistic distributions with application to models of heterogeneity, Econometric Theory 13(2):185–213, 1997.