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?
A partially observed array with three indices appears when data record relationships among triples of objects. If its entries have a low-rank structure, one can hope to recover the full array from far fewer than measurements. Cai, Li, Poor and Chen study this problem when the measurements are noisy and only a random subset of entries is seen. Their result gives a statistical error bound for a concrete two-stage method: spectral initialization followed by ordinary gradient descent on a nonconvex loss. It is a known theorem, proved in the pinned preprint, rather than an open conjecture.
The unknown symmetric order-three tensor is . It has a CP decomposition , where the nonzero columns form . Each unordered triple of coordinates is sampled independently with probability ; its six permutations share one sampling decision. On a sampled triple the observation is , with symmetric, centered, independent sub-Gaussian noise of variance at most . The observed tensor vanishes outside the sampled set .
For a candidate factor matrix , the objective is
Algorithm 2 obtains a leading -dimensional eigenspace from an off-diagonal Gram matrix of the mode-one unfolding of . Algorithm 3 uses Gaussian restarts, leading singular vectors, and greedy pruning to turn that subspace into a factor matrix . Algorithm 1 then applies the gradient step to . Eigenvalue ties, leading singular-vector choices, and pruning ties can produce several admissible executions; the result concerns every execution.
Incoherence measures how evenly the tensor and factors spread across coordinates and how nearly orthogonal distinct factors are. The condition number is the ratio of the largest to smallest factor norm. Write and . Distances , , and minimize their respective matrix norms over permutations of the columns.
The goal is Theorem 2.4, in the bounded-rank, bounded-incoherence, bounded-condition-number regime. Under its printed sampling, noise, restart, threshold and step-size conditions, for every it asserts, with probability at least ,
The rate is fixed to , consistent with the paper's local-convergence lemmas. Milestones formalize the gradient identity (36), local Hessian bounds (Lemma 5.1), spectral-subspace recovery (Lemma 5.7), factor retrieval (Theorem 5.9), and the paper's general-parameter recovery theorem (Theorem 2.8). The latter makes the dependence on and explicit.
The inequalities give two guarantees at once: geometric reduction of initialization error and an explicit noise floor. The bound controls the error in each coordinate row, which a Frobenius estimate alone does not supply. Together with the tensor-entry corollaries in the paper, they explain the accuracy of this practical nonconvex method under random subsampling. The authors also specify how the sample probability, noise level, rank and incoherence interact, so the result can be compared to other tensor-completion methods.
This mission asks for a machine-checked version of the known result. Its published ψ₂ norm definition is reused; the paper-specific tensor model, spectral initialization relations, loss and gradient iteration are new. The theorem statements compile with sorry, so none of their proofs is claimed as machine checked here. Proofs of the listed milestones, the main theorem, and faithful auxiliary concentration results are welcome; the paper's numerical experiments are outside this formalization.
The gradient loss is nonconvex, so global convexity cannot justify the iteration bound. The local Hessian estimate applies only near in both Frobenius and rowwise norm. A Frobenius estimate alone cannot establish the rowwise condition at every iteration. The spectral initializer must also select individual factors from a subspace despite nearly tied eigenvalues and noisy tensor contractions. These are the points where a direct appeal to standard smooth-gradient-descent theory stops short of the stated result.
Coordinates are Fin d and Fin r, with zero-based indexing; the PDF uses one-based indices. All logarithms are natural. Tensor and matrix norms are explicit finite-coordinate Euclidean norms. Minima over permutations range over all permutations of Fin r, and maxima in the incoherence parameters range over the indices specified by Definition 2.1. Sampling is on sorted triples, then extended by symmetry. The probability model is a single probability space carrying the sampling indicators, noise variables and Gaussian restarts, jointly independent; the paper leaves some cross-family independence implicit. Noise has mean zero, variance at most , and ψ₂ norm at most using the published extended-nonnegative norm. The last bound makes the paper's sub-Gaussian scale explicit.
The statements use , , nonzero true factor columns, , and . Theorems 2.8 and 5.9 use and round their real-valued restart count up to a natural number; this handles the boundary where . Theorem 2.4 places its claimed absolute error constants before the rank and incoherence bounds and all instance data. Probability is expressed as the outer measure of the bad event, since admissible-execution predicates quantify over choices and need not be measurable. Each good event explicitly asserts that an admissible execution exists before requiring the bounds for every execution; otherwise a failed pruning run would make a universal claim vacuous.
The remaining reusable infrastructure includes concentration for symmetric sampled tensors, finite-dimensional spectral perturbation with ties, and derivative estimates for the cubic factor map. The paper's leave-one-out iteration lemmas and their auxiliary estimators are not included in this initial milestone list; they remain natural contributions toward the full proof.
Banks hold claims on one another. When one bank cannot pay, its creditors receive less, which can push them into default in turn. Clearing models compute the payments and wealths that are consistent across the whole network. Regulators and researchers use them to measure systemic risk and to price interbank debt. The basic model is that of Eisenberg and Noe (2001), doi:10.1287/mnsc.47.2.236.9835. Rogers and Veraart (2013), doi:10.1287/mnsc.1120.1569, added bankruptcy costs: a defaulting bank recovers only part of its assets.
The value of a bank's debt or equity is an expectation over random endowments. For general endowments that expectation requires partitioning the endowment space into up to default regions (Gouriéroux, Héam and Monfort 2012), and with bankruptcy costs those regions need not be convex. Banerjee and Feinstein, Pricing of debt and equity in a financial network with comonotonic endowments (Operations Research 2022; arXiv:1810.01372), observe that when all endowments are driven by one factor (they are comonotonic), banks default in a fixed order as the factor falls. Default probabilities and the prices of debt and equity then have closed forms.
There are banks and an outside society node. Bank owes a total of ; the fraction of it is owed to bank (), and the fraction to society (Assumption 2.1). The matrix is the relative liabilities matrix. Banks start with endowments . A bank with negative wealth defaults and keeps a fraction of its external assets and of its interbank assets.
With componentwise, the clearing process is
and a variant , which replaces by its positive part, is used in the appendix. The greatest clearing wealth is the largest real solution of . Bank 's payment is and its equity is .
If the set of defaulting banks has indicator , the clearing equations are linear. With the diagonal 0–1 matrix of ,
Comonotonic endowments are for a nonnegative random factor and a nondecreasing map (Assumption 3.2). The solvency threshold of bank is (Definition 3.4). Banks are numbered so that , with and (Assumption 3.5). On exactly banks default; and are and at that default set, with and .
With , for every bank :
The goal is the theorem as printed, with one added hypothesis (see Formalization scope).
Theorem 3.6 turns the valuation of every bank's debt and equity in a network with bankruptcy costs into one-dimensional integrals of the factor, replacing the default regions of the general case. The default probabilities depend only on the thresholds , which in turn depend only on the map and not on the law of . The same formulas price debt and equity in the paper's numerical study of the European banking system, and they are the starting point for the comonotonic bounds of Lemma 4.1, which are not part of this mission.
The paper gives a one-sentence proof of Theorem 3.6 and proves its appendix results largely by citation (Tarski, Milgrom–Roberts, Rogers–Veraart, input–output theory). No part of it has been machine-checked. A formalization supplies the missing steps: the identification of the two clearing maps, the attainment of the thresholds, nonsingularity of the linear systems, and the decomposition of the expectations. It also produces, as a reusable by-product, the Rogers–Veraart clearing model with its greatest fixed point, which other financial-network results can build on.
The obvious argument is: banks default in order, on each interval of the wealth is affine in , so integrate piece by piece. Two steps of it fail as stated.
First, the threshold is an infimum, and the paper treats it as attained ("the minimal value such that firm is solvent"). With bankruptcy costs the wealth jumps when a bank defaults, even for continuous , so attainment needs an argument about the greatest fixed point under decreasing endowments. Without right-continuity of it is false.
Second, the greatest fixed point of is not reached by Tarski's theorem on , because is not monotone below . That every real fixed point lies above uses Assumption 2.1. Nonsingularity of also rests on Assumption 2.1. Matching the default set to the interval then combines monotonicity (Proposition A.6) with the ordering of Assumption 3.5.
Fin n; bank i is the paper's bank . The data are , , , (structure Network), with the standing assumptions bundled in Network.Standing. is the supremum of the real fixed points of in the lattice ; payments and equity follow Definition 2.2. Default sets are finite sets of banks. Inverses are Matrix.inv.i.When banks are hit by losses they sell assets to restore their leverage targets, and these fire sales depress prices for every other holder of the same assets. The resulting deviation of market capitalization from its fundamental value is a systemic externality: it depends not on any single bank's portfolio but on how the stock of each asset is distributed across banks. Awiszus, Capponi and Weber (arXiv:2003.10121, Operations Research 2022) ask which distribution of a fixed stock of assets among banks with fixed budgets minimizes this externality, as measured by the expected squared deviation of market capitalization from fundamentals. The question matters to macroprudential regulators, who can influence portfolio overlap among banks, and it connects to the literature on overlapping portfolios and price-mediated contagion (Greenwood, Landier and Thesmar, 2015; Capponi and Larsson, 2015).
The paper's answer is explicit: the optimal mean squared deviation has a closed form, the optimum is computed by a two-step "aggregate first, then allocate" procedure, and the optimal allocation is unique exactly when there are two banks.
There are assets and banks. A holding matrix records in entry the holding of asset by bank , so column is bank 's portfolio. Initial prices are normalized to .
Let . Then
the f-efficient holding matrix is unique if and only if , and in that case it equals
The result itself. Theorem 4.1 gives the smallest achievable mean squared deviation of market capitalization from fundamentals for a given asset supply, budget profile and systemic significance profile, as an explicit function of the shock moments. It is the benchmark against which the paper measures the inefficiency of observed and diversified holdings (Section 4.2 shows that full diversification is f-efficient only in a degenerate case) and drives the comparative statics of Section 5. Part b) says that with three or more banks efficiency leaves an affine family of optimal allocations of dimension , so a regulator has residual freedom to pursue other objectives at no cost in market efficiency.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The formal development delivers the theorem together with a reusable treatment of minimizing a positive definite quadratic form over a hyperplane, the existence part of the transportation-type linear system , , , and an exact rank computation for the structured matrix . The uniqueness characterization in part b) depends on that rank computation, which the paper carries out by Gaussian elimination on block matrices.
The minimization over is a -dimensional quadratic program whose objective is degenerate: it depends on only through the -vector . Strict convexity therefore cannot give uniqueness, since the objective is constant along every direction in which and the constraints do not change, and the obvious argument for part b) fails. Existence is not automatic either: is unbounded, and one must show that every point of the hyperplane is attained as by a feasible , which fails when is constant. The uniqueness statement is a dimension count: it needs the exact rank of the constraint matrix , whose rows carry exactly two linear dependencies under Assumption 3, so that the solution set has dimension , which is positive as soon as and .
Fin K, banks are Fin N, all quantities are real; holding matrices are Matrix (Fin K) (Fin N) ℝ. The paper's banks 1 and 2 are the indices 0 and 1.Matrix.inv, which returns on singular matrices. Every statement that mentions , or assumes for all (Assumption 2), and every statement that divides by assumes .Module.finrank of the kernel of .Fin.cast.The development needs the Sherman–Morrison identity for a diagonal-plus-rank-one matrix, the minimizer of a positive definite quadratic form under one linear constraint, explicit constructions in , and a rank computation. Contributions of reusable lemmas for these, and of proofs of the milestones in any order, are welcome.
A customer who is told that service will be delayed can use the announced wait to decide whether to stay, leave, or plan around the delay. A service operator needs to know whether a changing, customer-specific announcement actually predicts the eventual wait more accurately than a fixed announcement. Bassamboo and Ibrahim studied this question for the last-entered-service (LES) announcement, which reports the wait of the last customer to enter service, and for a static announcement based on the mean wait of delayed customers. Their empirical examples show that neither method wins uniformly across queueing regimes; the comparison depends on how the announcement and the eventual wait move together (Bassamboo and Ibrahim, 2021, §§3–4 of the submitted manuscript).
The mission isolates the paper's general comparison criterion. Its statement needs no particular arrival process, service discipline, or queue length. This makes the result a reusable mathematical test for predictors in other service systems as well as for LES. The paper itself notes that the criterion applies irrespective of the specific queueing model, subject to the moment conditions under which its mean-squared errors and correlations are defined (submitted manuscript, §4.2, p. 14).
Let be the real-valued waiting time of a delayed customer in steady state. Operationally, the paper takes the virtual waiting time and conditions on : has the conditional distribution of a positive wait. Let be a real-valued predictor issued to that customer. To compare a prediction with the outcome, the pair must be jointly distributed; their separate marginal distributions cannot determine the correlation. Both are represented as functions on one probability space in Lean.
The static announcement, denoted , always reports . A changing predictor can instead respond to the system's current state. The paper's mean-squared error of is the expectation of its squared discrepancy from the outcome:
Write and for variance and covariance. When both variances are positive, the Pearson correlation is . The coefficient of variation of the delay is . These are the quantities in §4.2 and equation (3) of the submitted manuscript (published article; mission citations use the submitted manuscript's page and equation numbers).
The first milestone establishes the error of the static predictor from its definition:
The next two milestones give the expanded error identity from the proof of Proposition 1 and its normalized form, equation (4). Suppose and with . Proposition 1 states
The goal is Corollary 1, equation (5). If has the same mean and variance as , it compares the two predictors at the exact threshold :
Both inequalities are non-strict. The corollary is stated for a general predictor ; applying it to LES requires a separate analysis of the LES wait and its correlation with the arriving customer's wait. The submitted manuscript supplies that model-specific analysis later in §5 (Bassamboo and Ibrahim, 2021).
Under the corollary's equal-mean and equal-variance assumptions, the comparison of two expected squared errors reduces to one correlation. A predictor with correlation at most offers no mean-squared-error improvement over the static announcement; a predictor above that threshold does. The equality case is included. Proposition 1 also records how a mean shift or a variance change modifies this comparison, which is useful when a proposed announcement is biased or more variable than the delay.
The paper proves these identities. This mission asks for machine-checked proofs of their statements in Lean; the draft theorems themselves are open proof obligations. A completed development would provide reusable definitions of predictor MSE, the constant mean announcement, Pearson correlation, and coefficient of variation, together with exact interfaces for later queueing results. It does not assert that the paper's LES limit theorems are already formalized.
The key mathematical work is passing from the expectation of a squared difference to the variance and covariance terms while keeping the two random variables on the same probability space. In Lean this requires the integrability consequences of square integrability, the relation between covariance and the centered product, and careful handling of the square-root normalization. Merely replacing MSE and correlation by unrelated real parameters would erase that work and yield an elementary numerical equivalence. The proposed definitions are therefore the expectations and covariance stated in the paper, and the goal quantifies over actual random variables.
The boundary also needs attention: the predictor has zero variance and ordinary Pearson correlation has a zero denominator. The term involving correlation is multiplied by , so the displayed identity still has a meaningful value under the Lean convention described below. Proposition 1's other denominator, , requires a positive delay mean and variance in the intended setting.
Lean uses an arbitrary measurable space with a probability measure and real-valued functions on that space. It does not construct the underlying queue; §4.2 makes the comparison at the level of the joint law of the delay and prediction. Each theorem explicitly assumes where both appear. This supplies finite second moments for the paper's variances and MSE and avoids Lean's default value for a nonintegrable real integral. The EA identity only needs .
Positive variance of is explicit in Proposition 1, its expansion, and the corollary. It gives the intended domain of correlation in the equal-variance corollary and prevents equation (4) from failing under division by zero. Proposition 1 additionally assumes , as expected for a positive conditional wait, so . No condition is imposed: at , Lean evaluates the zero-denominator correlation as zero and the entire correlation term vanishes. The error is defined with as in equation (3), although the proof writes the reversed difference. Contributions toward the integral identities, covariance normalization, and the final inequality are welcome; the four definitions may also serve other prediction-error formalizations.
In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.
The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.
Write for the set of all subsegments of with . An interval may be degenerate, meaning . A real-valued function on is continuous when its value varies continuously with the two endpoints. The required boundary condition is for every . No sign, monotonicity, or additivity condition is imposed. A partition into parts is a sequence , so its parts may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.
The intermediate setting is a nice multivalued function. Its graph is a compact subset of . The graph separates the bottom from the top inside the cylinder : those two sides lie in different connected components of . A representation of a nice graph is a continuous real function on that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.
For a prime , a segment , and a value , a zero partition is a sequence such that for each . The set contains exactly those pairs that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.
The goal is Theorem 1.1: for every positive integer and every continuous satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:
The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when , there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for . The milestone list includes the fixed-segment and continuous-family statements used to characterize , and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.
The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.
The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.
For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod- statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy , not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.
Lean represents by the endpoint pair with . The cylinder uses the closed value range ; a nice graph lies in its open interior . Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.
Every prime-step claim assumes prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes . The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.
Firms that serve several geographic markets must decide both how much to produce and where to sell it. A capacity limit couples those regional decisions: an extra unit sent to one region cannot also be sent to another. Different transport costs and demand curves make a collection of independent single-region Cournot models inadequate. Alsabah, Bernard, Capponi, Iyengar and Sethuraman study whether this coupled quantity game has a determinate outcome. Their 2020 author version proves a unique equilibrium allocation and characterizes it through firms' marginal profits. This mission concerns that result, Theorem 4.5 on p. 12 of that version.
There are firms and regions . Firm sells quantity in region . Its total output is , constrained by capacity . The total sales in region are . The inverse demand function gives the price when total sales are . Firm pays production cost per unit and transport cost per unit sent to region . Its profit at allocation is
A strategy for firm is any nonnegative regional allocation whose total is at most . A Nash equilibrium is a feasible profile at which no firm can gain by changing its entire regional allocation while the others hold theirs fixed. This is the feasible unilateral-deviation definition in the paper's Definition 3.1, p. 8.
The marginal profit in region is
For a vector of marginal-profit levels, condition (2) says and for every firm and region. Proposition 4.2 gives a unique nonnegative allocation satisfying these conditions, denoted , when lies in the box , where and . The reduced-form operator assigns firm zero marginal profit if its output at is below capacity. Otherwise it assigns the marginal-profit level at which its output under equals . This is the two-case definition on p. 11; it depends on the other firms' marginal-profit levels through .
Lemma 4.3 asserts that has exactly one fixed point in the marginal-profit box:
Theorem 4.5 identifies every equilibrium of the original quantity game with the allocation at that fixed point:
The goal includes existence of and the equivalence, so it asserts both existence and uniqueness of the equilibrium allocation. Its milestones follow the paper's supporting statements: existence of a pure equilibrium, marginal-profit conditions, existence and uniqueness of , continuity and comparative statics, fixed points of , and the link from an equilibrium to a fixed point. The Algorithm 4.1 computation clause of Proposition 4.2 and the iteration-convergence clause of Lemma C.5 are identified as partial milestones; their full printed text is retained in the milestone provenance.
The result establishes that capacities, regional demand, and unequal shipping costs still lead to a single predicted sales allocation under the paper's regularity conditions. It also gives a common language for comparing the original game with a smaller game in marginal-profit vectors. Subsequent results in the paper analyze changes in costs, capacities, prices, and consumer surplus relative to this equilibrium Alsabah et al., §§5–6; those later comparative-statics claims are outside this mission.
The mathematical result is proved in the cited paper. The goal here is a machine-checked Lean development of its model, its fixed-point characterization, and the existence and uniqueness theorem. The current proposal contains definitions and theorem statements, with proofs open. The pure-Nash relation is a published reusable definition; the market model, complementarity allocation, and operator are new interfaces that could also support later formalizations of the paper's comparative-statics results.
An equilibrium of the quantity game satisfies the marginal-profit conditions, but those conditions alone describe candidate allocations and do not replace feasible unilateral deviations. Conversely, a fixed point of does not become an equilibrium merely from the fixed-point equation: the capacity-constrained regional payoff problem still has to be connected to the allocation . Uniqueness also requires control of how all firms' regional sales respond when one marginal-profit coordinate changes. Lemma C.4 records weak and strict changes, including boundary cases where a firm stops selling in a region. The existence lemma invokes a general pure-strategy equilibrium argument; the statement is kept even though that infrastructure is substantial in Lean.
Lean uses Fin N and Fin R for zero-based firm and region indices. An allocation has type Fin N → Fin R → ℝ, with the firm coordinate first, the transpose of the matrix orientation in the paper. Finite sums give firm and region totals. The inverse demands are on , strictly decreasing and concave on nonnegative quantities; deriv is therefore the ordinary derivative at the quantities used here. The paper phrases Assumption 1 for direct demand on and then uses regularity of its inverse . The formal model makes that inverse-demand regularity an explicit assumption. It also states , as implicit in the interval , positive capacities, and nonnegative production and transport costs. Those sign assumptions are needed for the box and the two branches of to have the stated meaning. No positivity of prices at all quantities or finite choke quantity is assumed.
IsEquilibrium uses the published CarbonDoubleCount.Planner.IsPureNash relation, testing every feasible full strategy deviation. Qhat is chosen as the unique solution of condition (2), and Phi is computed from that allocation and the market capacities. On the stated box, the proposal's milestones establish that the selection and inverse branches denote the paper's objects. The intended theorem excludes encodings that choose an active set freely, pass or as arbitrary parameters, or substitute first-order conditions or coordinatewise deviations for Nash equilibrium. The definition layer and results on continuity, monotonicity, and fixed points are reusable parts of the development. Contributions that prove these stated targets or provide supporting analysis of the firm's concave payoff problem are within scope.
A visible patroller gives an attacker information: the attacker can observe when a location is vacant and wait for a favorable moment. This changes the patrolling problem from choosing how often to visit each location to choosing a movement rule that remains effective against an adversary who chooses the attack time. The preprint The Uniformed Patroller Game studies this setting on a star network, where the patroller moves between a central base and the locations she protects. Its main result characterizes a robust attack delay and a robust patroller reflection rule for every attack duration, as well as exactly when those choices are unique. The source here is arXiv:1908.07366v2, by Alpern, Chleboun, and Katsikas; the later journal article has a different title and author list.
The network has a centre and end nodes. Each end node is a location to defend; the centre is a base and is not an attack location. A Markov patroller strategy is a pair . When at , the patroller goes to each specified end node with probability and stays at with probability . When at an end node, she returns to with probability and otherwise stays at that same end node. Thus , , and . The strategy does not depend on which node the attacker selects.
The attacker chooses an end node and an integer delay . After the patroller leaves , the attacker counts consecutive periods of her absence. If she returns before periods pass, the count resets. Otherwise the attack begins in the th period of absence. It lasts periods and is intercepted if the patroller visits during that interval. The paper requires because a one-period attack could always begin immediately after departure. This mission also takes , ensuring another end node exists and the conditional attack event has positive probability under the admissible strategies.
Let be the first positive step at which the patroller, having just left for , returns to . The starting state is already the first period of absence. The interception probability is the paper's equation (17):
The patroller maximizes and the attacker minimizes it. A saddle point is a pair of strategies for which neither can improve by changing alone, with comparisons over all admissible and all end-node-and-delay pairs . A strategy is called optimal if it occurs in a saddle point. The source analyzes pure strategies in these parametric sets; a pure saddle remains a saddle if independent randomization of these strategies is permitted.
Theorem 1 asserts that some optimal patroller strategy has and pairs with an attack at any end node with . It also asserts two exact uniqueness regimes:
The patroller's centre-to-end probability is selected optimally; it is not fixed in the main statement. The attack node is immaterial by symmetry, but it remains an explicit part of every attacker strategy. The theorem is posed over the full strategy sets, so its uniqueness assertions cannot be satisfied by restricting those sets to the displayed choices.
The milestone list follows the source's symmetry reduction, Lemmas 1–3, equations (3) and (15), and Propositions 1–2. For , Proposition 1 identifies and the value . It also identifies optimal reflection probabilities below one. For odd , Proposition 2 identifies the unique optimal patroller strategy , permits every attacker delay, and gives
For general even , the statement that an optimum has is recorded separately. It is needed to support the delay-uniqueness clause, while the paper illustrates this interior maximum numerically in Figure 2 rather than proving it as a numbered result.
The theorem reduces the strategic choices in this game: regardless of attack duration, delay two is an optimal response, and full reflection is compatible with an optimal patrol. The uniqueness clauses explain when alternatives are possible. With odd duration, the zero-holding random walk makes all delays equally good for the attacker. With duration two, a range of reflection probabilities below one remains optimal for the patroller. Those facts distinguish a recommendation that is optimal from one that is forced by the game.
The paper gives arguments for its numbered results, but this mission's Lean theorems are open statements awaiting machine-checked proofs. A completed development would provide a reusable finite-path model of conditional hitting probabilities and a formal game-theoretic treatment of the full delay set. The even-duration interior-maximizer milestone also calls for an analytic proof of a property that the preprint supports with plots. The finite-path and generic saddle-point definitions can be reused outside this particular star network.
The apparently direct comparison of attack delays fails because the patroller's state at attack start depends on surviving the entire waiting period without a return to . The conditional distribution at that start time changes with . Likewise, increasing reflection probability can change both the trajectory and the event on which the payoff is conditioned. A comparison of one-step transition probabilities alone does not establish a comparison of . Exact uniqueness is more delicate still: at the chain alternates between centre and end nodes, creating genuine ties between delays for odd durations. The even-duration argument needs an optimum away from this boundary.
Lean represents the original star as Option (Fin n), with none denoting and some i denoting end node . It builds finite-step taboo path probabilities and defines by the ratio above, rather than by a closed-form solution or by the three-state reduction. The two-player saddle predicate is a separate generic definition; the paper-specific model supplies its strategy types and payoff. The definitions use real probabilities. The conditions , , , , , and are explicit. They make the relevant conditioning event nonempty and ensure the natural-number indices and mean the intended periods.
Lemmas 1–2 count the attack start as and count interception by ; the model instead uses at departure and later transitions from the attack-start state. Lemma 3's printed claim that odd makes delay two uniquely optimal conflicts with Proposition 2 at . The milestone states a corrected strict claim under , for all , and records the discrepancy. Contributions to the model's finite-path identities, the three-state symmetry reduction, the numbered lemmas, the case propositions, and the even-duration interior maximum are all within scope.
Financial networks, supply chains and contact networks share a failure mode: a node fails when enough of its counterparties have failed, and its failure in turn weakens its own counterparties. Threshold contagion on random graphs is the standard mathematical model of this. Amini, Cont and Minca (Resilience to contagion in financial networks, Mathematical Finance 2016) proved that on a configuration-model network the final fraction of failed nodes concentrates, as the network grows, around an explicit value determined by the smallest fixed point of a one-dimensional map.
In that model thresholds are fixed. In practice institutions recover while a crisis unfolds: capital is raised, earnings accrue, and a node that survives long enough can absorb more losses than at the start. Amini, Minca and Sulem (A Dynamic Contagion Risk Model with Recovery Features, Mathematics of Operations Research 2022; the mission follows the authors' preprint of February 2021) add this recovery feature: every surviving node's threshold grows linearly in calendar time, at a rate proportional to its connectivity. The main result, Theorem 5, identifies the scaling limit of the cascade with growth. It is the basis of the paper's analysis of equilibrium connectivity choice (§3), where agents trade off the rewards of links against contagion risk.
A network has nodes. Node has a connectivity (in-degree and out-degree both equal ) and an integer initial threshold . The empirical type distribution is and the mean connectivity is . Two regularity conditions are assumed: (C1) for a probability distribution on ; (C2) .
Each node owns out-going and in-coming half-edges. The directed configuration model matches out-half-edges to in-half-edges by a uniformly random bijection; self-loops and multiple links are allowed.
The cascade: at time the nodes with fail. Interactions happen at times whose gaps are i.i.d. exponential with rate . At each interaction one unrevealed out-link of a failed node, chosen uniformly, is revealed; its counterparty gains one failed link and fails if its count of failed links reaches its current threshold , where is the growth rate. Only surviving nodes grow. The cascade stops at , when no unrevealed failed link remains; is the number of failed nodes and the number of survivors of type .
The limit objects: is the probability that the order statistics of i.i.d. uniform variables on satisfy for ; and, for ,
; and the relaxed fixed point .
With : for every , with high probability . (i) If and for , then in probability. (ii) If is a stable fixed point ( just to the right of ), then
Theorem 5 gives the final size of a cascade with recovery as an explicit function of the type distribution and the growth rate. The paper uses it to define each agent's expected reward as a function of its connectivity and to study the equilibrium of the resulting connectivity game (§3). Without the theorem, the equilibrium analysis would rest on the heuristic of §2.3 alone.
On the formal side, the platform has no random graph model of configuration type, no network contagion process and no fluid limit of a random cascade. This mission introduces all three. The result is proved on paper (by Wormald's differential-equation method); none of it is machine-checked. The work is to formalize the proof, and the milestones are self-contained pieces of it: an order-statistic identity, an explicit ODE solution, an algebraic identification of the limit, a concentration bound for sums of exponentials, and a fixed-point existence result.
The obvious approach is to view the cascade as a Markov chain in the counts of surviving nodes by type and number of failed links, and to apply Wormald's theorem directly. Two things break. First, with growth a node's survival depends on the whole history of its failed-link count, not on its current value, so the state space grows with time: new states become relevant at each growth time , and the fluid limit has to be established inductively on successive time intervals. Second, the cascade stops at a random time, near the first zero of the limiting number of unrevealed failed links. Showing that the stopping time concentrates requires the stability condition on and a truncation of the type distribution in the degree, since may have infinite support. The fixed point need not be a crossing point of a smooth map, so the identification of the stopping time is delicate even when the drift is known.
tsums with summability hypotheses; is nonnegative with total mass .Many allocation problems in online advertising are decisions about order, not only about membership. A search engine that rewrites an incoming query into one of several ad-matching configurations, or a publisher that runs a sequence of ad allocations over a day, extracts revenue that depends on which configurations are used and on the order in which they are applied: advertisers' budgets are spent down along the way, so a configuration run early changes what a later one can earn. Classical submodular set functions cannot express this order dependence, and the guarantees developed for them do not apply directly.
Alaei, Makhdoumi and Malekian (arXiv:1009.4153v4; Management Science, 2021) introduce sequence functions, which assign a value to every finite sequence of actions, and identify a sequence analogue of monotonicity and submodularity under which a simple greedy rule is provably near-optimal. They apply the discrete version to query rewriting in sponsored search and a continuous version to online ad allocation with budgets.
Timeline:
Let be a finite set of actions. A discrete sequence is a tuple with and every ; for it is the empty sequence . Its length is , and denotes the set of all discrete sequences. The concatenation lists the elements of followed by those of . For the refinement is its prefix of length , with .
A sequence is dominated by , written , if can be obtained from by removing some of its elements while keeping the order of the remaining ones. Thus but .
A discrete sequence function is any . The marginal value of appending after is
The function is sequence-non-decreasing if whenever , and (display (10)). It is sequence-submodular if
(display (11)): appending the same sequence gains less after a longer history. Assumption 2 requires both properties.
The optimization problem (12) is, for a length budget ,
For , a sequence is -greedy if at every step its choice is within a factor of the best single-action marginal value (display (13)):
Under Assumption 2, for every , every -greedy of length and every sequence with ,
Applied to the optimum of (12), this is the paper's display (14), .
For sets, the bound of Nemhauser, Wolsey and Fisher is the reference guarantee for greedy selection. Theorem 3 transfers it to sequences: any objective that can be shown sequence-non-decreasing and sequence-submodular inherits a guarantee for a greedy rule, with no further analysis. The paper uses this for query rewriting (Theorem 4) and, through the continuous analogue, for budgeted online ad allocation (Theorem 2). The parameter covers the common situation in which the best next action can only be found approximately, for instance by solving a subproblem with an approximation algorithm.
Theorem 3 is proved in the paper. As far as a search of the Prove2Me catalog shows, no sequence-function model and no sequence-submodular greedy bound has been formalized there; set-function greedy bounds exist on the platform only as separate, set-based statements. This mission produces a machine-checked version of the discrete model and of the guarantee, which later missions on sequence or string submodularity can import.
The set-function argument compares the greedy set with the optimum by adding the optimum's elements one at a time to the current greedy set and using that the union is at least as valuable as the optimum. For sequences the comparison object is , and two features of the order break the direct transcription. First, sequence-submodularity only compares marginal values after a dominated history, so each comparison has to be arranged so that the shorter history is a subsequence of the longer one, in the right order. Second, the averaging over the elements of produces a factor , while the recursion needs the uniform factor ; the replacement relies on feasibility together with nonnegativity of , which comes from monotonicity. A formal proof also has to handle the indices of the refinement and the edge cases , and that the printed argument passes over.
All declarations live in the namespace SeqSubmod.Discrete.
List S over a type S with [Fintype S]; concatenation is ++, the empty sequence is [], and is A.length.List.Sublist (A <+ B), the subsequence order. It is neither the prefix order nor the subset order of the underlying sets.marginal u B A := u (A ++ B) - u A is , with the arguments in the paper's order.H[i] is the paper's and H.take i is . The maximum over is Finset.univ.sup', which needs [Nonempty S]. This is added and harmless: with no actions the only sequence is empty.A trivializing formalization is ruled out: a prefix or subset order, a reversed (11), a dropped , or an existentially quantified would each change the theorem, and none is used.
A complete development needs telescoping sums of marginal values along a list, an averaging argument over a finite sum, the recursion (40), and the inequality , which Mathlib provides. The definitions file is reusable by any later work on sequence functions, including the continuous model of the paper's §3, which is not part of this mission. Proofs of the milestones, alternative proofs of the goal, and tightness examples are all welcome contributions.
A defined benefit pension promises payments whose form depends on a member's employment and retirement status at death, and on the existence and later survival of a qualifying dependent. The same member can generate very different death benefits while employed, after leaving with preserved rights, or after retirement. A scheme may specify a salary-related lump sum before exit, a revalued preserved-rights benefit in deferment, a spouse's continuing pension after death, and instalments under a fixed pension guarantee. Coordination rules determine which payments coincide.
This mission formalises a finite-horizon actuarial contract in which the payable cash amounts and their dates follow explicit benefit switches, rather than being inferred from names such as “spouse's pension” or “death benefit”. The pension and multiple-state foundations are described by Dickson, Hardy and Waters (2020), Chapters 8–11, https://doi.org/10.1017/9781108784184. The contractual rules here are independently defined examples.
Scheme rules and governing documents determine legal entitlement and tax treatment. No salary multiple, spouse percentage, contribution refund or guarantee is universal.
Time is measured in integer anniversary ticks, numbered from valuation time zero. Let be a finite mortality horizon, the employment exit tick and the pension commencement tick. The coherent contract satisfies . A member death-year index means death occurs during and a death-related lump sum is paid at tick . The terminal index denotes no death within the observable horizon. A dependent's corresponding death index is , with the same convention. A same-tick death is treated as non-qualifying; within-year ordering needs a finer model.
The joint mortality law has masses summing to one. At member death , is the probability of a qualifying spouse, conditionally independent of the hypothetical dependent death index given . A spouse qualifies only when , then receives payments while . Eligibility is fixed at death; later mortality is checked at each due date.
An active death has , a deferred death has , and a retired death has . Define benefit amounts , and at settlement for these disjoint regimes. The active benefit can include an optional salary multiple, an accrued-service amount and a contractual refund. The deferred death lump uses preserved annual pension multiplied by revaluation and an explicit pension-to-capital factor measured in years; any contribution refund is a separate cash amount. The retired benefit is a distinct lump-sum rider if the scheme provides one. No component is automatically cumulative with another merely because both appear in the model.
Let be the original member pension payable at anniversary , conditional on the member surviving that date. Let , and be survivor pensions fixed from the death regime, with survivor indexation multiplier . The amounts can reflect salary or service to death, preserved rights, or a fraction of a retirement pension. The main survivor contract pays for ; a separate immediate alternative allows . Amounts are per instalment, with consistent monthly units when required.
A retirement guarantee of ticks covers pension due dates . After a retired member dies, remaining guaranteed member instalments continue to the contractual recipient. Under the parallel rule the surviving spouse also receives its separately payable pension. Under the replacement rule the survivor pension is suppressed while the guarantee remains payable, then resumes when eligible after its expiry. A separate commutation switch can replace all unpaid estate-guaranteed instalments with one lump sum at death settlement, priced using consistent forward discount factors. No guarantee or payment alternative is universal.
Existing joint-life mathematics provides basic survivor occupancy identities. This mission extends them to the three death regimes. For and :
The indicators are pairwise disjoint, preventing multiple death-regime claims.
The second family constructs the realised present value for a full benefit contract from the paid lump sum and the dated instalments. Write for the discount factor to time zero and for the sum of original member pension, qualifying survivor instalment and remaining guaranteed payment under replacement switch . Then
The death lump is zero for the censored member state. The instalment horizon obeys in the root: right-censored members and spouses remain alive at every priced tick. Extension beyond needs a new mortality model.
The principal target establishes an equality between mortality-event valuation and the payment-date component EPVs, together with a second equality accounting for guarantee coordination. With for expectation over the actual member and dependent death cells, for the separately priced death, member, spouse and guarantee payment streams, and for the qualifying retiree-survivor pension suppressed during the guarantee:
The overlap is separately priced using , survivor mortality, death regime and payment eligibility. It is not introduced as a residual defined by subtracting two values.
The event-based formulation follows member status and the amount payable at death. The payment-date formulation uses explicit mortality conditions at each cashflow date, as in the valuation models of Dickson, Hardy and Waters (2020), Chapter 11, https://doi.org/10.1017/9781108784184. Agreement provides an auditable reconciliation between those independently constructed views. Where the spouse receives income while guaranteed member payments continue to an estate, valuing the two promises separately is appropriate. Where a contract suppresses that survivor pension, the overlap term quantifies the adjustment required to prevent charging for both.
Supporting targets cover exit, retirement and guarantee endpoints, and frozen survivor entitlement. Further results mix dependent-age mortality scenarios and value child pensions with an explicit cessation age.
A death benefit calculated from salary or preserved rights at a member's death differs from a pension instalment conditional on living at a subsequent payment date. Moving from a double sum over member and dependent death times to a sum over payment dates must respect that distinction. In particular, multiplying an unconditional probability of marriage at every later instalment would introduce a new eligibility test absent from the contract. The overlap between an estate guarantee and a spouse pension creates a second risk of overvaluation when the intended rule replaces one stream with the other.
Boundary cases are sensitive to strict and weak inequalities. A guarantee ending at has no payment at that endpoint under the due-in-advance anniversary convention adopted here. Same-grid member and dependent death is not automatically resolved by a continuous-time assumption. The project therefore has to distinguish mathematical cashflow identities, genuine survival-law properties and scheme-specific premises throughout its theorem graph.
Lean 4 represents joint death-year cell masses and real-valued finite sums with targeted Mathlib imports. It supports arbitrary dependent-life mortality associations and user-supplied discount factors, salary schedules, preserved rights, revaluation multipliers and survivor indexation. Salary multiples, contribution refunds, deferred benefit valuations and retirement lump sums are switches or amounts supplied by a contract. The retirement guarantee has zero, parallel and replacement regimes. Payment streams may be represented on a finer integer grid to accommodate monthly schedules, but no mathematical identity in the annual kernel asserts exact continuous-payment equivalence.
The principal theorem assumes a normalised joint mortality law, , and . The event-to-payment equality follows from explicit realised payments, not a vacuous equality hypothesis, independence assumption or constant-rate restriction. It relies on genuine death-year and survivor eligibility indicators, rather than stipulating valuation equality in the hypotheses. Continuous-time integration and stochastic marital-history transitions remain future extensions. Finite spouse age-difference mixtures and age-limited child payments are included as separate supporting results. Statutory GMP/excess floors and pension tax rules are outside the contractual core until a scheme type and applicable legal basis are separately verified.
We develop a theory of exact transmission of finite-dimensional -algebras through quantum channels. These algebras describe hybrid classical-quantum information, allowing the dimension of the quantum system to depend on the classical message. Allowing arbitrary encodings and decodings yields a transmission set of algebra types, ordered by embedding, that unifies zero-error information theory with operator-algebraic error correction. We ask if this set admits a dominating algebra into which every transmittable algebra embeds. Our central finding is that domination can fail even in small dimensions. In its absence, several incomparable maximal algebras can describe different optimal uses of the same channel, forcing the user to select one depending on the operational task and the type of information to be preserved. We introduce hybrid capacities that reconstruct the only possible dominating algebra type and present a complete finite characterization of domination using minimal forbidden algebra types. We identify dominating algebras for channels whose operator systems are graph-isomorphic to -algebras, including highly divisible channels, and for channels with zero one-shot zero-error quantum capacity. Under tensor products, we prove that joint coding can produce new algebra types, giving an algebraic analogue of superadditivity from Shannon theory. Domination can fail for the joint use of two channels, even when both channels separately admit dominating algebras. Finally, we construct a channel whose -fold tensor powers have doubly exponentially many maximal algebra types, attaining the largest possible growth scaling for finite-dimensional channels. Consequently, new transmittable algebra types appear at arbitrarily large block-lengths for this channel, so its full transmission structure cannot be generated from any finite collection of bounded-block-length codes. △ Less
This mission is the statement-level formalization of Transmitting algebras through quantum channels (arXiv:2609.40054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main nonexistence result; Example 4.2 and (4.3) (Main nonexistence result; Example 4.2 and (4.3), PDF p. 30). 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Many systems studied in operations research and reinforcement learning are modelled as finite Markov chains with a large number of states : the stops of a taxi in a city, a random walk on a network, the conformations of a molecule. Estimating the transition matrix from one observed trajectory needs, in general, a trajectory long compared with the unknown entries. In many such systems the transition matrix has, at least approximately, a small rank : the observed chain is driven by a low-dimensional latent process, as in state aggregation, where (Zhu, Li, Wang & Zhang, arXiv:1907.00113, §1.1). Zhu, Li, Wang and Zhang show that a low-rank transition matrix can be estimated from a trajectory whose length is proportional to (up to logarithmic factors), and they give two maximum-likelihood estimators with explicit rates. This mission formalizes the rate of the second, rank-constrained, estimator in Kullback–Leibler divergence.
Let be a Markov chain on the states with transition matrix (, , ) and stationary distribution (). The chain is primitive (some power of has all entries positive), and is drawn from . Write and .
The right spectral gap is , where, with and the adjoint ,
The KL divergence of a transition matrix from is . From the trajectory, counts the transitions , and the averaged negative log-likelihood is . The empirical KL divergence is .
Assumption 1 of the paper: , and for constants . The -minoration (Remark 2) removes the : for all . The rank-constrained MLE (5) is any
In Lean these objects are IsStochastic, IsStationary, IsPrimitive, piMin, piMax, trajProb, rhoPlus, klDiv, negLogLik, empKL, Assumption1, Minorated, RankFeasible and IsRankMLE in the namespace LowRankMarkov.RankMLE.
There are universal constants such that, for , under minoration with and , every rank-constrained MLE satisfies, for all ,
The constants are not fixed numerically, so a sharper analysis does not invalidate the goal.
The bound says that, with high probability, the KL error of is of order up to the factors and , plus a term independent of controlled by . A trajectory of length of order , rather than , therefore suffices: the low rank is what makes the estimation problem sample-efficient. Lemma EC.1 converts the KL bound into a Frobenius-norm bound, and Lemma 3 is a uniform law for the empirical KL process of a dependent sequence over the paper’s cone class.
The result is proved in the paper; nothing in it has been machine-checked. The mission asks for a formal proof of the KL display. Two points need care beyond transcription: the printed hypotheses do not suffice (see Formalization scope), and the paper's proof of Lemma 3 symmetrizes the dependent summands as if they were independent (EC.8), so a formal proof must supply a valid argument for that step.
Comparing with is immediate; the difficulty is to control uniformly over a non-convex set of matrices, from one dependent trajectory. A union bound over a net of the feasible set loses polynomial factors in , and i.i.d. empirical-process tools do not apply directly to a Markov chain. The printed Lemma 3 covers the cone class , while the appendix proof restricts its shells to rank- matrices. This leaves a gap for matrices in of higher rank and for the claimed application to when . The paper combines a tail inequality for suprema of empirical processes of Markov chains (Adamczak 2008), a contraction step, the matrix Freedman inequality (Tropp 2011) for a matrix martingale, and a Bernstein inequality for Markov chains with a spectral gap (Jiang, Fan & Sun 2018) for the quadratic variations . None of these is in Mathlib.
States are Fin p, matrices Matrix (Fin p) (Fin p) ℝ, logarithms natural. A trajectory makes transitions, and its probability is ; probabilities of events are finite sums, so no measure theory is needed. is a real sSup; "" is not built into its definition. The nuclear and Frobenius norms come from the published definition CaiCandesShen.Convergence.Basic.
Hypotheses fixed relative to the page:
The statements rule out trivializing readings: are quantified before all data; the goal holds for every selection of minimizers, not for one fixed estimator; and exclude the junk values and that would collapse the thresholds; a sorry-free check shows the goal's hypotheses are jointly satisfiable (, uniform , ).
Not posed: Theorem 1 (nuclear-norm MLE), the Frobenius display of Theorem 2 (Lemma EC.1 turns the KL threshold into twice the printed Frobenius threshold, so the paper's one-line derivation gives ), Theorem 3 (lower bound), and the DC-programming results of §4. Useful reusable contributions: a Bernstein inequality for finite Markov chains with a spectral gap, the matrix Freedman inequality, and the reverse-Pinsker bound of Lemma EC.1.
Firms that already buy a service from an incumbent supplier regularly re-source the contract: they invite new suppliers, the entrants, to compete in a descending open-bid auction. Entrants may be cheaper but are unproven: before the contract can be awarded to an entrant, the buyer must pay for qualification screening (visits to the supplier's facility, purchasing and testing sample products), and an entrant passes only with some probability. Industry practice splits into screening every entrant before the auction (pre-qualification) and screening only the winner after it (post-qualification). Zhang, Chen and Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6), 2021, compare the two formats in equilibrium.
In the post-qualification format (POST), the incumbent needs no screening, so he faces a genuine dynamic decision: as the clock price falls and entrants drop out, when should he quit? His drop-out price determines the buyer's procurement cost in POST, and Theorem 2 of the paper characterizes it completely. This mission formalizes that theorem.
Costs lie in an interval . The incumbent's cost is . There are entrants with i.i.d. costs of density and c.d.f. , supported on . Screening one entrant costs the buyer , and an entrant passes with probability . In POST, the clock descends from ; when the incumbent drops out at price , the price jumps down by the decrement , and the incumbent ends up with the contract at price only if all remaining entrants fail screening. The paper assumes and Assumption 1: is nondecreasing and convex.
Before the incumbent quits, an entrant with cost stays until the price reaches his effective cost . With entrants left at price , the highest remaining entrant cost therefore has c.d.f. and density . Writing , the incumbent's value solves the Bellman system (8)–(10):
Here is the planned drop-out price. The integral covers the event that an entrant drops out first, at price ; the second term covers the event that the incumbent quits at and all entrants then fail screening.
Theorem 2 introduces four objects. is the floor of the minimum over of . The compete threshold is the first price at which falls below . The switching price is the least price above at which quitting is worth as much as competing down to . The candidate drop-out rule is .
For all , and :
and . The goal also asserts that are well defined and satisfy . It asserts the monotonicity of part (i): and are nondecreasing in , is nonincreasing in , and is nonincreasing in and nondecreasing in . Finally, is nondecreasing in and and nonincreasing in .
The proof in the e-companion (pp. ec5–ec11) provides the milestones, in attack order:
The theorem turns an infinite-horizon-looking stopping problem into a compete-or-fold rule. Either the incumbent stays in until the price falls to the threshold , or he drops out immediately. The choice depends only on how many entrants remain and on whether the price is above the curve . With Lemma 2 and Theorem 1 (the entrants' strategies), this completes the equilibrium of POST. The paper's comparison of POST and pre-qualification, and its closed form for the buyer's expected cost, both rest on this equilibrium.
The result is proved in the paper; it has not been machine-checked. A formal proof would check a long argument with an intricate induction: Lemma EC.2 interleaves the strict monotonicity of with the monotonicity of in and . It would also check the treatment of the boundary case , where the proof appeals to the convexity in Assumption 1.
The obvious argument differentiates in and reads off the sign. That fails because the derivative involves , which is itself the value of an optimization. Its sign is controlled by the explicit function only after an induction on shows that has the form wherever it matters. The induction must carry the ordering of , and across different and (Claim EC.1) at the same time. Another difficulty is that must be evaluated beyond the current price: is defined at the reference price and may exceed .
All prices and costs are real numbers, and is a natural number with . The standing assumptions (including Assumption 1) are hypotheses of every statement. One hypothesis is added to the page: is positive and continuous on . The page's own formulas divide by and differentiate (9) in . is defined as , not taken as a parameter, and is the integral of .
The max in (8) is a real supremum over the compact feasible interval; that it is attained is part of the goal. The integral in (9) is a signed interval integral, so is given by (9) for as well. The minimum defining is read as an infimum over , because the ratio has a zero denominator at . The page's is taken over the reals. "Optimal drop-out price" means a maximizer in (8): at two maximizers exist, so uniqueness would be false. The derivative (EC.7) is stated away from the kink . Milestones use the open price domain the proof uses.
The game-theoretic layer is not modelled. The hypothesis "entrants follow Lemma 2 and Theorem 1" is how the page derives (8)–(10), and the statement is about (8)–(10). A formalization that states only the sign pattern of or the inductive hypothesis would be trivializing; the goal states optimality of in (8) for every , , , together with part (i).
A development needs differentiation under a parametrized integral (the fundamental theorem of calculus for ), continuity of in , and real-analysis facts about convex functions crossing a line. These are reusable for other auction and optimal-stopping models. Proofs of any milestone are welcome, as are proofs of the fold-only case independently of the compete case.
Restaurants, clinics and amusement venues that announce a waiting-time standard compete not only on price but on how unpleasant the wait feels. Waiting-area entertainment (a piano player, a television, a play area) lowers the perceived cost of waiting, and when several providers sit in one service cluster, a food court, a mall, a strip of restaurants, a single entertainment option can serve all of their customers at once. Yuan, Dai, Chen and Gavirneni (MSOM 2021) model this choice and ask when providers that compete on price but jointly fund entertainment, a form of co-opetition, do better than a single provider serving the market alone.
The model builds on the waiting-time-standard and volume-based capacity framework of Allon and Federgruen (Operations Research 2007) and on linear cost-allocation schemes of the yardstick type. Its central comparison concerns the even cost split: does sharing the entertainment bill outweigh the margin lost to price competition?
Customers arrive at a provider as a Poisson stream and the service time is exponential. With service fee and entertainment level , a local monopolist faces the arrival rate
where is the maximum demand rate, the price sensitivity, the waiting cost per unit time, the announced waiting-time standard and the effectiveness of entertainment. Entertainment costs with . To keep the expected wait at the provider buys service rate at marginal cost , so its profit is
The monopoly profit is the greatest value of over , .
Under co-opetition two symmetric providers share one entertainment level. Write , , margins , a price-competition intensity and . Provider 's arrival rate is . The cost is split by with cost-sharing factor , and provider earns
Providers first set margins simultaneously; then they jointly choose to maximize . A symmetric equilibrium has , jointly optimal at , and no deviation , followed by the joint optimum it induces, raises a provider's profit. The equilibrium profit is . Throughout, the parameters satisfy and .
With an even split () there is a threshold such that, for every and every symmetric equilibrium at ,
No value of is fixed: the goal asserts only the threshold shape of the comparison.
and . 2. Proposition 3(i) at . A symmetric equilibrium exists, and every one satisfies
The result separates two effects of clustering. Sharing one entertainment option halves each provider's cost, which supports a higher entertainment level and more demand; price competition erodes margins. Proposition 7(ii) says that, under an even split, the comparison with a local monopolist is decided by a single cut-off in the competition intensity, which is what lets the paper conclude that co-opetition can restore monopoly profit levels when competition is mild, and it is the reference point for the paper's analysis of unequal cost-sharing rules (Propositions 6 and 8) and of the design of cost allocation.
The paper's proofs sit in an online supplement; no machine-checked proof of any of these statements is known. Formalizing them produces a verified analysis of a two-stage game with a joint second stage, including the existence of the symmetric equilibrium, which the paper uses but which requires a global, not first-order, argument.
The co-opetition equilibrium is defined by a two-stage game: a price deviation changes the jointly chosen entertainment level, so a provider's payoff as a function of its own price is a composition with an argmax and need not be concave. Verifying that the first-order point of Proposition 3 is a global best response, and that every symmetric equilibrium satisfies the first-order conditions, is the step a direct first-order computation does not deliver. The threshold of Proposition 7(ii) then requires comparing an implicitly defined equilibrium profit, through its root equation in , with the implicitly defined monopoly optimum, and showing that the difference changes sign exactly once in ; monotonicity of alone does not give a sign change.
Everything is real-valued. Prices are encoded by margins , for the equilibrium and for every deviation, matching the page's domain . The joint entertainment stage maximizes over , and a deviation is evaluated at every joint optimum it induces. is any greatest element of the set of monopoly profits over , . The goal and milestones fix ; Proposition 3 for is out of scope.
Disclosed conventions: the capacity bound is the strict instead of the page's (at equality a degenerate profile with zero margins and no entertainment makes both profits equal to and falsifies the strict clause); the demand is read as , as in §3 and Proposition 3(ii), since the §4 display double-counts ; the cost share is read as , the first of the page's two inconsistent forms (they agree at ); "decrease" is strict; "the opposite holds" is the strict .
The goal is stated about genuine equilibria of the game and the genuine monopoly optimum. Replacing by the closed form of Proposition 3, or by the formula of Proposition 1, would turn the goal into a one-variable real-analysis fact and is not the paper's statement.
A complete development needs: the monopoly first-order analysis (joint concavity on , ); strict concavity of the joint second stage for positive total margin; the envelope argument for a provider's deviation; existence of a symmetric equilibrium; implicit-function comparative statics in . Lemmas on implicitly defined roots of type equations are reusable. Contributions of intermediate lemmas, including the existence of the equilibrium, are welcome.
Many financial assets (corporate and municipal bonds, swaps, asset-backed securities) trade over the counter (OTC): there is no central exchange, and a trade requires that a buyer and a seller find each other. Empirically, a large share of OTC volume passes through intermediation chains, in which an asset moves from the original seller to the final buyer through several dealers. Search-theoretic models explain how such chains form. Duffie, Gârleanu and Pedersen (2005) introduced continuous-time search and bargaining in OTC markets, and Hugonnier, Lester and Weill (2016) let investors' valuations take a continuum of values, so that dealers emerge endogenously as the investors with intermediate valuations.
Shen, Wei and Yan add a search cost: an investor who looks for a trading partner pays a flow cost . Investors with extreme valuations then prefer to stay out of the market, and participation becomes an equilibrium choice. The paper's Theorem 1 is the foundation of everything that follows in it: every proposition on chain length, trading volume, price dispersion and welfare is stated "in the equilibrium of Theorem 1".
Time is continuous. A continuum of investors of total mass trades an asset in supply , with ; each investor holds or unit, and the asset pays a coupon of per unit of time. An investor of type values the coupon at . Types are redrawn independently at intensity from a probability density on with c.d.f. . Everyone discounts at rate .
A non-owner either stays out or searches to buy; an owner either stays out or searches to sell. Searching costs per unit of time. Write for the densities over types of buyers, sellers, inactive non-owners and inactive holders, and , . A buyer meets sellers at rate and a seller meets buyers at rate , with .
Let be the values of the four activities, and . When a type- buyer meets a type- seller, the surplus is
they trade iff , and the buyer, with bargaining power , pays .
For cutoffs , , non-owners search to buy iff and owners search to sell iff . A steady-state intermediation equilibrium (Definition 1) consists of cutoffs , densities satisfying the flow balances (12)–(18) and market clearing (19), and value functions solving the Bellman system (8)–(11) under which these cutoff rules are optimal. Types in are the intermediaries: they search to buy when they hold nothing and search to sell as soon as they hold the asset.
There is an explicit threshold , built from the right-hand sides of the cutoff equations
with , the explicit functions (66), (64) of , , such that for
a steady-state intermediation equilibrium exists, and every such equilibrium has cutoffs equal to the unique roots of (20) and (21), densities (55)–(63), value functions (79)–(82), and the trade rule "trade iff " with prices (6).
The milestones follow the paper's proof. Step I solves the flow equations for given cutoffs: (55)–(57), (61)–(63), the populations (64) and (65)–(66), and the densities between the cutoffs (58)–(60), together with the existence of the steady state. Step II derives the slopes (77)–(78), the value functions (79)–(82), the trade rule (83)/(7), the cutoff equations (20), (21) with their unique roots, and the threshold (84). Step III shows that the cutoff rules are optimal for the closed-form values.
Theorem 1 gives a closed-form description of an OTC market with endogenous participation and an endogenous dealer sector. The search cost splits the population into three groups (passive low types, intermediaries, passive high types), and the length of intermediation chains, trading volumes and price dispersion are all computed from the explicit densities and value functions. Every comparative-statics result of the paper (for example, that a lower search cost lengthens chains) is a statement about the equilibrium this theorem constructs.
The result is proved in the paper, with gaps: the verification of the trade rule outside the dealer region is called "straightforward", Step III treats one of four cases, and uniqueness of the solution of the Bellman system is not argued. No part of it is machine-checked. The mission asks for a complete formal proof, and its definitions give a reusable Lean model of a continuous-time search-and-bargaining steady state with endogenous participation, which no existing formalization provides.
Step I is not just algebra. Between the cutoffs, the flow equation (18) couples each density with integrals of the others, and its solution comes from a Riccati-type equation for . As printed, the densities (59)–(60) do not solve it. Step II differentiates parametric integrals of the positive part of the surplus, which needs the monotonicity of before that monotonicity is proved. That uniqueness is the main gap: the paper takes it for granted. Monotonicity of the right-hand sides of (20)–(21) in the cutoff rests on decreasing and increasing, which is asserted, not shown. The obvious approach, plugging the closed forms into Definition 1, gives only existence; uniqueness requires showing that every solution of the flow equations and of the Bellman system is the closed-form one.
All quantities are real numbers; is written lam and is Δbar. The standing assumptions are , , , , and a probability density on (nonnegative, integrable, total mass ); and . The densities are required to be nonnegative and integrable, and the value functions bounded and measurable on , so that no integral takes Lean's default value .
The equilibrium predicate is Definition 1 itself: flow equations (12)–(19), Bellman system (8)–(11) multiplied through by , and optimality of the cutoff rules ( below , above, and likewise for owners). The closed forms are separate definitions, and is defined from (20)–(21) as the common value of their right-hand sides at the crossing point; it is never a parameter. A formalization that defined the equilibrium by its closed form, or took as a hypothesis, would make the goal trivial and is excluded.
Corrections and conventions, all disclosed in the items:
The definitions are split into a model module (parameters, steady state, Bellman system, optimality, equilibrium, prices) and a closed-form module (, , the cutoff equations, , densities, slopes, value functions). The model module is reusable for the paper's later results (trading volumes, chain length, comparative statics in , , , ) and for the non-intermediation equilibrium of its Theorem 2. Proofs of individual milestones, and lemmas on the monotonicity of , and of the cutoff equations, are welcome as separate contributions.
Collaborative projects often assign different tasks to different firms while making each firm bear part of the cost of a late project. A supplier's decision to spend more time on its task can therefore impose delay costs on a manufacturer, and the manufacturer's own schedule can impose costs on the supplier. The incentives differ from those of one firm controlling the whole schedule. Song, Zhao, and Xu study this tension in a two-stage project and ask whether knowing the other firm's costs always improves the final schedule. Their answer includes a precise case in which the project finishes sooner when the supplier does not know the manufacturer's cost type. The held source is the authors' SSRN preprint, §§3–5.1 and Theorem 6; it was later published in Manufacturing & Service Operations Management.
The question matters for partnerships in which task costs are private but delays affect all participants. In such a setting, a change in information can change the supplier's first move, even though the manufacturer's final decision still responds to the work already done. The result concerns project duration, a directly observable outcome, rather than an abstract welfare comparison.
A serial project has one supplier task followed by one manufacturer task. The supplier is firm 1 and moves first. The manufacturer is firm 0, observes the supplier's action, and moves second. Each action is either keep (), retaining the benchmark task duration, or delay (), adding one period to that task. The project's delay relative to the benchmark is the number of delayed tasks: zero, one, or two periods. The paper considers this deterministic-duration setting under Assumption 1(b) and Condition 2 (preprint, pp. 10–12).
Firm saves in direct cost when it delays its own task. The first period of project delay incurs a shared penalty ; the second adds . The subscript identifies the firm that pays a share, and the superscript identifies the period of project delay. Each firm pays its share whenever the project is late, regardless of which firm caused the delay. For example, the profile gives the supplier payoff and the manufacturer payoff , while gives and . These are the payoffs in Figure 5b (preprint, Appendix p. 1).
Under symmetric information, both cost types are known. The outcome is a subgame-perfect equilibrium: the manufacturer chooses a best response after either supplier action, and the supplier chooses its preferred first action in light of those responses. Under asymmetric information, the supplier instead has a belief over possible manufacturer types. The belief assigns masses , , and to types with low, medium, and high savings relative to their two penalty shares. The supplier maximizes its expected payoff under that belief. The actual manufacturer, whose type need not coincide with the supplier's guess, still acts after seeing the supplier's choice (preprint, Assumption 2, p. 16).
The goal is the paper's Theorem 6. Let the two equilibria use the same supplier type and the same actual manufacturer type. Write and for their respective project delays. Away from payoff ties, the mission asks for the exact characterization
The milestones establish the manufacturer's dominant actions (Lemma 2), the supplier's action against manufacturer best responses (the supplier clause of Lemma 2), the five symmetric equilibrium cases (Theorem 2), and the asymmetric supplier decision threshold (Theorem 5). The final milestone is the paper's observation that only Case 2 of the symmetric equilibrium table can lead to a strictly shorter project under asymmetry. Their statements and indices come from the held preprint, pp. 12 and 17 and Appendix p. 5.
The characterization identifies exactly when less information changes a one-period symmetric outcome into a zero-delay asymmetric outcome. In the relevant regime, the manufacturer would keep after either supplier action. The information change matters because the supplier's belief may make keeping its own task more attractive than it is when the manufacturer's low-saving type is known. Outside the stated regime, the same model does not yield a strictly shorter project through this information change. This bounds the paper's counterintuitive claim to explicit, checkable cost and belief conditions (Theorem 6, p. 17).
Song, Zhao, and Xu prove the result in the paper. The mission's Lean statements are compiled, but the theorem proofs remain open. Formalizing them would create a machine-checked account of the complete two-stage game, its equilibrium predicates, and its belief-dependent outcome comparison. The general sequential-game interface and the finite-belief representation can support other small extensive-form games; the project payoffs and time-dependent risk-sharing conditions are specific to this paper. Contributions to the equilibrium lemmas, the belief threshold, and the final comparison are all useful.
One cannot compare the supplier's actions while holding the manufacturer's action fixed. The manufacturer responds after observing what the supplier did, and a medium-saving manufacturer changes its response between and . Nor can one infer the actual manufacturer's response solely from the supplier's belief: believed types determine the supplier's expected payoff, while the actual type determines the second move. These two dependencies make a simple comparison of isolated payoff entries insufficient. The strict case table also omits ties, and the paper's “keep otherwise” at the belief threshold requires care when an equilibrium is defined by weak payoff maximization.
Lean represents savings and penalty shares by real numbers, actions by a two-constructor type, and project delay by a natural-number count of delayed tasks. Assumption 1(b) and Condition 2 are bundled in a standing predicate: , , , and . Positive savings are explicit, as required by the paper's cost interpretation and used in its proof of Lemma 2. A separate genericity condition excludes equality at the four individual payoff thresholds. The goal also excludes : at that tie the paper's printed Theorem 6 and Theorem 5's “keep otherwise” convention do not determine the same strict if-and-only-if claim under weak best response.
The belief has finite support, nonnegative weights, and total weight one. Its class masses are computed from those types; they are never free probability parameters. Believed types satisfy Assumption 2's class ordering, but need not satisfy Condition 2's global-optimum inequality for the actual project. The actual manufacturer's type need not be in the belief's support. Symmetric and asymmetric equilibria are predicates over complete strategies, and the target quantifies over their outcomes. Theorem 5 uses a payoff-based decision rule that selects keep when expected payoffs tie, matching its “keep otherwise” clause; the goal excludes that tie. Defining the symmetric outcome by Theorem 2's table or the supplier's asymmetric action by Theorem 5's threshold would erase the mathematical content, so both are derived from the payoffs.
Patrolling protects a border or facility perimeter against an intruder who needs uninterrupted time to complete an attack. The defender controls when patrollers pass; the attacker controls when to strike. In a patrol game, the question is how to time patrols when the attacker can observe them (Lin, Optimal Patrol of a Perimeter).
An observing attacker can wait until a patroller has passed before starting. Lin's result shows that a randomised schedule still gives the defender the same optimal detection probability as against a blind attacker, in closed form.
Fix three parameters: a dispatch rate , an attack duration and a detection probability .
Defender. A pure strategy is a nondecreasing sequence of times in at which patrollers pass a fixed location. With the number of patrollers dispatched by time , the sequence is feasible if it satisfies condition (1) of the paper,
A mixed strategy is a probability measure on sequences under which almost every sequence is feasible.
Attacker. The attacker chooses an operating window with , watches the patrollers go by, and at a time of his choosing starts an attack that occupies and must end by . The choice of may depend on everything observed up to and including time : it is a stopping time of the arrival process.
Payoff. Each patroller passing during the attack detects it independently with probability . If the attack meets patrollers it escapes with probability , so the detection probability of against is
The defender moves first and maximises; the attacker responds and minimises. This Stackelberg game is . Its value is (2):
The claimed optimal schedule puts blue patrollers deterministically at , with , and . It puts a red patroller at each independently with probability . When is an integer there are no red patrollers, and the blue ones pass at fixed intervals of .
For all , , :
Items 2 and 3 state , attained at .
The result. Watching the patrollers gives the attacker no improvement in the game value. The value interpolates at , giving a closed-form trade-off between patrol rate, attack duration and detection reliability. The same schedule supports the paper's Theorem 3 (invisible patrollers) and Theorem 4 (a whole perimeter).
Formalizing it. The paper proves the result; this mission seeks a machine-checked proof. The development must specify the attacker's information, almost-sure feasibility of the random schedule, and the converse. It also supplies a reusable model of continuous-time patrol games with adaptive attackers.
For a fixed window, the blue count is fixed and its red slot is independent. An observing attacker instead chooses a stopping time from past arrivals. The proof must account for which red slots he has seen. The half-open window matters: with , an attacker starting at an empty red slot meets only patrollers.
The converse is harder because a feasible mixed strategy may have infinite expected count in every window even when each path has rate . An argument based only on the expected count therefore fails.
Lean namespace PerimeterPatrol.Visible. Schedules are maps (patroller passes at ) with the product -algebra. Feasibility requires Monotone s, , and the limit (1) along atTop, with counts given by Nat.card. A mixed strategy is an IsProbabilityMeasure that is almost surely feasible. The attacker's information up to time is the -algebra generated by the counts , . An attack is a start-time rule with a fixed window , , such that is measurable for that -algebra for every . The detection probability is a Bochner integral of a -valued function. is the pushforward of i.i.d. uniform draws on , with the red patroller at present iff the -th draw is below .
Conventions committed to:
Nat.floor and Nat.ceil, exact for positive arguments;The attacker class includes measurable adaptive stopping times; the optimal schedule must be a probability measure; and the value is characterized through the two game inequalities rather than an unrestricted real supremum or infimum.
Needed infrastructure: counting functions of nondecreasing sequences, the stopping-time and independence argument for the red slots, the strong law of large numbers (Mathlib's ProbabilityTheory.strong_law_ae) for the long-run rate of , and an averaging argument over start times for the converse. The counting and stopping-time lemmas for point processes on are reusable beyond this mission. Proofs of any milestone, and alternative routes to the converse, are welcome.
Not formalized here: Theorem 3 (p. 9) as a separate item, Theorem 4 (the perimeter game, p. 10), Theorem 5 (the finite-horizon simultaneous game, p. 11) and the remarks of §2.1 and §5.
Every day a hospital ward with a fixed number of beds decides which patients go home. Sending a patient home early frees a bed for the next admission, which matters when the ward is congested and arrivals board in the emergency department or elective surgeries are cancelled. Sending a patient home too early raises the chance that the patient is readmitted, which is costly for the patient and, under the U.S. Hospital Readmissions Reduction Program, for the hospital. Shi, Helm, Deglise-Hawkinson and Pan (SSRN 3202975; Operations Research 2021, doi:10.1287/opre.2020.2044) model this trade-off as a Markov decision process over a census of patients indexed by class and length of stay (LOS), fit personalized readmission-risk curves to hospital data, and implement the resulting discharge policy at a partner hospital.
The structural question behind their policy is who to discharge first. Hospitals usually rank patients by their current, absolute readmission risk. The paper's Theorem 2 (p. 15) instead ranks types by how fast that risk falls with a further day of stay: a type whose risk curve is flatter from now on should be discharged before a type whose risk is still dropping quickly. This mission formalizes that ranking result, in a corrected form.
There are patient classes and a maximum length of stay . A type is a pair of a class and a LOS . A state counts the patients of each type, and the census is . A discharge action counts the patients of each type sent home. Class has a minimum LOS , and an action is feasible at when (3), for (4), and every patient at LOS leaves.
Between two daily decision epochs and , new patients and readmitted patients arrive at LOS , and every patient who was not discharged ages by one day: (5) and (6). Each epoch costs the holding cost for beds (7), plus the discharge cost (8), where is the readmission risk of a class- patient discharged at LOS and is the readmission penalty. Each risk curve is continuously differentiable and nonincreasing in the LOS.
Strong dominance (Definition 1, p. 14): iff
Writing for one discharge of type , a schedule with trajectory over a horizon has total cost .
For an initial state, an arrival path and a horizon , let with , and . Then every feasible schedule has a feasible schedule with such that, for all ,
Since the feasible schedules are finitely many, some optimal schedule discharges a patient only after all patients.
Theorem 2 is the paper's main structural result. It turns a high-dimensional MDP, whose state is a census over types, into a ranking problem: once types are ordered by strong dominance, the remaining decision is how many patients to discharge (Corollary 1, p. 16), which the paper then approximates with a univariate linear-quadratic heuristic (§5). The ranking also has a direct operational reading: discharge by marginal, not absolute, readmission risk.
No machine-checked version of this result exists. Formalizing it settles exactly which hypotheses the interchange argument needs. Doing so already exposed that the statement as printed is false (see Difficulty), so the mission's output is the corrected theorem with a checked proof, together with a reusable finite-horizon, pathwise model of class-by-LOS patient flow.
The obvious argument is a single interchange: if a patient is discharged at epoch while a patient stays until a later epoch , swap their discharge epochs. The census path does not change, and Proposition 2 shows the discharge cost does not increase. The step that fails is the one the paper defers to Appendix B.3: the dominated patient, kept from to , may pass the maximum LOS before , and then the swap is not available. The appendix's repair does not close the gap. With , , , , no arrivals, , and one and one patient on day , we have , yet the unique optimum discharges the patient alone (cost 1013), and every schedule that obeys the rule costs at least 1014. The added hypothesis guarantees that the dominated patient can wait as long as the dominating one, so the swap always exists.
The remaining difficulty is bookkeeping: the interchange changes two cohorts by over an interval of epochs, and feasibility (counts, minimum LOS, forced exit at ) must be checked along the new trajectory. Repeated interchanges must also be ordered so that fixing one epoch does not break an earlier one.
Fin M, LOS indices Fin (J+1), counts natural numbers, costs real numbers. Epochs start at . Arrivals, new and readmitted, form one exogenous deterministic path, as Remark 4 (p. 12) prescribes for §4. Every statement is pathwise on a finite horizon , the setting of the paper's interchange argument. The long-run average cost (9) is not used, since a finite interchange cannot change it.deriv with the absolute values of (15).intervalIntegral.integral_eq_sub_of_hasDerivAt) and monotonicity of integrals are the analytic substrate for Proposition 2. The trajectory and interchange lemmas about class-by-age cohorts are reusable for other census models. Proofs of any milestone are welcome independently.Not formalized: Theorem 1 (existence of an average-cost optimal policy), Corollary 1 (threshold form), Propositions 1 and 3, and Lemma 1.
Flow networks model the movement of material, traffic, electricity, or gas through connected systems. In many such models, the required net flow at each vertex varies with a parameter, so the object of interest is a whole family of optimal flows rather than one solution. When edge costs are nonlinear, solving a new optimization problem for every parameter value gives no finite description of that family. Joachims, Klimm and Warode study two approximations of this parametric problem: one approximates each edge's marginal cost, and the other interpolates selected optimal flows. This mission concerns their marginal cost approximation result, Theorem 5.
The paper builds on an exact method for piecewise quadratic edge costs by Klimm and Warode. A piecewise linear approximation of each marginal cost has a piecewise quadratic integral, so it brings general convex costs into the class handled by that method. The question is how fine the linear interpolation mesh must be for the resulting flows to be close to optimal under the original costs. The paper gives local step size bounds involving the second derivative of each marginal cost. The target here is a corrected version of that guarantee, with the precise corrections stated below.
A network consists of finite sets of vertices and edges . Every edge has a tail and a head. The graph is strongly connected and has neither self loops nor parallel directed edges. For an edge flow , its net inflow at a vertex is the sum of flows entering that vertex minus the sum leaving it. Two balanced demand vectors determine a demand for . A flow is feasible when its net inflow equals that demand. In the directed case all edge flows are nonnegative; in the undirected case their signs are unrestricted.
Each edge has a marginal cost that is strictly increasing, differentiable, nonpositive on negative arguments, and nonnegative on positive arguments. Its edge cost is . The total cost is the sum of edge costs, and is the minimum total cost of a feasible flow at parameter . These sign conditions make the edge costs nonnegative. The paper calls them homogeneous marginal costs, although this is a sign condition rather than algebraic homogeneity. Section 5.2 gives the model and its approximation criterion.
For each edge, choose a strictly increasing mesh from to , where
The linear spline joins the values of at adjacent mesh points by straight chords. The minimum cost flow function for these spline marginal costs is tested under the original costs: . This convention is essential because a small optimal cost for the spline instance alone says nothing about the cost under .
The milestones follow the paper's argument in order.
The goal is the corrected Theorem 5. It states that either of the paper's two explicit step size regimes, involving , , , and , makes the spline instance's minimum cost flow function satisfy
The first regime bounds each step by a local maximum of and the magnitude of at a mesh endpoint. The second adds monotonicity and sign conditions on and uses its endpoint values. The formal theorem retains the constants , the factor in (18), and both distinct denominators in Theorem 5. Theorem 5, pp. 17–18 is the source for the exact formulas.
The guarantee applies to an entire interval of demand parameters. It converts local numerical accuracy of the marginal cost splines into a bound on the original total cost at every parameter value, while preserving feasibility. The edge flow bound explains why it suffices to approximate marginal costs on a finite interval even when edge flows are otherwise real valued.
The paper proves the intended result by a paper argument, but its printed Theorem 5 has a counterexample when a mesh crosses zero without including zero: the spline can lose the marginal cost sign condition, and at zero demand the spline optimum can have positive original cost while the true optimum has cost zero. The corrected goal records a valid target for machine checked proof. Formalizing it also yields reusable definitions of finite flow networks, convex separable edge costs, parametric approximation, and chord splines. No machine checked proof of this theorem is claimed by this mission.
Pointwise closeness of marginal costs does not directly compare the two optimized flows, which may differ on every edge. A direct comparison at the spline optimum must also account for the original optimum and for how the edge costs accumulate across the network. The interpolation estimate alone does not settle this: a mesh interval crossing zero can change the sign of its chord at zero, even when every step size bound in the printed theorem holds. The shape condition in Theorem 5(ii), read literally with the third differentiability assumption, also forces the second derivative to vanish on the negative half line. The mission keeps that condition as printed rather than silently replacing it with a more symmetric one.
Lean represents vertices and edges by finite types, net inflow by finite sums, and each edge cost by a real interval integral based at zero. A Boolean flag selects the directed case with or the undirected case with no sign constraint. The general finite lower and upper bounds of problem (14) are outside this mission. The optimal cost is the real infimum of feasible costs; the graph and balanced demand assumptions give feasible flows, and the sign assumptions bound their costs below. The spline is computed from its mesh values, with its end chords extended linearly outside . Meshes are indexed from zero in Lean, regardless of the paper's two indexing styles.
The corrected Theorem 5 requires zero to be a mesh point on every edge. In regime (i), it replaces by . In regime (ii), both entries of the factor are square roots of ; this matches the equality used in the printed proof. Lemma 4 and Theorem 5 explicitly require , since both step-size bounds and (15), (16) divide by it (with zero demands, a one-point mesh and , Theorem 5 would otherwise fail), and its second marginal cost family is continuous, strictly increasing, and sign preserving. These conventions and corrections are recorded in the source analysis for Theorem 5.
A proof must use the chord spline determined by and the mesh; replacing it by an arbitrary close function would discard the numerical claim. Likewise, the bound is never a hypothesis of Lemma 4 or of the goal: it is milestone 1, and assuming it would remove the combinatorial half of the argument. Milestone 6 is stated on rather than on all of as printed, because the linearly extended end chord of a convex function lies below it. Contributions to the flow bound, Lemma 4, the spline estimate, or the final connection between them are all within scope. The flow and spline definitions can also support other approximation results beyond this theorem.
Asset managers increasingly buy alternative data: satellite images, credit-card panels, web traffic. Raw data of this kind is worthless until someone has the skills to process it, and those skills are costly and uncertain to acquire. A fund can hire data scientists and still find that its models extract little. Huang, Xiong and Yang (Management Science, 2022) build an equilibrium model of a data seller who sells to investors who must first acquire such skills. They ask how the cost of acquiring skills feeds through the data market into the financial market: into how much the price reveals, the cost of capital and return volatility.
The model joins two lines of work. One is the classical noisy rational-expectations market of Grossman and Stiglitz (1980), in which prices partly reveal private information. The other is the literature on selling information started by Admati and Pfleiderer (1986, 1990), in which a monopolist seller degrades the information it sells to limit what the price leaks. The new feature is the "gold rush" of skill acquisition: an investor who pays the cost learns only afterwards whether her skill is high or low.
A risky asset pays and there is noise demand . A data seller observes with ; the precision is the data accuracy. The seller chooses a clarity and passes the data with personalized noise, so that a buyer of skill receives a signal of precision about . The value means the data are sold "as is".
A continuum of CARA investors with risk aversion is indexed by . Investor can acquire data-processing skills at cost , where is a cost parameter. The cost is continuous and strictly increasing in , with and as , and it is strictly increasing in . A skilled investor turns out high-skilled () or low-skilled () with probability each, with . A mass of investors becomes skilled.
In the asset market, the price reveals with precision , and is pinned down by the market-clearing equation (14). Skilled investors buy the data at a Nash-bargained price , where is the certainty-equivalent trading gain (15) and is the seller's bargaining power. Investors acquire skills until the marginal investor is indifferent, (19). The seller chooses to maximize the profit . An equilibrium is a clarity with its such that no other feasible clarity gives more profit.
The market outcomes are:
Fix . There is a threshold such that, for every data accuracy and every pair of equilibria at and , both clarities are finite and
The paper writes these as signs of derivatives in . The goal states them as comparisons between two cost levels, which is what the prose of the proposition asserts.
The result. Proposition 5 is the paper's headline. When skills are uncertain, a rise in skill-acquisition costs makes prices more informative and lowers the cost of capital and return volatility. When skills are certain, these outcomes stay unchanged (Proposition 4). The mechanism is that the seller cannot tailor one clarity to buyers of unknown skill. To keep buyers interested as costs rise, she provides clearer data, and more information leaks into the price. The result separates the data market from a pure cost shock to information production. It gives empirical predictions for markets where skill acquisition is costlier, such as private or international equities.
Formalizing it. The proposition is proved in the paper by expansion in around . A machine-checked version must make "sufficiently high " precise, with a threshold that holds uniformly over all equilibria. It must also control the exact finite- equilibrium rather than its limit. The mission also contributes the first noisy rational-expectations model with a strategic data seller on the platform: posterior variances, the equilibrium equation (14), the certainty-equivalent gain, and the seller's choice between finite clarity and selling "as is". No part of the paper has been formalized before.
Several comparisons follow at leading order in . As the equilibrium mass converges to the root of (C18), which is decreasing in , and the clarity, the data price and performance are, to first order, functions of that mass. The price-informativeness, cost-of-capital and volatility comparisons do not follow at leading order. At the ratio tends to whatever the cost, so these three outcomes are flat in to leading order. Their signs come from the correction to , and the correction must be controlled jointly with the seller's optimal clarity. A newcomer's first idea is to set in the equilibrium conditions and differentiate. That loses exactly the term that carries the result. A further difficulty is that the seller's optimum is defined by comparison with every feasible clarity, including selling "as is", not by a first-order condition.
All quantities are real numbers. The parameters satisfy , , and . Two of these go beyond the paper's §2 domains, and both are needed:
The cost family is any admissible : continuous and strictly increasing in on , , as , and strictly increasing in on . "Increasing" in the paper is read as strictly increasing. Clarity is either a finite or "as is". At "as is", (14) becomes and both conditional variances given a signal equal . These are the limits of the finite-clarity formulas. The value is excluded from the choice set because it gives no positive root of (14).
The posterior variances (8), (10), (12), the gain (15), the price coefficients (C1)–(C4), the cost of capital (C12), volatility (C13) and performance (21) are taken as closed-form definitions. Their CARA-normal derivation (Bayes' rule, market clearing, certainty equivalents) is not formalized. Equilibria are defined relationally: a feasible tuple whose profit is at least that of every feasible tuple, with no choice functions.
The goal concludes, rather than assumes, that the equilibrium clarities are finite. It quantifies over every equilibrium at each cost level. It does not define the equilibrium through the economy or through the paper's expansions, which would replace the theorem by its heuristic.
A complete development needs real analysis only: the intermediate value theorem, monotonicity, compactness on , and asymptotics in . Contributions are welcome on any milestone, on an independent proof of Proposition 4's counterpart, and on a formal derivation of the closed forms from Gaussian conditioning and CARA utility, which would be reusable for other rational-expectations models.
A buyer can face public and financial losses when a remote supplier violates labor, safety, or environmental standards, even if the buyer did not cause the violation directly. The buyer and an intermediate supplier can spend resources to help the remote supplier reduce this risk. Their incentives depend on who pays for the effort and who bears the loss when a violation is detected. Huang, Song, and Swinney model these choices in a fixed three-tier supply chain and characterize which firm takes the downstream responsibility effort. Their result gives a precise threshold rule for when the buyer should act, let the intermediate supplier act, or leave both of them idle (Huang, Song, and Swinney, SSRN author version, 2021, §§3–4).
The mission concerns the paper's base model and Theorem 1. It is a known result with a proof in the online supplement to the paper. The formalization target is to reconstruct that result as a theorem about the sequential game itself, with the parameter assumptions and boundary cases stated explicitly. The paper also studies external stakeholder pressure, two-tier comparisons, and variants of the effort model; those later results are outside this mission.
A Tier 0 buyer sources from a Tier 1 supplier, which sources from a Tier 2 supplier. The buyer sells one product with deterministic demand . Each tier has a fixed per-unit margin and chooses responsibility effort at linear cost , with . Only Tier 2 can experience a responsibility violation. Tier 0 and Tier 1 efforts are substitutes: their combined contribution is . Tier 2 effort complements that contribution and also has a baseline return . The effective total effort is therefore (§3.1, pp. 7–9).
An actual violation has probability . Conditional on a violation, the public detects it with probability , so the probability of a detected violation is . Each firm loses a fraction of demand times its margin, plus an indirect financial loss . Its total loss is . The paper's expected profit and loss-adjusted effort cost are
The ratio measures effort cost relative to the firm's loss from a detected violation. The paper assumes , which keeps Tier 2's best response positive even when the buyer and Tier 1 make no effort (§3.2, pp. 10–12, equation (1)).
The game is sequential. The buyer chooses first; Tier 1 observes it and chooses ; Tier 2 observes both and chooses . A best response at either supplier maximizes that supplier's expected profit among nonnegative efforts after the observed history. The buyer anticipates these responses and maximizes its resulting profit. The paper chooses positive effort when zero and a positive effort tie (§3.2, pp. 10–12).
The central target is Theorem 1 on pp. 14–15. The selected buyer optimum has no outcome in which both the buyer and Tier 1 exert positive effort. Its effort choices fall into three Table 2 rows: control, in which Tier 0 acts and Tier 1 does not; delegation, in which Tier 1 acts and Tier 0 does not; and no effort, in which neither downstream firm acts. Tier 2 still exerts effort in each row. Table 2 specifies all three efforts, the actual violation probability , and the detected probability (Table 2 and Theorem 1).
The threshold rule is
The milestone list follows the paper's two supplier best-response lemmas, the buyer's piecewise reduced profit in the proof of Theorem 1, and the comparisons that separate the candidate outcomes. Each milestone is stated about profits and best responses, rather than merely restating a Table 2 row (Lemma 1, p. 12; Lemma 2, p. 13; Online Supplement, p. 1).
The theorem identifies a buyer's optimal responsibility-management regime using the ratios , the Tier 2 baseline , and the model's risk parameters. The distinction matters because a buyer's direct effort can displace the Tier 1 supplier's effort: a low effort cost for the buyer alone does not settle which firm should act. Table 2 also turns the chosen regime into an explicit violation probability, so the result characterizes both private effort and the supply chain's responsibility outcome (Theorem 1 and discussion, pp. 14–15).
The source paper proves Theorem 1; the Lean declarations in this mission are open proof targets. Formalizing them will supply reusable definitions for a three-player sequential effort game and a checked route from the suppliers' optimality conditions to the buyer's full equilibrium classification. Later statements about stakeholder pressure and the two-tier comparison can build on the same model once the base theorem is proved.
Tier 1's best response changes at : below that point it offsets some of the buyer's effort, while above it Tier 1 exerts zero effort. The buyer's reduced profit therefore changes form at the same boundary. Optimizing a single smooth expression across all nonnegative would miss that change. The equality cases also matter: at the control–delegation boundary the two choices have equal buyer profit, and the paper's convention selects positive buyer effort (§4.1 and Online Supplement §A, proof of Theorem 1).
Lean represents all parameters, efforts, profits, and probabilities as real numbers. The three tier indices are explicit fields, and every player's feasible efforts are nonnegative. A separate sequential-game definition gives the argmax meaning of both supplier best responses and buyer optimality. The paper-specific model defines , , the exponential risk function, equation (1), the Table 2 rows, and . The goal quantifies over every pair of supplier best-response strategies; it does not define those strategies as the formulas to be proved in Lemmas 1 and 2. Buyer optimality ranges over every feasible effort, rather than over the three candidate rows.
The model's standing predicate records , , , , , , , , and . Positive demand, nonnegative indirect loss, positive total loss, and positive make economic sign and division conventions explicit where the source uses them without a separate assumption. The denominator of is positive in the only region where Theorem 1 uses it, . Real logarithms and square roots are used only with positive arguments in the applicable equilibrium rows. At , the control effort is zero and its row coincides with the no-effort outcome; the theorem retains the paper's weak inequality.
The initial reusable work is the sequential-game interface and the two best-response characterizations. Contributions that prove those results, the reduced-profit identity, the domination and comparison statements, or the full threshold classification all advance the mission. Statements obtained by assuming the Table 2 formulas are already optimal would bypass the result being formalized.
Some organizations grow by asking each member to recruit a successor. The incentive facing a member depends on where the revenue generated by later members goes. A transfer rule may reward the recruiter, keep the revenue with the entrant, or divide it among several predecessors. Hougaard, Moreno-Ternero, and Østerdal ask which fixed rule gives the greatest total expected payoff when members choose recruitment investments for themselves. Their model covers a sequential hierarchy with no fixed terminal generation, so both incentives and the possibility of a very long hierarchy matter. The authors also discuss recruitment and blockchain rewards as interpretations of the same transfer problem. Hougaard et al.
The paper distinguishes a centralized benchmark from a decentralized design problem. In the centralized benchmark, investments can be chosen to maximize the hierarchy’s total value directly. In the decentralized problem, each agent chooses an investment privately after the allocation rule has been announced. The result targeted here is the paper’s Theorem 2 for the decentralized problem, in the authors’ Universidad Pablo de Olavide working-paper version dated August 3, 2021. Its page numbering and theorem labels refer to that version. Hougaard et al.
Agents are numbered . Agent is present initially. If agent has arrived, she invests and recruits agent with probability . The common technology is strictly increasing and strictly concave, starts at , takes values below one, has an unbounded right derivative near zero, and has convex ratio on positive investments. These conditions apply throughout the model. A member may invest any nonnegative amount; there is no budget ceiling. Hougaard et al., §2
Each arrival creates one unit of value. An allocation scheme has entry for the share of agent ’s unit given to agent . Shares are between zero and one, shares to a later agent are zero, and each row sums to one: . Write and for the probability that agent arrives. Conditional on arriving, agent receives her own share, pays her investment, and may receive shares from later arrivals. The paper denotes this conditional expected payoff by ; equation (1) gives its full series. Hougaard et al., pp. 7–9
A profile is a Nash equilibrium of a scheme if, for every agent and every alternative , changing only to cannot raise that agent’s conditional payoff. This includes agents reached with probability zero under the current profile: each is still a player in the induced game. The hierarchy’s expected length is , and its expected investment is . Transfers cancel in the total, so the social value is associated with the profile rather than the scheme and equals when the series are finite. Hougaard et al., pp. 8–10
A scheme is decentralized socially optimal when at least one of its equilibria has social value at least as high as every equilibrium under every valid allocation scheme. This existential choice of a supporting equilibrium matters because a scheme can have more than one equilibrium. The comparison concerns outcomes agents can sustain in equilibrium, rather than all investment profiles, including those a planner could impose without incentives. Hougaard et al., pp. 10–12
Let keep agent ’s initial unit with agent and give the entire unit created by each later agent to that agent’s immediate predecessor:
with every other entry zero. The goal asserts both existence and uniqueness:
Equality is entrywise equality of schemes. The goal does not assert that every scheme has a unique equilibrium. Under , the supporting equilibrium is constant, , with . Hougaard et al., Theorem 2, p. 12; proof of Proposition 1, p. 27
The milestone list follows the claims used in the paper’s proof: finite investment gives finite expected length; the best length at fixed expected investment is attained; a constant profile of the same length uses less investment than a nonconstant profile; a weighted gross-return identity accounts for all later arrivals; a nonconstant equilibrium is surpassed in social value by the unique constant profile of equal length, supported as an equilibrium; the equilibrium under is identified; and the two parts of Theorem 2 are established separately. The length and value comparisons use the source’s own quantities , , , and . Hougaard et al., proof of Theorem 2, pp. 20–27
Theorem 2 identifies the complete transfer table that gives the largest attainable social value under private investment choices. It rules out every other feasible scheme, including schemes that spread a successor’s revenue across several predecessors. The result also fixes a reference point for the paper’s comparison with centralized investment and for its later analysis of rules that optimize the initiator’s payoff instead. Those later results concern different objectives and are outside this mission. Hougaard et al., §§3–4
The paper proves the result on paper. The formalization task is to give a machine-checked proof of its exact claim, including the infinite-horizon payoffs and the quantifiers over all schemes and their equilibria. The definitions of nonnegative-action equilibrium, sequential survival weights, and extended-valued expected returns can also support later work on sequential incentive systems. No proof of this theorem is supplied by the draft statement itself.
The obvious hope is that a rule that fully rewards the immediate recruiter must produce the best outcome because it ties each payment to the next successful addition. That observation does not compare all possible equilibria: a different rule may redistribute receipts from several future arrivals and change investment at every stage. The hierarchy has no finite horizon, and an agent’s gross expected receipts can be infinite. A complete argument must control those series while comparing a nonconstant equilibrium to a constant one, then establish that no different transfer entry can support an equally good outcome. The paper’s proof organizes these obstacles in Steps 0–5. Hougaard et al., pp. 20–27
Lean represents agents by natural numbers, with zero as the initial agent. Profiles and schemes are real-valued functions; validity requires nonnegative investments and row-stochastic, lower-triangular transfer shares. The technology structure carries every standing assumption of §2. Differentiability is stated on positive investments together with continuity at zero from the right, consistent with the paper’s infinite right derivative there. Hougaard et al., pp. 7–10
Expected length, expected investment, and gross receipts are sums in extended nonnegative reals. Conditional payoffs and social values use extended reals. The value convention assigns negative infinity when expected investment is infinite; otherwise it uses the finite real difference . Step 0 supplies the finiteness of in that latter case. The maximum-length function takes a supremum over profiles with exactly the specified expected investment, and its milestone includes finiteness and attainment. These choices retain the source’s possible infinite payoffs and avoid an accidental zero value for a divergent real series. Hougaard et al., footnote 8 and proof of Theorem 2, Step 0
Steps 2–3 require a disclosed boundary reading: “nonconstant” means differing investments among agents with positive probability of arrival, and the profile has finite expected length. Without these conditions, a profile can differ only after recruitment has stopped, or have infinite length, making the printed comparison false. The Step 3 identity carries the no-self-transfer condition used where the paper invokes it. The goal itself has no such extra conditions. The equilibrium definition ranges over every agent and every nonnegative unilateral deviation, and decentralized optimality compares every equilibrium of every valid scheme; neither class is empty by definition. Contributions proving the eight milestones, the goal, or reusable lemmas for their infinite sums and concavity claims are in scope. Hougaard et al., pp. 9–10, 24–27
Some goods can only be made by copies of themselves. RepRap and Prusa 3D printers print the parts of new printers, seed stock is grown from seed, and livestock herds breed. For such a good the inventory is also the production capacity: a unit sold today is a unit that will not replicate tomorrow. A firm launching such a good has to decide, at every instant, how much of its stock to use for replication and how much demand to serve. Demand for an innovative good is not exogenous either. It diffuses through the market by word-of-mouth, so sales held back today also slow future demand.
B. Hu and Z. Sun (Management Science) model this as a deterministic optimal control problem. Their demand side is the Bass diffusion model (Bass, 1969) in the supply-constrained form of Ho, Savin and Terwiesch (2002) and Kumar and Swaminathan (2003), where cumulative sales rather than cumulative demand drive imitation. Hu and Sun add diminishing word-of-mouth. Their main structural result, Theorem 1, says that under a condition they call Strong Replicability the optimal policy switches only once and can be found by a one-dimensional search.
Time runs over , where is the life cycle. The firm controls a production rate and a sales rate . The state consists of the cumulative demand , the adjusted cumulative sales and the inventory . The demand rate is
where is the market size, the coefficient of innovation and the coefficient of imitation. Problem (1) of the paper is
subject to
Here is the price, the unit replication cost, the holding cost rate, the replication rate, the discount rate and the rate at which word-of-mouth decays. Unmet demand is lost. The paper assumes and . Production is on when and off when . Sales are on when and off when .
Strong Replicability is condition (2),
It says that letting a unit replicate for a short time and selling the offspring later is worth more than selling the unit now.
Two levels of the launch inventory organise the answer. is the level at which keeping production and sales always on depletes the inventory exactly at . is the level at which keeping production off and sales on depletes it exactly at .
Assume Strong Replicability. Then:
In each case, optimal means that the profit is at least
for every admissible trajectory , not only for policies of the stated shape. The switching times are not given in closed form, and the theorem asserts only that they exist.
Theorem 1 turns an infinite-dimensional control problem into a choice of one switching time. Its managerial content is that a firm with a replicating good should, when stock is scarce, run replication at full capacity and hold back sales, losing some early customers, as long as the stock built up will eventually be sold. Proposition 2 says that under Strong Replicability the firm never sells out before the end of the life cycle. The paper's numerical study (§4) and its extensions (§5: backlogged demand, liquidity, stochastic diffusion) are built on this characterization.
The result has a published informal proof (pp. 36–37 of the manuscript), which applies necessary conditions from Pontryagin's maximum principle and then a perturbation and exchange argument. None of it is machine-checked. A complete formal proof would establish global optimality, against all integrable controls, for a nonlinear controlled ODE with mixed state–control constraints. That is a sufficiency statement, which the necessary conditions alone do not give.
The maximum principle gives necessary conditions only, and Problem (1) is not concave: the dynamics of are bilinear in and , and the constraint couples control and state. So the obvious route, solving the Pontryagin system and reading off the optimum, does not prove optimality. The paper's own argument is an exchange argument. It postpones sales or shifts production forward and claims each change improves profit, and it applies the change recursively ("by making the same argument recursively"). Making it rigorous requires comparison results for the Bass system under perturbed sales, which are delicate. Postponing sales lowers the adjusted sales , and with it all future demand. The existence of the switching times also needs a continuity argument on the depletion time as a function of the switch.
The Lean development lives in the namespace SelfReplic.Strong and uses real numbers throughout.
Params with fields m, price, c, h, r, alpha, beta, rho, w, T, IL. The predicate Params.Standing collects the page's assumptions , , , . It adds the sign conditions , , , , , , which the paper uses but never states. Params.StrongRepl is condition (2).IsAdmissible) have integrable controls and continuous states on . The three ODEs hold in integral form at every , the constraints , hold at every , and . The integral form is used because bang-bang controls are discontinuous. Continuity and integrability prevent any integral from silently taking Lean's default value . Nonnegativity of follows from , as on p. 8.IsOptimal) compares the discounted profit with every admissible trajectory of the same parameters.IsLowLevel, IsHighLevel), evaluated at the same parameters with replaced.A formalization that states Theorem 1 inside its own policy class (the best policy of shape (a) is the best of shape (a)) would be empty. Here the competitor in every case ranges over all admissible trajectories.
Not formalized: Theorem 2 (Weak Replicability), whose closed form (3) for the production interval is inexact when ; Corollaries 1–2; the second half of Proposition 2, which fails when ; the unnumbered bang-bang claim of p. 9; Propositions 3–4 (§5).
Contributions that would be reusable beyond this mission include existence and uniqueness for the controlled Bass system in integral form, a comparison lemma for and under pointwise-ordered sales, and a sufficiency (verification) theorem for bang-bang controls of problems that are linear in the control.
Manufacturers that sell through retailers increasingly also sell directly to consumers, through their own web stores or outlets. The operations literature calls this supplier encroachment. The classical analysis (Arya, Mittendorf and Sappington, 2007) assumes an exclusive reseller: the reseller carries only the encroaching supplier's product. In that setting a supplier whose direct channel costs more per unit than the reseller's still sells through the reseller, and a supplier whose direct channel is cheaper never does.
Real resellers are rarely exclusive. A retailer that carries one brand usually carries competing brands too, and its order from one supplier depends on its order from the others. Hotkar and Gilbert (Management Science, 2021) study what changes when the reseller is non-exclusive. Their headline finding, Proposition 5, is that both conclusions of the exclusive model can reverse.
Two suppliers, , sell partially substitutable products through one reseller. Supplier 1 can also sell directly. The reseller orders and ; supplier 1 sells units directly. The substitutability between the two suppliers' products is , written below. Supplier 1's direct product is a perfect substitute for her product at the reseller. Prices clear the market linearly:
Production and reselling cost nothing. A direct sale costs supplier 1 an extra per unit, and may be negative: the direct channel can be more efficient than the reseller. With wholesale prices , the reseller earns , supplier 1 earns , and supplier 2 earns .
The game has three stages:
Supplier 1 holds a belief about supplier 2's price. In stage III her quantity and her conjecture of the reseller's order from supplier 2 are mutual best responses computed with (Lemma 1). In an equilibrium (the paper's (4.7)–(4.16)), beliefs equal the actual prices. The reseller best-responds at every price pair, anticipating supplier 1's reaction. Neither supplier gains from a unilateral price change. After a deviation by supplier 2, supplier 1's belief stays where it was. This is not a subgame-perfect equilibrium, because supplier 1 cannot observe .
The paper restricts the direct cost to (p. 9). It identifies thresholds (Table 2) that separate three regimes:
The sign of is that of
which has a unique root in .
With an exclusive reseller, efficiency alone decides channel use: a costlier direct channel is used alongside the reseller, and a cheaper one replaces it. Proposition 5 shows that this rule fails once the reseller also carries a competitor.
The result explains why observed channel structures need not reflect relative channel costs. It also shows which assumption of the exclusive model drives its conclusions.
As far as the mission's searches found, no part of this model has been machine-checked. The mission formalizes a game with unobservable prices and belief-based stage-III conjectures. Such games occur throughout the supply-chain contracting literature, and the equilibrium predicate here can be reused for them. The paper's proofs are algebraic, but they verify deviation incentives across a piecewise-defined reseller response, with polynomials of degree eight in . A formal proof has to check every branch.
The reseller's best response is piecewise in : supplier 1 sells directly only while is below a threshold, and her conjecture about can hit zero. The paper analyzes the reseller's choice under a restriction (Lemmas 1–3) that rules out the conjecture for small , and argues that the excluded region cannot occur in equilibrium. Deviation prices, however, can push the reseller into that region. There the reseller's objective is not concave in , and supplier 1 may find a price cut that triggers a jump in the reseller's order. A proof of Lemma 4 cannot simply cite first-order conditions inside the restricted region: it has to rule out such jumps for every deviation price. Numerically this succeeds for , but it fails for close to .
The uniqueness claim in part (a) is a statement about every strategy profile, including the reseller's off-path rules. It cannot be obtained by exhibiting one profile. The equilibrium prices themselves are not unique for , so this claim concerns the channel use only.
Everything is real-valued and lives in NonExclEncroach.Channels. The conventions are:
The goal quantifies over this equilibrium predicate. Stating Proposition 5 with the quantities read off Table 1, or as the sign of alone, would reduce it to the sign of , and is ruled out.
Three statements depart from the page, and each departure is disclosed in its Formalization Note:
Not formalized: Lemma 3, whose threshold is correct only when ; the appendix lemma eliminating equilibria with ; and Propositions 1–4 and 6–8.
Contributions welcome: proofs of the milestones, a general existence theorem for the reseller's order rule, and an analysis of the game for near .
Managers are often accused of short-termism: boosting current cash flow at the expense of long-run firm value. Hackbarth, Rivera and Wong (Management Science, 2022; working paper SSRN 3060869) study short-termism inside a dynamic-agency model of a levered firm. A risk-averse manager exerts two unobservable efforts: long-term effort , which raises the growth rate of firm size, and short-term effort , which raises current profitability. The firm issues perpetual debt with coupon , and shareholders choose the manager's incentive contract and the default time.
Debt distorts incentives through debt overhang (Myers, 1977): shareholders bear the cost of effort but share its benefits with bondholders, so they underinvest. The paper's question is whether debt also distorts the mix between short- and long-term effort, and whether that distortion is a separate agency cost or a consequence of underinvestment. Proposition 5 answers the second question: if shareholders commit to the long-term effort an unlevered firm would choose, they voluntarily choose the unlevered short-term effort too. Excessive short-termism is then an indirect cost of debt, transmitted only through long-term effort.
Firm size evolves as and is absorbed at a lower boundary . Profitability evolves as , and the two shocks have correlation . Efforts lie in the effort box , . Effort costs , where may have either sign (complements or substitutes). Everyone discounts at , the manager has CARA coefficient , and the corporate tax rate is .
The paper reduces the shareholders' problem to an ODE for the equity value . Write
where is the manager's incentive-risk term. The levered HJB (18) is . With it is the unlevered HJB (25). The unlevered value solves (25), has , is twice continuously differentiable on , and has linear growth, as in Proposition 3. Its maximizers form the unlevered effort policy.
Two constrained problems compare commitment regimes. Both impose, at a default threshold , value matching , smooth pasting , and transversality as .
For every coupon , every unlevered value solving (25), every associated effort policy , every function and every threshold ,
The unlevered value and its policy are hypotheses, matching the objects used in the paper's statement and proof.
with the paper's . 2. Section of the joint maximizer (A.4.2). For every slope , maximizes over . 3. (A.26). For every and , the maximum over of is attained at , so the right-hand sides of (A.29) and (A.27) agree.
The result. Proposition 5, together with Proposition 4 (with independent effort costs, debt does not affect short-term effort), shows that debt affects the two efforts asymmetrically. Debt distorts long-term effort directly through underinvestment, and short-term effort only through its interaction with long-term effort in the cost and risk terms. A contract or covenant that pins down long-term effort therefore removes the short-termism distortion as well. The converse fails: committing to does not recover . The paper's calibration (§5) quantifies the value of these commitment regimes. Proposition 5 guarantees that two of them coincide, so the no-underinvestment numbers are also the no-overhang numbers.
Formalizing it. The result is proved in the paper, and no part of the model is formalized anywhere to our knowledge. This mission produces a machine-checked statement of the levered-firm HJB, the unlevered effort policy as a constrained maximizer, and the two commitment problems. It also gives a corrected version of the appendix display (A.26), which as printed omits a factor , the factor in one cross term, and contains a stray sign. These objects can be reused for later statements of the paper, such as Proposition 4 and the comparative statics of §4.4.
The proof has no analytic depth. The work is in the encoding, where the obvious readings fail in specific ways:
All quantities are real numbers. The parameters form a structure, and the standing assumptions of §2 (, , , , , , ) are one predicate. Its single added clause is , which the transversality limit presupposes. No concavity assumption and none of the paper's Conditions 1–2 are imposed.
Conventions committed to:
deriv f and deriv (deriv f), and is required to be on the open set .IsGreatest of the image, so attainment is part of the statement.The trivializing encodings are ruled out: NU maximizes over , NO fixes , and comes only from the unlevered maximization at , never from a hypothesis about the levered integrand.
Not in scope: the continuous-time contracting results (Proposition 1, which needs martingale representation), the verification theorems (Propositions 2, 3, 6, 7, which rest on Strulovici–Szydlowski 2015), Proposition 4, Lemmas 1–2 and the calibration. Contributions are welcome on all three milestones and the goal. The model file is self-contained and depends only on Mathlib.