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?
Classical Max Cut asks for a partition of the vertices of a weighted graph that maximises the total weight of edges crossing it. Its best-known approximation algorithm, due to Goemans and Williamson, rounds a semidefinite relaxation and guarantees ratio . Quantum Max Cut is the analogous problem for a family of local Hamiltonians: each edge contributes a two-qubit term that rewards the two qubits for being antisymmetric, and one asks for the maximum energy of the sum. Estimating it precisely is QMA-complete (Piddock and Montanaro), so attention has turned to efficient approximation algorithms, and to the question of which classes of quantum states can certify a good fraction of the optimum.
A short history of the approximation ratio on weighted graphs:
Let be a simple graph on with nonnegative edge weights (the paper's standing assumption). Each vertex carries a qubit; a state is a vector , and it is a unit state if . With the Pauli matrices acting on qubit written , the quantum Max Cut Hamiltonian is
each edge counted once. The term equals twice the projector onto the singlet , so is positive semidefinite, and
Two weight statistics appear throughout: the total weight and, for a vertex , , the largest weight of an edge incident to (zero for an isolated vertex).
A tensor product of 1- and 2-qubit states is obtained by partitioning the qubits into blocks of size one or two (a pair need not be an edge of ), choosing a unit vector of or for each block, and multiplying the block amplitudes. Product states (all blocks of size one) and singlets placed on a matching are examples; a generic entangled state of three qubits is not.
For every graph with nonnegative weights there is a tensor product of 1- and 2-qubit states such that
The constant is the exact minimum of the optimisation problem (28) of the paper.
The proof combines an upper bound on with three candidate states:
The result shows that the limitation of product states for quantum Max Cut is not a limitation of efficiently describable states: allowing entanglement only within disjoint pairs of qubits already guarantees a fraction strictly above on every weighted graph, including those (a single heavy edge) where product states are stuck at exactly . The accompanying algorithmic statement (an efficient randomized algorithm with ratio ) improved the best known efficient approximation ratio at the time. The upper bound of Lemma 1 is a quantitative form of monogamy of entanglement on a star: the centre qubit cannot be maximally entangled with all of its neighbours.
The theorem is proved in the paper; none of it is formalized. A complete development gives a machine-checked model of a frustrated quantum spin Hamiltonian on arbitrary weighted graphs, a formal upper bound on its ground-state energy, and an explicit certified family of entangled states. The final step, (28)–(29), is evaluated in the paper "by a computer"; a formal proof replaces that evaluation.
The obvious upper bound, , is too weak: it allows every edge to be maximally entangled simultaneously, and with it no ratio above follows. The improvement needs the star bound of Lemma 1, which the paper derives from the Lieb–Mattis theorem on the spin of the ground state of bipartite antiferromagnets, restricting the problem to the Hamming-weight-one sector where the Hamiltonian becomes a weighted graph Laplacian. Neither Lieb–Mattis nor the angular-momentum decomposition of is available in Mathlib. The combinatorial side (Lemma 2) needs a careful choice of a maximal incident edge at each vertex and an argument that these edges form no cycle. Eq. (25) is an exact energy computation for a state that is entangled across a matching.
Fin n, basis configurations Fin n → Fin 2, states (Fin n → Fin 2) → ℂ, operators complex matrices indexed by configurations; onSite i σ places a matrix on qubit . The graph is a SimpleGraph (Fin n); weights are w : Sym2 (Fin n) → ℝ with ∀ e, 0 ≤ w e in every statement. sums over the ordered representatives of the edges, so each edge is counted once. The energy is the real part of .onSite, energies of computational basis states (equal to cut values), partial-trace style computations for tensor products of blocks, and a Laplacian/Gershgorin bound; the Hamiltonian layer is reusable for later quantum Max Cut missions. Contributions of any of these as separate lemmas are welcome.Permutation of tensor factors is a basic operation in quantum information and in the algebra of braids. A braid representation assigns an operator to each crossing so that different drawings of the same braid act identically. A Yang–Baxter equation adds spectral parameters to this local consistency condition; such families appear in integrable lattice models and in constructions of quantum gates. The paper by Zhang, Kauffman, and Werner asks when one operator family built from permutation and partial transpose can meet both requirements. It connects two familiar operations on bipartite matrices with algebraic relations on three tensor factors.
The article studies several related representations and two main theorems. This mission concerns Theorem 1 in §6.3 and the source equations that support it. The theorem is a classification of a specific three-term family, not a claim about arbitrary Yang–Baxter solutions. The paper's printed wording has degenerate counterexamples already present elsewhere in the same article. The target here makes their exclusions explicit, so that the formal statement records the intended classification. The source is the first arXiv version, quant-ph/0606005v1; page and equation numbers below refer to that version.
Fix an integer and let with its standard basis. The permutation operator acts on by . The partial transpose transposes the matrix index belonging to the second copy of . Write . This operator is and satisfies . In dimension two the paper also uses ; the star's position matters, since and are different matrices. These definitions and identities are in §2.1, pp. 5–6.
For fixed complex coefficients and , the family under study is
Here is the spectral parameter: it is the coefficient of . On , the subscripts and mean that an operator acts on the first two or last two factors, with the identity on the unused factor. The braid relation is . The paper considers two parameterized versions, with multiplicative law in equation (14) and additive law in equation (15):
The equations are identities for all indicated parameter pairs, with fixed. The source gives the braid relation as (54), defines the family in (69), and states the two Yang–Baxter forms in §3.1 and §5.
For and , classify this family by three equivalences. At every nonzero ,
If , the family satisfies the additive equation (15) for all exactly when and . The family satisfies the multiplicative equation (14) for all exactly under the same dimension and coefficient condition. The source's “only for” statement and the sufficiency part of its proof support equivalences; the explicit guards correct the printed exceptions. This is the mission goal.
The milestones capture the source's operator identities and ; the dimension-two braid and mixed relations (66)–(67) for and ; the second dimension-two braid branch displayed in (70); the coloured identity (74) for ; the necessary coefficient system (127) above dimension two; and Appendix B's higher-dimensional exclusions, stated with the same corrected guards. These are the source's own named or displayed claims in the order useful to a reader of the goal.
The result locates the precise dimension in which this particular linear combination supplies braid and spectral-parameter solutions simultaneously. It also distinguishes two braid branches: gives the parameterized family , while gives another fixed braid matrix. Above dimension two, with the stated nonzero conditions, neither branch survives as a solution of the three requested relations. This keeps a tempting general-dimensional extrapolation from being treated as a theorem.
The source result is a published mathematical argument, but these Lean statements are proposed open goals. A completed mission would produce machine-checked proofs for the classification and its selected intermediate identities in one reusable matrix representation. The definitions of permutation, partial transpose, and the two three-factor placements may also serve later formalizations of braid and Yang–Baxter calculations. This mission does not claim to formalize the paper's second theorem, its full virtual braid group development, or its later applications to gates and Hamiltonians.
The dimension-two formulas are finite matrix identities, but the classification asks for necessity as well as sufficiency. Verifying the displayed solution matrices alone cannot rule out other coefficients. In higher dimension the paper compares terms in an expansion on three tensor factors. Its observation that the ambient vector space has dimension does not by itself establish independence of the 15 operators being compared; a formal proof must justify every coefficient conclusion that it uses. Appendix B's sentence about a unique solution at fixed parameters also has degenerate counterexamples, so the milestone records only the necessary equations (127). These issues make the source's computational looking argument a substantive formalization task.
The Lean model takes and represents two-factor and three-factor operators by matrices indexed by Fin d × Fin d and Fin d × Fin d × Fin d. Fin d starts at zero while the paper labels basis vectors from one; this only changes names of indices. Tensor placement is defined entrywise, with the identity matrix on the unused factor. Scalars and spectral parameters are complex. The goal quantifies over every natural-number dimension , every fixed with , and every indicated spectral parameter. In (14), the paper introduces and , hence initially nonzero. The Lean predicate quantifies over all complex ; for polynomial matrix identities these formulations are equivalent.
The definition is retained explicitly. Replacing it by an unrelated matrix with a convenient identity, fixing the dimension to two in every definition, or varying the coefficient as the spectral parameter would change the problem. The guard excludes the higher-dimensional braid family from §6.1, (60), and excludes the rational additive solution in §3.2, (21). At , all three basic matrices are scalar, so the paper's implicit convention is stated. Contributions that establish the shared identities, the two-dimensional coefficient classification, or the uniform higher-dimensional exclusions all advance the target.
A quantum computer that runs long computations must protect its data with a quantum error-correcting code and must compute on the encoded data without letting errors spread. The simplest gates with that property are transversal gates: a code is laid out in several code blocks, and a transversal gate couples each physical subsystem of one block only to the corresponding subsystem of the other blocks, so a single fault never becomes several faults inside one block (Gottesman 1997; Aliferis, Gottesman, Preskill 2006). Every known code has some encoded gate that is not transversal, and fault-tolerant schemes pay for the missing gates with expensive constructions such as magic-state distillation. Whether some code has a universal transversal gate set was a long-standing question.
Timeline.
A composite quantum system consists of finitely many physical subsystems , subsystem having dimension . Operators on are complex matrices on . A product operator is with acting on subsystem , and is the group of unitary product operators ().
A quantum code is a subspace of the state space, represented by the orthogonal projector onto it; its dimension is the dimension of the encoded system, and the code is nontrivial when this dimension is at least . An error is detectable when . The code is local-error-detecting when every error on any single subsystem is detectable: for every operator acting on one subsystem.
A unitary is logical when it preserves the code space,
and denotes the logical unitary product operators. An encoded unitary is a unitary operator of the code space (, ). A set of unitaries is universal when every encoded unitary is approximated to arbitrary accuracy by the actions , , on the code space.
For a code made of blocks , each with subsystems at the same positions and a block code , the joint code is . The transversal part collects subsystem of every block, and a transversal unitary is a product of unitaries, one on each transversal part.
For block codes , each local-error-detecting, with , the set of transversal logical unitaries is not universal:
The same conclusion for product operators on the physical subsystems of a single local-error-detecting code with .
In attack order: Lemma 1 (logical unitaries form a group); Lemma 2 (logical unitaries in a closed group of unitaries form a closed subgroup); is a compact group; the derivative step ; elements of the Lie algebra of are sums of local Hermitian operators; for a logical sum of local Hermitians; the identity component of acts on the code space as a scalar; has finitely many actions on the code space up to phase; Theorem 1; and the detectability of an error on a single transversal part.
The result. The theorem rules out the simplest route to fault tolerance for every code that detects single-subsystem errors, which includes every code of distance at least . It explains why every fault-tolerant architecture needs a non-transversal ingredient (state injection and distillation, code switching, gauge fixing, measurements with feed-forward), and it is the starting point for later refinements: approximate and covariant versions for continuous symmetries (Faist et al. 2020), and restrictions on the level of the Clifford hierarchy reachable transversally (Bravyi–König 2013).
Formalizing it. The result is proved; no machine-checked proof of it is known to exist. The mission produces a checked statement of the theorem for arbitrary finite-dimensional subsystems and arbitrary (non-stabilizer) codes, together with a reusable layer: tensor-product operators on index-typed subsystems, codes as projectors, logical operators, local error detection, encoded universality and block codes. Related platform items are QAlgorithms_Defs_QECC (qubit stabilizer codes, detectability for submodule codes) and QAlgorithms.GottesmanIntro.knillLaflamme (the error-correction criterion), which use a different model of codes and are not imported here.
The paper's argument runs through Lie theory: is a closed subgroup of the compact group , so it is a compact Lie group with finitely many connected components; its identity component is generated by exponentials of its Lie algebra, and local error detection forces that Lie algebra to act on the code space by scalars. None of this is about the code alone; the difficulty is the passage from a closed matrix group to its Lie algebra and back (exponential coordinates, connectedness of the identity component, finiteness of the component group of a compact Lie group). Mathlib has the matrix exponential and compactness of the unitary group but not Cartan's closed-subgroup theorem or the Lie algebra of a closed matrix group.
A frequent first idea, that itself is a finite group, is false: every global phase is a logical product unitary, so always contains a circle. Only the action of on the code space is finite, and only up to phase; a statement that ignores the phase is false.
Subsystem is a finite index type (so ), and the system has basis ; operators are Matrix over ℂ, unitaries are Matrix.unitaryGroup. A code is its projector (Hermitian, idempotent) and its dimension is Matrix.rank; "nontrivial" is . Closure is in the standard topology on complex matrices, which is the topology of any norm. Exponentials are NormedSpace.exp with the factor of the physics convention (footnote 1).
Disclosed restatements:
Universality is defined only through approximation of encoded unitaries, local error detection quantifies over every matrix on one subsystem, and is the full intersection of with the logical unitaries, so no hypothesis trivializes the conclusion; at rank the conclusion is false, which is why the rank hypothesis is and not .
A complete development needs the Lie algebra of a closed subgroup of Matrix.unitaryGroup, connectedness of the identity component via exponentials, and finiteness of the component group of a compact matrix group. These parts are reusable far beyond this mission, and contributions of them, as well as alternative proofs of Theorem 1 that avoid Lie theory, are welcome.
Many operations decisions are made over discrete, high-dimensional choices whose cost can only be estimated by simulation: how many bikes to place at each station, which subset of facilities to open, how to allocate servers in a queueing network. Each evaluation of a candidate decision is a noisy run of a simulator, and the goal is to select a decision whose true expected cost is close to optimal with high probability. Classical ranking-and-selection procedures compare every candidate, which is hopeless when the number of candidates is or .
Zhang, Zheng and Lavaei (arXiv:2010.16250, Operations Research, 2023) show that when the expected cost is L♮-convex (on : submodular), the problem can be solved with a number of simulation runs that grows only polynomially in , by running a stochastic subgradient method on a convex extension of the objective and rounding the result. Their headline upper bound for the case is simulation runs; this mission formalizes its correctness half.
A decision is a set , identified with its indicator vector . A simulator returns, at decision , a random output whose mean is the objective . Independent runs give independent outputs. Three assumptions are standing:
A consistent permutation of orders its coordinates decreasingly, ; the neighbouring points are and . The Lovász extension (2) is
The estimator (4) of its subgradient at uses two fresh runs per coordinate, . Algorithm 2 starts at a vertex , truncates each estimate coordinatewise to (), takes a step with the projection onto , and averages . Algorithm 1 then simulates times at each neighbouring point of and returns one with the smallest sample mean. A solution is -PGS (probability of good selection) if, with probability at least , its objective value is at most above .
With , , , and
Algorithm 2 with followed by Algorithm 1 returns with
whatever tie-break the final argmin uses.
The milestone list follows the paper's proof: the deterministic properties of the Lovász extension (permutation independence, Lemma 2(i)–(iv), eq. (6)), unbiasedness of (4), the truncation-bias bound (Lemma EC.2), the Azuma-type inequality (Lemma EC.1) and its application to the iterates (Lemma EC.3), the projected-step regret bound (Lemma EC.4), and the rounding guarantee (Theorem 1).
The theorem certifies that a first-order method solves stochastic submodular minimization to PGS accuracy. At the proof's parameter choices, its simulation budget is ; the paper gives an asymptotic upper bound that also includes a term proportional to . Section 5 of the paper shows lower bounds of order . The truncation step improves the asymptotic dependence on relative to untruncated SSGD (p. 20).
The result is proved in the paper; nothing in it is machine-checked. A formalization adds three things. It pins the choices of Theorem 2 to the explicit constants of its proof. It repairs two statements: Lemma EC.2 is false at the printed truncation level (counterexample below), and Lemma 2(ii) is false as an equality of argmin sets. And it produces reusable infrastructure: the Lovász extension on the box with its subgradient, and a tail form of Azuma's inequality that Mathlib does not have (Mathlib's version takes conditional moment-generating-function bounds).
The deterministic layer is classical but has edge cases: ties among coordinates (several consistent permutations), the boundary of the box, and . The convexity of the Lovász extension of a submodular function is the substantial fact there.
The probabilistic layer is where the obvious argument breaks. The iterates are random and depend on all earlier simulation runs, and the consistent permutation at is a discontinuous function of , so the estimator at step is evaluated at random points chosen by the past. The analysis must condition on the past, use the independence of fresh runs, and control a biased estimator: truncation makes steps bounded but biased, and the bias bound must hold uniformly over points where the true subgradient coordinate can be as large as . Lemma EC.3's printed proof treats as sub-Gaussian with proxy , which a sum of absolute values is not, so its tail estimate has to be obtained differently. Finally, the rounding step evaluates sample means at random points determined by , so Hoeffding's inequality is applied conditionally on .
Decisions are Finset (Fin d), points of the box are Fin d → ℝ in Set.Icc 0 1, and indices are 0-based (nbr α i is ). The Lovász extension is evaluated with a canonical consistent permutation (Tuple.sort of ); a milestone shows any consistent permutation gives the same value. Submodularity is the published definition NonmonotoneSubmod.Shared.Submodular.
The simulator is a family of mutually independent random vectors indexed by slots: for each iteration , coordinate and one gradient slot, and for each neighbouring point and replication one rounding slot. Each slot is measurable and its output at each is centred at and sub-Gaussian with proxy (Mathlib's HasSubgaussianMGF). Since each slot is read at one point only, identical distribution is not assumed. The failure probability is bounded for the event "some minimizer of the sample means is bad", as an outer measure, so no measurability of the output is presupposed.
Deviations from the page, all disclosed in the item notes:
Trivializing readings are excluded. The oracle is centred at and has independent slots; is a permitted variance proxy, so a zero-noise oracle is allowed. The bias is that of the truncated estimator. The hypotheses of the goal are jointly satisfiable (for example , , , , , with a zero-noise oracle). Contributions of reusable lemmas, in particular the Lovász-extension layer and the tail-form Azuma inequality, are welcome as separate theorems.
DiscreteConvex.MConvexSetsB.lovasz_convex_iff_submodular). https://doi.org/10.1137/1.9780898718508Whether a customer joins a queue depends on how long she expects to wait. In the classical observable-queue model of Naor (1969), the service rate is known, and a longer queue only means a longer wait: customers avoid the crowd (ATC), so the more willing others are to join, the less willing the individual is. Many services do not publish their capacity. Staffing in banks, clinics and government offices varies by shift for internal reasons that a customer in the waiting area cannot see. A customer who knows the distribution of capacity, but not its realization, can learn something from the queue itself, and what she learns depends on how others behave.
Yang, Shang and Liu (SSRN 4159035, 2022; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1139) show that this inference can reverse the classical conclusion: an individual may follow the crowd (FTC), joining more often when others join more. Their Proposition 2 characterizes, in closed form, the reward–cost ratios at which this happens. Follow-the-crowd behaviour is the source of multiple equilibria and of the value of disclosing capacity, which the later sections of the paper study.
The service rate of a single-server queue is with prior probability and with probability , where and . Customers arrive as a Poisson process of rate , receive reward from service, and pay per unit of time spent in the system. An arriving customer sees the number of customers present, not the rate. Assumption 2 requires , so that a customer facing an empty queue always joins. The queue never exceeds , and for .
The other customers follow a joining vector : a customer who sees others joins with probability . Given , the queue length is a birth–death process with stationary law
A tagged customer who sees updates her belief of high capacity by Bayes' rule, which takes the closed form
and her expected utility of joining is
Her best response is to join when (Assumption 1) and at the empty queue, and to balk otherwise. Her ex-ante joining probability is
Finally, the threshold profile , , joins at queue lengths up to , joins with probability at , and balks above. We write , and for the quantities under .
There exist and with if and only if, for some ,
In attack order:
The goal is an exact characterization: it says for which parameter values a rational, Bayesian customer's tendency to join increases with that of the crowd. With known capacity, the congestion effect alone acts and the behaviour is always ATC. FTC is therefore a pure consequence of inference from the queue. The characterization is what the paper's equilibrium analysis (multiple equilibria under FTC) and its comparison of capacity disclosure policies build on.
The formalization adds two things. First, it checks a closed-form characterization against its definitions at every parameter value. The "if" direction of Proposition 2 as printed fails: at , , , , , (so ), the printed interval condition holds at , but the tagged customer starts joining at state 5 while state 5 is still unreachable, and never increases. The goal is the corrected statement. Second, none of the paper's results is machine-checked anywhere; the mission produces the first formal development of a Bayesian strategic queue.
The paper's proof of Proposition 2 runs as follows. The utility increases in , so at a unique the customer's threshold moves from to , and continuity of the law in makes jump up. The step that fails is the jump: it adds , which is zero when state is unreachable under , that is, when . The correction moves the upper endpoint from the belief at to the belief at .
The converse direction, which the paper does not argue, needs the congestion effect in quantitative form. Between crossings, the best response is fixed and is a fixed cumulative probability of a queue that grows stochastically with , so it cannot increase. Every increase must come from a jump at a reachable state, and turning that into the interval condition requires the strict monotonicity of the belief in on . Neither monotonicity in the joining vector (Lemma 2) nor first-order stochastic dominance (the congestion effect) follows from a one-line computation. Each is a ratio comparison of truncated sums, and , in which every coordinate of enters many terms.
All objects live in one definition item, FollowCrowd.Inference.Model, built on Mathlib alone. States are natural numbers, and joining vectors are functions , of which only the coordinates enter the law. is Nat.floor, and sums run over Finset.range (Nbar + 1).
The formalization commits to five conventions, each disclosed in the item statements:
The trivializing formalization to rule out is one that takes the crossing point or the jump of as a hypothesis. The goal quantifies over and and compares values of , which is defined from the primitives. The hypotheses are satisfiable (Figure 1's parameters satisfy them), and the counterexample to the printed statement is checked in Lean in exact arithmetic.
A complete development needs:
The likelihood-ratio and stochastic-dominance lemmas for truncated product-form laws are reusable beyond this mission. Contributions are welcome on any milestone, and in particular on the two monotonicity results (Lemma 2 and the congestion effect), which both directions of the goal use.
Firms launching a new product often open a sign-up waitlist before they can serve everyone, and many of them reward customers who invite friends with a better place in line. Robinhood (commission-free trading) and x.ai (AI email scheduling) ran such referral priority programs, the first with full priority for referrers and the second with a partial jump in line (paper, p. 2). The design question is operational as much as it is about marketing. Priority for referrers brings in more customers, but those customers add to the congestion that the waitlist exists to ration, and every customer moved forward pushes someone else back.
L. Yang, Invite your friend and you'll move up in line: optimal design of referral priority programs (Manufacturing & Service Operations Management 23(5), 2021; doi:10.1287/msom.2020.0868), treats the waitlist as a queue and the referral reward as a scheduling policy, and asks which posted delays maximize the number of customers acquired. Its predecessor, Yang and Debo (2019, Management Science), fixed the scheduling policy to full priority for referrers. The 2021 paper optimizes over all operationally achievable policies, and its main result, Proposition 4, shows that the optimum depends on the base market size: depending on that size it is partial priority, full priority, or a policy that deliberately idles the server.
The waitlist is a single-server queue with exponential service of rate , the firm's capacity. Base customers arrive as a Poisson process of rate , the base market size. Every customer values service at and pays a waiting cost per unit of time spent in the system. On arrival a customer joins with probability . A joining customer chooses a referral effort at cost , and with probability her friend arrives and makes the same decisions. A referral converts if the friend joins.
The firm posts two expected delays: for customers whose referral converted, and for everyone else. A joining customer who exerts effort while others join with probability gets expected utility
Joining is then a compound Poisson stream with geometric batches, and the system throughput is .
Problem 1 maximizes the throughput over and , subject to:
labelled (6a), (6b), (6c);
The paper assumes throughout (Assumption 1). The first-best problem is Problem 1 without incentive compatibility. A posted policy is work-conserving if (6a) binds; full priority if (6a) and (6b) both bind; partial priority if (6a) binds, (6b) is slack and ; and strategic delay if (6a) is slack, so that the server is idled on purpose.
Let be the first-best effort. If , there is a unique cutoff such that, for :
The goal asserts the existence and uniqueness of the cutoff, not its numerical value. The paper gives a closed form for through the root of a cubic, but the goal does not depend on that form.
In the order of the paper's proof:
The result changes the design rule. Giving referrers priority is not always right, and when it is right it should not always be full priority. When the base market is moderately large, a partial reward is enough: it makes customers indifferent between referring and not, which is all the first best needs. When the base market is small, the reward needed to induce first-best referrals would let referrers overtake everyone, and that is not operationally achievable. The firm then does better by adding delay for non-referrers on top of full priority, even though this idles capacity. The cutoff is where these two regimes meet. The paper's Proposition 5 (its comparative statics in ) and the numerical sections build on it.
The paper proves the result by hand, by KKT reasoning and algebra on rational functions, and has no machine-checked version. Formalizing it pins down exactly what "the first best can be achieved" and "optimal in the second best" quantify over. It also forces the details that the written proof handles loosely to be checked: the paper writes the range "(subject to )" where it means ; (A.5) prints a minus sign that should be a plus; and the positivity of is argued circularly. The development is elementary real analysis, so a complete proof is a realistic target.
Uniqueness of the cutoff does not follow from any one regime. It needs the first-best effort to be strictly monotone in , so that the root of the cubic maps to exactly one base market size, together with an exact sign pattern of on . Part (iii) is a global optimality claim over every mechanism feasible for Problem 1, FIFO included. The incentive constraint is an argmax over efforts, and the feasible set is not convex, so checking first-order conditions at the proposed tuple is not enough. A full proof must bound every referral-generating mechanism and then show that the bound is attained by a mechanism satisfying all the constraints. The second step, implementability, is where the strict form of (A.6) comes in.
All quantities are real numbers. The parameters form a structure Env, and is a separate argument, because the goal fixes before quantifying over . The standing hypotheses are , , and Assumption 1, . The positivity of , and is an addition: the paper uses it without stating it. is a hypothesis wherever appears.
Problem 1 is encoded constraint by constraint, as printed:
Under stability every denominator in (6a)–(6c) is positive. "Achieves the first best" means feasible for Problem 1, with throughput equal to the maximum (IsGreatest) of the first-best problem's throughputs. "Optimal in the second best" means maximum over all Problem-1-feasible throughputs. Part (ii) names no delays on the page, so the delays of part (i) at are used; milestone 3 shows they are the only possible ones.
Two encodings would make the goal trivial or empty, and neither is used. The first-best value is never defined as the closed form , and incentive compatibility is never dropped from Problem 1. The cutoff is an existential with uniqueness, quantified before , not a closed form at which the trichotomy is merely checked. A sorry-free check, outside the proposal, exhibits feasible tuples on both sides of the cutoff (, , , and ), so the hypotheses can be satisfied.
Out of scope: Lemma 1 (the achievable region, which Problem 1 states directly), Proposition 1 (ii), Propositions 2, 3 and 5–9, and the numerical sections. Proofs of any milestone are welcome. Milestones 4 and 5 (the cubic and the cutoff) and the relaxation bound are independent of one another and can be attacked in parallel.
A mixed strategy assumes a player can draw from any distribution. A real player may only have a limited or imperfect source of randomness, and an opponent may observe part of it. Repeated games with bounded randomness ask how much a player can guarantee in that situation. Gossner and Vieille (2002, Games Econ. Behav. 41(2), 206–226) studied a repeated zero-sum game in which the maximizer's only source of randomness is an i.i.d. sequence she observes privately. Valizadeh and Gohari (2017) generalized this to a leaked randomness source, in which the opponent observes a correlated sequence, and characterized the long-run max-min value. This mission formalizes the next question, studied in Valizadeh and Gohari, Playing Games with Bounded Entropy: Convergence Rate and Approximate Equilibria (arXiv:1902.03676v1, 2019; published as Simulation of a Random Variable and its Application to Game Theory, Math. Oper. Res. 2021): how fast does the max-min value of the -stage game approach its long-run limit?
Timeline:
Alice (maximizer) and Bob (minimizer) have finite nonempty action sets and , and Bob pays Alice when the actions are . A joint pmf on finite alphabets is publicly known. At each stage a fresh pair is drawn, independently of the past. Alice observes and Bob observes . Both then act, and both actions are publicly monitored.
Strategies are deterministic. Alice's stage- action is , and Bob's is . Each player's only randomness is their own source. The payoff is the expected average
with the expectation taken over the i.i.d. sources.
Logarithms are base 2. is the Shannon entropy and the conditional entropy. For , , is the Rényi entropy and the conditional Rényi entropy. The total variation distance is .
The benchmark (Definition 4) is built in three steps:
There exist , , and with the following property. For all sequences , , , there are Alice strategies such that for all Bob strategies and all ,
The milestones are the results that the paper's proof (§3.3 and Appendix A) uses, in attack order:
Theorem 6 makes the convergence of the -stage max-min value quantitative. With and it gives a rate of . Combined with the cited upper bound, it says how long a game must be before limited, partially leaked randomness costs Alice at most . Lemma 14 is of independent use: it bounds how well a deterministic function of one correlated source can imitate an independent random variable in total variation, and it is stated with Rényi entropies of both orders and . The paper also uses it for approximate equilibria.
On formalization: none of these results has a machine-checked proof. The mission produces finite pmf-level definitions of Shannon and Rényi entropy in bits, a model of repeated games with history-dependent deterministic strategies, and the random-mapping simulation bound. The proofs exist on paper (§3.3, Appendix A). The work is to formalize them, which includes an instance of Riesz–Thorin interpolation for finite measure spaces that Mathlib does not have.
Alice cannot randomize at will, so the natural strategy, playing the mixed action that attains , is not available. She has to manufacture mixed actions from her source, and Bob's correlated observation leaks information about them. In the paper's block construction, the actions of block are a function of the previous block's source. Three steps of this argument are hard to formalize:
Conventions:
stdSimplex ℝ 𝒜.Real.logb 2, with .Fin n).Standing readings and added hypotheses:
The goal must not be trivialized:
Not posed: Theorem 31 (Riesz–Thorin), the block payoff bound of p. 24 (which rests on (32)), and the block summation (33)–(35). Contributions are welcome on all of them. The entropy, total variation and random-mapping layers can be reused for other one-shot simulation and channel-resolvability statements.
Small retailers often cannot pay for their orders out of their own capital and borrow from banks to do so. Banks in turn are regulated: risk-control rules such as value-at-risk caps limit how much they may lend against an uncertain revenue, and they charge fixed fees to process a loan. Loan insurance, offered by insurers or guaranteed by governments, relaxes those caps for a premium. The common view, in practice and in policy discussions of financing for small firms, is that a higher credit limit and a cheaper loan help every firm in the supply chain.
Wang and Cai (Management Science, 2023) study a supplier selling to such a capital-constrained buyer and show that the common view fails in a precise region of parameters. They build on the capital-constrained newsvendor literature, which studies how financing frictions distort ordering and pricing (Buzacott and Zhang, 2004; Kouvelis and Zhao, 2012), and on the price-only wholesale contract of Lariviere and Porteus (2001), whose equilibrium price and quantity are the benchmark without any capital constraint.
Demand for a product with retail price has distribution function , complementary distribution , density on and failure rate , and satisfies the increasing generalized failure rate (IGFR) property: is increasing. The expected sales of an order are .
A supplier with unit cost sets a wholesale price . A buyer with initial capital then chooses an order and how to finance it:
The supplier earns . The game is a Stackelberg game solved backwards, with the paper's goodwill tie-breaking rule: a firm indifferent between choices picks the one better for the other firm. and denote the supplier's and the buyer's equilibrium profits.
The equilibrium is described through explicit thresholds. is the buyer's additional revenue from insurance at price (the paper's equation (A-7)); the buyer insures exactly when . are the two roots of . With , and defined in the paper's appendix, and . The insurance-cooperation region (Area II) is
In it, the equilibrium price is : the supplier lowers its price just enough for the buyer to be willing to insure.
Assume , and the paper's global assumptions, and Area II. Then
The monotonicity is stated along every segment of (or ) on which the hypotheses hold at each point, and for every equilibrium at the two ends.
In attack order: the buyer's best response and the threshold (Lemma A.7), its monotonicity and unimodality (Lemma A.7, "Moreover"), the shape of the supplier's profit in (Lemma A.8), the monotonicity of (Lemma A.9), the equilibrium in Area II (Proposition 1 item 1(b), including existence), the comparative statics of (Proposition A.8, "Moreover"), and the closed-form equilibrium profits in Area II (proof of Proposition 2).
The result reverses an intuition that regulators and firms rely on: a tighter or costlier bank loan, normally a loss for everyone, here benefits the supplier, because the buyer is pushed towards insurance and the supplier then needs to cut its price less to keep the buyer insuring. The buyer loses at the same time, so the two firms' interests over bank credit terms conflict in this region. The paper builds on this a parallel statement about curtailing loan insurance (Proposition 3) and a Stackelberg prisoner's dilemma (Proposition 5); both are outside this mission.
The paper's proofs are derivative computations through the implicit function theorem applied to piecewise-defined thresholds, with several details left to figures. A machine-checked proof would pin down the exact hypotheses under which the region exists and the claims hold, settle the role of the tie-breaking rule (without which no equilibrium exists in Area II), and give a reusable formal model of a capital-constrained newsvendor with several financing modes. No part of the paper has been formalized before.
The obvious argument differentiates the closed-form equilibrium profits in and . It requires first knowing that the equilibrium is the price throughout a segment of parameters, which in turn needs the full best-response analysis of the buyer (three financing modes, two binding regimes for each loan cap), the unimodality of , and the comparison of the supplier's profit at with its profit at the competing price . Each threshold is defined as a root of an equation involving and , and the region boundaries and themselves move with and . The implicit function theorem gives local derivative signs; turning them into strict monotonicity along a segment needs continuity of the thresholds across the switches between regimes.
All quantities are real numbers. Demand is a probability measure on with a density that vanishes on , is continuous and positive on the positive open support, with finite mean and the IGFR property; continuity, positivity and the finite mean are added to the paper and disclosed. Expected sales use the published SupplyChainTheory.expSales. IGFR is imposed where the failure rate is defined, on the positive support with ; this includes bounded-support demand laws such as the uniform distribution. Prices range over . The loan limits are parameters; their value-at-risk derivation is not modelled. In the supplier's threshold , an inverse of expected sales above its range is treated as inside the minimum with the finite unconstrained order. Lemma A.8's buyer profit is nonincreasing in price; strict decrease additionally requires positive initial capital, since with zero capital and a positive bank fee the buyer can earn zero throughout a high-price interval.
Every threshold is defined from the paper's own equation as an infimum or supremum of an explicitly named set, never passed as a free parameter. The goal is about the game's equilibria (IsEquilibrium) on the region AreaII; restating it about and the closed-form profits, or defining the profits or Area II through the equilibrium's expected shape, would trivialize it and is excluded. Proposition 1 item 1(b) asserts existence of an equilibrium in Area II, so the goal is not vacuous.
A complete development needs the inverse functions and and their continuity and derivatives, the newsvendor with a spending cap, and the implicit-function arguments for the roots. The capped newsvendor and the financing-mode best response are reusable for other supply-chain-finance missions. Contributions to any milestone, and to the missing lemmas about under IGFR, are welcome.
School districts in the United States are held to end-of-year proficiency targets, and many pay teachers a school-level merit-based incentive when the school is proficient at the year's standardized test. Alongside such pay schemes, districts buy interim assessments: mid-year tests that reveal where a school stands, at a reported cost of 20 or more per student (Topol et al. 2012). The common view is that better information can only help. Virudachalam, Savin and Steinberg (Management Science, 2023; preprint SSRN 3884543) model this as a principal–agent problem with a dynamic agent and ask when the district should pay for the interim assessment at all. Their answer is that it is often worthless, even when it is free, because accurate bad news can demotivate teachers and accurate good news can make effort too expensive to reward under a budget.
The empirical record on merit pay is mixed: school-level bonuses in New York City showed no effect (Fryer 2013), while the IMPACT reform in Washington, D.C. raised teacher effectiveness (Dee and Wyckoff 2015). Accountability built on proficiency thresholds shapes where effort goes (Neal and Schanzenbach 2010). The model isolates one question from this literature: the value of midyear information to a budget-constrained district whose teachers respond optimally.
This mission formalizes the paper's result for a school that starts the year not proficient (Proposition 1).
The school year has two halves. The school's proficiency state is at times (start, middle, end). At the start of each half, teachers choose an effort that the district does not observe, at cost . From state the school is proficient at the end of the half with probability ; from it becomes proficient with probability . Here is the response-to-effort parameter, the baseline proficiency factor and the improvement potential factor.
At midyear, teachers see a formative assessment result with true positive rate and false positive rate , where . A free interim assessment () reveals exactly, which is the case , .
The district pays if the school is proficient at the end of the year. Teachers solve a two-period dynamic program. In the second period they maximize , and in the first period the expected second-period value minus . When several efforts are optimal they take the largest. Write for the resulting probability of ending proficient. With a budget the district solves
and it invests in the interim assessment only if this strictly raises the optimal value.
The relevant constants are the second-period threshold and
The accuracy condition (14) is .
Let and write for the district's optimal value.
a) If , then for every budget , so the district does not invest, whatever the formative accuracy.
b) If and (14) holds, the two decisions coincide for and for . For every ,
The milestones follow the paper's proof:
Lemma A1, which gives the Bayes posterior, comes first.
The proposition shows that information can have zero or negative value to a principal whose agent responds dynamically. When there is no baseline proficiency (), the interim assessment never helps a school that starts behind. When , it helps only for low or moderate budgets. With larger budgets the formative-only district can afford to induce effort that the interim district cannot. The two value curves are explicit step functions of the budget, so the result is a complete decision rule rather than an existence statement.
The paper proves these results by hand across about thirty appendix pages of case analysis. None of it is machine-checked. A formal development would verify the case splits: the four-step response curves, the budget breakpoints, and the boundary behaviour at each threshold, where tie-breaking decides the outcome. It also produces a reusable small dynamic-programming model with Bayesian updating of a binary signal, budget-constrained optimization over an incentive, and value-of-information comparisons.
Each piece is elementary. The difficulty is that the district optimizes over the teachers' best response, and that response is defined by two nested maximizations whose maximizers jump at thresholds. Evaluating requires knowing that first-period effort is bang-bang, which is not visible from (7) because the posterior that drives second-period effort depends on nonlinearly. It also requires ordering four second-period thresholds against the first-period threshold, and this is where (14) enters. Only then does become a monotone step function, so that the supremum over affordable incentives is attained at a threshold.
The obvious argument compares the two value curves step by step. It needs the breakpoints of both curves to be ordered (, ). It also has to handle a region where the ordering of and changes with (Lemma A12). At every breakpoint, ties decide whether the interim assessment is strictly better.
All quantities are real numbers. Params bundles . Params.Standing is Assumptions 1–2 with three disclosed tightenings: , and (the thresholds divide by , , , and at part b) fails). Effort ranges over and the effort cost is (Assumption 3 with ). The decision is a Bool, and the interim assessment is the accuracy pair , so both decisions run through one model. Condition (14) is stated cross-multiplied.
Teachers' efforts are the greatest maximizers over . PrStar sums the joint law of under these efforts. optProb is the supremum of PrStar over affordable . Investment means strict improvement.
is taken from (A155), a product. The printed (17) divides by , which is a misprint. The second region of the goal requires strictly. At the two curves coincide on that range by (A214), so the interim assessment is not strictly better there.
Neither PrStar nor optProb may be defined by the paper's piecewise formulas. The goal is about the optimum of the dynamic program, and with such definitions it would reduce to (A214) and algebra.
The S0 = P analysis (Proposition 2, Lemma 2 for , Lemma 3 b)–e)), Corollary A1 b) and the remark that the two regions of b) overlap for some are not formalized. Proofs of any milestone are welcome, and so are general lemmas on maximizers of convex piecewise-affine objectives on an interval and on suprema of monotone step functions under a budget.
Expected utility theory describes a decision maker who ranks risky prospects (probability distributions over outcomes) by the expected value of a Bernoulli utility function on the outcomes. The classical von Neumann–Morgenstern theorem, extended by Grandmont to separable metric outcome spaces, says that a complete preference over lotteries has a continuous and bounded Bernoulli utility exactly when it is continuous and satisfies the independence (affinity) axiom. Two features of that classical picture are restrictive in applications. Many decision makers are indecisive between some prospects, so their preferences are preorders rather than total orders; such preferences are represented by a family of utilities (a multi-utility), a line of work going back to Aumann and to Dubra, Maccheroni and Ok. And in finance and economics the prizes are usually unbounded (wealth levels, consumption streams), and the utility functions used in practice are Lipschitz rather than bounded, so that differential arguments can be applied to the induced value functions.
Ok and Weaver (arXiv:2104.11205; Mathematics of Operations Research, 2023) characterize exactly those preferences that admit an expected multi-utility representation with Lipschitz Bernoulli utilities. The lotteries are the probability measures with finite first moment, the natural domain of Lipschitz expectations, and the topology is that of the Wasserstein 1-metric.
Let be a separable metric space with its Borel -algebra. A lottery is a Borel probability measure on , and
is the set of lotteries with finite mean distance (equivalently, finite first moment). The Wasserstein 1-metric is , the infimum over couplings of and , probability measures on with marginals and . For the mixture of and is .
A preorder on is a reflexive, transitive relation. It is affine if for all and ; this is the independence axiom. It is Lipschitz (Definition 4.1) if whenever fails there is a constant such that
A family of Lipschitz functions represents if exactly when for every .
The proofs pass through the Kantorovich–Rubinstein space of finite signed measures with and , normed by over 1-Lipschitz , and through the space of Lipschitz functions vanishing at a base point.
For a separable metric space and a preorder on ,
No constant is fixed in the statement: each carries its own Lipschitz constant and may be any family.
The theorem identifies the behavioural content of using Lipschitz expected utilities: the independence axiom together with a quantitative, metric form of continuity in which the tolerance for mixing shrinks in proportion to the Wasserstein distance of the perturbing lotteries. Because no completeness is assumed, it covers incomplete preferences, and with them stochastic orders such as first-order stochastic dominance on partially ordered prize spaces (Section 4.2 of the paper). The paper derives further consequences from it: the single-utility version for total preorders (Corollary 4.7), the uniqueness of the representing cone up to weak* closure, and applications to affine cores of non-expected-utility preferences and to Anscombe–Aumann acts.
The result is proved in the paper. As far as a search of the Prove2Me corpus shows, none of it is formalized: the platform has a Kantorovich–Rubinstein duality theorem on normed spaces and a discrete one, abstract Lipschitz-free spaces built from finite molecules, and a von Neumann–Morgenstern theorem for abstract mixture spaces, but no Wasserstein space of a general metric space, no measure-theoretic , and no multi-utility theorem. A complete development would give a reusable Kantorovich–Rubinstein layer (duality on separable metric spaces, and its dual) of independent interest in optimal transport.
The "if" direction is a direct estimate once the duality bound for 1-Lipschitz is available. The "only if" direction is a separation argument, and the obvious version of it fails: separating the cone from a point requires to be closed in a space whose dual consists of Lipschitz functions. The natural candidate, the space of all signed measures with weak convergence, has the wrong dual (continuous bounded functions), and the KR norm is not complete, so the Hahn–Banach step needs the identification , which rests on the density of finitely supported measures and on Kantorovich–Rubinstein duality for non-compact separable spaces. Closedness of is where Definition 4.1 enters, through the specific form of the bound; plain continuity of does not give it.
MetricSpace, SeparableSpace, MeasurableSpace and BorelSpace instances. Lotteries are Measure X; is a set of measures (Delta1 X), and a preorder is any relation R : Measure X → Measure X → Prop that is reflexive and transitive on . Nothing is required of R outside , and every statement quantifies over only.RWPI.SqrtLasso.transportCost with cost , valued in ; it is finite on , and its toReal is used in Definition 4.1. Mixtures are ENNReal.ofReal (1 - t) • p + ENNReal.ofReal t • q, the weight being named t. Affinity uses and Lemma 3.1 , as on the page.SignedMeasure X; the integral against a signed measure goes through its Jordan decomposition, and is valued in . No normed-space instance is built: closedness of is stated as "every point of has a ball of positive radius disjoint from ", and Theorem 2.3 as an isometric bijection between and the linear functionals on bounded by the KR norm.Needed infrastructure beyond Mathlib: Kantorovich–Rubinstein duality on separable metric spaces, the Jordan-decomposition calculus of integrals of Lipschitz functions against , and a Hahn–Banach separation in a normed space given by a seminorm on a set. Contributions to any milestone, and alternative proofs of the goal that avoid part of the KR layer, are welcome.
Parallel computing systems split each incoming job into pieces that are processed simultaneously on several servers. When the pieces of one job must also start together, each server keeps the order of arrival, and a job cannot begin until every server it needs has finished its earlier work, the result is a synchronized parallel queue. Waiting times in this model are coupled across servers in a way that the classical single-server or many-server theory does not capture, and the model gives an upper bound for the performance of split-merge and fork-join networks under blind (random) routing.
Olvera-Cravioto and Ruiz-Lacedelli (arXiv:1501.00186; Mathematics of Operations Research, 2021) show that, as the number of servers grows, the stationary waiting time converges to the endogenous solution of a high-order Lindley equation, the maximum of a branching random walk. The tool is the predecessor graph of Karpelevich, Kelbert and Suhov, given a rigorous labelling and coupled with a weighted branching tree.
There are identical servers. Jobs arrive as a Poisson process of rate , . In this mission every job consists of exactly pieces, with . The pieces are routed to distinct servers, all assignments being equally likely. The service requirements of the pieces of one job have an arbitrary joint law on , so the pieces may be dependent. Inter-arrival times, routings and service vectors are independent. is the law of a randomly chosen piece, and .
The dynamics follow two rules (Definition 2.1). Under synchronization, all pieces of a job start together, once each immediate predecessor (the previous job at each of its servers) has finished there. Under fairness, each server is first come, first served. A job arriving at time therefore starts at , where is the time server becomes free, and server is then busy for more units.
The tagged job is the first arrival after time . Start the system empty at time . is the tagged job's waiting time, excluding service.
The limit object is the -ary weighted branching tree. Its nodes are words over , and each edge carries independent marks and . The path sums are and . The endogenous solution (3.9) of the high-order Lindley equation is
Suppose that for some , and
Then for every the limit exists almost surely and is finite, is almost surely finite, and
The theorem has two parts, each with its own consequence. The stability part identifies a stability region, , for a network in which the usual load condition is not sufficient. The many-server part describes the stationary waiting time of a large network explicitly, as the maximum of a branching random walk, with convergence of all moments. The tail asymptotics of (the paper's Theorem 3.4) rest on it. For the statement reduces to the Lindley representation of the M/G/1 waiting time.
The source proves the result on paper. No machine-checked proof of it, or of the stability of the synchronized queue, exists. Formalizing it builds the following, none of which is on the platform:
The obvious argument treats the predecessor graph as a tree with independent edge weights, and both of those assumptions fail.
The statement is the case of jobs of fixed size . For random job sizes the limit printed in the source is not correct, because the immediate predecessors of a job are size-biased; that case is not formalized. For fixed size, Assumption 3.1 (i) and (iii) hold automatically, (ii) is (3.5), and for every .
Conventions:
List (Fin m), written root-first.Formalizations that would trivialize the goal are ruled out:
The development needs:
WassersteinDRO.Duality.wassersteinDistance;Contributions are welcome on the general tools: the first-moment identity on branching trees, Borel–Cantelli arguments for maxima of path sums, and the equivalence between convergence and weak convergence with moments on .
A DC function is a difference of two convex functions. Programs whose objective and constraints are DC functions model sparse estimation with nonconvex penalties, affine sparsity constraints, piecewise-affine regression and several problems in signal processing and finance. Constraints of DC type make the feasible region nonconvex and nonsmooth, and the usual Karush–Kuhn–Tucker theory and its constraint qualifications do not apply directly.
Lu, Sun and Zhou (arXiv:2111.09263, Mathematics of Operations Research, 2022) propose a penalty method and an augmented Lagrangian method for such programs. Each subproblem only has to be solved approximately, in a sense that a single convex subproblem per inner iteration can certify. Their main result for the penalty method is that every feasible accumulation point of the iterates is a B-stationary point, the strongest first-order condition used for nonsmooth nonconvex programs, under a new pointwise Slater constraint qualification (PSCQ).
Timeline:
Let be closed and convex, and let be an open convex set. For :
The program is
with feasible region . The definitions used throughout are these.
Algorithm 3.1 fixes , , , tolerances with , and an exponent . It sets and requires each iterate to satisfy
for every -active and at . Here:
If along a subsequence of a run of Algorithm 3.1, and , and the PSCQ holds at , then
The statement fixes no constants; it holds for every admissible choice of and every convergent subsequence.
In the order the proof uses them:
The supporting results of §§1–2 follow: 6. (1.16), Danskin's formula. 7. (2.1): . 8. Proposition 2.1: . 9. Corollary 2.1. 10. Theorem 2.1: under the PSCQ, B-stationarity reduces to on each .
The theorem certifies that a practical method, one whose subproblems are solved only approximately, reaches the strongest standard stationarity notion for DC-constrained programs. It does so without the piece-uniqueness assumption, so limit points may sit where some is nondifferentiable, which is the typical case in sparse and piecewise-affine models. Theorem 2.1 and Corollary 2.1 are useful in their own right: they describe the tangent cone of a nonconvex DC feasible region as a finite union of cones of convex sets.
Formalization status: the result is proved on paper. The local Prove2Me prior-art search found no machine-checked version of this theorem. Proposition 2.1 is stated in the paper without proof (it refers to Pang et al.), so a complete development must supply that argument.
Passing to the limit in (3.7) faces two obstacles. The inequality is available for pieces that are -active at , while the conclusion concerns active pieces at . Also, , so the penalty term cannot simply be dropped in the limit. The PSCQ must provide enough strict feasibility for the limiting comparison to remain meaningful.
The limiting minimization property is posed on each convex set , while B-stationarity concerns the nonconvex set . Relating their tangent cones is a separate difficulty. Proposition 2.1 requires a Slater-type tangent-cone result whose proof the paper leaves to the literature.
The space is EuclideanSpace ℝ (Fin n), and gradients are fderiv. Indices are Fin (m+1) with m = I: index 0 is the objective and constraint is i.succ. Each has a nonempty, finite set of pieces. The conventions committed to are these.
tangentConeAt, which admits negative scalings, is not used.ClarkeGradients.MaxFunctions.HasOneSidedDirDeriv, a limit along , never a limUnder value. B-stationarity therefore asserts that exists and is nonnegative.(max a 0) ^ p with a real exponent.Ruling out trivial readings.
Deliberately absent.
The tangent cone, B-stationarity, the PSCQ and Danskin's formula are reusable for other nonsmooth constrained programs. Contributions are welcome on any milestone, and in particular on the tangent-cone results (2.1) and Proposition 2.1, and on directional derivatives of convex functions on open sets.
Retailers increasingly pair products with free in-store experiences: yoga classes at Lululemon, playgrounds at Toys "R" Us, cooking classes at Whole Foods. The experience is free to anyone who travels to the store, so it attracts buyers and free riders (visitors who enjoy the experience without buying) alike. The retailer earns revenue only from product sales, but pays for every visit to the experience. Whether a free experience pays for itself, and whether consumers gain from it, is the question of Mutlu, El-Amine and Sahin (SSRN 4617261; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2021.0339).
The paper models the joint choice of experience and product with the multivariate logit (MVL) model of Russell and Petersen (2000), which builds a global choice model over baskets from conditional logit choices, via Besag's (1974) characterization of joint distributions from conditionals and the autologistic model of Cox (1972). The monopoly analysis (§3.1) yields two results: Theorem 1 on the optimal price and profit as functions of the experience quality, and Theorem 2, which says that low-quality experiences benefit both the retailer and its customers.
A monopolist sells a main product at price and offers a free experience of quality . A consumer chooses (obtain the experience or not) and (buy the product or not). The parameters are the product's nominal utility , the travel cost , the product's unit cost , a memorable-event utility , a synergy sensitivity , and a cost sensitivity .
The baseline utilities are and . Obtaining both offerings together saves one travel cost and creates a brand synergy , so the interaction term is . Each basket has utility and probability
The experience costs per user, and the retailer's profit is
Without an experience the model is the binary logit: with .
An optimal price maximizes over all real , and maximizes ; and are the optimal profits. Consumer welfare is the logit log-sum with the experience and without it.
There is a threshold such that for every ,
for all optimal prices , , which exist. In addition, some quality leaves the retailer strictly worse off than offering no experience. The threshold is existential, as in the paper; no particular value is claimed.
The result. Theorem 2 identifies a regime in which a free experience is a win-win: the retailer raises its price (Theorem 1) yet sells enough more, through the complementarity between experience and product, to raise profit, and consumers gain despite the higher price. Theorem 1 marks the limits of that regime: experiences of high quality attract so many free riders that profits fall without bound. Together they explain why experiential retail is typically offered at modest quality, and they are the benchmark for the paper's duopoly (§3.2) and conditionally-free (§4) analyses.
Formalizing it. The paper's lemmas and proofs are in an appendix that is not part of the held working paper; the published proof has never been machine-checked. A complete development would give the first verified analysis of optimal pricing under the MVL basket model, including existence of optimal prices, which the paper presupposes when it writes . The milestones are the clauses of Theorem 1 that the goal rests on.
The optimal profit is a supremum over prices of a ratio of exponential sums, and the experience quality enters through three channels at once: the experience-only basket, the synergy , and the cost , which is paid also for free riders. The obvious route, solving the first-order condition in closed form, fails: unlike the binary logit, where the optimal markup solves a Lambert-type equation, the MVL first-order condition mixes the free-rider basket into the denominator, and the optimal price need not be monotone in (Figure 1(a)). Comparing welfare requires the optimal prices themselves, not only the optimal profits, and the comparison is between two different optimization problems.
All quantities are real numbers. Parameters form a structure with fields ; the standing assumptions , , , are one predicate carried by every statement. and are unconstrained, and prices range over all of . The model uses only and , not the constant, piecewise-linear or linear variants the paper mentions.
Conventions committed to:
A statement at a fixed price, at alone, or under an assumed (possibly non-existent) optimum would be trivial or vacuous and is ruled out: the goal quantifies over all optimal prices, asserts their existence, and covers a whole interval .
Not formalized: the remaining clauses of Theorem 1 ("if is decreasing in , then is also decreasing in ", which needs as a function, and the comparative statics in and ), and Theorems 3–8 (duopoly and conditionally-free offerings).
Needed infrastructure: continuity and coercivity arguments for existence of a maximizer over , a parametric envelope argument for , and logit inequalities. Proofs of the milestones, of the existence of optimal prices, and reusable lemmas on logit pricing are welcome.
During the Covid-19 epidemic, governments had to decide not only whether to impose social distancing but how to schedule it over time: when to escalate, when to relax, and whether a relaxation might later have to be reversed. Epidemiology supplies the dynamics (the SIR model of Kermack and McKendrick, 1927), and optimal control supplies the language for trading off deaths against the economic cost of distancing. Most of the prior theoretical literature on optimal epidemic control assumed a cost of distancing that is linear in the reduction of the transmission rate, and focused on numerical solutions.
Kruse and Strack (Cowles Foundation Discussion Paper 2229R, 2020; later published as Optimal Dynamic Control of an Epidemic, Operations Research, 2024, doi:10.1287/opre.2022.0161) characterize the shape of every optimal policy for a general convex cost of distancing and a convex death-rate function. Their main structural result is that, when hospital-capacity effects are moderate, optimal policies are single-peaked: measures are escalated and then relaxed, never relaxed and re-escalated.
The population is split into a susceptible share , an infected share and the rest. A planner chooses a measurable transmission rate , with . With recovery rate the shares follow
from , , with and . A vaccine arrives at . The planner minimizes
where the death-rate cost is convex, strictly increasing and with . The cost of distancing is convex, non-increasing and continuous on , with for . A control is optimal if it minimizes over all admissible controls.
Write . Proposition 1 of the paper provides a positive costate along every optimal path, and the gain from reducing the transmission rate is ; the optimal control minimizes over . Assumption 1 (limited capacity effects) asks that be with
where is the left derivative of at .
Under Assumption 1, for every optimal control there is such that
Thus has at most one local maximum on . The monotonicity claim refers to the version of singled out by the paper's convention (see Formalization scope).
In the paper's order of proof:
Proposition 7 rules out a whole class of policies (relax, then tighten again) for every convex cost of distancing, not only for the linear costs earlier work treated. The same argument also gives Proposition 8 of the paper, a three-phase bang-bang structure under linear cost. It also explains the factor : it is the reciprocal of .
The mission produces a machine-checked development of a deterministic optimal-control problem with measurable controls: existence of an optimal control, a Pontryagin principle with a state-dependent terminal cost, and a qualitative analysis of the adjoint system. The paper's result is proved on paper; none of it is formalized. The SIR model, its integral-form solutions and the costate machinery are reusable for other epidemic-control papers.
Existence and the necessary conditions rest on the existence theory and the Pontryagin principle for measurable controls, which Mathlib does not have. The general Pontryagin principles already on the platform do not apply, because they require a globally Lipschitz vector field or a cost that is smooth in the control.
The step specific to the paper is the reduction of the two multipliers to one costate, followed by the analysis of the gain . The gain is , but its derivative involves and , so exists only almost everywhere. It must be bounded through a case split on the size of relative to . Showing that is single-peaked requires turning this almost-everywhere bound into a strict sign change of at each critical point. A naive appeal to " at critical points" fails because need not exist there.
All objects live in EpiControl.SinglePeak; parameters are a structure Params with a predicate Standing for the assumptions of §2. Conventions:
IsCostate) taken as a hypothesis in every statement about or , never an arbitrary function and never a Classical.choose.Infrastructure that a complete development needs: Carathéodory solutions of the SIR system, existence of optimal controls (a Filippov-type argument), a Pontryagin principle for measurable controls with terminal cost, and Lipschitz/almost-everywhere differentiability arguments. Contributions of these general results as separate theorems are welcome.
Value functions of parametric optimization problems appear wherever one optimization problem sits inside another. In a minimax program the outer problem minimizes the maximal value function ; in bilevel programming and in the value-function approach to equilibrium problems the same object enters as a constraint. Optimality conditions for the outer problem therefore need generalized derivatives of , and is in general neither smooth, nor convex, nor locally Lipschitz.
Classical estimates of the subdifferential of a value function, going back to Clarke's Optimization and Nonsmooth Analysis (1983) and to Rockafellar and Wets' Variational Analysis (1998), take a convex hull over all optimal solutions, or assume inner semicontinuity of the solution map, or joint convexity. Guo, Ye and Zhang (arXiv:2303.01474, Mathematics of Operations Research, 2024) give estimates for the limiting and horizon subdifferentials of a maximal value function without any of these assumptions, when the inner problem is concave in . Their device is Wolfe's 1961 dual: weak duality bounds the maximal value from above by the value of a minimization problem over primal–dual pairs, to which minimal-value-function techniques apply. The estimates then feed into stationarity conditions for nonconvex–concave minimax programs (§4 of the paper).
Let and . For a parameter the parametric maximization problem is
The maximal value function is (with on an empty feasible set), and the solution map is . The Lagrangian is , and . The multiplier set of at is .
The Wolfe dual of is subject to , ; its value is . For its multiplier set at is
For at a point where is finite, a regular subgradient satisfies ; the limiting subdifferential collects limits of with , ; the horizon subdifferential collects limits of with additionally .
Throughout, and are twice continuously differentiable, and is concave and every convex for near the reference point . Restricted sup-compactness at means is finite and some compact set meets for every near with . Two constraint qualifications enter: a stable parametric CQ for at a solution (Definition 2.3), and a stable CQ for the system , in (Definition 2.4), each asking that a CQ hold at nearby points and that multipliers of nearby points have subsequences converging to multipliers at the limit.
Under the standing assumption, restricted sup-compactness at , a stable parametric CQ at every , and a stable CQ for (3.11) at every with , :
A supporting item (proof of Theorem 3.3 (i), p. 17) states that a regular subgradient of at makes a local minimizer of that problem (3.16), for every .
The estimates (3.13)–(3.14) bound the limiting subdifferential of a maximal value function by a union over solutions rather than a convex hull, and they do not presuppose that is locally Lipschitz: (3.14) is exactly what is needed to derive Lipschitz continuity (Corollary 3.3 of the paper: if the right side of (3.14) is and is continuous, is Lipschitz near ). The paper uses them to obtain stationarity conditions for nonconvex–concave minimax programs, including cases (Example 3.1) where the solution map is not inner semicontinuous and the problem is not jointly convex.
The result is proved in the paper; no machine-checked version exists. The mission formalizes the statement and its proof, which requires subdifferential calculus for extended-real functions, the exact-penalty consequence of a local error bound, and multiplier rules for problems with a nonsmooth term, none of which are in Mathlib today.
The obvious route to differentiates the maximum directly (a Danskin-type argument), which needs compactness and continuity uniform in and yields a convex hull; it fails exactly when is not Lipschitz. The Wolfe-dual route replaces the maximization by a minimization over , but the resulting problem (3.16) has a nonsmooth objective () and a constraint system in which is a variable, so the KKT conditions follow only from a calmness/error-bound argument, not from a smooth Lagrange multiplier rule. The limiting estimate then requires passing to the limit simultaneously in solutions, primal multipliers and dual multipliers , and the latter can be unbounded unless the stable CQ controls them; this is the role of Definition 2.3(ii).
Parameters are in EuclideanSpace ℝ (Fin n), decisions in EuclideanSpace ℝ (Fin m), multipliers in Fin q → ℝ; is given by components . and are EReal-valued suprema/infima over the feasible sets. Regular subgradients and the limiting subdifferential are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the horizon subdifferential is defined from regular subgradients with , . Second derivatives are gradient/fderiv of explicit functions of data.
The paper leaves "a CQ" abstract. Here it is the local error bound of (3.11), which every CQ listed in the paper implies (p. 8), so the formal statements are at least as strong as the paper's for each listed CQ. A stable CQ is the error bound at all feasible points near the reference point plus Definition 2.3(ii); a stable parametric CQ is Definition 2.3 with (i) read for local maximizers (the problem is a maximization) on a neighbourhood. Error-bound distances use the product sup norm, equivalent to the Euclidean one up to the constant.
A real-valued (junk value on empty or unbounded feasible sets) or a CQ hypothesis that already asserts the KKT conclusion of (3.12) would trivialize the goal; neither is used. A sanity file proves the standing assumption, a solution, a multiplier and restricted sup-compactness for Example 3.1 of the paper.
Needed infrastructure, reusable beyond this mission: Fermat's rule and sum rules for limiting subdifferentials of locally Lipschitz functions, exact penalization under a local error bound (Clarke calmness), and closedness of linear images of complementarity sets. Contributions on any of these are welcome.
Public and private buyers often procure the same input over several periods from a pool of competing suppliers: road maintenance, defence supply, energy, and IT services are typical cases. Between periods, conditions change. Input prices, regulations or technology shift, and so does the cost of serving the contract. A buyer who can write a complete contract commits in period one to what she will buy and pay in every future state of the world. Real procurement contracts rarely do this. They are incomplete: the first-period contract fixes the first-period deal, and later terms are renegotiated once the new state is known.
Incompleteness is usually costly in mechanism design. A buyer who learns a supplier's cost in period one cannot commit not to use that information later. This is the ratchet effect (Laffont and Tirole 1988), and suppliers anticipate it by hiding their costs. V. Gretschko and M. Pollrich (Incomplete Contracts in Multi-period Procurement, Management Science 2021; held version: ZEW Discussion Paper No. 19-040, 2019, titled Incomplete Contracts in Dynamic Procurement) show that in a two-period procurement model this loss can be avoided entirely. An English auction reveals who has the lowest cost but not what that cost is. Followed by a single spot offer, it gives the buyer exactly the surplus of the optimal complete contract. Related results on auctions with limited commitment are due to Skreta (2015), Liu, Mierendorff, Shi and Zhong (2019), and Vartiainen (2013).
A buyer buys one unit in period 1 and units in period 2 from one of suppliers, and values each unit at . She can buy in period 2 only if she bought in period 1.
Costs. Supplier privately knows a first-period cost . The costs are independent, with density on , and is bounded away from zero there. The distribution function is . At the start of period 2 a publicly observed state is drawn from a probability measure , and the second-period cost of a supplier is . Here is strictly increasing, with derivative .
Virtual costs. The first- and second-period virtual costs are
Assumption 1 requires both to be non-decreasing in .
Thresholds. The threshold is where crosses . The threshold is where crosses .
Complete contracts. A direct mechanism maps reported costs to a period-1 allocation , a state-contingent period-2 allocation and transfers . It is incentive compatible (IC) if truthful reporting is optimal for each supplier given truthful reports by the others. It is individually rational (IR) if each supplier's expected profit is non-negative. Its buyer surplus is the expected value .
Incomplete contracts. In the English auction with reserve , the price falls from the reserve. The last remaining supplier wins at the price at which his final opponent quit. After observing and , the buyer makes the winner a take-it-or-leave-it offer , which he accepts iff it covers his cost .
With reserve and the offer
the following hold.
The result says that, in this model, the commitment power of a complete contract is worth nothing to the buyer once she uses the right auction format. The English auction screens enough to identify the efficient supplier, and it conceals enough that the buyer cannot exploit what she has learned. This supports the observed use of open descending auctions followed by spot negotiation, and it contrasts with sealed-bid formats, whose bids reveal the winner's cost exactly. Example 2 of the paper shows that a standard-auction implementation with option contracts is not sequentially rational.
As far as a search of the Prove2Me catalog shows, none of these results has been formalized. The Mathlib-based library has one-period optimal auction and screening results (Myerson's optimal auction, envelope lemmas for single-period screening, sequential screening). It has nothing on two-period procurement, nothing combining an English auction with renegotiation, and nothing on the value of incomplete contracts. A formalization would check the optimal complete-contract benchmark, with its two-period envelope argument, and the equilibrium-plus-surplus claim of Proposition 3. It would also make explicit several conventions the paper leaves implicit, listed below.
The obvious argument for optimality, pointwise maximization of the virtual surplus, needs the envelope formula for all IC mechanisms. In this model a supplier's profit depends on a whole second-period schedule . The envelope therefore involves differentiating an integral over the state space under only measurability and boundedness assumptions, and every interim quantity is an integral over the other suppliers' costs.
For the English auction, "revenue equivalence" is not available off the shelf. The auction's period-2 payment depends on and on the first-period price, and the induced direct mechanism is not one of the direct mechanisms above with an -independent transfer. Equality of surplus must come from computing the auction's expected supplier profit (Lemma 2 and the profit formula ) and matching it with the optimal mechanism's. The thresholds add a further difficulty. With merely non-decreasing virtual costs and a density that need not be continuous, equations (1) and (2) need not have solutions, and the crossing points must be handled at the boundary.
Representation.
Env Ω over an arbitrary measurable space Ω, with a Standing predicate for the assumptions of §2 and an Assumption1 predicate.Fin n → ℝ, with law the product density on . Interim quantities overwrite one coordinate (Function.update).Conventions and additions, each disclosed in the items.
Ruled out. A formalization that stated the goal as "the English auction's allocation equals Proposition 1's allocation", or that defined the English-auction surplus by a virtual-surplus formula, would be trivial. The goal compares the surplus computed from the auction's outcome (winner, price, offer, acceptance) with every admissible IC/IR mechanism, and asserts attainment.
Not formalized. Proposition 2 (standard auctions with option contracts), Examples 1–2, and the extensions in §5.
Infrastructure. A complete development needs:
The envelope and order-statistic lemmas are reusable beyond this mission. Contributions of any of these, or of the milestones in any order, are welcome.
Inventory sharing (also called lateral transshipment) lets a retailer that runs short buy leftover stock from another retailer instead of placing an expensive emergency order. Between retailers under one owner, or retailers that do not compete, pooling is known to raise profits, and a suitably chosen transfer price can make independent retailers act exactly as a centralized firm would (Rudi, Kapur & Pyke 2001; Hu, Duenyas & Kapuscinski 2007, Management Science 53(8)). Real sharing agreements, however, are often struck between stores that compete for the same customers, for instance dealers of the same brand competing on service quality. Guo and Jiang ask what changes when the retailers compete on service: which transfer price the retailers want, whether they want to share at all, and whether any transfer price still reproduces the centralized outcome.
Two retailers sell one product at price . Each holds pre-season inventory bought at unit cost ; unmet demand can be filled by a quick-response order at unit cost , and a unit shipped between the retailers costs . The standing assumptions are
Retailer chooses a service level at cost , and faces demand with
where is a random vector on with an exchangeable joint law that has a density; . Service choices must keep both deterministic demands non-negative.
Without sharing, retailer earns . Under a sharing agreement at transfer price , a retailer short of stock buys the rival's leftover at before ordering from the manufacturer; its profit (equation (3) of the paper) adds the revenue and subtracts the purchase cost and the residual quick-response cost. Sharing is non-moot only for . With exogenous inventories , a symmetric equilibrium is a profile from which no retailer gains by a feasible unilateral deviation. A centralized owner sets and earns , given by (A.1) of the Online Appendix; each retailer's share is .
The paper's closed forms are without sharing and with sharing, where and are expectations of piecewise-linear functions of over the regions in which a transfer happens.
Assume at . Then
for every and all symmetric equilibria at , at and without sharing; and if , every symmetric sharing equilibrium at every non-moot satisfies
Lemma A.1(a)–(b) (the exchange identities); Lemma 2(a) (no-sharing equilibrium is ); Lemma 3(a), uniqueness (a sharing equilibrium is ); the closed forms (A.9) and (A.11) at symmetric profiles; Lemma 3(b) and 3(c) in ; Proposition 1(a) through the identity ; Proposition 1(c) for ; and the identity from the proof of Proposition 2.
The result separates the two roles a transfer price plays. Between non-competing retailers it only redistributes pooled profit; under service competition it also changes how hard the retailers compete, and the largest non-moot price softens competition most. Proposition 2 says the retailers therefore pick , always sign the agreement at that price, and still fall short of the centralized profit whenever : inventory sharing cannot by itself undo service competition. This contrasts with the coordination results for non-competing retailers cited above and with the paper's own Lemma 1 for .
The paper's proofs are informal calculus on iterated integrals against a density. A formal development makes explicit which steps hold for every exchangeable law and which need extra conditions. Two such conditions surfaced during planning: the sign of , and the existence of equilibria. No part of the paper had been machine-checked before this mission.
The obvious argument differentiates in and finds , which is positive only if . The paper asserts " for any given that " without proof, and it is false: for i.i.d. bimodal demand with , , , , , , , the closed-form service level turns negative before , the profit peaks near , and at that price it equals the centralized half-profit. The goal is therefore stated under the guard at . A second difficulty is that equilibria are defined by global best responses, while the paper's closed forms come from first-order conditions. The uniqueness direction needs the differentiability of expectations of kinked payoffs, for which the density matters. The existence direction is not true in general and is not part of the mission.
All quantities are real numbers. The law of is a probability measure on with , and Lebesgue. Exchangeability comes from the Online Appendix (); the main text states only equal marginals. The paper's iterated integrals are expectations of region indicators; open and closed region boundaries agree up to null sets. Service levels carry no sign restriction. Deviations must keep both deterministic demands non-negative. The bound of (A.7) is not imposed because no formalized result uses it. "Optimal" means "a maximizer": at every price is optimal. "Prefer" is weak, following the paper's tie-break rule (1).
The goal quantifies over equilibria defined by best responses. Stating it about the closed forms in place of equilibria would trivialize it into the milestones, and is ruled out. Since the goal is universally quantified, a sanity file checks that its hypotheses are jointly satisfiable (uniform demand, Figure 2's parameters, ) and that equilibria exist at . Existence for is open in this formalization.
A complete development needs: change of variables under the coordinate swap; integrability of bounded piecewise-linear functions on ; differentiation under the integral sign for kinked payoffs; and first-order conditions for concave or locally concave functions on an interval. The exchange identities and the symmetric-profile closed forms can be reused for other symmetric two-location sharing models. Proofs of any milestone are welcome, and so is an existence result for under explicit conditions.
Clustering methods must infer a partition from noisy observations, while the quality of a partition is usually judged against labels that the method cannot see. Fei and Chen study a balanced sub-Gaussian mixture model in which a semidefinite program (SDP) estimates a cluster matrix from pairwise distances. Their Theorem 1 relates its error to a simpler integer program allowed to know the true cluster centers. This comparison makes the SDP's error interpretable through an explicit benchmark, even when exact recovery is unavailable. The paper also investigates semi-random perturbations, but this mission targets the Model 1 comparison on which that broader discussion builds.
The tension is that an SDP solution may be fractional. Its entries express pairwise affinities, whereas an assignment matrix places each point in exactly one cluster. The result bounds the fractional matrix's entrywise error by an integer assignment error without assuming that the SDP solution itself is integral. That is the hidden-integrality claim relevant to this mission.
There are observations in and clusters. The true label of point is , and every cluster contains exactly points. For unknown centers , the observations have the form
The noise vectors are independent, measurable, zero-mean, and sub-Gaussian. Their vector sub-Gaussian norms are at most . The minimum center separation and signal-to-noise ratio are
The SDP uses the squared-distance matrix . It minimizes over real matrices with row sums , diagonal entries one, nonnegative entries, and symmetric positive semidefiniteness. Write for any optimum. The true cluster matrix is when and otherwise. Its error is measured by the entrywise norm .
The benchmark is an Oracle Integer Program. An assignment matrix has zero-one entries and exactly one one in each row. The true assignment is . The oracle sees the centers and augmented observations with the fixed , so its noise is four times the realized noise in . It minimizes
The Oracle error is the largest among assignments satisfying . The Oracle feasible set has no balance constraint. In contrast, the SDP retains the row-sum constraint inherited from balanced clustering.
The goal is the paper's quantitative comparison. It asserts that universal constants and exist such that, when
an event of probability at least has, for every realized SDP optimum , the bound
The constants are independent of , the centers, the labels, and the noise law. The event and the SDP optimum are chosen after the random observations are realized. The theorem fixes the factor two and the failure-probability expression exactly as printed.
The eight milestones follow the statements in Section 5: the six structural properties of the SDP error matrix (Fact 2), the basic inequality (16), the signal estimate (Proposition 3), the two noise estimates (Propositions 1 and 2), the representation of the remaining term (Lemma 1), the identity between the integer program and Oracle error (Lemma 2), and the final deterministic bound. Each milestone keeps the paper's constants and its own hypotheses. Together they expose the interfaces needed to close Theorem 1.
Theorem 1 transfers a question about a real matrix optimum to a finite assignment benchmark. The Oracle benchmark can itself be bounded under additional assumptions, as Fei and Chen do in their separate Theorem 2. The present target preserves the comparison even in regimes where the benchmark does not vanish. It therefore expresses an error guarantee rather than an exact-recovery assertion.
A complete Lean proof would connect a probability model, finite-dimensional semidefinite feasibility, and the paper's integer assignment comparison. At present these mission statements are draft proof obligations: compiling a statement with sorry checks its formulation but does not prove the result. The development reuses published definitions of scalar and vector sub-Gaussian norms; proving the new lemmas and the main theorem remains open within this mission.
SDP optimality gives an inequality for the squared-distance objective, but it does not directly bound the entrywise difference from . Noise enters that objective through both a Gram matrix and mixed center-noise terms. A direct entrywise comparison also ignores the row-sum and positive-semidefinite structure that constrains the SDP error.
On the benchmark side, replacing a fractional matrix error by an arbitrary rounded assignment would not retain the stated factor. The paper identifies an intermediate linear program whose value can be controlled at integer cardinalities. Formalizing the result requires preserving that cardinality constraint, the exact coefficient , and the distinction between the observed points and the oracle's augmented points.
Points, clusters, and coordinates use finite index types; Lean indices start at zero while the paper's and start at one. All matrices are real. The trace inner product is represented by a double sum, the matrix norm is entrywise, and the spectral norm in Proposition 2 uses the operator norm. The minimum separation ranges over distinct center pairs, which is nonempty when . Oracle maxima are finite, nonempty, bounded sets; the true assignment is a feasible candidate. The normalized denominators are nonzero under and with balanced labels.
The random model uses one probability space and the same noise realization in both and . Measurability, zero mean, independence, and the extended-nonnegative vector sub-Gaussian norm bound are explicit. High-probability conclusions use measurable events and quantify over every optimum at each realized data set. Deterministic milestones take a fixed realization and do not add a probability space. The universal constants occur before all model parameters. These choices rule out a vacuous instance-dependent SNR constant, a norm that assigns zero to heavy-tailed noise, and an SDP optimum chosen before observing the noise.
The scope is Theorem 1 and its selected Section 5 statements. Theorem 2's separate Oracle-error rate, the rounding algorithm, semi-random Model 2, and the stochastic-ball special case are outside this proposal. Reusable work includes the SDP and assignment interfaces, matrix-error identities, and finite integer-program comparisons. Contributions that prove the eight source milestones or establish their supporting concentration and finite-dimensional optimization results are welcome.
Firms that advertise online choose whom to target from the customer data they hold, and the industry's working assumption is that more granular data can only help: a firm that knows more about each consumer can at worst ignore the extra information. Despotakis and Yu (SSRN 3900394; Management Science, 2022, doi:10.1287/mnsc.2022.4604) show that this fails once consumers draw inferences from being targeted. A consumer who receives an ad learns something about how well the product suits her, and she decides whether to spend effort clicking on that basis. When the firm uses more dimensions of data, the set of consumers it targets changes shape, and the signal that being targeted conveys becomes weaker. In equilibrium the firm can then earn strictly less with more data than with less.
The result belongs to a line of work on targeted advertising as a signal, and on the value of customer data to a firm whose actions consumers observe and interpret. It is a commitment problem: the firm would like to promise to use less information, but cannot.
A unit mass of consumers is interested in a product sold at an exogenous price . A consumer's utility from the product is
where are her matching values on two components of the product and is her private weight on the first. The three are independent and uniform on . The consumer does not know and until she clicks.
The firm sends ads at unit ad cost . Under single-dimensional (sd) targeting it observes and chooses a targeting set ; under multidimensional (md) targeting it observes and chooses .
A targeted consumer does not see but expects a set . Her posterior is uniform: under sd targeting is uniform on and uniform on ; under md targeting is uniform on . She clicks at click cost if and only if her posterior expected surplus is at least ; the weights that click form the click set . After clicking she learns and buys if and only if .
Against a click set , the ad value of a consumer is times the probability that she clicks and buys, minus ; under md targeting . The firm's profit from targeting is the integral of the ad value over .
A non-trivial equilibrium is a targeting set of positive measure that maximizes the firm's profit over all targeting sets, against the click set that consumers who correctly expect produce. An md equilibrium is symmetric if is symmetric about the 45-degree line. and denote equilibrium profits. Two thresholds from the paper enter the statements: the click-cost threshold of Equation (7), above which no non-trivial symmetric md equilibrium exists, and the ad-cost threshold from the proof of Proposition 1.
For every there is such that for every there is such that for every both a non-trivial sd equilibrium and a non-trivial symmetric md equilibrium exist, and
for every such pair. The goal fixes neither nor ; the right end of the click-cost interval is the explicit threshold of Equation (7).
The result is a clean counterexample to the monotonicity of the value of information for a firm whose actions are observed by strategic receivers. It isolates a mechanism, inference from being targeted, that does not need competition, price discrimination or privacy costs to make extra data harmful. The paper uses it to explain why firms might coarsen the data they act on, and §5 revisits the comparison with endogenous pricing and with consumers who do not know which dimension the firm targets on.
On the platform this mission is the first model of targeting with consumer inference. The model layer, uniform posteriors on an expected targeting set, click sets defined by posterior expected surplus, and equilibria defined as fixed points over arbitrary measurable targeting sets, is reusable for other signalling-through-targeting results. The result is proved on paper, with Lemmas 4 and 5 argued in sketch form; to our knowledge no part of it has a machine-checked proof.
Both equilibria are fixed points: the firm's best response depends on the click set, and the click set depends on the expected targeting set through a posterior average. The md firm may choose any measurable subset of the square, so the reduction to the two-line class of Equation (6) is part of the work, and Proposition 2 asks for uniqueness among all symmetric measurable equilibria, not only within .
The comparison itself is not a monotonicity argument. As approaches , the md click set shrinks to the threshold where the md equilibrium disappears, while the sd profit stays positive only because lies strictly below , where the sd profit vanishes. Making this precise requires the piecewise closed forms of the expected surplus (with logarithms) and control of both profits uniformly as , which the page leaves implicit. Comparing the closed forms at a single numerical point does not give the statement for every price.
All quantities are real numbers. Consumer populations are Lebesgue measure on and , so probabilities are lengths and areas. Targeting sets are measurable subsets of the unit interval or square, "non-trivial" means positive measure, "symmetric" means invariance under , and "unique" means unique up to a null set. The tie-breaks follow the page: buy at , click at equality, and indifference is allowed in the firm's optimization. Click thresholds are arbitrary reals, so an empty click set is expressible.
Equilibria are defined as fixed points, never by the paper's closed forms and ; otherwise Propositions 1 and 2 would be definitional and the goal a comparison of two formulas. The paper's is defined as the least click cost at which , which would make a literal statement nearly true by definition; the goal therefore asserts the existence of the region instead, and it includes existence of both equilibria so that the comparison is not vacuous.
Added or restricted hypotheses: Propositions 1 and 2 are stated only in the regimes Proposition 3 uses; Proposition 1 uses strictly (at equality the cutoff is and the targeting set is null); Lemma 4 adds ; Lemma 5 is stated in – form because its limit is not shown to exist; and the price is throughout.
A complete development needs set integrals and product measures from Mathlib, convexity of the expected surplus in , and real analysis of the piecewise closed forms. Proofs of any milestone, and alternative arguments for Lemmas 4 and 5, are welcome.
Utility networks such as water pipelines, gas distribution systems and power grids are exposed to attacks on their physical components. An operator who cannot monitor every component must decide where to place a limited number of detectors, without knowing which components an adversary will target or how many of them. Dahan, Sela and Amin (arXiv:1705.00349, Operations Research 2022) model this as a two-player zero-sum game between a defender who places detectors and an attacker who chooses a set of components to disrupt. Their game sits in the line of security games and network interdiction models (Washburn and Wood 1995; Tambe 2011), with set cover and set packing as the combinatorial structure that governs its equilibria.
The practical question the paper answers is whether the defender needs to know the attacker's resources. The main result, Theorem 2, says it does not, within a range described by a set packing number of the network.
A detection model consists of a finite set of nodes, a finite set of components, and for each node the set of components a detector at monitors. Every component is monitored from at least one node. For let , and define the detection function
the number of attacked components in that some detector of monitors.
The defender (P1) has detectors and chooses a positioning . The attacker (P2) has resources and chooses an attack plan . Both may randomize: , . The attacker's payoff is the expected number of undetected attacks
the defender receives , and this zero-sum game is . A Nash equilibrium is a profile with for all ; the set of equilibria is . The value is . The expected detection rate of a profile is
A set cover is a set of nodes monitoring every component; is the minimum size of a set cover (MSC). A set packing is a set of components no node monitors two of; is the maximum size of a set packing (MSP). The paper's case of interest is and : the defender cannot monitor everything, and the network is large compared with the attacker's resources.
For every there is such that
and every inspection strategy that is part of an equilibrium of is part of an equilibrium of every with . The goal fixes no value of : it asserts only that one number serves all admissible .
The result. Theorem 2 separates the defender's problem from the attacker's resources. The defender may solve the game for a single attack resource, , a linear program over attack plans of size one, and use the resulting inspection strategy against any attacker with fewer than resources; the guaranteed detection rate is the same. Together with Proposition 2 of the paper, this reduces the problem of choosing the fewest detectors that achieve a target detection rate to games with , and so to linear programs whose size does not grow with the attacker's resources. The linearity (18) of the value in is the quantitative form of the statement.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. A formalization fixes the boundary conventions the paper leaves implicit (the empty attack plan in the rate, ), supplies the existence of equilibria of finite zero-sum games that the paper takes for granted, and makes explicit the cases of step (i.a), which the printed argument does not cover.
The central difficulty is step (i.a): an optimal attack strategy of may concentrate its probability on a few components. Scaling its attack probabilities by can exceed , so it need not define a strategy of . The required conclusion is stronger than the existence of an equilibrium: an optimal single-attack strategy must exist whose probability on each component is at most .
Theorem 1 also requires strict use of both players’ resources in equilibrium, even though their action sets permit smaller plans. Without that result, the expected detection rate cannot be identified from the game value by dividing by . The marginal-realization claim in Lemma EC.4 must work for every vector in the stated polytope, including its boundary.
Everything is finite and there is no measure theory. The game is an instance of the published finite zero-sum game BlottoLP.Flow.ZeroSum: the attacker is the row player over the subtype , the defender the column player over , mixed strategies are nonnegative real weight functions summing to , and payoffs and the rate are finite double sums. An inspection strategy therefore never uses more than detectors. is the optimal value of (LP1); and are the infimum and supremum of the cover and packing sizes, well defined because every component is monitored from some node.
Conventions fixed in Lean: the ratio is (an empty attack plan counts as detected), which the case of Theorem 2 requires; is assumed wherever is quantified, since at every profile is an equilibrium; Lemma EC.3 assumes ; cyclic windows are indexed from . The standing assumptions , of §3.3 are hypotheses of each statement that uses them.
A trivializing formalization is ruled out: the equilibrium predicate is exactly (5) over the correct strategy sets, and a sanity check exhibits an equilibrium of in a network with . The extrema used in the statements have nonempty, bounded domains under their hypotheses, and the empty attack plan has an explicit rate convention. When the goal is vacuous, as in the paper.
Infrastructure needed: the minimax theorem for finite zero-sum games, Farkas' lemma (on the platform as LinearOptimization.farkas_lemma), and finite sums over subsets. The coverage-function facts, the cyclic strategies, and the marginal-realization lemma are reusable for other security and inspection games. Proofs of any milestone, and alternative proofs of step (i.a), are welcome.
Interior-point methods solve a conic optimization problem by following the minimizers of a barrier function for the cone. Their iteration count is governed by the barrier's parameter : the best known algorithms need iterations to reach accuracy (Nesterov and Todd, 1997). A cone can be used natively by a solver only once a logarithmically homogeneous self-concordant barrier (LHSCB) with a small parameter is known for it, together with efficient oracles for its derivatives.
Coey, Kapelevich and Vielma (arXiv:2103.04104v2; Mathematics of Operations Research, 2022) study cones defined by spectral functions on Euclidean Jordan algebras. This framework covers vectors, real symmetric matrices and complex Hermitian matrices at once. The paper implements the resulting cones in the solver Hypatia. One of its two new barrier results concerns the root-determinant cone, the hypograph of the geometric mean of the eigenvalues. For symmetric matrices this is the hypograph of over the positive semidefinite cone, a standard modelling device for D-optimal experimental design and for determinant maximization. Before this paper, the usual way to represent it was an extended formulation with auxiliary variables and a semidefinite constraint.
A Jordan algebra is a real vector space with a bilinear product that is commutative and satisfies the Jordan identity , where . It has a multiplicative identity . It is Euclidean if . An idempotent is a with . It is primitive if it is non-zero and is not the sum of two orthogonal non-zero idempotents. A Jordan frame is a family of pairwise orthogonal primitive idempotents summing to . Every Jordan frame of has the same size , the rank of .
Every has a spectral decomposition over a Jordan frame, with real eigenvalues . From these, , , and a real function acts by . The inner product is the trace form . The cone of squares is ; means . The quadratic representation is , where .
The root-determinant is on . With and , the root-determinant cone and its candidate barrier are
A function is a -LHSCB for a cone if it is and convex on and tends to at the boundary. It must also satisfy and , and the parameter satisfies .
The goal holds for every finite-dimensional Euclidean Jordan algebra of rank , not for one matrix algebra.
which are (105), (107) and (108). 6. The scalar inequality (109c): for every . 7. The compatibility inequality (103) on :
The result gives the root-determinant cone a barrier whose parameter is one more than the optimal parameter of its domain , so it cannot be improved by more than one (p. 24). It also removes the extended formulation: a solver works with the cone in its natural dimension. The paper pairs the barrier with closed-form oracles for the gradient, Hessian product and inverse Hessian product (§7.4, Lemma 7.1), and reports computational gains in Hypatia. Because the statement is uniform over Euclidean Jordan algebras, it covers the vector, real symmetric and complex Hermitian cases at once.
The result is proved in the paper; this mission formalizes it. To the best of the curators' knowledge, it has no machine-checked proof, and Lean's Mathlib has no theory of Euclidean Jordan algebras, spectral decompositions in them, or barrier functions for their cones. Formalizing Proposition 7.1 therefore also yields a reusable layer: the Jordan-algebraic setting, the cone of squares, the quadratic representation, and an LHSCB predicate on arbitrary normed spaces.
The obvious route checks self-concordance of directly. That requires bounding the third derivative of by the -power of its Hessian in every direction. The two logarithmic terms interact, and no simple direct estimate is available. The paper instead uses a compatibility criterion of Nesterov and Nemirovskii, which reduces the barrier property to the single inequality (103) between derivatives of and . In Lean that criterion is not available and must be established for this cone; it is the deepest milestone.
The derivative identities (105), (107) and (108) require differential calculus of spectral functions on a Jordan algebra: derivatives of , of , and of , expressed through the eigenvalues of the scaled direction . Deriving them from the structure axioms needs, among other things, the fact that the eigenvalues of and are those of scaled and squared, uniqueness of the spectral decomposition, and positivity of the eigenvalues on . Only the final scalar inequality (109c) is elementary.
is a real finite-dimensional inner product space carrying a structure EJA V d. The structure bundles the Jordan product (bilinear, commutative, Jordan identity), the unit and the Euclidean property. It also bundles, for every , eigenvalues and a Jordan frame of primitive idempotents with , and the identity . The spectral theorem (Faraut–Korányi III.1.2) says such data exist for every Euclidean Jordan algebra of rank , so this is the paper's setting. Primitivity forces to be the rank: without it, a frame could be padded with zeros and would change.
The ambient space is . Directional derivatives are iterated Fréchet derivatives on the diagonal, and "boundary" is the topological frontier. The barrier limit is taken within the interior at every frontier point.
The following conventions are fixed:
Properness is a separate predicate from LHSCB, because is not pointed.
A trivializing formalization is ruled out by these choices. Specializing to or , dropping primitivity, allowing , dropping convexity, or imposing the barrier limit at only some boundary points would each prove a different, weaker or vacuous statement.
Proposition 6.1 (the -LHSCB for the matrix monotone derivative cones) and Lemma 7.1 (the inverse Hessian oracle) are deliberately absent. The first needs matrix monotonicity and Löwner's integral representation and is independent of Proposition 7.1. The second is an oracle formula that the goal does not use.
Contributions are welcome at every level: the scalar inequality (109c); the cone and homogeneity facts; the spectral calculus behind (105)–(108); and the compatibility reduction. The Jordan-algebraic infrastructure and the LHSCB predicate are reusable beyond this mission.
Whether more competition among banks makes the financial system safer or more fragile is a long-running question in banking theory and regulation. The competition-fragility view holds that competition erodes bank margins and charter values and so encourages risk-taking; the competition-stability view, formalized by Boyd and De Nicolò (2005), holds that competition lowers loan rates, which reduces the incentive of borrowers to choose risky projects. Empirical studies of deregulation episodes, such as the removal of interstate branching restrictions in the United States, have found evidence for both views.
Dam and Sengupta (2024) point out that such episodes do not merely add competitors to a single market: they integrate previously separate markets with different customer compositions. In their model integration changes both the number of competing banks and the ratio of borrowers to depositors each bank faces, and the second channel can reverse the conventional prediction in one of the integrating markets. This mission formalizes that result, Proposition 2 of the paper, together with the equilibrium characterizations it rests on.
There are two banking markets . Market has depositors, borrowers (entrepreneurs) and banks, and is a model constant. A borrower chooses the risk of a unit-size project, which returns with probability and otherwise. At loan rate the borrower maximizes ; a maximizer is a borrower-optimal risk.
Inverse deposit supply and inverse loan demand in market are and , where and are aggregate deposits and loans. Banks are financed by deposits only, so . Each bank chooses a loan volume to maximize its expected profit, display (2),
A Cournot equilibrium is a profile of volumes from which no bank gains by changing its own volume. The segmented market equilibrium (SME) of market is the Cournot equilibrium of this game; its loan rate is and its borrower-optimal risk .
The integrated market has depositors, borrowers and banks, with profit (7) of the same form. Its Cournot equilibrium is the integrated market equilibrium (IME), with loan rate and risk . The customer composition of a market is the ratio of borrowers to depositors, and . Market 2 is labelled as the borrower-heavy one, .
The comparison is organized by the two terms of display (11):
the bank-competitor effect (more banks) and the bank-customer effect with respect to market (a different customer composition).
If , then for all Cournot equilibria of the three markets and all borrower-optimal risks at their loan rates,
Proposition 2 shows that a single deregulation episode can lower loan rates and borrower risk-taking in one integrating market while raising them in the other, even though the number of competing banks doubles. Its consequence for empirical work is that the competition-fragility and competition-stability views can both be consistent with the same episode, depending on each market's initial customer composition; it also separates within-market competition (captured by , which reproduces the classical Boyd–De Nicolò prediction) from across-market competition. Corollary 1 and the bank-merger analysis of §3 build on the same equilibria.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The formal work this mission adds is the Cournot layer: the paper's proof of Lemma 6 argues only through the first-order condition, whereas the formal statements require that the closed-form profile is a global best response for every bank and that no other equilibrium, symmetric or not, exists.
The algebra of (11) and of the sign comparisons is elementary once the equilibrium rates are known. The substantive step is the equilibrium characterization. A bank's profit is a cubic in its own volume, so the first-order condition is necessary only at an interior choice and is not sufficient. A complete argument must rule out corner equilibria in which some banks lend nothing, show that every equilibrium is symmetric, and show that the stationary point is a global maximum over all nonnegative volumes. The integrated market has banks indexed by Fin (2 * n), so the cast from to the real number enters every closed form.
All quantities are real numbers, the number of banks is a natural number, and banks are indexed by Fin n (segmented) and Fin (2 * n) (integrated). A Cournot equilibrium is the published feasible pure-strategy Nash equilibrium CarbonDoubleCount.Planner.IsPureNash, with feasible set for each bank and payoff given by display (2)/(7). The loan and deposit rates are functions of the aggregate equilibrium volume. A borrower-optimal risk is a maximizer of over ; it is never defined by a closed form. The standing assumptions , , of p. 6 are bundled in one predicate, and is a separate hypothesis.
Added or chosen conventions: the volumes are nonnegative; equation (1) is stated for ; Lemma 6(a) assumes and is stated for banks (the appendix prints , while Lemma 1 needs ); "sufficiently weak/strong" in Proposition 2 is the strict comparison of with , and the tie is not covered, as on the page.
A trivializing formalization would define , , , by the closed forms (4), (5), (9), (10), which reduces the goal to arithmetic; the goal instead quantifies over all Cournot equilibria and all borrower-optimal risks, and the weak/strong conditions are stated through the defined effect terms, not through and . All hypotheses are satisfiable: the parameters , , , , satisfy the premise of (b-i), and , , , , that of (b-ii).
Contributions welcome: proofs of the milestones, in particular a reusable characterization of symmetric Cournot equilibria for cubic profits of this form, which also covers the merger analysis of §3.
Many assets, such as corporate and municipal bonds, securitized products and new issues, trade over the counter: there is no central exchange, and an asset reaches its final buyers through a sequence of bilateral trades between dealers. Empirical work on these markets documents intermediation chains, in which a block of securities passes through several dealers, each of whom keeps part of it for her own customers and sells the rest onwards: in US municipal bonds, Li and Schürhoff (2019) find that chains account for 82% of the trades that start with a customer selling to a dealer, and in registered securitizations Hollifield, Neklyudov and Spatt (2017) find that about 27% of customer sales give rise to a sequence involving more than one dealer (figures as reported by Colliard and Demange, p. 1). Colliard and Demange (SSRN 3244321, forthcoming in Management Science) build a model of this process in which the length of the chain, the prices and the quantities are all equilibrium outcomes, and the friction that makes the chain finite is asymmetric information about how much each dealer's customers want to buy.
The equilibrium of that model rests on one object, the collected demand , defined by a functional equation. This mission formalizes the existence and properties of and the theorem that the strategies built from it form an equilibrium of the dealer game.
An asset pays a sure return per unit. Dealers arrive in sequence. Each is available to trade with probability , independently. Dealer 's customers buy up to units at price ; the customer demand is private information of and is drawn i.i.d. from a distribution on with finite mean. Write . may have atoms. Dealers borrow cash at the funding spread .
A dealer of type who accepts a take-it-or-leave-it offer (volume at unit price ) sells to her customers and has financing needs , which she covers by borrowing or by making a new offer to the next dealer, with . If the next dealer accepts with probability , her expected profit (5) is
A rank-free equilibrium (Definition 1) is a strategy (an acceptance rule and a new-offer rule ) that does not depend on the dealer's position in the chain, such that is the acceptance probability induced by , the new offer maximizes over all feasible offers, and a dealer accepts exactly when this maximal profit is non-negative.
The collected demand is the function on solving
The maximizers form the set of targeted values (10); a selection is a function with for all .
For bounded, continuous and solving (9), and any selection , put . The strategy "accept iff ; on acceptance with offer with
(and no offer when )" is a rank-free equilibrium. Moreover , , the offer's expected transaction payoff is , and the dealer's profit is .
Theorem 2 is the existence result on which the rest of the paper is built. The comparative statics of dissemination length, customer purchases and prices along the chain (Propositions 1–4, Implications 1–6) are all statements about this equilibrium. It shows that the infinite-horizon screening problem of each dealer, against a chain of unknown length, reduces to the one-dimensional equation (9), and that the reduction is exact: the expected transaction payoff from the new offer is .
The paper proves Theorem 2 in Appendix A; Lemma A.2 is proved in an Online Appendix that is not part of the source. To the knowledge of this mission, none of these results has a machine-checked proof. The mission's output is a checked existence-and-optimality argument for a dynamic screening game with a discontinuous survival function, together with the fixed-point theory of the operator , which is not an expectation operator and does not fall under standard Bellman-operator results.
The operator takes a supremum over the moving interval of a product with the survival function , which jumps downward at every atom of . Standard dynamic-programming theorems assume a continuous kernel or a finite state space; here attainment of the supremum and continuity of rely on being left-continuous and non-increasing, and on . In the equilibrium part, the natural first step, verifying optimality only against the strategy's own offer or against offers accepted with a fixed probability, does not work: a deviation changes the set of types that accept it, so the acceptance probability must be recomputed from the acceptance rule for every candidate offer. The deviation can change both its unit margin and its probability of acceptance, making a uniform payoff bound the central difficulty.
All objects live in the namespace DealerDissem.RankFree, in one definitions file. Parameters are bundled with , , . is a Measure ℝ that is a probability measure, gives no mass to and has an integrable identity; is the measure of (closed, so acceptance probabilities are exact at atoms). , , , are functions ℝ → ℝ; every hypothesis and conclusion about them is restricted to , and uniqueness in Theorem 1 is equality on . Suprema in (9) and (46) range over . Acceptance rules are predicates , and is computed as the -measure of the acceptance set. is (14) solved for (the paper's (16)), and ; at , and Lean's value is irrelevant.
Definition 1 (ii) is encoded as: after acceptance the strategy's offer is feasible and maximizes (5) over every feasible offer; and acceptance holds iff some feasible offer gives a non-negative profit. The equilibrium predicate requires measurable acceptance events for feasible offers, so the quantity called a probability in Definition 1 (i) has that meaning. Added hypotheses, each where the printed sentence is false otherwise: in "this case surely occurs for "; for the bound ; non-negative in the contraction milestone.
A trivializing formalization is ruled out: is never a free parameter, optimality is against all feasible offers rather than the strategy's own, must solve (9) at every , and must be a maximizer, not merely a point of .
A complete development needs suprema over compact intervals of upper semicontinuous functions, the Banach fixed-point theorem on bounded continuous functions on , and Markov's inequality for . The fixed-point machinery for sup-over-interval operators is reusable for other sequential search and screening models. Proofs of any milestone are welcome, as is a proof of Theorem 2 from the milestones.
Public procurement agencies and group-buying platforms increasingly run framework agreements: suppliers post prices, and the agency then decides which suppliers' products appear in the catalogue from which buyers choose. Chile's ChileCompra framework agreements and drug formularies work this way. The agency faces a trade-off. Showing many products serves buyers with heterogeneous tastes. Showing few products makes suppliers compete harder on price.
Saban and Weintraub (2021, Operations Research; SSRN 3453144) formulated this as a mechanism design problem and solved it when the agency may use arbitrary payments. In practice, payments are pay-as-bid: a supplier included in the catalogue is paid the price it posted. In addition, the selection rule must be anonymous (it may depend on prices, not on identities) and monotone (a price cut never hurts the supplier who makes it). Choi, Saban and Weintraub (2022; SSRN 3785023) ask which selection rule maximizes expected consumer surplus under these constraints. Their answer, for symmetric suppliers with two possible cost levels, is a simple three-parameter rule: the k-soft reserve.
There are suppliers . Each supplier's unit cost is with probability and with probability , independently, with .
Demand. Buyers are a single representative consumer with consumer surplus
where is the vector of market shares and the vector of prices. In the symmetric affine model (Model 2), and has on the diagonal and off it, and is positive definite. Given a nonempty assortment and prices , the demand maximizes over with and for (Problem (1)). Total demand is one: there is no outside option.
Mechanisms. An assortment function includes supplier when . A reserve price forces whenever . The rule is equitable if it is anonymous, , and monotone: lowering weakly raises and weakly lowers every other . The allocation is .
The k-soft-reserve rule excludes supplier if , or if and at least suppliers price at most ; otherwise it includes . With it is the no-competition rule, which includes every supplier priced at most .
Problem (8). Suppliers play a symmetric Bayes–Nash pricing strategy . The agency chooses to maximize
subject to: neither type gains by deviating to any price in (BN-L, BN-H); and (IR); equitable (AM); and the reserve constraints RP(1), RP(2).
For every optimal solution of Problem (8) there is such that
The goal does not fix the optimal , or ; those depend on all the parameters, and the paper computes them numerically.
The result. Problem (8) is an optimization over all equitable assortment functions, an infinite-dimensional space of -valued maps, coupled to equilibrium constraints. The problem is a mixed-integer and non-convex program (p. 14). Proposition 1 collapses it to a search over three numbers, . The paper's numerical study of the best soft-reserve rule, and its comparison with the centralized benchmark of Saban and Weintraub (2021) (Proposition 3), both rest on this reduction. The companion Proposition 2 () narrows the search further.
Formalizing it. The result is proved in the paper; this mission produces the first machine-checked version. The proof is short but informal at several points that a formalization must make precise. The interim utility is written by anonymity in a binomial form that presupposes anonymity of the demand. Two mechanisms are claimed "identical in equilibrium" when one of them keeps suppliers with zero demand that the other excludes. Lemma 2's displayed inverse of swaps its diagonal and off-diagonal entries. No proof exists in Lean or any other proof assistant.
The obvious argument copies on the equilibrium path and makes it as harsh as possible off the path. The difficulty is that off-path behaviour is exactly what sustains equilibrium. One must show that replacing by a -soft reserve never makes a deviation more attractive, for every deviation price and every number of low-type opponents. This requires comparing demands under two different assortments at the same prices. That comparison holds only because demand in this model is monotone in the assortment and in prices. Neither property is automatic for a general quadratic program; both rest on the symmetric structure of . The choice of is the minimal number of low-type suppliers at which high types receive zero demand, and showing that it is well defined uses monotonicity again.
All objects live in the namespace PayAsBid.SoftReserve and are defined in one definition file. Suppliers are Fin n (0-indexed), prices are real vectors, types are Bool (true is ), and inclusion is Bool with false < true. Demand is a chosen maximizer of Problem (1), and 0 when Problem (1) has no feasible point. Expected values are finite sums over the type profiles. The interim utility (5) sums over full profiles with the deviator's own price replaced; this equals the paper's sum over opponents' types.
Conventions and additions to the page, each disclosed in the item where it occurs:
The domain conditions rule out a trivializing reading. Without them, a mechanism that excluded everybody on some profile would earn the junk surplus , which exceeds every genuine surplus in the reduced model, and the goal would fail. The hypothesis of the goal is optimality, not feasibility, as on the page. A companion verification file proves that an optimum exists: for the no-competition rule with is optimal. The hypothesis is therefore not vacuous.
A complete development needs:
The demand lemmas (milestones 1, 3, 5) are reusable for any assortment problem with affine demand and no outside option. Contributions are welcome on every milestone; Lemmas 1 and 3 are self-contained, and milestones 4–5 are the analytic core.
In budget aggregation, a group has to split a fixed public budget among several projects, and each member proposes her own ideal split. A rule is needed to turn the proposals into one split. The question was studied for preferences by Freeman, Pennock, Peters and Wortman Vaughan (2021), who asked whether strategyproofness, efficiency and proportionality can be combined; the paper formalized here answers no for . With preferences an agent cares only about the total distance from her ideal split. Many budgets are not like that: when projects are complementary, generous funding of one project does not make up for starving another. Leontief utilities model this: an agent's benefit is set by the project that gets the smallest fraction of what she proposed for it.
Brandt, Greger, Segal-Halevi and Suksompong (arXiv:2402.15904v3) show that, with Leontief utilities, the rule that maximizes the product of the agents' utilities is the only continuous rule that resists coalitional manipulation and gives every coalition its proportional share of decision power. The rule and several of its properties come from the same authors' work on donor coordination, Coordinating charitable donations with Leontief preferences (JET, 2025). The fairness axiom is the core fair share notion of Fain, Goel and Munagala (2016) and Aziz, Bogomolnaia and Moulin (2020), adapted to distributions.
There are agents and alternatives (projects) . A distribution is a vector with and ; the set of distributions is the simplex . Each agent reports a peak , her ideal distribution. A profile collects the peaks, and a mechanism is a map .
Let ; it is nonempty because sums to one. Agent 's Leontief utility from a distribution is
which lies in and equals exactly at . The minimizers form the set of agent 's critical alternatives, and for a group , .
The axioms are as follows.
The Nash product rule is
and the paper notes, citing the donor coordination paper, that the maximizer is unique.
For every mechanism ,
Both directions are part of the goal. "" says NASH has the three properties, and "" says no other mechanism has them.
The milestones are the paper's own results, in the order the proof uses them:
Five of these results are cited by the paper from Brandt et al. (2025) rather than proved in it: uniqueness of NASH, Lemma 1, Lemma 6, Lemma 7, and the efficiency and group-strategyproofness of NASH.
Theorem 3 characterizes a mechanism by its axioms. A designer who asks for continuity, resistance to coalitional misreports, and proportional coalition power gets exactly one mechanism with Leontief utilities, so no further choice is needed. This contrasts with the paper's impossibility results for and preferences (Theorems 1 and 2), where efficiency, strategyproofness and proportionality cannot hold together for . Core fair share is stronger than both efficiency (Proposition 3) and proportionality (Proposition 4), so the positive result covers both.
The theorem is proved on paper. No machine-checked proof of it, or of the cited results from the donor coordination paper, is known. The mission provides a definition layer for simplex-valued Leontief utilities, critical alternatives, coalition blocking with shares and group-strategyproofness. It states the characterization and every intermediate result its proof cites, so proofs can be built bottom-up, including the cited results that the paper does not prove.
Group-strategyproofness constrains only utilities, while the theorem identifies whole distributions. Turning one into the other needs efficiency (Lemma 7), which is why Proposition 3 sits early in the chain. The key step, Lemma 9, compares at and at . These are profiles at which several agents change their reports simultaneously, and continuity together with group-strategyproofness has to rule out a change of outcome. Agent-by-agent arguments do not suffice, because each single deviation can move the critical sets of the other agents. Continuity of NASH (Proposition 1) is also not immediate: as a peak coordinate tends to , that alternative leaves and the minimum defining changes form.
Agents and alternatives are Fin n and Fin m, indexed from , with [NeZero n] [NeZero m] for the paper's convention that and are positive integers. Distributions are elements of Mathlib's stdSimplex ℝ (Fin m), profiles are functions Fin n → stdSimplex ℝ (Fin m), and mechanisms map profiles to distributions. All values are real, including the shares and . Continuity is Continuous for the subtype topology, which is the topology of the paper's definition (Definition 7).
The formalization makes these commitments.
These choices rule out the trivializing readings: an unsatisfiable core axiom, an identically zero utility, NASH as an arbitrary mechanism, and a one-directional goal presented as a characterization.
A complete development needs finite-minimum and product inequalities on the simplex, a compactness argument for existence of the maximizer, strict log-concavity arguments for its uniqueness, and the decomposition (flow) certificate of Lemma 6. The Leontief and core definitions can be reused in work on donor coordination, fair mixing and participatory budgeting. Contributions on any milestone are welcome, especially formal proofs of the results the paper cites from Brandt et al. (2025).