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?
Lie 2-algebras allow a Lie bracket to satisfy its laws up to a specified higher operation. They arise when an ordinary Lie algebra extension has a cocycle in degree three rather than degree two. Baez, Crans, Stevenson, and Schreiber use this language to relate a finite-dimensional model attached to a compact simple Lie group to an infinite-dimensional construction made from paths and loops. Their paper also constructs a Lie 2-group at integral levels; the algebraic comparison is Theorem 5.1 of the pinned preprint, the target of this mission.
The comparison matters because the two descriptions expose different features. The finite-dimensional algebra displays its degree-three cocycle directly. The path algebra comes with a central term built from an integral over the path interval. Showing that these models are equivalent makes it possible to use the smaller skeletal description while retaining the structure carried by based loops. The main result states more than a loose correspondence: it puts both models in a strictly exact sequence of Lie 2-algebras.
Let be a finite-dimensional simple real Lie algebra with an invariant positive-definite inner product . Fix . Write for the smooth functions with , and for those also satisfying . Their brackets are pointwise. A prime denotes differentiation with respect to the interval coordinate, with one-sided derivatives at the endpoints.
A 2-term -algebra has vector spaces , a linear map , binary brackets in degrees and , and a ternary bracket . A homomorphism has components : a chain map in degrees zero and one and a skew bilinear correction . The correction obeys the three compatibility equations of Definition 2.7. A 2-homomorphism is a linear chain homotopy with the extra bracket equation of Definition 2.8. Two algebras are equivalent when there are homomorphisms in both directions whose composites are 2-isomorphic to the identities.
The skeletal algebra has , , zero differential, the ordinary bracket on , trivial action on , and
The path algebra has , , and . Its degree-zero bracket is pointwise, , and its action on degree one is
Finally, has in both degrees, identity differential, its pointwise bracket in both binary slots, and zero ternary bracket. These are the formulas of Example 2.15, Proposition 4.2, and Lemma 5.2.
The main target is the strictly exact sequence of Theorem 5.1:
Strict exactness means that is injective, its image is the kernel of , and is surjective on both the object and morphism vector spaces. The composite is the zero homomorphism, including its bilinear component. This is a statement for every real ; no integrality condition is attached to the Lie-algebra result.
The five milestone targets are the paper's numbered Lemmas 5.3, 5.4, 5.5, 5.7, and 5.8. They state, in order, that is equivalent to zero, that the endpoint and integral formulas define , that is its strict kernel via , that any smooth endpoint interpolation defines a reverse homomorphism , and that is the identity while is 2-isomorphic to the identity. Their exact formulas are in the theorem items and milestone statements.
The theorem identifies the skeletal degree-three cocycle with the path model's integral central term at the level of Lie 2-algebra equivalence. It also locates the based-loop algebra within a strict exact sequence, so the comparison retains information about kernels and morphisms as well as objects. The paper uses this algebraic result alongside a separate group-level construction whose integral-level conditions have a different role; the conclusion of §6 distinguishes the two.
The paper proves the result on paper. This mission asks for machine-checked proofs of the displayed homomorphism and 2-homomorphism equations and of strict exactness. A completed development would also leave reusable definitions for smooth based paths, central loop integrals, and the component presentation of 2-term homomorphisms. The paper's Fréchet Lie 2-group construction and its topological realization are outside this mission.
The endpoint map alone does not define a homomorphism of the relevant 2-term algebras. Its bilinear component must account for the central integral in and for the nonzero ternary bracket in . The integral formula contains a boundary term for general paths, so treating it as the loop cocycle without that term changes the statement. The reverse homomorphism depends on a smooth interpolation , and equivalence requires its composites to match the identity at all three component levels, together with the 2-homomorphism equation. Smoothness, endpoint behavior, and the signs in the graded brackets all affect these equalities.
Lean represents a path by a function on that is smooth on and constant outside it, fixed by clamping to the interval. This removes irrelevant differences between extensions of the same interval path. The underlying Lie algebra has a continuous bilinear bracket, Jacobi identity, invariance of the inner product, and simplicity. The continuous-bracket requirement is automatic in finite dimension. The inner product can be any invariant positive-definite form; the normalization by the basic form divided by used for the group construction is not imposed. All levels are included.
The formal object called a Lie 2-algebra is its 2-term presentation. Theorem 2.10's equivalence with the categorical presentation is used as the paper's interpretation and is not re-proved. The record stores the operations, while the homomorphism records explicitly enforce the chain map and equations (3)–(5), and 2-homomorphisms enforce both chain-homotopy equations and equation (7). It does not separately store the HDA6 coherence equations. Composition is recorded by the paper's component formula (6). The data for are defined directly from Proposition 4.2, without building the Fréchet Lie 2-group first. The source's exact integral coefficients, real summand, and nonzero ternary bracket are fixed in the definitions; removing any one of them changes the target.
Contributions to the analytic closure of smooth paths under pointwise brackets, the interval integration identities, and the homomorphism equations are useful beyond the final theorem. Proofs of the five stated lemmas and of the final exactness and equivalence claims are the intended contributions.
We give an overview of relative tensor products (RTPs) for von Neumann algebra modules. For background, we start with the categorical definition and go on to examine its algebraic formulation, which is applied to Morita equivalence and index. Then we consider the analytic construction, with particular emphasis on explaining why the RTP is not generally defined for every pair of vectors. We also look at recent work justifying a representation of RTPs as composition of unbounded operators, noting that these ideas work equally well for L^p modules. Finally, we prove some new results characterizing preclosedness of the map (ξ, η) \mapsto ξ\otimes_φη.
This mission is the statement-level formalization of Relative tensor products for modules over von Neumann algebras (arXiv:math/0301061v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Density of the intrinsic bounded-vector domain (§5, bounded-vector density, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
23 results of the paper are not stated yet, because the library lacks an interface they need:
The walled Brauer algebra organizes the linear operators that commute with a general linear group acting on a tensor product of vector spaces and their duals. Its diagrams mix crossings and contractions, with a wall distinguishing the two tensor factors. This makes it useful in mixed tensor representation theory, where the ordinary symmetric group algebra no longer records every commuting operator. Sartori and Stroppel compare this diagram algebra with a level-two cyclotomic quotient of a degenerate affine walled Brauer algebra. Their comparison identifies a concrete part of the larger algebra by an explicit change of generators Sartori–Stroppel, Theorem 6.2.
The paper's result is a proved theorem. This mission asks for a machine-checked proof of its algebraic statement. The source builds the cyclotomic quotient using parameters arising from parabolic category , but the target here is the resulting algebra isomorphism. The dimension comparison that the authors obtain through category is included as a separate milestone, in the exact numerical form used in their injectivity argument Sartori–Stroppel, Theorem 5.2, Corollary 5.8, and Lemma 5.9.
Fix . An orientation is a word of length containing exactly upward arrows and downward arrows. The walled Brauer algebra is a complex algebra with an idempotent for each orientation. At an adjacent pair of positions , equal arrows admit a crossing . Unequal arrows admit a changed-orientation crossing , an orientation-preserving contraction , and a changed-orientation contraction . The relations (Br1)–(Br6) specify orthogonal idempotents, sources and targets, quadratic and braid relations, and interactions among crossings and contractions Sartori–Stroppel, Definition 2.1.
The degenerate affine walled Brauer algebra adds commuting elements and their relations with the oriented generators. Its level-two cyclotomic quotient imposes a quadratic relation on in each first-arrow component Sartori–Stroppel, Definitions 2.5 and 2.8. Write this quotient as . It uses positive integers and an integer , with
The later follow the quadratic recurrence determined by the upward cyclotomic polynomial; they are fixed by these parameters. These are the paper's parameters (5.4), with values in Sartori–Stroppel, Definition 5.1 and Lemma 2.9.
For each position and orientation , let project away from the generalized eigenspace of with eigenvalue . The spectral truncation is , with . The intermediate products are and . This gives the corner algebra Sartori–Stroppel, Definition 5.6. The elements , polynomial square roots, and resulting images are defined by (6.1)–(6.4) Sartori–Stroppel, Definition 6.1.
The goal is the full form of the paper's isomorphism theorem:
Here , , and satisfy Assumption 5.5: and . The inequalities separate the relevant eigenvalues. The explicit condition is needed for Theorem 5.2 in the paper's dimension argument; Assumption 5.5 alone does not imply it Sartori–Stroppel, Assumption 5.5 and Theorem 5.2.
The milestone list records the finite-dimensional inverse and square-root result (Proposition 4.2), the inverse sandwich identity (Lemma 8.7), the changed contraction parameter (Lemma 8.4), the equal-orientation involution (Lemma 8.5), the Jucys–Murphy image identity (Lemma 6.6), and the dimension of the spectral corner (Corollary 5.8 with Lemma 5.9). The last two are stated in algebraic forms that avoid taking the sought map or category as extra hypotheses.
The theorem gives an explicit dictionary between diagram generators and operators in a cyclotomic quotient, including the change from the quotient's loop parameter to the source parameter Sartori–Stroppel, Remark 6.3. It also identifies the whole corner, rather than merely producing a homomorphism into it. This lets properties of the larger algebra be transported to the diagram algebra when their hypotheses are met. The paper discusses graded cellular and Koszul consequences, and an oriented-category extension, separately Sartori–Stroppel, Remarks 6.4–6.5.
A formal development must establish that the presentations do not collapse, that every required oriented relation survives the generator assignment, and that the image fills precisely . The milestone statements isolate several of the authors' central identities, while the final theorem retains injectivity and surjectivity. A proof would also create reusable infrastructure for quotient presentations with source and target idempotents and for inverses in idempotent corners.
The formulas for the images involve inverses and square roots after a spectral truncation, and the quotient need not be semisimple. Substituting a scalar directly into a formal power-series identity does not justify the key contraction identity in that setting; the authors explicitly point out this obstruction Sartori–Stroppel, Remark 6.3. The oriented relations also contain dotted symbols that stand for several local choices, so a single equation between global sums does not fully state every relation. Finally, proving that the map exists is only one part of the theorem: its image and kernel require separate control.
Lean represents both algebras as quotients of free complex algebras by the paper's generators and relations. An orientation is a Boolean sequence with exactly true entries; true denotes an upward arrow. Positions start at zero in Lean, so a paper index corresponds to Lean index . Relations involving dotted generators are imposed for every composable choice with the same source and target. Invalid orientation choices are zero. The affine quotient uses ; the source of the theorem uses . The recurrence fixes every rather than leaving later parameters free.
The , intermediate , and are defined from the polynomial spectral-idempotent characterization, rather than supplied as arbitrary hypotheses. An inverse of is selected by its two inverse equations in the corner . Square roots are not unique in the source, so each theorem holds for every family of polynomial square roots satisfying ; the factorized form is used. A vacuous hypothesis, a collapsed or under-related presentation, a freely chosen , or a merely linear map does not express this target. The conclusion requires multiplication, the specified generator values, injectivity, and range exactly .
The category construction and the paper's later applications are outside this mission. The needed reusable pieces are the finite-dimensional algebra lemma, oriented presentation machinery, polynomial spectral idempotents, and corner algebra operations. Contributions that strengthen the supporting algebraic library or close any of the stated milestones are within scope.
The Birman–Murakami–Wenzl (BMW) algebras were introduced by Birman and Wenzl and by Murakami to study the Kauffman link polynomial; they are deformations of the Brauer algebras and act as centralizer algebras of quantum groups of orthogonal and symplectic type on tensor powers of the natural module. Their cyclotomic generalization was introduced by Häring-Oldenburg (J. Pure Appl. Algebra 161 (2001)) as the BMW analogue of the Ariki–Koike algebras, the cyclotomic Hecke algebras of type . Representation theorists care about when such an algebra is semisimple: in the semisimple case its representation theory is governed by a combinatorial index set (multipartitions with extra data), and outside it one needs decomposition numbers.
For the Ariki–Koike algebra the answer is Ariki's criterion (J. Algebra 169 (1994)). For the ordinary BMW algebra () it is due to Rui and Si (J. Reine Angew. Math., [17] in the paper). Rui and Xu proved that the cyclotomic BMW algebra is free and cellular for odd under their u-admissibility conditions (arXiv:0801.0465), and Goodman and Hauschild Mosley (arXiv:math/0612064) and Yu (PhD thesis, Sydney, 2007) obtained freeness by other routes. Rui and Si (arXiv:0807.4149, 2008) extended cellularity to even and, by computing Gram determinants of cell modules, gave a semisimplicity criterion for all . That criterion is the goal of this mission.
Let be a field and positive integers. Fix non-zero with and the pairwise distinct, and a sign . Put if is odd and if is even, , ( odd), ( even), and
These are the u-admissible parameters of Assumption 2.2. The cyclotomic Birman–Wenzl algebra is the unital associative -algebra generated by () and () subject to the relations a)–k) of Definition 2.1: among them the Kauffman skein relation , the braid relations, , the skein relations between and , the unwrapping relations for all , the tangle and untwisting relations, , and the cyclotomic relation . The Ariki–Koike algebra is generated by with , the braid relations, , commuting and .
Write for " for ", and set
For and :
(a) if for some , or for some , then is not semisimple;
(b) if for all and no lies in , then
and for , is semisimple if and only if (a) ; (b) whenever , ; (c) for all ; (d) for all . For the goal states that semisimplicity implies (a)–(d).
The page states (b)(2) as an equivalence for all . The goal keeps only necessity at : Proposition 6.2 and Lemma 6.3 describe the same cell module of and list different exclusions ( against for odd ), and at contains neither.
The rank (Theorem 2.14); the corner identities (Lemma 3.1) and (Corollary 3.2), corrected at the two-strand boundary by requiring some ; Proposition 6.1, which says that is non-zero exactly when () and no lies in ; Proposition 6.5(b), non-semisimplicity when that determinant vanishes; and the reduction " not semisimple not semisimple" from the proof of Theorem 6.8.
The criterion gives a closed list of parameter values at which the cyclotomic BMW algebra fails to be semisimple, and so, by Graham–Lehrer theory, the parameters at which all cell modules are simple and pairwise non-isomorphic. Outside that list the algebra's simple modules, their dimensions and the decomposition of tensor-type modules are given by the combinatorics of up-down tableaux; inside it, the list says which Gram determinants vanish and where decomposition numbers begin. For it specializes to the semisimplicity criterion for BMW algebras, and its conditions (a)–(b) are Ariki's conditions for .
As far as is known, none of this is machine-checked: Mathlib has no BMW, Brauer, Ariki–Koike or Iwahori–Hecke algebras and no cellular algebras. The mission formalizes the statements of the paper on a presentation of by generators and relations; a solver must supply a basis (or at least a dimension count), the cellular structure and the Gram-determinant computations. The paper leaves several of its proofs to the reader ("by arguments in the proof of [19, 5.41]"), so the formal proofs would also close gaps in the published argument.
Non-semisimplicity in part (a) needs only one degenerate bilinear form on a non-zero cell module, but showing that the module is non-zero, or that does not collapse, already needs a lower bound on the dimension of a presented algebra, which no rewriting argument provides: the rank is proved in the literature through seminormal representations. Sufficiency in part (b) requires the Gram determinants of all cell modules , which the paper obtains by a recursion over up-down tableaux; vanishing of a single factor must be traced through branching and Morita-type functors between levels , and . Ariki's criterion for is itself an external input.
and are RingQuot quotients of FreeAlgebra F on finite generator types; indices are 0-based (the Lean T i is the paper's ), and is a separate generator tied to by relation a). The sign is the free parameter and are computed from , so the parameters are u-admissible by construction. The are pairwise distinct (Assumption 2.2(1) divides by ; the paper extends 2.2 to coincident through [19, 3.11]). "Semisimple" is Mathlib's IsSemisimpleRing. The condition is written as for , not through orderOf, which is for elements of infinite order. Relations d) and g) both use , which equals the paper's for these parameters; were they different, the presentation would collapse. The corrected corner milestones require or some in Lemma 3.1, and or some in Corollary 3.2. At , , , , and , every vanishes, exposing the missing condition. is expressed as the Hankel determinant of the , and is the subalgebra generated by the first generators.
A presentation that collapses to the zero algebra would make the goal false in part (a) but trivially true elsewhere; the rank milestone rules this out. Replacing semisimplicity by non-vanishing of Gram determinants would turn the goal into a different theorem and is not acceptable.
A complete development needs a basis theorem for , cellular algebras and Graham–Lehrer's semisimplicity criterion, the Ariki–Koike algebra and Ariki's criterion, and Gram-determinant computations. The cellular-algebra layer and the Ariki–Koike algebra are reusable beyond this mission; contributions of any of these, or of the milestones on their own, are welcome.
Topological quantum computing represents a gate operation by moving anyons around one another. A compiler must turn a requested single-qubit unitary into a finite braid or gate word, with enough accuracy and a length that grows slowly as the error tolerance shrinks. For Fibonacci anyons, the matrices generated by the standard elementary braids have algebraic entries, which makes exact arithmetic available during compilation. Kliuchnikov, Bocharov and Svore gave an approximation algorithm whose output length scales logarithmically with inverse precision, the asymptotic scale required by their worst-case lower bound. Their method joins a sample from a cyclotomic integer ring to an exact-synthesis routine Kliuchnikov–Bocharov–Svore, 2013.
The result concerns what every successful run outputs. Its additional claim about average runtime depends on a number-theoretic conjecture and is separate from the output-quality theorem. Keeping these assertions distinct matters: a short accurate circuit conditional on finding a solvable norm equation does not imply that a sample can be found quickly.
Fix the tenth root of unity , , and . The ring contains expressions with integer coefficients. Arithmetic is reduced using and . The automorphism sends to . The Gauss complexity of is . This quantity controls the number of steps in exact synthesis §III, pp. 3–5.
An exact unitary is the paper's two-by-two complex matrix built from , an integer phase , and the normalization . Its gates are , , and the scalar phase . A circuit is a finite sequence of these gates, evaluated by matrix multiplication in sequence order. Its length counts and gates; the scalar phase has no braid cost in the paper's convention.
The target rotation is . Approximation uses the phase-invariant distance
Figure 15 approximates a real input by through Fibonacci numbers. Figure 13 combines two such approximations into a cyclotomic integer in a specified geometric region. Figure 12 scales and rotates , asks for a solution of a norm equation to obtain , and runs Figure 4's exact-synthesis loop on the resulting exact unitary Figures 4, 12, 13 and 15.
For every angle , every precision , every allowed sample index, and every norm-equation solution used by Figure 12, its returned circuit satisfies
for one positive absolute constant . The statement is about all possible outputs, including all allowed tie and solution choices. It does not assert that the norm equation has a solution for every input. This is the first sentence of Theorem 21, p. 14.
The milestone list records Proposition 4's integer-valued complexity gap, Lemma 5's decreasing step and asymptotic ratio bound, Theorem 6's exact synthesis and length estimates, the §V distance identity, Lemma 18's real-approximation bounds, and Lemma 19's count of equiprobable samples, their membership in the parallelogram of Figure 14, and the corrected complexity bound. They describe the interfaces needed to connect algebraic synthesis to geometric approximation. The source text is preserved in each milestone even where the formal statement makes a documented correction.
The target gives a finite circuit whose accuracy is specified by a matrix distance rather than by a coordinate surrogate. Its length bound is uniform in the rotation angle, the sample choice, and the norm-equation solution. Consequently, once a suitable sample and solution are supplied, exact synthesis cannot silently add a superlogarithmic number of gates. The paper's conditional runtime sentence concerns how quickly such a sample is obtained and remains outside this theorem Theorem 21, p. 14.
A machine-checked development would produce reusable coordinate arithmetic for , a verified implementation of the exact synthesis loop, Fibonacci-based real approximation, and a phase-invariant matrix-distance calculation. These are useful beyond this single target wherever the Fibonacci-anyon gate set is used. The present files contain compiled statements and definitions; the theorem proofs remain open. Contributions proving the stated milestones, establishing ring and matrix identities, and checking the sampler's geometric inequalities are welcome.
The obvious idea of rounding the target phase does not by itself give an exactly implementable unitary: the upper-left entry must be extendable to a matrix satisfying . The sampler must keep in a narrow region while leaving a norm equation for that can be solved. Even after that, a short exact circuit requires a decrease in at each synthesis step. The length bound cannot follow merely from the fact that some finite circuit exists. These are the separate mathematical constraints reflected by the milestones §§III–V, pp. 3–14.
Lean represents as four integer coordinates. Its multiplication uses the paper's cyclotomic relations, and its conjugation and bullet automorphism are coordinate maps. Matrices have type . The synthesis output is a list of , , and gates. The first minimizing exponent in breaks ties in Figure 4; the angle-reduction integer may be any valid one. Rounding in APPROX-REAL uses Lean's nearest-integer operation.
The formalization corrects two printed algorithm signs: Figure 12's final matrix is instead of , and Figure 13's uses a plus sign before the sine term. The first is required by the displayed distance formula; the second by the geometry of the sampled region. Lemma 18 is restricted to , since its bound fails at . Lemma 19's Gauss-complexity bound is , because is already of order ; its formal statement covers every with , and renders "each output occurs with the same probability" as equal fibre sizes of the explicit sample index. These corrections and scope choices are documented next to the affected items pp. 11–14.
Random sampling is represented by an explicit index in its allowed range. SOLVE-NORM-EQUATION is represented by any satisfying its output equation; EASY-SOLVABLE is omitted from the output guarantee because it filters samples without changing the claimed quality of one successful output. The goal's constant precedes all angles, precisions, samples, and solutions. The output must be the circuit produced by the defined Figure 4 loop applied to Figure 12's data; choosing an arbitrary short circuit or making the norm-equation hypothesis impossible would not state the paper's result.
Let be the natural representation of and its dual. The walled Brauer algebra describes the endomorphisms of mixed tensor space that commute with , through mixed Schur–Weyl duality. It was introduced in this role independently by Turaev, Koike and Benkart–Chakrabarti–Halverson–Leduc–Lee–Stroomer around 1989–1994. It is also a diagram algebra in its own right, defined for every parameter in the ground field. Its representation theory controls the decomposition of mixed tensor space, and it serves as a test case for the cellular and "tower of recollement" methods used for the Brauer and partition algebras.
Cox, De Visscher, Doty and Martin (arXiv:0709.0851, 2007) determine the blocks of in characteristic zero. They also classify the semisimple walled Brauer algebras and give a linkage principle in positive characteristic. Their characteristic-zero answer has the shape familiar from algebraic Lie theory: blocks are orbits of a Weyl group, , under a dot action shifted by a vector . The analogous result for the ordinary Brauer algebra, with the Weyl group of type , is due to Cox, De Visscher and Martin (arXiv:math/0601387, 2009).
Fix , an algebraically closed field and . A Brauer diagram on strands pairs up nodes, northern and southern. Lines joining the two rows are propagating lines; the others are arcs. Put a wall after the first nodes of each row. A diagram is walled if no propagating line crosses the wall and every arc does. Two diagrams are multiplied by stacking the first above the second. Each closed loop formed in the middle row is removed and contributes a factor . The walled Brauer algebra is the -span of the walled diagrams with this product. The permutation diagrams span the group algebra of .
The algebra is cellular. Its cell modules are indexed by bipartitions with and , for . Here is the number of northern arcs. In characteristic zero the simple modules , the heads of the cell modules, are indexed by the same set. The one exception is , which is excluded when and . At , the algebra is and its unique simple has the empty bipartition as label. Two simple modules lie in the same block when no central idempotent of separates them.
A box in row and column of a Young diagram has content . Two bipartitions are -balanced when the boxes of can be paired with those of , and the boxes of with those of , so that the contents in each pair sum to .
For , the weight lattice is , with coordinates indexed by . Put
The group permutes the coordinates and acts by the dot action . A bipartition is sent to the weight .
For of characteristic , , and labels of simple -modules,
For every in characteristic , two labels are in the same block if and only if they are -balanced, and each block contains a unique minimal weight.
The milestones, in proof order, are the following.
The goal reduces the block structure of to a combinatorial test. Two weights are in the same block exactly when their -shifted vectors are permutations of each other, a check that takes linear time. Within a block there is a unique minimal weight. The Weyl-group description is the starting point for the paper's positive-characteristic linkage principle, in which the affine Weyl group takes the place of . It also places the walled Brauer algebra alongside the Brauer algebra and the algebraic groups as an algebra whose characteristic-zero blocks are governed by a reflection group.
The result has been proved since 2007. As far as is known, no part of it has been machine-checked. This mission produces three things.
The obvious first idea is to treat the walled Brauer algebra through mixed Schur–Weyl duality, as a centraliser algebra. That gives only a quotient of when is a small integer, and nothing at all when is not a natural number, so it cannot reach the full statement. The obstruction is the non-semisimple regime (, ), where cell modules have nontrivial composition factors.
The necessary condition is a scalar computation, obtained by evaluating a central-like element on cell modules. Sufficiency is the hard direction. It needs explicit nonzero homomorphisms between cell modules that differ by a removable strip of boxes, built from the two-box homomorphisms of Theorem 6.2 by an induction using restriction and induction along the tower . The final step, matching balance with dot orbits, is a combinatorial argument on edges of skew diagrams in which the shift by must be tracked exactly.
YoungDiagram, with 0-based cells; contents are unchanged by the shift. Nodes are Fin (r+s). The weight lattice is Fin r ⊕ Fin s → ℤ, where Sum.inl i is the paper's coordinate and Sum.inr j is coordinate . is Equiv.Perm (Fin r ⊕ Fin s).Two corrections to the printed text are adopted. Lemma 8.1 is stated "for all ", and the reflection formula on p. 31 is read as , the transposition of two coordinates. The label exception in Theorem 2.7(iii) is applied only when ; its literal wording would incorrectly leave without a simple module.
A trivializing formalization would replace the block relation by a relation defined through contents or orbits, or would replace the algebra by a centraliser algebra or by . Both are excluded: the block relation is the algebra's own central-idempotent relation, and the algebra is the diagram algebra itself.
Contributions are welcome at every layer. Useful general infrastructure includes associativity of diagram composition, Young symmetrizers and Specht modules over a field of characteristic , and the Jucys–Murphy content formula. Proofs of the combinatorial Section 8 results and of the cellular structure of are also needed.
Sending classical messages through a quantum device requires choosing input states that remain distinguishable after noise. The one-shot classical capacity measures the best information rate when each channel use is signaled with a separate input state. For many channels the optimization is difficult because it ranges over all ensembles of quantum states. Fermionic systems provide a finite-dimensional setting in which the noise has a direct description on elementary operators, but the optimal signaling states still need not be obvious. Bravyi's 2005 paper isolates a family of fermionic product channels, computes the best rate from Gaussian input states for any number of qubits, and proves that this restricted rate is the full one-shot rate for one or two qubits.
The system has qubits, with computational basis indexed by bit strings . The Jordan–Wigner Majorana operators are tensor products of Pauli matrices: has on qubits before , on qubit , and identity afterwards; replaces with . Their ordered monomials , , form a basis of all operators on the qubits. The paper gives these operators and their monomials in Eq. (3).
A fermionic product channel is determined by attenuation coefficients . On each monomial it acts by , and linearity defines it on every operator. A state is a positive semidefinite matrix of trace one. For a finite ensemble of output states , with nonnegative weights summing to one, its Holevo quantity in bits is
The supremum of over all finite ensembles of outputs of is . A Gaussian state has the specific form of Definition 1: , each , and for Hermitian quadratic and linear combinations of Majorana operators. Requiring Gaussian input states gives . Setting gives an even Gaussian state. These are separate classes; the even class supplies an intermediate entropy minimum. Definition 1 and Eq. (13) are on page 4.
Write for the coefficients in decreasing order, and let . The main formula, Theorem 1 and Eq. (6), is
It holds for every and every unsorted . The milestones identify the covariance and Gaussian-preservation facts, the exact even and general Gaussian minimum-output entropies, and an ensemble attaining the capacity.
The second clause of Theorem 1 states
Thus restricting the input ensemble to Gaussian states loses no one-shot capacity in these dimensions. The paper does not prove this equality for arbitrary .
The formula replaces an optimization over arbitrary finite Gaussian ensembles with binary entropies of sorted attenuation coefficients. In the one- and two-qubit cases it also settles the unrestricted one-shot optimization for this channel family. The intermediate result relates signaling directly to minimum output entropy; the even-Gaussian and Gaussian minima make the distinction between the two state classes explicit. These relationships are established in Sections II–IV of the paper.
The mathematical results are proved in the 2005 paper. This mission asks for machine-checked proofs of their exact finite-dimensional statements. The definitions of bit-valued von Neumann entropy, finite output ensembles, ordered Majorana monomials, Gaussian-state predicates, and covariance matrices can support later work on fermionic channels. The submitted goal and milestones are presently proof obligations rather than claims of existing Lean proofs.
The channel is simple on each Majorana monomial, but the entropy of a general output state is not determined by its one- and two-point correlations. Even within the Gaussian class, optimizing only the even Gaussian states gives a different formula from optimizing all Gaussian states: linear Majorana terms change the optimum. A direct search over density matrices therefore does not expose the closed expression in Theorem 1. For the unrestricted two-qubit clause, one must also relate arbitrary states to the Gaussian class; the paper invokes a three-qubit parity result for that step. The distinctions and parity result appear in Sections III–IV.
Lean represents qubit basis vectors by Fin n → Fin 2 and operators by complex matrices on that finite type. Majorana indices start at zero in Lean, so the paper's correspond to consecutive indices . The Jordan–Wigner tensor factor at coordinate acts on qubit ; the monomial product follows increasing Majorana index. The channel is defined on all matrices by the trace-orthogonal monomial expansion of Eq. (4), not merely on covariance matrices. Attenuations may equal zero or one. Entropies use logarithms to base two, with .
Every capacity uses a real supremum over all finite normalized ensembles, with arbitrary ensemble size. The inputs are density matrices, and their channel outputs must be density matrices. The Gaussian capacity requires every input to satisfy Definition 1; Lemma 2 ensures these outputs are Gaussian too. The minimum-output quantities are real infima over their stated input classes, and the corresponding milestone theorems assert attainment. For the actual channels the relevant sets are nonempty and bounded: the maximally mixed state supplies an output state, while every Holevo quantity lies between zero and . This representation rules out restricting the Gaussian ensemble to the displayed optimizing family, assuming the goal's coefficients are initially sorted, or replacing bit entropy with natural-log entropy.
The development needs finite-matrix functional calculus, positivity, matrix exponentials, permutation and singular-value reasoning, and finite ensemble entropy bounds. Contributions to those reusable layers and to the paper's covariance, Gaussian-preservation, and minimum-output results are within scope. Lemma 3 is stated in its even-Gaussian form, which its proof establishes; the displayed lemma says only “Gaussian.”
In many retail settings, recorded inventory is not reliable. Shrinkage, misplacement and recording errors mean the shelf count is unknown, but a stock-out is visible. Bai, Chen and Stolyar (SSRN 3865728; Operations Research Technical Note, 2022, doi:10.1287/opre.2022.2305) study the extreme version of this: a single-item lost-sales system whose inventory level is observed only when it is zero.
For the discounted cost criterion, Bensoussan, Çakanyıldırım and Sethi (2007) showed that optimal feedback policies exist for this model. Whether a stationary policy minimizes the long-run average cost was left open. Average-cost problems for partially observable systems are harder because of the vanishing-discount argument they rely on. It needs a uniform bound on relative value functions, and on a space of beliefs such bounds are not automatic. The paper settles the question for this model.
In each period the inventory level is . The decision maker orders , with . The order arrives at once and ordering costs nothing. Then an i.i.d. demand is realized, and unmet demand is lost:
The period cost is the holding and lost-sales cost , with . Its expectation given is . The demand is nonnegative, has a density with distribution function , a finite positive mean and a positive variance.
Only the signal is observed. The decision maker therefore acts on a belief , the conditional distribution of the current inventory level. After ordering from belief , the next belief is if . If it is the posterior , the law of (with ) conditioned on being positive. The probability of is .
This yields a completely observable MDP (COMDP). Its states are beliefs with finite second moment, (Assumption 1), taken with the topology of weak convergence. Its cost is and its transition kernel is
For a policy , is its -discounted cost and its average cost per period (a ). The optima are and over all history-dependent randomized policies. Write , and .
There are a sequence and a measurable stationary policy that is average-cost optimal among all policies. With finite and
finite, satisfies the average cost optimality inequality (ACOI)
Theorem 1 gives existence of a stationary average-cost optimal policy for a partially observed inventory system with lost sales. In that setting the belief space is infinite-dimensional and the state is never fully revealed except at zero. The ACOI also supplies the structure needed to study such a policy. The paper leaves open whether the ACOE (the equality form) holds.
The reduction is reusable. Feinberg's general conditions, (W*) and (B), apply to many belief MDPs. The problem-specific work is the uniform bound B(ii), obtained here through a coupling estimate (Lemma 4) for lost-sales paths under arbitrary, even anticipating, controls.
The paper proves Theorem 1, Theorem 2, Lemma 3 and Lemma 4. Lemma 2 and the (W*) claim are cited from Feinberg (2016) and Feinberg, Kasyanov and Zgurovsky (2016) and are not proved in the paper. As far as is known, none of these results has a machine-checked proof; the general vanishing-discount theory for MDPs on Borel spaces is itself not yet formalized.
The obvious route to B(ii) compares with by running from the policy that is optimal from . This fails: a policy is a function of the belief, and the beliefs generated from and from differ, so the same policy produces different orders. The paper goes the other way and bounds above by . This needs a policy started from that mimics 's orders while the two systems have not yet merged. The constant must be uniform in close to , so per-period estimates that grow like are useless.
The (W*) claim has its own difficulty. The observation kernel is discontinuous at , so the known criterion for weak continuity of belief kernels, which needs observations continuous in total variation, does not apply. Continuity has to come from the density of .
The Lean development lives in the namespace PartialLostSales.ACOI. It reuses the published FeinbergLiang.ACOE layer: MDP, history-dependent randomized Policy, vDisc, vOpt, avgCost, wOpt, IsAvgOptimal, uRel, uTilde, IsDiscountSeq, KInfCompact and AssumptionWStar. All costs and values lie in . Its conventions are:
ℝ≥0 with the Euclidean topology, and actions in the subtype .ProbabilityMeasure ℝ≥0 with finite second moment. They carry the weak topology and Mathlib's (Giry) σ-algebra, which is the Borel σ-algebra here.MDP satisfying IsCOMDP, which pins the lower bound , the cost and the kernel pointwise; milestone 1 shows one exists.The paper states that COMDP and POMDP policies correspond with equal values (Feinberg, Kasyanov and Zgurovsky 2016). The goal is stated in the COMDP, and that equivalence is not formalized.
Added hypotheses. Demand is nonnegative. Lemma 4's control rule is measurable, but adaptedness is not required.
Totality devices. The posterior when , and the map of a posterior back into the belief subtype, have else branches that are never used.
Indexing. Lemma 4 indexes periods from with weight . Its costs are realized costs, since controls may anticipate.
Trivializing formalizations. Several encodings would make statements trivial, and none is used. The kernel and cost of the MDP are never left free. The ACOI carries explicit finiteness of and , so it is not an inequality that holds when . Optimality is over all policies, not only stationary ones. The ACOI uses , not or a free constant.
Not formalized.
FKZAvg.WStar.theorem_2 (v).Contributions of general value include Feinberg's average-cost theory on Borel spaces (Lemma 2) and weak continuity of belief kernels with discontinuous observations.
Many infinite-dimensional Lie groups arising in geometry and physics — loop groups, gauge groups, groups of diffeomorphisms and of volume-preserving diffeomorphisms — have interesting central and abelian extensions, and these extensions are usually found first at the level of Lie algebras, as continuous 2-cocycles. Whether such a Lie algebra extension comes from a Lie group extension is a genuine question: in infinite dimensions there is no Lie's third theorem, and topological obstructions from and appear. K.-H. Neeb's paper [Ne04] answers it for abelian extensions of a connected Lie group by an arbitrary smooth -module whose identity component is a quotient of a vector space by a discrete subgroup. It generalises the central case treated in [Ne02] and the classical finite-dimensional theory.
Timeline:
Let be a connected real Lie group modelled on a Banach space, with Lie algebra , the bracket being that of left-invariant vector fields. A smooth -module is an abelian Lie group with a smooth action by group automorphisms. Throughout, its identity component is : there is a smooth homomorphism from a Banach space which is a local diffeomorphism onto with discrete kernel . The action differentiates to an action of on and an action of on ; write .
A continuous 2-cocycle is an alternating continuous bilinear map satisfying the Chevalley–Eilenberg cocycle identity; it defines the Lie algebra on with bracket
It integrates if there is a Lie group extension — a principal -bundle whose conjugation action on is the given one — whose Lie algebra is equivalent to .
Three invariants enter:
For , the extension integrates to with connected if and only if
If is connected, the second condition reads .
The criterion turns the existence of a Lie group extension, a global geometric object, into two homomorphisms that can be computed from and the topology of : periods on and fluxes on . The paper applies it to diffeomorphism groups, to acting on spaces of -densities, and to Lichnerowicz cocycles on groups of volume-preserving diffeomorphisms; it also underlies the exact sequence relating to (Theorem VII.2).
The results are proved in the paper; none of them, nor the objects they are stated in (period group, flux, characteristic homomorphism, abelian Lie group extensions), has been formalized before. Formalizing them produces the first machine-checked integrability criterion for Lie algebra extensions, together with a reusable layer for abelian extensions of Banach–Lie groups on top of Mathlib's LieGroup and GroupLieAlgebra.
The necessity of both conditions follows from the long exact homotopy sequence of the principal bundle , once the connecting maps are identified with on and with the flux on ; each identification is a Stokes-theorem computation on a group that is not given in coordinates. Sufficiency is harder. The obvious approach, building directly from a local group cocycle, fails when is not simply connected: the cocycle on the universal cover does not descend, and the obstruction is exactly the flux. One has to construct the extension over , show that the lifted splits centrally, take the quotient, and then recognise the resulting kernel as by comparing characteristic homomorphisms. Mathlib has no long exact homotopy sequence of a bundle, no integration of differential forms on manifolds, and no construction of Lie groups from local data.
All Lie groups are real and modelled on Banach spaces, with smooth meaning ((⊤ : ℕ∞), not analytic); this is a special case of the paper's sequentially complete locally convex spaces over or . All types are in Type. Conventions committed to:
Extension) is a Lie group charted on with smooth , surjective smooth , , a smooth local trivialisation near , the prescribed conjugation action, and a topological linear isomorphism compatible with , and the brackets."Integrates" is never a restatement of the two conditions: it asserts the existence of such an extension, and dropping the bracket clause, the conjugation clause or the local trivialisation would make it a different statement.
Lemma III.7 is stated with an isomorphism; with a mere homomorphism, as printed, it is false. A complete development needs path lifting and the homotopy sequence for principal bundles, Stokes' theorem for maps , the universal covering group of a Banach–Lie group, and quotients of Lie groups by discrete central subgroups; all of this is reusable beyond this mission. Contributions of any of these pieces, and of further results of the paper (Proposition IV.5, Corollaries VI.5 and VI.6, Theorem VII.2), are welcome.
Arrival streams to service systems (call centres, hospitals, web servers) are rarely stationary: their rate changes with the time of day, with external events, or with the state of a self-exciting mechanism. Two asymptotic regimes are standard. When the rate varies slowly relative to service times, the system is approximated by a sequence of stationary systems, one per rate level (the pointwise stationary approximation). When the rate varies rapidly, the opposite simplification is expected: the fluctuations average out, and the arrival stream looks like a homogeneous Poisson process with the long-run average rate.
Zheng, Honnappa and Glynn (arXiv:1807.06805v1, published as a Technical Note in Operations Research, 2021) make the rapid regime precise for a general class of arrival processes. The arrival process need not be a doubly stochastic Poisson process; a Hawkes process is allowed. Their Theorem 1 says that, after a time acceleration combined with an independent thinning, the arrival process converges in law on path space to a Poisson process. The remaining results of the paper (total-variation behaviour, first-order corrections in the Markov-modulated case, the infinite-server queue) refine this limit and are not part of this mission.
A probability space carries a filtration and an arrival counting process : , is integer valued, non-decreasing and right-continuous, and it is simple, meaning that it increases by exactly one at each arrival epoch. has an -compensator : a predictable process with and non-decreasing right-continuous paths such that
is an -martingale. When , the process is the stochastic intensity of .
Assumption 1. There is a deterministic with as .
For , let be iid Bernoulli() random variables independent of . The thinned, accelerated process and its scaled compensator are
runs at speed and keeps each arrival independently with probability , so the mean rate stays of order while the intensity fluctuates on the time scale . The σ-algebra is generated by and the marks of the arrivals that have occurred.
is the space of right-continuous real paths on with left limits, with the Skorokhod topology.
Under Assumption 1,
where is a Poisson process with constant intensity . The goal fixes no rate of convergence and no constants; it asserts convergence in law on path space and the identity of the limit.
Theorem 1 justifies replacing a rapidly fluctuating arrival stream by a homogeneous Poisson stream of rate in the analysis of the system it feeds. If collects the other primitives of a queue (service and patience times) and is independent of , then , and any performance functional continuous at converges to its value under Poisson input (p. 4). The second half of the paper shows that this approximation holds in law on path space but not in total variation, which is why the statement is the right form of the result.
The result is proved on paper, in two lines that cite a general limit theorem. No part of it has been machine-checked. This mission produces the first formal statement and proof of a Poisson limit for point processes driven by their compensators, the cited theorem (milestone 4), which applies well beyond this paper: superposition limits, rare-event thinning, and Hawkes-process limits all reduce to it. Milestone 2 is a reusable thinning lemma for compensators.
Milestones 1 and 3 are elementary: the first is pathwise, the second is a time change in Assumption 1. Milestone 2 is a conditional-expectation computation with a random number of summands, and needs the marks to be independent of all the information in , not only of (see the scope section).
The difficulty is milestone 4. Convergence of the compensators at each fixed time identifies the limit only through a martingale characterisation of the Poisson process (Watanabe's theorem). Path-space convergence additionally needs tightness of the counting processes. Finite-dimensional convergence of is not enough: the statement is about laws on , and the step from fixed times to path space is part of the work. The goal also does not follow from milestones 1 to 4 verbatim: the goal assumes the marks independent of only and does not assume , while milestone 2 needs both stronger hypotheses.
All declarations live in the namespace RapidRatePoisson.WeakConv. Conventions:
ℝ≥0. Every statement involving assumes . Processes are ℝ≥0 → Ω → ℝ. Marks are ℕ → Ω → Bool, indexed from 1, and markSeq β is the random sequence .MartingaleHT.InfiniteServer.IsUnitJumpCountingPath, required of every path.IsCompensator: Mathlib's IsStronglyPredictable and Martingale with respect to a Filtration ℝ≥0). This is the standard meaning of the term. The page's paraphrase without predictability makes Theorem 1 false: for Poisson(1) and , with an independent increasing pure-jump process of mean with finitely many jumps, is a martingale and , but is Poisson(1) for every .TendstoInMeasure).PuhaWardFluid.Limit.ConvInDist with on real paths, which is equivalent to weak convergence of the laws. "As " is stated along every sequence in , which is equivalent by metrizability. The limit ranges over every process satisfying the published RankBasedSDI.LoadBalancing.IsPoissonProcess with rate on any probability space.markSeq (β ε) from the whole path of , for each separately.The trivialising readings are ruled out. The goal is convergence in with , not finite-dimensional or one-time-marginal convergence. The limit carries the Poisson predicate and is not an arbitrary process. The compensator is predictable, not the literal "increasing process making a martingale". A sorry-free check (not uploaded) shows the goal's hypotheses can be met together: the deterministic instance with the trivial filtration, , and uniform marks on .
Needed infrastructure: martingale characterisation of the Poisson process, tightness criteria for counting processes, and conditional expectation over random index sets. All of it is reusable beyond this mission. Contributions to milestone 4 and its supporting lemmas are especially 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.9780898718508In a fork-join network every arriving job is split into several tasks that are processed in parallel and then joined; the job leaves only when its last task is done. Such networks model parallel computing (map-reduce jobs split across machines), assembly and order fulfilment (an order waits for every component), and health care (a patient waits for several test results). When different job types compete for the same parallel resources, the order in which a shared resource serves the types determines how long jobs wait for their slowest task, and therefore how many jobs are in the system.
Optimal control of such networks is hard even with exponential distributions, because the state is the vector of all buffer contents and the dimension grows with the number of types and servers. E. Özkan (arXiv:2002.01496, Mathematics of Operations Research 2022) studies the problem in the conventional heavy-traffic diffusion regime, in which every shared server is critically loaded, and proposes a scheduling policy that tracks the solution of a linear program. The main result is that the policy is asymptotically optimal for the probability that the total holding cost exceeds any threshold. The approach generalizes the network of Figure 2 with a single shared server, controlled by Özkan and Ward (Mathematics of Operations Research 44, 2019), and follows the asymptotic-optimality programme of Bell and Williams (doi:10.1214/aoap/1015345343).
There are job types , shared servers and a set of dedicated servers. Shared server processes the types , ; type is processed by the shared servers and by its own dedicated servers (possibly none). A type- job forks into one task per server in . Inter-arrival times of type are with i.i.d., mean and variance ; service times are i.i.d. with means , and squared coefficients of variation , ; all sequences are independent and have exponential moments (Assumption 1).
Let and be the numbers of tasks waiting in front of dedicated server and of shared server (type ). The number of type- jobs in the system is , and the cost rate is with . The control is how each shared server divides its effort among its buffers: an admissible policy is head-of-line within each buffer and work-conserving, and it may even anticipate the future (Definition 1).
A sequence of systems indexed by has arrival rates with every shared server in heavy traffic, and , while each dedicated server is either in heavy traffic, (the set ), or in light traffic, (Assumption 2). All systems start empty. Diffusion scaling is , and similarly and the workload with .
For the LP (18) minimizes subject to (), and ; its value is . The QP (19) picks the LP optimum of least Euclidean norm. The proposed policy (Definition 2) works in review periods: at the start of a period server computes the QP-selected target for the current state. If no buffer exceeds , the server serves one job. Otherwise it serves the excess jobs while idling one type that maximizes , until no excess is left.
With the limit of Proposition 2 — a semimartingale reflected Brownian motion (SRBM) with data in the heavy-traffic coordinates and for light-traffic dedicated servers — for every run of the proposed policy, every and every ,
Theorem 2, together with the lower bound of Theorem 1 (which holds for every admissible policy and is not part of this mission), shows that the proposed policy is asymptotically optimal for the objective simultaneously for all and . The paper then derives asymptotic optimality for the discounted cost (Theorem 3). The policy needs only the solution of an LP and a QP at review epochs, so it scales to large networks where dynamic programming does not.
The results are proved in the paper, with the exception of Proposition 2, whose proof is omitted as following "from standard methodology"; its milestone is therefore a statement the paper asserts. None of the results is formalized. A formal development would produce reusable pieces: Lipschitz sensitivity of LP values and of minimum-norm LP solutions, Chernoff-type bounds for maxima of i.i.d. partial sums, and a precise model of a fork-join network under head-of-line, work-conserving control.
The cost is not a function of the workloads alone, so the usual heavy-traffic argument (diffusion limit of the workload plus a continuous mapping) only gives a lower bound. Achieving it requires state-space collapse for the cost: the buffers in front of each shared server must stay within of the LP-optimal split at all times up to , under a policy whose review periods are random and whose target moves with the state. The proof controls up to review periods per server at once, which needs tail bounds of order uniformly over periods. The light-traffic behaviour of a shared server that idles one type during a Step-3 period depends on heavy traffic of the full server. The natural shortcut — proving tightness of the scaled buffers directly — fails, because the LP may have many optimal solutions; the QP selection and its Lipschitz property (Lemma 1 Part 3) are what make the target trackable.
Fin J, Fin I, Fin K (0-based); dedicated servers carry an owner map, and the standing structure (, , , positive rates) is part of the Network definition. Sums over and maxima over range over incident pairs only.Reiman84.QueueLength.IsDriftedBM and IsReflectionPair; since is a positive diagonal matrix it is absorbed into the regulator. Weak convergence in Proposition 2 is the published PuhaWardFluid.Limit.ConvInDist.Whether 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.
A principal who cannot observe workers' effort must use payments tied to an observable result. In a team, each worker's effort affects the same result, so an individual bonus must support both workers' incentives. The principal may also choose who controls the production method. Giving that choice to a worker changes the actions the workers can take after a deviation and can change the wage bill needed to sustain cooperation. Upton's working paper studies this interaction in a repeated two-agent team. Its Proposition 7 identifies environments where assigning the method choice to one worker reduces the principal's wage cost even when the workers cannot profitably collude in another equilibrium.
The result is a statement about an organisational choice, not just a comparison of two formulas. A lower bonus under delegation matters only if it actually sustains the intended repeated-game outcome, if centralisation can sustain that same outcome, and if the delegated arrangement survives the agents' opportunity to coordinate. Those requirements are represented explicitly in this mission.
A principal employs agents A and B in an indefinitely repeated project. In each period, each agent either works, paying an effort cost , or shirks, paying none. There are two possible states, and , occurring independently over time with probabilities and . There are two production methods, and ; is correct in state . With workers, project success has probability under the correct method and under the incorrect one. The paper's Assumption 1 orders these probabilities, gives the correct method an advantage, and requires complementarity of effort (§2, pp. 7–8).
Each agent also pays an adoption cost when method is used. Write . The method labels are chosen so , while may have either sign. The principal offers nonnegative, stationary success bonuses and pays nothing after failure. Under centralisation the principal chooses the correct method; under delegation A chooses the method while both agents choose effort (§2–§3).
The target outcome is both agents working with the correct method in every state. Its implementation is evaluated in the equilibrium class used by the paper: after any deviation, agents switch to a statewise stage-game Nash equilibrium as a grim-trigger punishment. A possibly mixed punishment is allowed. Current payoffs and expected continuation values enter the one-shot deviation constraints with weights and , where is the common discount factor (§4, pp. 12–18).
The main target is Proposition 7, p. 29. Let be the least equal centralised success bonus and the paper's delegated bonuses. The proposition asserts that some adoption-cost differences satisfy
such that delegation implements the desired outcome and costs strictly less than every centralised bonus pair that implements it:
Centralisation must itself implement the desired outcome at , so this universal comparison has content. The resulting delegated outcome must also be collusion-proof: no feasible state-dependent joint outcome lottery can give both agents at least their intended expected payoff and one agent strictly more. This is the strong form established by the paper's surplus argument; it implies its footnote 30 criterion against alternative subgame-perfect equilibria.
The milestone path records the centralised minimum in equation (9), the ordering of delegation thresholds, delegated implementation in Proposition 3, the wage-cost equivalence in equations (73)–(74), the eight surplus constraints (59)–(66), Claim 1's reduction to three constraints, the threshold comparisons (75)–(77), and the link from maximal joint surplus to collusion-proofness. The formulas for the thresholds and bonuses are definitions shared by all these statements.
The theorem gives a nonempty parameter region in which control of a production method has an incentive value that exceeds the principal's best centralised wage arrangement. It also certifies that the saving does not rely on an equilibrium the workers would replace with a Pareto-better arrangement. This is the paper's organisational comparison, with its equilibrium and collusion qualifications carried together (Proposition 7 and its proof, pp. 29, 38–39).
Upton proved the mathematical result in the cited paper. The Lean files in this mission compile as definitions and open theorem statements; they do not yet contain machine-checked proofs of Proposition 7 or its milestones. A completed development would certify the finite stage-game calculations, the repeated-game incentive constraints, the threshold algebra, and the surplus comparison. The finite-game layer and the mixed Nash formulation can be reused in other repeated team-production models.
The direct wage comparison is only one part of the result. Delegation changes A's available actions: A can choose either method as well as effort, whereas centralisation fixes the correct method. It also changes the feasible punishment equilibria and therefore the continuation value after a deviation. A calculation that compares with without checking these equilibrium conditions would leave the organisational claim unproved. Collusion adds a separate comparison across all feasible joint outcomes in both states. The agents can prefer different methods because their adoption-cost differences have different signs, so checking only the two work/shirk outcomes under the correct method misses possible gains from choosing the wrong method (§4 and §7).
Lean uses Fin 2 for states and methods: index means or , and index means or . Effort is Boolean. A separate finite-game definition carries feasible actions, real payoffs, independent mixed strategies and Nash inequalities. The paper-specific model builds the centralised and delegated stage games from the success probabilities, bonuses, effort costs and adoption costs. All payoffs and thresholds are real. The desired-path and punishment values are expected per-period values normalised by , as in §4. The principal's wage cost for the desired path is .
The standing assumptions explicitly include , , and . These state the probability domain and exclude the single-state boundary at ; together with Assumption 1 they keep all success probabilities in and the displayed denominators positive. Proposition 3 has a further disclosed guard : its printed unrestricted condition can make equation (23) negative, contrary to the paper's limited liability rule. Equation (75) has a sign typo in an intermediate bracket; the mission states its intended threshold ordering instead. These corrections are recorded in the moderation notes.
The implementation predicate retains the stage payoffs, feasible actions, Nash punishments and one-shot deviation inequalities. Its closed-form wage bounds are results to establish, not its definition. Collusion-proofness quantifies over all feasible state-contingent joint outcome lotteries, a stronger class than footnote 30's alternative equilibria. Contributions to the threshold inequalities, mixed-punishment lower bounds, and statewise surplus comparisons are welcome; each can be proved independently against the shared model.
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.
A convex form is a homogeneous polynomial of even degree whose value is convex as a function of its real variables. Every convex form is nonnegative, so it is natural to ask whether it can always be written as a sum of squares (SOS) of real polynomials. This matters in polynomial optimization because an SOS certificate can be searched for through semidefinite programming, while pointwise nonnegativity is generally harder to certify. Parrilo posed the convex versus SOS question in 2007. Blekherman proved nonconstructively that convex forms outside the SOS cone exist in sufficiently many variables. Saunderson constructed an explicit quartic example in 272 variables, together with a finite certificate of its failure to be SOS Saunderson, pp. 1–3.
An octonion is an eight-dimensional real normed division algebra. Write for conjugation and for the sum of squares of its eight coordinates. For two lists and of octonions, let and . The octonionic Cauchy–Schwarz form is
Each octonion contributes eight real coordinates, so this is a quartic polynomial in real variables. The paper's companion form is
To measure the SOS relaxation, and are the minimum and maximum of a form on the Euclidean unit sphere. For a degree- form, is the largest for which is SOS. When , the paper defines
These are values of the specific polynomial, not free parameters. The SOS predicate concerns finite sums of squares in the real multivariate polynomial ring Saunderson, pp. 2–4.
For every , the target is the full Theorem 1.2:
The milestone list includes the near-constant-on-the-sphere convexity criterion, its bound-based corollary, the octonionic inequality, the matrix identity for , the symmetry-reduced SOS characterization, the explicit feasibility system, and the exact SOS threshold at . The threshold is a separate claim: is SOS for and is not SOS for Saunderson, Theorems 1.2 and 4.11.
The theorem supplies an explicit counterexample to the assertion that convexity of an even-degree homogeneous polynomial forces an SOS representation. At , it is a concrete quartic in variables. Its gap also gives an explicit case where the basic SOS lower bound for optimization on a sphere is more than a factor two away in the paper's normalized measure. Thus the example links an algebraic separation of two cones with a numerical limitation of an optimization relaxation Saunderson, pp. 2–4.
The mathematical theorem is proved in the cited paper. The work here is to encode its octonion multiplication table, quartic polynomial, symmetry action, and finite feasibility certificate in Lean, then close the formal proofs. The group and polynomial definitions can also support other examples based on Clifford systems or structured SOS relaxations. The statements in this proposal compile with sorry; they are proof targets, not machine-checked proofs.
Nonnegativity of follows from octonionic Cauchy–Schwarz, and near-constant values on the sphere yield convexity after the stated correction. The obstacle is proving that has no SOS representation: evaluating a nonnegative polynomial at a few points cannot rule out SOS. The paper uses its symmetry to reduce the SOS question to eight nonnegative coefficients and then exhibits an infeasible three-row system. The corresponding positive SOS decomposition at marks the exact boundary Saunderson, §§3–4.
The variables are indexed by and the forms live in MvPolynomial over . The first eight rows of each matrix column are , the last eight are . The octonion product is computed from the paper's right-multiplication table; the inner product conjugates its first argument. The squared Euclidean norm is the polynomial , and the unit sphere is defined by the corresponding real sum, not by the default norm on a function type. The SOS predicate is Mathlib's polynomial IsSumSq.
The symmetry group called in the paper is represented by its concrete matrix model preserving the span of nine Clifford matrices. The eight use the equivalent orthogonal-projection formula: supplies the normalized basis of the Clifford subspace, and the three matrix projections select scalar, traceless symmetric, and skew-symmetric parts. The paper's printed unscaled are orthogonal with squared trace norm ; the factor in the definition accounts for this normalization. No assumption that the polynomial is SOS enters the definition of ; it is built from the octonion product itself.
For the general degree- milestones, and a nonempty finite variable type make explicit the paper's positive-degree, positive-dimension setting. Lemma 2.2 uses arbitrary lower and upper bounds, as its proof and its application at do. The scalar extrema and SOS bound are represented by real sSup and sInf; these operations return default values on empty or unbounded sets. The goal has , where the sphere is nonempty and compact and the extrema have their intended meaning. Formal work is welcome on these endpoint facts, the octonionic identities, invariant polynomial spaces, and the finite infeasibility certificate.
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 controller watches a one-dimensional random state (an inventory level, a cash reserve, an exchange rate) and may push it upward at any time, paying a proportional cost per unit of push. A running cost is paid on the controlled state . Minimizing the discounted sum of the two costs is the classical singular control problem, called singular because the optimal push is typically not absolutely continuous in time. Since Beneš, Shepp and Witsenhausen (1980) the expected answer has been a barrier strategy: reflect the state at a fixed lower level and do nothing above it.
For Brownian motion and diffusions this is well understood. For processes with jumps, the known proofs rely on the scale function of a spectrally one-sided Lévy process (jumps of one sign only). Yamazaki (Math. Oper. Res. 2017) solved the spectrally negative case this way. Financial and inventory data have jumps of both signs, and for a general Lévy process no scale function exists. Noba and Yamazaki (arXiv:2008.03021, Math. Oper. Res. 2023) prove that a barrier strategy is still optimal for a general Lévy process when the running cost is convex, and that the optimal barrier solves one explicit equation.
Let be a real Lévy process with , described by its triplet : with
Under the process starts at , i.e. it is .
A strategy is a nondecreasing, right-continuous process adapted to the natural filtration of , with ; an initial jump is allowed. The controlled process is (2.2). For a discount rate , a unit cost and a running cost , the cost of from is
and is admissible if the same expectation with in place of and without is finite (2.4). The value function is .
The barrier strategy at is ; then is reflected at the lower barrier , and its cost is (3.6). With the right derivative of and the process reflected at and started at , set
Standing assumptions: is convex, of polynomial growth, and (Assumption 1); for some (Assumption 2(ii)).
For every starting point , the barrier strategy at is admissible and
under Assumptions 1 and 2(ii) only. The paper first assumes is not a driftless compound Poisson process (Assumption 2(i)) and, for unbounded variation, that with of polynomial growth (Assumption 3); §4.2 and §5 remove both, and the goal carries neither.
The fifteen milestones follow the paper's proof:
The theorem gives a complete solution, for all Lévy processes with exponential moments, of the singular control problem with convex running cost: the optimal policy is a barrier, and the barrier is the root of a monotone function of . It contains the Brownian, spectrally negative and spectrally positive cases, and processes of bounded and unbounded variation, subordinators and compound Poisson processes. Because depends only on the law of the reflected process , can be computed by Monte Carlo or, when the Wiener–Hopf factorization is known, by transform inversion (Remark 4).
The result is proved in the paper; it has no machine-checked proof. Formalizing it requires a Lévy-process layer that Mathlib does not yet have: reflected Lévy processes, first-passage times, and an Itô formula for semimartingales with jumps used against Lebesgue–Stieltjes integrators. The milestones isolate statements that do not need all of it: Lemma 12 is real analysis about a smoothed convex function, Theorem 1 compares barrier strategies only, and Proposition 1 is a reusable verification lemma for singular control.
The standard route computes in closed form, picks by smooth fit, and checks the variational inequality. For a general Lévy process has no closed form: the scale function, which carries the one-sided proofs, does not exist when jumps of both signs are present. The paper works instead with derivatives of with respect to the barrier, expressed through the first down-crossing time (Lemma 6). This needs the regularity of for , which fails for driftless compound Poisson processes, hence the separate treatment of §5. In the unbounded-variation case, is only if is, so the verification lemma cannot be applied directly. The paper smooths , solves the smoothed problems, and passes to the limit through the barriers and the values (Lemmas 14–15).
Two definition files. SingCtrlLevy.Barrier.Levy gives the triplet, , the Lévy process (measurable, , independent and stationary increments, càdlàg paths, characteristic function ), bounded variation, the driftless compound Poisson triplet, Assumptions 2(ii) and 3, the classes and the generator . SingCtrlLevy.Barrier.Model gives strategies, the cost, the barrier strategy, , , , Assumption 1, the smoothing of (4.35) and .
Conventions:
is the infimum of the set , never "the optimal barrier", and is the explicit reflection at . The goal ranges over every nondecreasing, right-continuous, adapted strategy satisfying (2.4), and the value function is never replaced by a junk infimum. None of the three trivializes the statement.
Welcome contributions: measurability and integrability lemmas for reflected Lévy processes, first-passage regularity (Lemma 1 of the paper), an Itô formula for functions of Lévy processes plus nondecreasing càdlàg controls, and the real-analysis lemmas on . The Lévy layer and the verification lemma can be reused beyond this mission.
Food importers that also produce domestically must decide whether to commit to purchases before the domestic harvest or negotiate after observing it. This choice matters when suppliers must plant before the harvest is known: a late negotiation leaves them exposed to unsold production, while an early contract commits the importer to purchases it may no longer need. Mu, Hu, Reddy and Gavirneni model this problem using India's imports of pulses as motivation and compare the two contracting times within the same bargaining framework (Mu et al., accepted manuscript, 2022). The mission asks how the comparison changes when the importer bargains with several suppliers at once.
The source paper distinguishes ad hoc negotiations, held after the buyer's internal yield is observed, from forward negotiations, held before yield is observed. A single forward supplier need not improve the buyer's expected net utility relative to a single ad hoc supplier. Proposition 3 identifies a supplier-count effect: with sufficiently many suppliers, forward negotiations yield the buyer more utility. Its claim concerns the equilibria of the actual contracting games, including the suppliers' production choices and the payments determined by Nash bargaining (Mu et al., Proposition 3, PDF p. 9).
The buyer has demand one and an uncertain internal yield uniformly distributed on . Consuming gives utility ; any supply beyond demand is discarded. Every supplier has the same positive unit production cost and produces before is realized. The buyer has bargaining power , leaving for a supplier. This mission studies the positive-production regime (Mu et al., §§3–4, PDF pp. 3–8).
In the all-ad-hoc game, each of suppliers chooses a production quantity before yield is observed. Once is known, each supplier bargains with the buyer over a purchase and payment . The other negotiations are assumed successful and their agreed quantities remain fixed when the buyer and one focal supplier bargain. Each supplier's expected profit is its expected payment less . A symmetric equilibrium uses the same production and yield-dependent agreement for every supplier; no supplier can increase expected profit by changing its production quantity and then bargaining under the same other agreements.
In the all-forward game, all suppliers bargain before yield over a quantity and payment . The other contracts remain fixed in a focal negotiation. Suppliers produce exactly their contracted quantities, as §4.1 assumes. The buyer's expected net utility is the utility of its internal yield plus all purchases, capped at one, less all payments; one supplier's profit is . Both games use the generalized Nash bargaining product of the buyer's and supplier's gains over disagreement, maximized over individually rational agreements (Mu et al., §4.1, PDF pp. 7–8).
The main target is Proposition 3. Write and for the buyer's equilibrium net utilities in the all-ad-hoc and all-forward games, and and for one supplier's equilibrium profit. For each regime, increasing strictly improves the buyer's net utility and strictly reduces the suppliers' aggregate profit:
In addition, there is a positive threshold beyond which the buyer prefers forward negotiations:
The target quantifies over every symmetric equilibrium and asserts that equilibria exist for every positive supplier count. The milestone path records the source's ad hoc stage outcome, pure ad hoc production quantity, single-supplier ad hoc result, pure forward quantity, single-supplier forward result, four multiple-supplier payoff formulas, and the quadratic payoff-gap threshold. The four formulas are intermediate identities about the equilibria; the goal remains the comparison of the underlying games (Mu et al., Lemmas 1–2 and Propositions 2–3, PDF pp. 5–9; proof of Proposition 3, PDF pp. 14–15).
The result identifies a precise limit to the single-supplier comparison. Forward contracts coordinate production with purchase commitments, but the buyer also commits before knowing its own yield. Proposition 3 says that competition among sufficiently many suppliers changes the buyer's expected payoff comparison even though the buyer's exogenous bargaining power is unchanged. For the model, this supports analyzing supplier count and contracting time together rather than treating them as independent decisions (Mu et al., §4.1, PDF p. 9).
The paper proves these claims analytically. Here the definitions and theorem statements compile in Lean, while the proposed theorems remain open proof obligations. Completing the mission would machine-check the existence, payoff identities, monotonicity claims, and threshold for the stated equilibrium concepts. Its quantity-and-payment Nash bargaining definition and symmetric-game interface can also support related sourcing models. No machine-checked proof of this paper's Proposition 3 is claimed by this draft.
Holding a supplier's agreement fixed changes the buyer's disagreement payoff in every other negotiation. Consequently, the buyer's gain in one bargain depends on the quantities already agreed with the remaining suppliers. A direct comparison that treats each supplier as an independent copy of the single-supplier game misses that dependence. The ad hoc game adds a second stage: production is chosen before yield, while purchases and payments are determined after yield for every feasible realized value. A proof must keep these two decisions and the changing disagreement points consistent across supplier counts (Mu et al., §4.1 and Appendix B, PDF pp. 7–9, 13–15).
All monetary amounts, quantities and utility values are real numbers. Supplier count is a positive natural number. Uniform-yield expectation is represented by the interval integral . Consumption is capped at demand one. Only the two pure games are represented: ad hoc suppliers and no forward suppliers, or forward suppliers and no ad hoc suppliers. Agreements in the ad hoc game are functions of yield, constrained on . The Nash product is compared only over feasible, individually rational pairs, where both bases of the real powers are nonnegative.
The model uses the purchase cap of equation (A.2): an ad hoc supplier cannot sell beyond the buyer's remaining need. A focal negotiation holds other suppliers at their agreed quantities, and a production deviation holds those other agreements fixed, the passive-beliefs reading of Appendix B. Forward suppliers produce their contracted quantities. These choices are recorded explicitly because changing any of them changes the formulas. The paper writes in its standing focus; the goal uses , since the stated strict ad hoc monotonicity fails at equality. The printed in the forward supplier-profit formula of the proof of Proposition 3 is read as , the count used throughout that paragraph. PDF pages are indexed from one because this accepted manuscript has no printed page numbers.
The goal cannot be satisfied by declaring the four payoff expressions to be the games' values: the equilibrium predicates specify Nash bargains, production incentives, and the resulting integrated payoffs independently of the printed closed forms. Likewise, the existence clause prevents the universal comparisons from holding because there are no equilibria. Contributions that establish stage bargaining, equilibrium existence and characterization, integral payoff identities, or the algebraic threshold all advance the result. The mixed forward/ad-hoc regime, buyer's-remorse extension, and hybrid supplier cases are outside this mission (Mu et al., §§4–5 and Appendix A, PDF pp. 8–13).
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.
Many goods are maintained by several parties at once: a shared infrastructure, a fishery, an industry's reputation, a public research base. Each party bears the full cost of its own investment while every party enjoys the benefit, so each prefers that someone else pay. This free rider problem is classically studied as a war of attrition, and continuous-time versions are a standard tool in operations research for timing decisions under uncertainty.
Kim and Kwon (arXiv:2208.11217, published in Operations Research, 2024) model the stock of the common good as a declining diffusion and let two players invest in it at fixed plus proportional cost. Their point concerns the stability of mixed strategy equilibria, in which players randomize the time of investment. When the good can be invested in only once, Georgiadis, Kim and Kwon (Games and Economic Behavior 131, 2022) showed that any asymmetry in costs destroys the mixed equilibrium; Theorem 1 of the present paper recovers this. When investment can be repeated indefinitely, an impulse control game, the paper shows that a mixed equilibrium survives moderate asymmetry. The verification argument extends the single-player impulse control analysis of Alvarez and Lempa (SIAM Journal on Control and Optimization 47(2), 2008) to a randomized two-player setting.
The stock lives on an interval with and, absent investment, solves with , natural boundaries, Lipschitz coefficients with linear growth, and the transversality condition . Write , let and be the increasing and decreasing positive solutions of , and let for the common flow profit , continuous and increasing.
Player may invest at any time, paying to raise the stock by , with and . Time is split into periods, each ending at an investment. Players randomize through a uniform randomizer per player and period: an investment occurs when a survival process falls below the randomizer. Simultaneous attempts are settled by a fair coin. Player 's payoff is the expected discounted profit minus its own discounted investment costs, (22).
The profile has threshold , atom probability and targets . In the first stage of a period, player 1 waits and player 2 invests with probability when the stock reaches from above. In the second stage each player invests at hazard rate , positive exactly on the common mixed region . Every investment by player raises the stock to . With and , Assumption 5 states that solve and . These are the single-player optimal thresholds for cost .
Under the standing assumptions and Assumptions 1, 2, 4 and 5, there is such that for every there are and with
together with payoff functions satisfying the §4.2 conditions, such that with the rates (29) is a subgame perfect equilibrium. Here is the minimizer of (Lemma 2). The goal leaves unquantified, as the paper does: the §4.4 example gives for .
Lemma 2 (shape of , ) and identity (B.20); Lemma B.8 (i) and (ii) (closed-form payoff functions satisfy the §4.2 conditions); Lemmas B.7 and B.6 and Theorem 2 (the verification theorem); Lemma B.8 (scalar conditions (B.21)–(B.23) suffice); parts (i) and (ii) of the proof of Theorem 3 (the scalar conditions hold for near ).
The result shows that the instability of mixed equilibria in timing games of public good provision is an artefact of one-shot investment. With repeated investment, player 2 can promise a probability of investing at , which raises player 1's continuation value and pulls player 1's investment threshold to , so that both players share the same mixed region. Theorem 2 is, to the authors' knowledge, the first verification theorem for a mixed strategy equilibrium of an impulse control game. Proposition 7 of the paper compares this equilibrium with a pure strategy one from a social planner's view, and it presupposes Theorem 3.
Theorem 3 and its lemmas are proved in the paper. None of it is formalized in any proof assistant. A formalization would provide a machine-checked randomized impulse game, with periods, survival processes, tie coins and deviations adapted to a player's own information. It would also provide a verification theorem in that setting and the real-analysis chain behind the explicit construction. The diffusion layer reuses the published definitions of Kwon's variable contributions game (same authors, same model).
The analytic half (Lemma 2, Lemma B.8, the proof of Theorem 3) is real analysis on , , and . Its delicate point is the global maximum of : the local maximum at beats the boundary value at only under (B.23), which holds only for close to .
The verification half is the hard part. The obvious approach, a Dynkin formula on for the candidate payoff, does not apply. The opponent's investments arrive at a state-dependent hazard rate, so the argument must kill the process at that rate within each period and then sum the per-period identities. The limit over periods needs monotone convergence, using and the lower bound . Player 2's atom at creates a discontinuity in time of player 1's payoff, and a deviation by player 1 at exactly that instant produces a tie whose expected value must be bounded with the boundary condition .
The Lean development uses the published VarContrib.RegularMPE.Model, Setting (μ, σ, π, k, r, I, x₀, the generator gen, the resolvent R, the controlled state equation IsStateSol) and EthierKurtz.HasBrownianItoIntegral. Everything else lives in the namespace InvestCommonGood.MixedTSSPE, in three definition files. Model holds , , , , , the standing assumptions and Assumptions 1, 2, 4, 5. Game holds the randomizers, plays, , deviations, the payoff (22) and the SPE. Conditions holds the §4.2 conditions, (28), (29) and the closed forms of Lemma B.8.
Committed conventions:
0 (player 1) and 1 (player 2); times are ℝ≥0, and random times are WithTop ℝ≥0, where ⊤ means never;Standing hypotheses beyond the printed text, each used by the paper without proof:
Pinned readings: Assumption 5 includes , and Assumption 4 includes the convergence of . The §4.2 conditions include positivity of the denominators of (29) on .
The goal concludes the equilibrium property of the randomized game itself. "There exist , satisfying (B.21)–(B.23)" or "the §4.2 conditions are satisfiable" are milestones, not substitutes for the goal. Contributions are welcome on either half: the real-analysis chain is self-contained, and the verification lemmas are reusable for other randomized timing games.
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.