Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Open Markovian quantum systems with fast and full Hamiltonian control can be reduced to an equivalent control system on the standard simplex modelling the dynamics of the eigenvalues of the density matrix describing the quantum state. We explore this reduced control system for answering questions on reachability and stabilizability with immediate applications to the cooling of Markovian quantum systems. We show that for certain tasks of interest, the control Hamiltonian can be chosen time-independent. -- The reduction picture is an example of dissipative interconversion between equivalence classes of states, where the classes are induced by fast controls.
This mission is the statement-level formalization of Reachability, Coolability, and Stabilizability of Open Markovian Quantum Systems with Fast Unitary Control (arXiv:2308.00561v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
61 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.7: Asymptotic cooling equals constant-Hamiltonian pure-state global attraction (Theorem 4.7: Asymptotic cooling equals constant-Hamiltonian pure-state global attraction, PDF p. 17). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
11 results of the paper are not stated yet, because the library lacks an interface they need:
A complete analysis of multi-mode bosonic Gaussian channels is proposed. We clarify the structure of unitary dilations of general Gaussian channels involving any number of bosonic modes and present a normal form. The maximum number of auxiliary modes that is needed is identified, including all rank deficient cases, and the specific role of additive classical noise is highlighted. By using this analysis, we derive a canonical matrix form of the noisy evolution of n-mode bosonic Gaussian channels and of their weak complementary counterparts, based on a recent generalization of the normal mode decomposition for non-symmetric or locality constrained situations. It allows us to simplify the weak-degradability classification. Moreover, we investigate the structure of some singular multi-mode channels, like the additive classical noise channel that can be used to decompose a noisy channel in terms of a less noisy one in order to find new sets of maps with zero quantum capacity. Finally, the two-mode case is analyzed in detail. By exploiting the composition rules of two-mode maps and the fact that anti-degradable channels cannot be used to transfer quantum information, we identify sets of two-mode bosonic channels with zero capacity.
This mission is the statement-level formalization of Multi-mode bosonic Gaussian channels (arXiv:0804.0511v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gaussian dilation induces a completely positive covariance map (Proposition 1: Unitary dilations of Gaussian channels, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
33 results of the paper are not stated yet, because the library lacks an interface they need:
Operator-sum or Kraus representations for single-mode Bosonic Gaussian channels are developed, and several of their consequences explored. Kraus operators are employed to bring out the manner in which the unphysical matrix transposition map when accompanied by injection of a threshold classical noise becomes a physical channel. The action of the quantum-limited attenuator and amplifier channels as simply scaling maps on suitable quasi-probabilities in phase space is examined in the Kraus picture. Consideration of cumulants is used to examine the issue of fixed points. In the cases of entanglement-breaking channels a description in terms of rank one Kraus operators is shown to emerge quite simply. In contradistinction, it is shown that there is not even one finite rank operator in the entire linear span of Kraus operators of the quantum-limited amplifier or attenuator families, an assertion far stronger than the statement that these are not entanglement breaking channels. A characterization of extremality in terms of Kraus operators, originally due to Choi, is employed to show that all quantum-limited Gaussian channels are extremal. The fact that every noisy Gaussian channel can be realised as product of a pair of quantum-limited channels is used to construct a discrete set of linearly independent Kraus operators for noisy Gaussian channels, including the classical noise channel, and these Kraus operators have a particularly simple structure.
This mission is the statement-level formalization of Operator-sum Representation for Bosonic Gaussian Channels (arXiv:1012.4266v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
34 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §III Eq.(3.11): explicit phase-conjugation Kraus family (§III Eq.(3.11): explicit phase-conjugation Kraus family, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
36 results of the paper are not stated yet, because the library lacks an interface they need:
This paper defines the squashed entanglement of a quantum channel as the maximum squashed entanglement that can be registered by a sender and receiver at the input and output of a quantum channel, respectively. A new subadditivity inequality for the original squashed entanglement measure of Christandl and Winter leads to the conclusion that the squashed entanglement of a quantum channel is an additive function of a tensor product of any two quantum channels. More importantly, this new subadditivity inequality, along with prior results of Christandl, Winter, et al., establishes the squashed entanglement of a quantum channel as an upper bound on the quantum communication capacity of any channel assisted by unlimited forward and backward classical communication. A similar proof establishes this quantity as an upper bound on the private capacity of a quantum channel assisted by unlimited forward and backward public classical communication. This latter result is relevant as a limitation on rates achievable in quantum key distribution. As an important application, we determine that these capacities can never exceed log((1+eta)/(1-eta)) for a pure-loss bosonic channel for which a fraction eta of the input photons make it to the output on average. The best known lower bound on these capacities is equal to log(1/(1-eta)). Thus, in the high-loss regime for which eta << 1, this new upper bound demonstrates that the protocols corresponding to the above lower bound are nearly optimal.
This mission is the statement-level formalization of The squashed entanglement of a quantum channel (arXiv:1310.0129v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetric convex minimization of the pure-loss test bound (Section 6.1 after Eq.(26); Appendix A.1, 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.
22 results of the paper are not stated yet, because the library lacks an interface they need:
Let be a Banach--Lie group with involutive automorphism , be the -eigenspaces in the Lie algebra of , and be the identity component of its group of fixed points. An Olshanski semigroup is a semigroup of the form , where is an open -invariant convex cone in and the polar map is a diffeomorphism. Any such semigroup carries an involution * satisfying . Our central result, generalizing the L"uscher--Mack Theorem for finite dimensional groups, asserts that any locally bounded *-representation with a dense set of smooth vectors defines by "analytic continuation" a unitary representation of the simply connected Lie group with Lie algebra . We also characterize those unitary representations of obtained by this construction. With similar methods, we further show that semibounded unitary representations extend to holomorphic representations of complex Olshanski semigroups
This mission is the statement-level formalization of Analytic extension techniques for unitary representations of Banach-Lie groups (arXiv:1102.0213v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Enlarging the domain of an essentially self-adjoint symmetric operator (Lemma 4.8, PDF p. 12). 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.
24 results of the paper are not stated yet, because the library lacks an interface they need:
The capacity of a classical-quantum channel (or in other words the classical capacity of a quantum channel) is considered in the most general setting, where no structural assumptions such as the stationary memoryless property are made on a channel. A capacity formula as well as a characterization of the strong converse property is given just in parallel with the corresponding classical results of Verd'{u}-Han which are based on the so-called information-spectrum method. The general results are applied to the stationary memoryless case with or without cost constraint on inputs, whereby a deep relation between the channel coding theory and the hypothesis testing for two quantum states is elucidated. no structural assumptions such as the stationary memoryless property are made on a channel. A capacity formula as well as a characterization of the strong converse property is given just in parallel with the corresponding classical results of Verdu-Han which are based on the so-called information-spectrum method. The general results are applied to the stationary memoryless case with or without cost constraint on inputs, whereby a deep relation between the channel coding theory and the hypothesis testing for two quantum states is elucidated.
This mission is the statement-level formalization of General formulas for capacity of classical-quantum channels (arXiv:quant-ph/0206186v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Attainment of the four sequence cutoffs (Lemma 1; Appendix I, pp.30–31, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
22 results of the paper are not stated yet, because the library lacks an interface they need:
Positive maps which are not completely positive are used in quantum information theory as witnesses for convex sets of states, in particular as entanglement witnesses and more generally as witnesses for states having Schmidt number not greater than k. It is known that such witnesses are related to k-positive maps. In this article we propose a new proof for the correspondence between vectors having Schmidt number k and k-positive maps using Jamiolkowski's criterion for positivity of linear maps; to this aim, we also investigate the precise notion of the term "Jamiolkowski isomorphism". As consequences of our proof we get the Jamiolkowski criterion for complete positivity, and we find a special case of a result by Choi, namely that k-positivity implies complete positivity, if k is the dimension of the smaller one of the Hilbert spaces on which the operators act.
This mission is the statement-level formalization of The Jamiołkowski isomorphism and a conceptionally simple proof for the correspondence between vectors having Schmidt number and -positive maps (arXiv:quant-ph/0702255v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is k-positivity is equivalent to Schmidt-number block positivity (Theorem 3 (Main theorem), proved through PDF p.8, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
We derive analytical expressions for the single mode quantum field state at the individual output ports of a beam splitter when a single-photon Fock state and a coherent state are incident on the input ports. The output states turn out to be a statistical mixture between a displaced Fock state and a coherent state. Consequently we are able to find an analytical expression for the corresponding Wigner function. Because of the generality of our calculations the obtained results are valid for all passive and lossless optical four port devices. We show further how the results can be adapted to the case of the Mach-Zehnder interferometer. In addition we consider the case for which the single-photon Fock state is replaced with a general input state: a coherent input state displaces each general quantum state at the output port of a beam splitter with the displacement parameter being the amplitude of the coherent state.
This mission is the statement-level formalization of Quantum Interference between a Single-Photon Fock State and a Coherent State (arXiv:1009.1844v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is MZI composition and full reciprocity relations (§III/A, Eqs.(21)–(22), 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
We consider two properties of the set of quantum states as a convex topological space and some their implications concerning the notions of a convex hull and of a convex roof of a function defined on a subset of quantum states. By using these results we analyze two infinite-dimensional versions (discrete and continuous) of the convex roof construction of entanglement monotones, which is widely used in finite dimensions. It is shown that the discrete version may be 'false' in the sense that the resulting functions may not possess the main property of entanglement monotones while the continuous version can be considered as a 'true' generalized convex roof construction. We give several examples of entanglement monotones produced by this construction. In particular, we consider an infinite-dimensional generalization of the notion of Entanglement of Formation and study its properties.
This mission is the statement-level formalization of On properties of the space of quantum states and their application to construction of entanglement monotones (arXiv:0804.1515v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Discrete Jensen inequality for upper-bounded extended costs (Proposition A-1: discrete Jensen inequality, PDF p. 31). 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.
55 results of the paper are not stated yet, because the library lacks an interface they need:
The relative entropy of entanglement is defined as the distance of a multi-partite quantum state from the set of separable states as measured by the quantum relative entropy. We show that this optimisation is always achieved, i.e. any state admits a closest separable state, even in infinite dimensions; also, is everywhere lower semi-continuous. We use this to derive a dual variational expression for in terms of an external supremum instead of infimum. These results, which seem to have gone unnoticed so far, hold not only for the relative entropy of entanglement and its multi-partite generalisations, but also for many other similar resource quantifiers, such as the relative entropy of non-Gaussianity, of non-classicality, of Wigner negativity more generally, all relative entropy distances from the sets of states with non-negative -quasi-probability distribution. The crucial hypothesis underpinning all these applications is the weak*-closedness of the cone generated by free states, and for this reason the techniques we develop involve a bouquet of classical results from functional analysis. We complement our analysis by giving explicit and asymptotically tight continuity estimates for and closely related quantities in the presence of an energy constraint.
This mission is the statement-level formalization of Attainability and lower semi-continuity of the relative entropy of entanglement, and variations on the theme (arXiv:2105.08091v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness (Theorem 5 (seed): attainability, lower semicontinuity, compactness and uniqueness, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
29 results of the paper are not stated yet, because the library lacks an interface they need:
A brief proof of the statement that the zero-set of a nontrivial real-analytic function in -dimensional space has zero measure is provided.
This mission is the statement-level formalization of The Zero Set of a Real Analytic Function (arXiv:1512.07276v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A nontrivial real-analytic function has a Lebesgue-null zero set (Proposition 0, PDF p. 1). 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.
A generic quantum channel can be represented in terms of a unitary interaction between the information-carrying system and a noisy environment. Here, the minimal number of quantum Gaussian environmental modes required to provide a unitary dilation of a multi-mode bosonic Gaussian channel is analyzed both for mixed and pure environment corresponding to the Stinespring representation. In particular, for the case of pure environment we compute this quantity and present an explicit unitary dilation for arbitrary bosonic Gaussian channel. These results considerably simplify the characterization of these continuous-variable maps and can be applied to address some open issues concerning the transmission of information encoded in bosonic systems.
This mission is the statement-level formalization of The optimal unitary dilation for bosonic Gaussian channels (arXiv:1009.1108v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Complex kernel and rank relations for Gaussian channel data (Section II, Eqs.(6)–(10), 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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
We extend the definition of the conditional min-entropy from bipartite quantum states to bipartite quantum channels. We show that many of the properties of the conditional min-entropy carry over to the extended version, including an operational interpretation as a guessing probability when one of the subsystems is classical. We then show that the extended conditional min-entropy can be used to fully characterize when two bipartite quantum channels are related to each other via a superchannel (also known as supermap or a comb) that is acting on one of the subsystems. This relation is a pre-order that extends the definition of "quantum majorization" from bipartite states to bipartite channels, and can also be characterized with semidefinite programming. As a special case, our characterization provides necessary and sufficient conditions for when a set of quantum channels is related to another set of channels via a single superchannel. We discuss the applications of our results to channel discrimination, and to resource theories of quantum processes. Along the way we study channel divergences, entropy functions of quantum channels, and noise models of superchannels, including random unitary superchannels, and doubly-stochastic superchannels. For the latter we give a physical meaning as being completely-uniformity preserving.
This mission is the statement-level formalization of Comparison of Quantum Channels by Superchannels (arXiv:1808.02607v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majorization of channels by all paired entropy tests (Theorem 7, continued p.19, PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Many problems in robust optimization, adversarial learning, distributionally robust learning and min-max games have the max-structured form
where is smooth in but not convex, and concave in . The function is neither smooth nor convex, so gradient methods do not apply directly and convex duality does not close the problem. The standard target is then a near-stationary point: a point close to its own proximal point. In Hilbert spaces this notion and the matching algorithms are well developed (Davis and Drusvyatskiy 2019, doi:10.1137/18M1178244; Thekumparampil et al. 2019, arXiv:1907.01543). Many applications, however, live on simplices or spectral sets where the natural norm is or a Schatten norm and the natural proximal geometry is a Bregman divergence (entropy, for example).
R. Zhao (Mathematics of Operations Research, 2024; arXiv:2003.04375) gives a primal-dual smoothing framework for this problem in arbitrary finite-dimensional normed spaces. The dual variable is smoothed by a strongly convex function, and the primal problem is handled by an inexact Bregman proximal-point method. This mission formalizes the outer-loop guarantee of that framework: an explicit iteration bound after which the method returns an -near-stationary point.
Let and be finite-dimensional real normed spaces with arbitrary norms. Write for a nonempty closed convex set, the domain of a convex lower semicontinuous , and for a nonempty convex compact set. The function is convex and continuous on . is jointly continuous, is concave, and is differentiable and -weakly convex on for some :
A distance generating function is continuous and 1-strongly convex on , and differentiable at every point of with a -Lipschitz gradient (). Its Bregman divergence is . For , the proximal point minimizes over . A point is an -NS point if, for some such , .
Dual smoothing: for a 1-strongly convex continuous on , set , , and .
Algorithm 1 fixes , and , and starts from . Iteration finds with , where is with in place of . It stops at the first with and outputs .
For , and , every run of Algorithm 1 stops at a first index
and is an -NS point. Here is the optimal value, or any lower bound of on .
Corollary 4.1 bounds the number of outer iterations, that is, approximate proximal subproblems, needed to reach an -NS point. The bound is for fixed , and it holds in any norm. In the paper this count is combined with an accelerated primal-dual solver for each subproblem to obtain the overall gradient complexities (its Corollary 4.2 and Table 1). The paper reports these as the first complexity results for near-stationarity of (1.1) in the non-Hilbertian setting. The outer-loop count is the part of that analysis that does not depend on the inner solver, so it applies to any inner method that meets the -accuracy of Step 2.
The result is proved in the paper. It has no machine-checked proof on Prove2Me or, as far as is known, elsewhere. A formal development would provide reusable infrastructure: strong convexity of Bregman proximal objectives built from weakly convex parts in a general normed space, existence of Bregman proximal points in finite dimension, and the stability of proximal points under uniform perturbation of the objective.
The arithmetic of the final bound is short. The work lies in the analytic facts underneath it, which a Hilbert-space intuition gets wrong. In a general norm is not smooth and weak convexity cannot be rewritten as convexity of . Strong convexity of must therefore come from the gradient inequality and the 1-strong convexity of , passed through a supremum over . The paper's remark cites only and the strong convexity of . The weak convexity of and the convexity of are also needed. Existence of the proximal point is not automatic: it requires lower semicontinuity of on the closed set , which comes from compactness of and joint continuity of , together with coercivity from strong convexity in finite dimension. Finally, Theorem 4.1 is stated at the termination index, and termination itself (Theorem 4.2) requires .
are E, F with NormedAddCommGroup, NormedSpace ℝ and FiniteDimensional ℝ. No inner product is assumed. Gradients are fderiv, dual norms are operator norms on E →L[ℝ] ℝ, and differentiability is assumed at every point of where a gradient is used. Maxima are real suprema over the subtype . Strong convexity is Mathlib's StrongConvexOn. The proximal point is a predicate IsProx, not a function. Iterates are indexed from 1. A run constrains only the iterations actually executed, those before the first stop. is real-valued, with values off irrelevant. The optimal value is encoded as any lower bound of on , and -optimality in Step 2 as a bound against every . If , Lean sets (no smoothing); the paper leaves this case undefined, and all statements remain true. Hypotheses of the paper not used here are omitted, which only strengthens the statements: the Lipschitz bounds (1.2)–(1.3), Assumption 1.3, , essential smoothness and property (i) of the distance generating functions. Lemma 4.3 is stated as (4.12) for . Theorem 4.1 is stated at a first stopping index, without a termination claim.
Trivializing formalizations are ruled out. The norms are general, not Euclidean. Weak convexity is the gradient inequality (1.4). The suprema are over a nonempty compact with continuous integrands, so they are finite. Existence of proximal points and termination are conclusions, never hypotheses. is the first stopping index of a genuine run.
Welcome contributions: the strong convexity of and (milestones 2–3), a general existence lemma for minimizers of strongly convex lower semicontinuous functions on closed convex sets in finite dimension, and the quadratic-growth estimate at a minimizer of a strongly convex function.
An online marketplace can sell its own product while hosting a third-party seller whose product competes with it. The marketplace earns a commission on the seller's sales, but it can also charge to fulfill the seller's orders. That service improves the seller's offering and changes competition for both products. Lai, Liu, Xiao and Zhao study when a fulfillment-by-platform program raises Amazon's own profit in a model with price and service competition Lai et al., SSRN preprint 3270958. The question matters to a platform choosing whether and how to offer fulfillment while it also acts as a retailer.
Amazon sells product A and a third-party seller sells a substitutable product S. Amazon purchases A from an OEM supplier at wholesale price ; the OEM's unit production cost is . The seller obtains S at unit cost and pays Amazon a commission at rate on its selling price . The products have market bases . Amazon's fulfillment-service quality is and the seller's own service quality is . The unit fulfillment cost is for either provider.
The cross-price sensitivity measures how a rival's price increases demand. The cross-service sensitivity measures how a rival's service quality reduces demand; measures the own-product service benefit. Without fulfillment by Amazon (no FBA), demands at retail prices are the paper's equations (1)–(2):
With FBA, the seller pays Amazon a per-unit fee and its fulfillment quality becomes . Equations (3)–(4) therefore replace by in both demand equations. Amazon's no-FBA profit is ; its FBA profit is . The seller's corresponding profits are and §3–§4.1, pp. 9–13.
The sequential game has three stages without FBA: the OEM chooses , then Amazon and the seller simultaneously choose retail prices. With FBA, Amazon first chooses ; the OEM then chooses , and the retailers choose prices simultaneously. The fee must let the seller earn at least its no-FBA equilibrium profit. The model compares Amazon's profit in the two resulting equilibria, including Amazon's fee choice §4.1, equation (5).
The goal is Proposition 2. There are thresholds such that, throughout the model's domain ,
The upper threshold may lie above ; the theorem asserts its classification only on . When the loss interval meets that domain, Amazon loses from FBA at the intervening sensitivities. The target is about equilibria of the sequential games, rather than values stipulated by formulas Proposition 2, p. 19.
Lemmas A.1 and A.2 characterize the two unique equilibrium outcomes in closed form. Proposition 1 (i) gives the seller's maximum fee consistent with a strict benefit. Lemma A.3 gives the unique optimal fee and identifies it as the smaller of Amazon's unconstrained optimum and . Four statements come from the proof of Proposition 2: Amazon's gain is convex in when the fee is (case (1)), convex when the fee is (case (2)), convex for the equilibrium fee on , and strictly positive at Online Appendix, pp. 34–38. Two comparisons from §4.2 complete the list: the seller's equilibrium sales are at least as high with FBA as without (Lemma 3, p. 15), and its equilibrium price is strictly higher with FBA (Lemma 1, p. 14), stated with the hypothesis that the printed proof uses, since without it the printed lemma can fail.
The result separates three economic effects of FBA. Improved seller fulfillment can increase its sales, which can increase Amazon's fee and commission revenue. It also removes Amazon's service advantage and changes the retailers' prices. Proposition 2 says the combined profit effect can change sign twice as consumers become more sensitive to service comparisons §4.3, p. 19. A one-direction comparative static would miss that pattern.
The paper presents analytic proofs of the equilibrium and threshold results. This mission asks for machine-checked proofs of those known claims under an explicit parameter and sales regime; the draft statements themselves use sorry and are not proofs. The general two-player price-game interface and the explicit sequential-equilibrium relations can also support other models of marketplace pricing. The closed forms make it possible to test algebraic dependencies without building the goal theorem into the definitions.
Each retail player changes the other player's demand, and the OEM anticipates their simultaneous price choices. The FBA fee then changes all three subgame decisions and is constrained by the seller's benchmark profit. A direct comparison of the two Amazon profit formulas at arbitrary prices cannot answer the question: the prices and wholesale price must themselves be equilibrium choices. A pointwise sign check at a few values of also cannot establish the two-threshold classification. The paper's appendix isolates the fee regimes and states a convexity conclusion, but its printed positivity argument at invokes a fee-above-cost condition that does not follow from its fee problem proof of Proposition 2, p. 38.
All prices, wholesale prices and fees are real numbers. The demands are the printed affine formulas, with no positive-part truncation. Params.Standing contains and . It additionally requires and , making the market bases, service quality and unit costs have their economic signs. Interior requires the seller's no-FBA equilibrium sales to be positive for every . These additions make explicit the nonnegative-sales branch used in the appendix's participation argument. They exclude some numerical parameter sets illustrated in the paper; this is a restricted formal version of the printed result.
The fee relation encodes equation (5)'s weak participation inequality and additionally requires the seller's FBA equilibrium sales to be nonnegative. Without that clause the quadratic seller profit can satisfy participation at a fee producing negative sales. No condition is imposed: although the model narrative describes such a fee, equation (5) has no such constraint and the paper's fee solution can fall below . The seller's strict-benefit statement retains Proposition 1 (i)'s strict inequality. Real division in the appendix formulas is safe in the stated parameter regime, since every denominator is positive.
Definitions include the reusable simultaneous price game, four demand functions, six profit functions, the two sequential equilibrium relations, the fee optimization relation, and the appendix's closed forms. Contributions are welcome on their uniqueness, the participation boundary, convexity of the equilibrium gain, and the two-threshold goal. An encoding that simply defines the fee to be would erase Lemma A.3 and does not meet this mission's target.
Sharing-economy platforms (ride-sharing, car-sharing, peer-to-peer lending) sit between two groups. They charge consumers a price and pay self-scheduling workers a wage, and they compete with rival platforms on both sides at once. How a platform pays its workers is a design choice that varies across the industry: some announce a fixed wage per job, some a fixed commission rate on the consumer price, and some, as Uber did in its "upfront pricing" experiments, set prices and wages job by job. Drivers and regulators have argued over these schemes, and whether the choice matters for the platforms' own profits is a question in its own right.
Zhang, Chen and Raghunathan (SSRN 3555993, published in Management Science, 2022) answer it in a parsimonious duopoly model with linear demand and supply. Their main comparison, Proposition 3, shows that every scheme can be the most profitable one. Which one wins depends on whether consumers or workers switch more readily between the platforms. Many two-sided platform models, for example ones in which supply does not respond to the rival's wage, find no such reversal.
Two platforms , with , charge consumer prices and pay wages per transaction. Six parameters define
the demand and the worker supply of platform . Here measures how readily consumers switch platforms, the price sensitivity of loyal consumers, how readily workers switch, and the wage sensitivity of loyal workers. A transaction needs both a consumer and a worker, so the transaction volume is and the profit is
The standing assumptions are Assumption 1, , and Assumption 2, .
Three wage schemes define three games:
DCR is solved by Nash equilibrium. FCR and FW are solved by subgame-perfect equilibrium: a stage-2 price rule must give a Nash equilibrium of the pricing game after every pair of stage-1 announcements, and no stage-1 announcement may be improved on. The paper studies symmetric equilibria with positive demand and supply. Write for the resulting platform profits.
Write for the DCR equilibrium commission rate and
for the left side of the paper's Inequality (13). For every symmetric equilibrium of each game with positive demand and supply:
The goal is stated about the equilibria of the three games, not about the closed-form prices.
Proposition 3 makes the choice of wage scheme a substantive strategic variable. The fixed-wage scheme is either the best or the worst for the platforms, and the fixed-commission scheme is never the worst. The ranking of profits equals the ranking of equilibrium prices and reverses that of wages. The paper's welfare results (Propositions 4 and 5) build on it, since consumer and worker surplus orderings are read off the same price ranking.
Formalizing it adds three things:
The result is proved in the paper; nothing in it has been machine-checked.
The comparison itself, once the equilibria are known, is rational-function algebra. The difficulty is the equilibrium characterizations.
Params.Standing.A formalization that compares only the closed-form prices, or uses the literal untruncated payoff (which makes every statement about equilibria vacuous), is not this mission.
Competing brands often buy their products from the same contract manufacturer (CM). A weaker brand can exploit this. The paper's opening example is the Chinese retailer Netease Yanxuan, which advertises that its goods use "the same materials, the same factories, and the same workers" as international brands such as Adidas, Coach and MUJI. A weak brand that discloses its common supplier in this way borrows part of the leader's reputation. This practice is called brand spillover.
The obvious view is that a weak brand should use any spillover it can get. Wu, Zhang and Zhou (SSRN 3891915, Management Science 2021) show that this view is incomplete. A supplier that serves both brands has to keep the strong brand willing to outsource. If the weak brand's spillover makes that too expensive, the supplier stops serving the weak brand, or it extracts the spillover's value through its prices. The paper's main result, Proposition 4, says when the weak brand is better off committing in advance not to use the spillover. This mission formalizes that result together with the equilibrium analysis it rests on.
Two firms sell substitutable products. Firm S has brand power and Firm W has brand power . With quantities the market-clearing prices are
Each firm can produce in-house at unit cost , or buy from the CM, whose own unit cost is normalized to . A sourcing structure is one of , , , : the first letter is Firm S's choice and the second Firm W's, with for outsourcing and for insourcing. Brand spillover can occur only under . There, if Firm W uses it, its brand power becomes , where is the level of brand spillover.
The game has four stages:
At stage 4 the quantities are the first-order-condition solutions, and each firm's profit is the square of its quantity. At stage 2, for each structure, the CM maximizes its revenue over the outsourcing firms, subject to participation constraints. A constraint says that a firm does at least as well outsourcing at the offered price as deviating to insourcing. The CM then induces the structure with the highest optimal revenue. The standing assumption keeps Firm W in the market.
The thresholds used below are , and .
Assume . Let be Firm W's profit at an equilibrium without commitment, and its profit at an equilibrium with commitment. If the structure without commitment is , then . Otherwise
Proposition 4 splits the parameter space into three regions. In the first, the supplier would drop the weak brand: it induces , and Firm W pays the insourcing cost. In the second, the supplier captures the spillover through a higher wholesale price, and the weak brand loses ground to the strong one. In the third, the spillover pays. The comparative static behind the second region is Proposition 2(b): brand spillover can lower the profit of the firm it benefits. The analysis also identifies when the strong brand is hurt by the weak brand's spillover and should act to prevent it (paper, abstract and §5).
The paper proves the result by hand, and no formal proof exists. A complete development would give machine-checked proofs of:
Formalizing the statements has already found two slips in Proposition 3: a sign in , and a boundary point that the printed case split assigns to the wrong structure.
The CM's feasible sets are not convex. Each participation constraint compares two squared quantities, , so it admits two branches: a price below a bound, or a price so high that the quantity changes sign. The paper's proofs treat only the first branch. A complete proof must rule out the other branches as optimal, so maximizing a concave quadratic is not enough.
The goal compares equilibrium outcomes, not formulas. Each side combines an optimal-price problem with a choice between structures. The no-commitment side changes regime along the curves , , , which contain square roots. Firm W's profit has a kink at .
BrandSpillover.Commitment.Model. The profit functions use the referenced general linear Cournot payoff SupplierAudit.Competition.cournotPayoff with substitution parameter . All quantities and prices are real numbers.Quantum computers must correct errors faster than they accumulate, and quantum low-density parity-check (LDPC) codes are the leading candidates for doing so with little overhead: every check involves a bounded number of qubits, so syndromes can be measured by local circuits. In 2021–2022 the first asymptotically good quantum LDPC codes appeared, with dimension and minimum distance both linear in the code length : the expander lifted product codes of Panteleev and Kalachev (arXiv:2111.03654) and the quantum Tanner codes of Leverrier and Zémor (arXiv:2202.13641). A code is only useful if errors can be corrected efficiently. Leverrier and Zémor (arXiv:2208.05537) give two decoders for quantum Tanner codes that correct every error of weight up to a constant fraction of : a sequential one running in linear time, and a parallel decoder running in a logarithmic number of rounds of local updates. This mission is about the parallel decoder.
Timeline:
Let be a finite group and , with . The quadripartite left-right Cayley complex has four copies of as vertices, , and one square for every . The set of squares has elements, and every vertex sees its -neighbourhood as an array: columns are indexed by , rows by . The left Cayley graph and the right Cayley graph are assumed to be non-bipartite Ramanujan graphs: every adjacency eigenvalue other than has absolute value at most .
Two local codes , with are fixed. Write and . The code consists of the vectors whose view on every , , lies in the dual tensor code : every local view is a sum of a word whose columns are in and a word whose rows are in . is defined in the same way on with , . The local codes and their duals have distance at least . Both dual tensor codes are -product-expanding: every codeword splits as with , where counts non-zero columns and non-zero rows.
A -type error is decoded in three phases. In the preprocessing phase every chooses a minimum-weight local error with the local syndrome of ; the mismatch is . The mismatch decomposition writes , with a sum of -columns and a sum of -rows. Postprocessing outputs . The parallel decoder (Algorithm 3) runs rounds of four substeps, one for each of . In a substep, every vertex of the current class simultaneously looks for a non-zero local dual tensor codeword on with , picks one of maximum weight, splits it as with minimal, and updates , and .
Fix and . For all large enough, every error with
is corrected by every run of the parallel decoder. With , each round satisfies , so once , and then lies in the span of the -generators.
The theorem shows that asymptotically good quantum LDPC codes can be decoded against adversarial errors of linear weight by rounds of local computation, each vertex acting only on its own -neighbourhood. This matters for fault tolerance, where decoding latency is a bottleneck. The milestones carry independent value. Theorem 9 is a linear minimum distance bound for quantum Tanner codes in the quadripartite setting. Theorem 12 is the local-to-global "weight reduction" principle on which both decoders rest. Lemmas 4–5 are spectral facts about Cayley graphs and square complexes that are reusable for any expander-based code.
The paper's results are proved, not open; none has been machine-checked. The sequential decoder's correctness (Theorem 13) is posed separately on the platform as an open goal in the mission Decoding quantum Tanner codes (Leverrier, Zemor), which shares this mission's published definitions; this mission does not restate it. Formalizing the present chain would give a complete, checked proof that a parallel decoder exists for good quantum LDPC codes, and would expose the constants. Two printed constants are corrected here (see the scope section), and sharper constants or simpler arguments are welcome.
The obvious argument is to bound the mismatch and its norm, apply Theorem 12 repeatedly, and let all vertices of a class flip at once. That argument fails because parallel flips are not sequential flips. A vertex's best local move against the mismatch at its turn need not be the move a converging sequential run would make, and a round could stall even though a sequential run never does. Lemma 18 resolves this with a virtual sequential run, a partition of its increments into "good" and "bad" ones (Claim 1), and the maximum-weight rule at every vertex. Without that rule the lemma is false. Theorem 12 itself is a counting contradiction. It uses robustness, the expander mixing lemma twice, and two notions of "exceptional" vertices, and it needs large. Theorem 9 needs the coset-minimization of Lemma 7 before the same counting can start.
The development builds on the published layers QAlgorithms_Defs_TensorCode and QAlgorithms_Defs_TannerDecoder. These define the complex, , , , the span, minimum local corrections, the mismatch, Algorithm 2 and the output . The conventions are:
(g, (i, j)) : G × (Bool × Bool), squares are G × A × B, and weights are hammingNorm cast to ℝ.Corrected constants. Theorem 9 is stated with instead of the printed , because Lemma 8 and the proof's give . The goal's error bound uses instead of , which is what the corrected distance supports. Both corrected statements are weaker than the printed ones.
No trivialization. Every vertex must flip a maximum-weight admissible move whenever one exists, and runs range over all such choices. "Logarithmic time" is the per-round contraction factor, not mere eventual termination. Validity is membership of in the -generator span, with the paper's postprocessing output. A formalization that lets vertices idle, drops the maximum-weight rule, or proves only eventual termination does not prove this theorem.
Needed and reusable infrastructure:
Contributions proving the graph lemmas or Lemma 18, whose proof is pure counting, are especially welcome.
High-dimensional statistical learning (HDSL) fits a model with parameters from samples when may far exceed . The standard guarantees for sparse estimators, such as the Lasso, rest on restricted strong convexity (RSC) or restricted eigenvalue conditions on the empirical risk (Negahban et al., 2012; Loh & Wainwright, 2015). These conditions fail or are hard to verify for many losses that matter in operations research and machine learning: nonsmooth losses, losses of neural networks, and M-estimation problems whose population risk is not strongly convex near any sparse vector.
Liu, Ye and Lee (arXiv:1903.00616v2; Operations Research, 2022) remove RSC entirely. They regularize the empirical risk with a folded concave penalty, the minimax concave penalty (MCP) of Zhang (2010), and analyse not a global minimizer (intractable, since the problem is nonconvex) but any point satisfying a weak second-order stationarity condition. They also replace exact sparsity by approximate sparsity: the best sparse vector need only be -optimal for the population risk. Their main result, Theorem 1, gives an excess-risk bound whose sample complexity is poly-logarithmic in .
Observations are i.i.d. copies of a random element of a measurable space . A loss , with parameter , defines the population risk , assumed finite for every and bounded below, the empirical risk , and the regularized objective
with tuning parameters . Norms: is Euclidean, is , is the max norm and counts nonzero entries.
The standing assumptions are:
A vector satisfies the S³ONC (significant subspace second-order necessary conditions, Definition 1) at a sample if it is a KKT point of , with subgradients , and whenever . With , Theorem 1 fixes , where is the constant of the Bernstein inequality (12).
For and any random with satisfying the S³ONC almost surely:
(i) if almost surely and , then with probability at least ,
(ii) if is no worse in than a Lasso solution , the -free bound (22) holds under (21).
are universal constants. The goal fixes the polynomial rate ; the general-rate result is Proposition 1.
The theorem shows that second-order stationarity, which first- and second-order methods can certify (the paper's Theorem 2 gives a pseudo-polynomial algorithm), suffices for poly-logarithmic sample complexity in without convexity or RSC. The paper builds on it for nonsmooth losses through smoothing (Theorem 3) and for regularized neural networks (Theorem 4). The same definitions layer (MCP, S³ONC, A-sparsity) serves those results.
The result is proved on paper, in the electronic companion of the cited preprint. Nothing of it is formalized: the platform has no folded concave penalty, no S³ONC and no excess-risk bound for sparse M-estimation without RSC. This mission provides the definitions, the goal and the proof chain as stated by the authors, with two disclosed adjustments (see Formalization scope).
The obvious argument bounds uniformly over the box and then compares with . It fails: a covering of a -dimensional box costs a factor , not , in the sample size. The usual repair, RSC, which localizes the estimator near a sparse target, is exactly what the paper does without. is moreover only a stationary point of a nonconvex objective, not a minimizer, so no optimality inequality over the whole space is available. The probabilistic part requires keeping the constants consistent across several union bounds and two Bernstein inequalities, with failure probabilities that must stay summable in the sparsity level. In Lean, an additional obstacle is that suprema over uncountable sparse sets are not obviously measurable.
Fin p → ℝ is the sup norm). is the published Orlicz norm HighDimProb.Concentration.subexponentialNorm, always together with an explicit witness of sub-exponentiality. The paper cites the equivalent moment form; the difference is absorbed by the universal constants.bernstein_weighted supplies one.The trivializing formalizations are ruled out explicitly: constants chosen after the instance, junk values of non-integrable expectations, empty infima or undefined derivatives, the sup norm in place of the Euclidean norm, and an estimator chosen by the theorem.
Welcome contributions: proofs of the milestones in order; a Lean proof that Assumption 3 implies (12), via the published Bernstein inequality; a measurable-selection or outer-measure lemma for suprema over sparse boxes, which is reusable across high-dimensional statistics.
Firms often buy key components from the very rivals they compete with in the end market. The paper's examples: Lockheed Martin has sourced engine control systems and gearboxes from AgustaWestland, its competitor in national helicopter markets, while avoiding single sourcing from it in markets where it holds an information advantage; vertically integrated generic-drug makers such as Teva supply active ingredients to finishing-only rivals such as Apotex. Such co-opetitive supply relationships raise an informational problem studied in operations management: the buyer's order quantity reveals what the buyer knows about demand, and the supplier, who is also a competitor, can use that signal when setting her own output. The buyer may therefore distort his orders to hide his information, and the supplier may lower her wholesale price to make revealing it worth his while.
S. H. Jung and P. Kouvelis (SSRN 3555184, 2020; published in Manufacturing & Service Operations Management) analyse this trade-off in a stylized model with a single outside supplier as the buyer's alternative. Their main result, Proposition 4, gives the supplier's equilibrium wholesale price in closed form and identifies when she pays an information rent to learn demand and when she prices to keep the buyer from leaving.
A vertically integrated firm (VI, "she") with production cost normalized to and a downstream outsourcing firm (DO, "he") compete in quantities. The market-clearing price is , where is total output and the demand shock is or (), each with probability . Only the DO observes . Play proceeds in two stages.
In state the VI earns . The paper solves the quantity subgame in closed form. Below the separating/pooling threshold of its equation (3) the DO's order reveals the state (separating quantities, Lemma 1); between and the pooling cap of equation (4) the DO orders the same amount in both states and tops up from the outside supplier in high demand (pooling quantities, Lemma 2); at or above he buys only from the outside supplier (Proposition 1). Averaging the VI's state profit gives , and , and the VI's objective is equation (6):
The analysis is carried out under the paper's standing assumptions: and . The constant is the nonzero solution of equation (7), .
For there is solving such that, for every admissible ,
and for , for every admissible . Here means this price is nonnegative and the unique maximizer of on , and means , approached as . The cap itself is excluded; at the crossing , the separating boundary can attain the same value.
Proposition 4 turns a two-stage signaling game into a two-parameter phase diagram. The VI pays an information rent, by pricing at below the outside price, only when demand uncertainty is low () and the outside market is inefficient (). Otherwise she prices just below the level at which the DO walks away, and the DO conceals his information by pooling and dual sourcing in high demand. The paper builds its welfare comparison (Proposition 5) and its numerical study of the value of the partnership and of information on this characterization.
The result is proved on paper but has no machine-checked proof. The work is explicit real analysis: a piecewise objective with square roots, branch thresholds and a jump, and an optimization over a half-line. The formal statement also records corrections the paper needs (see the scope section), so that a proof checks the intended theorem rather than its typeset version.
is neither concave, monotone nor continuous: the separating piece itself has four sub-branches (the low-demand order hits zero, the DO starts dual sourcing), and jumps down to at . A first-order condition on one formula does not work. The comparison of the two candidates, against , involves nested radicals in and , and its sign changes along a curve that has no closed form. The paper locates that curve only through the monotonicity of in and the sign of its boundary limit; establishing both requires polynomial inequalities over a two-dimensional region with irrational coefficients.
Everything is in ; the parameters are the two reals and , and the decision variable is . The two-point prior is written out as an average of the two states; no measure theory is used.
max 0, and Real.sqrt radicands are nonnegative wherever they are used. Printed slips in the proofs (a for in a limit formula, for ) are corrected in the Lean and disclosed.Contributions welcome: proofs of the milestones, which are self-contained real-analysis statements; reusable lemmas on piecewise-defined maximization and one-sided limits of branch functions; and, separately, a formal treatment of the quantity-subgame equilibria of Lemmas 1–2.
An application platform can increase average quality by excluding low-quality developers, or it can pay high-quality developers to join. Either choice changes the number of applications, the consumer audience, and the fees the platform can charge. Huang, Lyu, and Xu study these linked effects in a two-sided market with consumers and two developer types. Their SSRN paper, §5.1.1 compares exclusion with a targeted subsidy from the platform's perspective. The comparison matters when a platform must decide whether to restrict entry or use payments to shape the mix of applications.
The paper appeared in Management Science in 2021. This mission uses the 43-page SSRN posting, whose page and equation numbering are the source for every target below. Its online appendices are absent from the held posting, so several closed forms that the paper says are available there cannot be cited as printed appendix statements.
A two-sided platform serves consumers and application developers. A fraction of developers are high quality, with application quality ; the remaining fraction are low quality, with quality normalized to zero. Write for the consumer network size, for the total developer network size, and for the high- and low-quality developer counts. Their average quality is when .
Consumers receive base value , a cross-side benefit , and a benefit from total application quality. The separate average-quality preference is fixed to zero in this mission, matching §5.1. Developer types receive cross-side benefits and , while congestion costs them . Consumers and developers also face uniformly distributed differentiation costs on and . The platform chooses a developer access fee and a consumer access fee .
Under exclusion, only high-quality developers can enter, so and . Under subsidization, low-quality developers may enter, and the platform pays each high-quality entrant a fixed amount . The paper's demand equations determine the network sizes from the fees. The resulting profits are
where is the platform's operating cost. The model defines an optimum by comparison with every feasible outcome of the same strategy. Thus the goal concerns the platform's choices and induced participation, rather than a comparison of two isolated algebraic formulas.
The main target is a corrected form of Proposition 4, p. 26. For optimal, interior exclusion and subsidization outcomes in the nonnegative-subsidy regime,
It also asks for a feasible subsidy outcome that reproduces the optimal exclusion outcome: no low-quality entrant, the same consumer and high-quality developer counts, and the same platform profit. The goal is quantified over outcomes that optimize the original fee-and-participation model.
Five milestones follow the paper's attack path: the reduced exclusion profit in §4.1, p. 12; the exclusion optimum in Proposition 1.1(1), pp. 12–13; the reduced subsidy profit in §4.2, p. 16; the optimal subsidy in Proposition 2.2(1), p. 17; and the replication claim in the discussion following Proposition 4, p. 26. Each milestone carries the statement from the SSRN pages and its page provenance.
Profit dominance would mean that, within the specified parameter regime, a platform with the subsidy option can attain at least the exclusion profit. The quality comparison says this gain may come with a lower average quality, even while the consumer and total developer networks grow. The replication clause gives the strategy comparison a direct interpretation in terms of fees and participation. These are distinct claims: a larger total network need not contain more high-quality developers.
The result is already claimed in the paper, but the printed Proposition 4 contains statements that do not hold as written. A formal proof would establish the corrected result for the exact fee, subsidy, and demand model, and would clarify the required regime and interior conditions. The reusable outputs are the model definitions and the reduced-profit identities; other quality-regulation comparisons could build on them. No machine-checked proof of this proposition is claimed here. The draft Lean theorem is an open target.
The fee choices affect participation on both sides, while quality affects consumer demand and developer payments affect the platform's net revenue. Comparing the two optima therefore requires more than observing that a subsidy can raise high-quality participation. In particular, an unconstrained algebraic optimum for can be negative, but the actual subsidy strategy requires . The paper's claim that exclusion is a special case also has to respect this constraint while keeping the same realized network sizes and profit.
The source's part (3) shows another difficulty: high-quality participation, total developer participation, and developer access fees can move in different directions. Treating those quantities as interchangeable would prove a different and sometimes false comparison.
All parameters, fees, network sizes, and profits are real numbers. The Lean model uses the paper's untruncated linear demand equations at . Feasibility requires nonnegative consumer and developer counts; it also requires , , and for subsidization. The high-quality count in consumer demand makes total quality equal to . The composite parameters use the coefficients and signs printed in §§3–4.
The standing parameter condition includes , , , and ; it puts no extra sign on or . The strict inequalities on strengthen the source's because the exclusion inverse demand divides by and the comparison requires both developer types. Separate strict-concavity conditions make explicit the paper's joint-concavity assumption and its use of unique optima. The main theorem assumes interior optimal participation and .
That last restriction is needed for the printed profit-dominance claim. For example, , , , , , , , and give . The paper's printed part (3) also claims and . At its Figure 3 parameters with , . At , , , , , , , , , , and , the subsidy developer fee is , the exclusion fee. The goal therefore states larger total developer and consumer networks and leaves out the false fee comparison.
The goal cannot be discharged by defining profit as its reduced quadratic formula or by merely substituting the reported optimal closed forms: the fee-and-demand definitions and optimality over feasible outcomes remain part of the statement. The development needs real algebra, strict concavity of quadratic objectives, inverse-demand identities, and inequality reasoning at the feasible boundary. The equation identities and basic optimization lemmas are useful contributions beyond this comparison.
A seller who faces the same buyer again and again, a firm that contracts repeatedly with a supplier, or a platform that allocates resources to a returning user can adapt its terms over time. The buyer's behaviour reveals information about their preferences, and mechanisms can link rounds through bundles, discounts and promised future utility. When the principal does not know the distribution of the agent's preferences, adapting looks attractive. This is the repeated-interaction setting of the paper.
Balseiro, Kim and Russo ask whether such dynamics help when the principal evaluates a mechanism by its worst-case regret over a set of possible distributions, the robust objective common in dynamic pricing and online learning. Their answer, under two conditions that hold for a broad class of games, is that dynamics are useless. The optimal minimax regret over rounds is exactly times the single-round minimax regret restricted to point-mass distributions, and repeating a single-round direct mechanism achieves it. This mission formalizes that reduction (Theorem 1 of the paper).
A game consists of a set of shocks , a set of outcomes with a no-interaction outcome , a principal utility and an agent utility , with . The agent's shocks are i.i.d. from a distribution that the agent learns in Round 0 and the principal never sees. The agent observes privately at the start of round .
A dynamic mechanism fixes report spaces , with a report QUIT in . It also fixes decision rules , which depend on the current report, the public history and a private uniform . Finally it fixes a recommended strategy , with and . Here is everything the agent knows and is the agent's private uniform. After QUIT every outcome is .
The principal utility and agent utility of a strategy are the expected sums and . is incentive compatible (IC) if, for every distribution on and every feasible strategy , following gives the agent at least as much as . Because QUIT is a deviation, IC contains individual rationality. With the set of IC mechanisms:
where is the set of distributions the principal guards against.
A direct static mechanism repeats a single-round rule . The agent reports a shock or PASS (which yields ), the rule ignores the history and the round, and the recommended strategy is truthful. is the class of such single-round mechanisms that are IC. Assumption 1 says that for every . Assumption 2 (extreme-point convexity) says that for .
Under Assumptions 1 and 2,
Moreover, an that is within of the single-round infimum satisfies . The multi-round problem has an optimal mechanism if and only if the single-round problem does. No constant is fixed: the statement identifies the value, its near-optimal solutions and the existence of optimal solutions.
In proof order:
Theorem 1 replaces a -round dynamic mechanism design problem, whose decision variables are history-dependent rules over arbitrary message spaces, by a single-round problem over direct mechanisms and point masses. The single-round problem is often a linear program or is solvable with Myersonian methods. The paper uses this to compute the minimax regret for repeated selling of one good (Proposition 3) and to characterize the optimal mechanism of a principal–agent contract model (Proposition 4). For these games it shows that adaptive learning schemes cannot beat a myopic, non-adaptive mechanism under the minimax-regret criterion.
The result is proved on paper. The Lean statements in this mission compile, but their proofs remain open. A complete development would give a machine-checked model of repeated principal–agent interaction with a fully strategic, forward-looking agent: arbitrary report spaces, private randomization, augmented histories, and IC against all history-dependent deviations. It would also check a revelation-principle-type reduction (Lemma 4) whose informal proof leaves measurability and integrability implicit.
The obvious argument restricts nature to point masses and then "repeats the best single-round mechanism". It fails twice. First, an optimal dynamic mechanism may be IC only because of its dynamics; the lower bound needs a single-round mechanism whose IC follows from IC of against deviations that mimic another point mass (Lemma 4). Second, a repeated mechanism must be IC against deviations that condition on the whole past. Showing that one round of such a deviation is itself a single-round deviation (Claim 1) requires the agent to simulate past shocks and the principal's randomness from private noise. Behind both steps sit time-averaged and conditional outcome laws that must be realized as measurable rules of a single uniform.
The Lean game (FutileDynamics.StaticOpt.Game) gives the shock and outcome spaces, utilities, and no-interaction outcome. The mechanism model (FutileDynamics.StaticOpt.Model) imports it and fixes the following conventions, all disclosed in the items:
k : Fin T is round ), and uniforms live on unitInterval.Θ × Bool: reports , and every is PASS and yields . CONTINUE/QUIT is true/false.The statement admits several trivializing formalizations, and the model rules each out:
A complete development needs:
These pieces are reusable for any repeated-game or dynamic-mechanism formalization. Proofs of the milestones, of the lower and upper bounds, and of auxiliary measurability lemmas are welcome.
In participatory budgeting, residents of a city vote on how to spend part of a public budget on a list of proposed projects, each with a known cost. The practice has been adopted by cities in North America and Europe, including New York City, Chicago, Madrid and Paris, the last two each spending more than 100 million euros through participatory budgets in 2017 (Cabannes, 2004; paper §1). Every deployment must choose a ballot: voters may be asked to approve some projects, to rank them, or to fill a knapsack within the budget. The ballot determines how much information about the residents' preferences reaches the aggregation step, and so how much welfare the chosen set of projects can guarantee.
The implicit utilitarian framework of Procaccia and Rosenschein (2006) makes this question quantitative. Voters are assumed to hold cardinal utilities, which the ballot reveals only partially; the quality of a ballot-plus-aggregation pair is measured by its distortion, the worst-case ratio between the best achievable welfare and the welfare it actually obtains. Benadè, Nath, Procaccia and Shah (Management Science, 2021; AAAI 2017 conference version) apply this lens to participatory budgeting and compare the input formats used in practice. Their main positive result is that threshold approval votes with a randomly drawn threshold reach distortion , against for a rule that uses no information at all and for any deterministic threshold.
There are voters and a set of alternatives (projects). Alternative costs , and the budget is . Write , and let
be the family of inclusion-maximal budget-feasible sets.
Voter has a utility for each alternative, utilities are additive over sets, and they are normalized: . The social welfare of a set is .
A threshold approval vote at threshold is the set . A randomized threshold rule chooses a threshold at random and maps the resulting profile to a (possibly random) set in . In the formalization, a rule is a finite mixture of arms; each arm has a probability, a threshold, and a deterministic aggregation map from approval profiles to (ThresholdRule), and its expected welfare is the weighted sum over arms (ThresholdRule.expWelfare). The rule never sees the utilities, only the approval sets. The distortion of a rule is bounded by when
and the distortion associated with an input format is that of the best rule for it.
The goal fixes only the shape , with an absolute constant chosen before , and the costs, and it covers every .
For , with , , , cost buckets ( uses ) and counts . In the statements involving , it is an optimal member of for the given utility profile (IsWelfareOptimal).
The theorem separates randomized from deterministic elicitation: with a fixed threshold no aggregation rule beats (Theorem 3.4 of the paper), while drawing the threshold at random brings the distortion to , close to the lower bound of Theorem 3.6. It is the paper's argument for threshold approval as a practical, low-burden ballot, and it supports the empirical comparison in the paper's §5 between input formats on data from real participatory budgeting elections.
The result is proved in the paper; no machine-checked version is known. A formalization yields a reusable layer for implicit utilitarian voting with budgets (feasible-set families, normalized additive profiles, randomized rules over partial ballots, distortion), on which the paper's other bounds (Theorem 3.3 for rankings, Theorems 3.4 and 3.6 for lower bounds) and the related literature on distortion can be stated. It also makes explicit the reading of distortion under a random threshold that the proof actually uses.
The obvious rule picks the threshold and then funds the most-approved projects greedily. It fails because one threshold cannot serve both high-utility and low-utility voters, and because popular projects may be expensive: approval counts say nothing about costs. Mixing over thresholds alone does not help either; the ratio for a single badly chosen threshold can be of order . What has to be shown is that one fixed mixture, chosen before any utilities are seen, recovers a share of the optimum simultaneously for every profile, despite rounding of utilities into intervals, budget constraints within each cost class, and the loss of everything below the smallest threshold.
All objects live in PBElicit.RandThresh (definition file PBElicit.RandThresh.Setting). Voters are Fin n; alternatives are a Fintype with = Fintype.card A. Utilities are real, nonnegative and normalized (IsUtilityProfile); costs satisfy , which the paper uses when it calls a single alternative budget-feasible. Rules must return sets of (IsMaxFeasible); the paper's mechanisms return feasible sets, which are extended to maximal ones. The maximum over is stated as "for every "; distortion bounds are multiplicative. Logarithms are base . The milestones take , as the paper's proof does; the goal does not.
Distortion is read as the optimum over the total expected welfare (threshold and aggregation together), which is what the proof of Theorem 3.5 bounds; the paper's displayed definition puts the expectation over the threshold outside the ratio. The interval bound (8) is formalized as its outer inequality, because the printed middle step fails when a utility equals a threshold exactly.
The rule is fixed before the utilities, sees only threshold approval votes, and must return an inclusion-maximal feasible set; choosing the rule after the profile (which makes distortion trivially) is excluded by the quantifier order, and the uniform rule of Observation 3.1 only gives distortion , so a bound is a genuine improvement.
Welcome contributions: proofs of the milestones, the reduction from general to the next power of , and further results of the paper stated on the same definitions.
Many allocation problems hand out indivisible goods without money: course seats, shifts, donated food, inherited items. An integral allocation of such goods can rarely be envy-free. With one good and two agents, someone always envies. The standard remedies are of two kinds. Randomization restores fairness in expectation: the probabilistic serial rule of Bogomolnaia and Moulin (J. Econ. Theory 2001) yields a fractional allocation that is envy-free and can be implemented as a lottery over integral allocations. Approximation restores fairness after the draw: envy-freeness up to one good (EF1), introduced by Lipton, Markakis, Mossel and Saberi (EC 2004) and named by Budish (J. Political Economy 2011), asks only that any envy disappear once a single good is removed from the envied bundle.
The two remedies pull apart. Giving all goods to one agent chosen uniformly at random is envy-free ex-ante, but after the draw one agent holds everything. Round-robin picking with a uniformly random order is EF1 after every draw, and proportional but not envy-free in expectation (Proposition 2 and Example 1 of the paper). Freeman, Shah and Vaish (arXiv:2005.14122, 2020; with Aziz, Operations Research 2024) ask whether one lottery can be fair in both senses at once. They show that it can, and that the answer depends on how the lottery is built, not only on which fractional allocation it implements.
There is a finite set of agents and a finite set of goods. Agent has an additive valuation with values . A fractional allocation is a matrix with the share of good given to agent , and . An integral allocation gives each agent a bundle , with bundles pairwise disjoint, and . A randomized allocation is a finite lottery over integral allocations. It implements the fractional allocation .
is envy-free (EF) if for all . An integral allocation is EF1 if for all with some satisfies . A lottery is ex-ante EF if the allocation it implements is EF. It is ex-post EF1 if every allocation it draws is EF1.
The eating protocol runs for one unit of time on the goods , each of mass one. At every moment each agent eats her favorite good among those not yet fully consumed, at rate one. Recursive Probabilistic Serial (Algorithm 1) proceeds in stages, starting from . Stage computes and decomposes it as by the generalized Birkhoff–von Neumann theorem, Theorem 1 of the paper. It then draws with probability and continues on . The final bundles are .
For every instance, every way of breaking ties between equally valued goods, and every decomposition rule satisfying the conclusions of Theorem 1,
Theorem 2 shows that ex-ante envy-freeness and ex-post EF1 are compatible for additive goods. Algorithm 1 is a constructive witness. The paper builds on this in two directions. A polynomial-time variant (§3.2) computes such a lottery. An impossibility result (Theorem 3) shows that adding ex-post fractional Pareto optimality is too much. The paper also extends the approach to bads and mixed manna (§7), where the natural extension guarantees only ex-post EF2.
The result is proved on paper. No formalization of probabilistic serial, the eating protocol, EF1 of randomized allocations or the rectangular Birkhoff–von Neumann theorem with floor and ceiling bounds is known to us in any proof assistant. Mathlib has the square doubly stochastic case (doublyStochastic_eq_convexHull_permMatrix), and Prove2Me has it as FamousTheorems.birkhoff_von_neumann. This mission asks for a machine-checked proof of Theorem 2 about an explicit definition of the eating protocol and of Algorithm 1.
The proof is short on paper but hides two pieces of continuous-time bookkeeping. First, the eating protocol is a process in time. The stage statements need a description of it in which "agent ate a positive share of while was still available" can be stated and checked. Second, the ex-ante argument conditions on the history of earlier draws. Because the decomposition may have exponentially many branches, it has to be turned into an induction over the recursive lottery. The obvious shortcut, proving the result for "the" BvN decomposition of each stage, fails because the decomposition is not unique and the theorem must hold for all of them. Weight-zero terms of a decomposition can violate Lemma 1. They are never drawn, but any argument over the whole support must exclude them explicitly.
Agents and goods are finite types with decidable equality. The good set is the whole type of goods, and is [Nonempty N]. Values are real and non-negative. All quantities are in , and is Nat.ceil of a real quotient. Integral allocations are bundle maps N → Finset G, and lotteries are finite lists of (probability, allocation) pairs.
The eating protocol is a definition computed event by event. Between events every agent eats a fixed good chosen by a choice rule. The next event comes when the time budget ends or a good being eaten is exhausted. The minimum runs only over goods actually being eaten, so no division by zero occurs. events suffice, and later iterations change nothing. Algorithm 1 is a definition: a recursion over stages producing a lottery over stage histories.
The only free parameters of the goal are the tie-breaking rule, constrained to choose a most valuable available good, and the decomposition rule, constrained to satisfy Theorem 1's conclusions. The eating outcome, the lottery and its support are computed by the definitions, never assumed. A statement taking or the lottery as free variables with envy-freeness as a hypothesis would trivialize the goal and is not this mission.
Conventions that differ from the page:
Not included are Proposition 1, the §3.2 polynomial-time variant, the SD-EF remark after Theorem 2, and §§4–7 (Theorem 3, the group-fairness results, the MNW characterization, bads). A proof of Theorem 1 in this rectangular form, with the floor and ceiling bounds, would be reusable well beyond this mission, for example in other fair-division and assignment results. So would a clean theory of the eating protocol. Contributions to either are welcome.
In call centers, hospitals and other service systems, customers who wait too long leave: each has a patience time, and abandons the queue once the wait in queue exceeds it. Empirical work has found that service times and waiting are dependent. Customers who waited longer often need longer (or shorter) service, and those who were served are a self-selected group: they had enough patience to wait. Two models of this dependence are in use.
The two models suggest different statistical procedures. Estimating an exogenous dependence means fitting a two-sided censored bivariate distribution. Estimating an endogenous one means a univariate patience estimate (Kaplan–Meier) plus a conditional service-time distribution per delay. Wu, Bassamboo & Perry (2022) prove that, as far as the law of the queueing dynamics is concerned, every exogenous dependence is an endogenous one. The simpler estimation procedure therefore never loses generality.
A service system has identical servers. Customers arrive one at a time, at times , and are served first come, first served. A customer who finds a free server starts service at once. Otherwise the customer waits, and abandons if the wait exceeds the customer's patience.
The offered wait of customer is the time the customer would wait with infinite patience. With the sorting operator (which sorts a vector of in increasing order), , and interarrival times , the offered-wait vectors follow the recursion
Here is the patience of customer and the service time it requires at offered wait .
The queue is described by the process , . Its components are:
and , the numbers of customers in service and in queue;
, which lists the idle servers as zeros, followed by the remaining service times in increasing order;
, the elapsed waiting times of the customers in queue, in decreasing order and padded with zeros;
, the time to the next arrival.
Exogenous dependence . The pairs are i.i.d. with joint density on , and independent of the arrivals and the initial state. The service time does not depend on the wait. The patience marginal is .
Endogenous dependence . The patience times are i.i.d. with density . Customer has a virtual service-time process whose value at has density . These are independent across customers, of the patience and of the arrivals.
and denote the laws of the process . The two dependencies are equivalent (Definition 1) if these laws agree for every arrival process and every , whenever the initial states agree in law.
For every joint density on , the pair
is an endogenous dependence (a patience density and a conditional service-time density), and it is equivalent to :
The theorem shows that the systems with exogenous dependence form a subclass of those with endogenous dependence. Two consequences follow:
The formula for also explains the self-selection effect. It is the service-time density of a customer, conditioned on having patience exceeding the offered wait.
The paper's proof omits the verification step "for brevity". It also states the law-determination facts (milestones 2 and 6) without proof, and treats an initially empty system. A formal proof would supply the per-customer density computation, the measure-theoretic construction of the coupled system, and the measurability of the path map.
The obvious argument would compare the two systems customer by customer with the same random draws. It fails: in the exogenous system the service time and the patience are drawn together before the customer meets the queue, while in the endogenous system the service time is drawn after the offered wait is known. Equality holds only in law, through a coupling built on a new probability space, and the coupled pairs must be shown to be i.i.d. with density even though they are constructed from the state of the queue.
Two technical points are not visible in the paper. First, the law of the whole path must be shown to be determined by the primitives. This requires measurability of a map built from sorting, counting and an infimum over arrival indices. Second, the conditional densities in (1) and in steps (ii)–(iii) are ratios whose denominators can vanish, so null sets need care.
Everything lives in the namespace DelayDep.Equiv. The conventions are:
NNReal. The law of is the image measure on NNReal → State n with the product σ-algebra, which is the σ-algebra of the finite-dimensional distributions.withDensity.Every law equality includes the almost-everywhere measurability of both path maps as part of its conclusion. Without it, the equality could hold trivially through Lean's convention that the image of a measure under a non-measurable map is . For the same reason, the goal also asserts that (1) defines densities, so that the endogenous systems it quantifies over are not vacuous.
Out of scope are Theorem 2, the necessity half of Lemma 1, Example 1, Theorem A.1 and the estimation section §4. Useful contributions are: