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?
Many models in decision theory, insurance and risk management do not act on random outcomes directly but on their distributions. A distributional transform is a map that sends a probability distribution on to another distribution . The most important class is that of probability distortions, for an increasing function on . They are the core of the rank-dependent utility theory of Quiggin (1982), the dual theory of choice under risk of Yaari (1987), the distortion premium principles of insurance pricing (Wang, Young and Panjer, 1997) and the probability weighting of cumulative prospect theory. Spectral risk measures such as Expected Shortfall are expectations under a distorted distribution.
In each of these theories is postulated. Liu, Schied and Wang (SSRN 3419388; Mathematics of Operations Research, 2021, doi:10.1287/moor.2020.1090) ask the converse question: which transforms of distributions are probability distortions? Their Theorem 1 answers it with three order-theoretic properties and no functional form. This mission formalizes that theorem and the steps of its proof.
A distribution is a Borel probability measure on , identified with its cdf . Write for the set of all distributions and for those with bounded support. The left quantile and the right quantile of are
is smaller than in stochastic order, , if for all . For a strictly increasing continuous with , the shape transform is the law of for .
is the class of functions that are increasing and right-continuous with , . A transform on a set of distributions is a probability distortion if for all , for some .
For the paper's Definition 2 introduces three properties:
The proof also uses (support unbounded below, bounded above) and (bounded below, unbounded above), and, for , the functional .
For or and ,
Both domains are part of the goal.
The theorem identifies probability distortions as the transforms that respect three structural features of a distribution: its order, its behaviour under weak limits, and its invariance under monotone reparametrisation of the outcome scale. It explains why distortion-based preferences and risk measures are the natural ones on distributions, and it is the base of the paper's further results on risk measures (§5) and on the sensitivity of distributional transforms (§6). Example 9 of the paper shows that lower-semicontinuity cannot be dropped.
The result is proved in the paper; to our knowledge no part of it has been formalized. The mission produces a machine-checked proof of Theorem 1, a formal account of how monotonicity and shape covariance force quantile representations, and reusable infrastructure: quantiles of probability measures on , stochastic order, shape transforms and probability distortions on Mathlib's ProbabilityMeasure ℝ. Formalizing Chambers' axiomatization of quantiles (milestone 3) is a contribution in its own right; the paper cites it and does not prove it.
The "if" direction is routine. The "only if" direction has two hard steps. The first is Chambers' axiomatization: showing that a monotone, shape-covariant functional on must be a quantile at a level independent of the distribution, which requires controlling the functional on distributions with flat stretches of the cdf, where the left and right quantiles differ. The second is the passage from to : monotonicity alone yields only one-sided inequalities for distributions with unbounded support, and the other inequality requires lower-semicontinuity along sequences produced by shape transforms that compress or stretch a tail. The obvious attempt, approximating by truncations and passing to the limit, gives only one of the two inequalities in each case.
Distributions are MeasureTheory.ProbabilityMeasure ℝ; is Set.univ and is the set of measures with for some . The paper's atomless probability space is not needed: every Borel probability measure on is the law of a random variable on such a space, so these are the same sets. The hypothesis is Set.MapsTo T M M. Cdfs are Mathlib's ProbabilityTheory.cdf. Quantiles are real-valued sInfs and are evaluated only at levels where the paper's quantile is finite: for , on and on . The stochastic order reuses the published StochasticOrders.Usual.UsualOrder (the survival-function form, which the paper notes on p. 5 is equivalent to its definition). Shape transforms are the order isomorphisms ℝ ≃o ℝ, acting by pushforward. Weak convergence is convergence in Mathlib's topology on ProbabilityMeasure ℝ. Lower-semicontinuity is the paper's closure property, not Mathlib's LowerSemicontinuous. A function is a real function constrained on , and "probability distortion" is the cdf identity on .
Shape transforms range over all increasing homeomorphisms of , not only affine maps; restricted to affine maps the "only if" direction is false (the super-quantile transform of Example 4 is a counterexample). No continuity, constant-preservation or support hypothesis is added to Theorem 1.
A complete development needs: elementary quantile calculus for measures on (Galois connection with the cdf, behaviour under pushforward), the portmanteau theorem for weak convergence (in Mathlib), Chambers' theorem, and the explicit approximating sequences of pp. 7–9. The quantile and stochastic-order lemmas are reusable well beyond this mission. Proofs of individual milestones, in particular Chambers' theorem, are welcome independently.
Markowitz's mean-variance problem trades off the expected terminal wealth of a portfolio against its risk. Over several periods the scalarized form of this problem is time inconsistent: a strategy that is optimal today for a fixed risk-aversion parameter is generally no longer optimal tomorrow for the same parameter, so the investor would deviate from her own plan (Björk & Murgoci 2014; Björk, Murgoci & Zhou 2014). The literature has responded by redefining optimality (equilibrium strategies) or by searching for a time- and state-dependent risk aversion that restores consistency (Karnam, Ma & Zhang, Annals of Applied Probability 27, 2017). Dynamic convex risk measures and their time consistency are developed in Detlefsen & Scandolo 2005 and Riedel 2004.
Kováčová and Rudloff (arXiv:1806.10981, Operations Research 2021) take a different route. They keep both objectives, measure risk by a time consistent dynamic convex risk measure, and treat the dynamic mean-risk problem as a family of vector optimization problems. They show that this family is time consistent with respect to weak minimizers and that its value functions, the upper images, satisfy a set-valued Bellman principle. This mission formalizes that Bellman principle.
Fix a horizon and a finite probability space with a filtration , trivial, , and for every nonempty event . denotes the -measurable random vectors with values in ; orders between random vectors are pointwise and componentwise.
A market has assets with adapted discounted prices . An investor holds positions on , subject to closed, conditionally convex constraint sets . With wealth at time , the feasible portfolios are
that is, self-financing strategies with initial value that respect the constraints. The terminal wealth is and .
Risk is measured by a dynamic convex risk measure : each is normalized, conditionally translation invariant, monotone (decreasing) and conditionally convex. It is time consistent: implies . The mean-risk function is
and the mean-risk problem minimizes over with respect to the cone . Its upper image is
and at the terminal time (5.2).
For every and every -measurable ,
The right side has a closure and no ordering cone.
The upper image is the infimum of in the complete lattice of closed upper sets, so it is the natural value function of a vector optimization problem. Theorem 5.1 expresses the value function at time through the value functions at time by a one-period problem, exactly as a scalar Bellman equation does. Computationally this is what makes the problem tractable: one solves a convex one-period vector optimization problem per node, backwards in time, and recovers the whole efficient frontier at every node and an efficient strategy forward along the realized path (Sections 6 and 7 of the paper do this for 2,500 periods). Conceptually, it shows that the mean-risk problem is time consistent in the set-valued sense without computing the moving scalarization in advance.
The paper proves Theorem 5.1; no machine-checked version exists. Formalizing it produces a Lean development of dynamic convex risk measures on finite filtrations, of conditional vector optimization in , and of upper images, none of which is currently on the platform beyond the static conditional convex risk measure reused here.
The equality has two halves of different character. Replacing the image by the upper image enlarges the feasible set of the one-period problem, and the new points must be shown to be limits of points already attained: this needs monotonicity of together with its continuity, which holds only because is finite. Removing the cone from the right-hand side needs translation invariance of with an -measurable shift and the monotonicity of with respect to the larger cone . Both closures matter: without them the identity fails in general, since the image of a closed set under need not be closed. The natural first idea, to define recursively, proves nothing: the content of the theorem is that the upper image built from whole multi-period strategies agrees with the recursion.
Fintype with an ambient σ-algebra ; the filtration is a Mathlib Filtration ℕ with and ; is a probability measure with for every nonempty measurable .CondConvexRisk.Representation.IsCondConvexRiskMeasure with respect to (axioms a.s. on ); time consistency is stated pointwise for measurable arguments. On a finite space with positive probabilities, a.s. equality of measurable functions is equality, so all of the mission's own statements are pointwise.condExp.A complete development needs: conditional expectation on finite filtrations (tower property, pull-out of -measurable factors), continuity of convex functions on finite-dimensional spaces, and elementary closure arguments in . The results on dynamic risk measures (Lemma 2.1) and on (Lemma B.1) are reusable beyond this mission. Proofs of any milestone are welcome independently.
In many sequential decision problems an unknown quantity is revealed only when paid for: a medical test, a sensor reading, a database query. Stochastic submodular cover is the common abstraction: items are probed one at a time at a cost, each probe reveals a random outcome, and probing stops once the revealed outcomes jointly reach a coverage target. It contains stochastic set cover, Boolean function evaluation and active-learning formulations (Golovin–Krause).
A fully adaptive solution chooses every probe after seeing all previous outcomes. In practice decisions are often batched: a plan is fixed, executed in parallel, and revised only a few times. The question of this mission is how much is lost when the number of revisions, the rounds of adaptivity, is limited to .
Timeline.
Let be a finite ground set and a monotone submodular function with . There are items ; item has an integer cost and realizes to a random element . The items are independent. Probing item costs and reveals . A set of probed items with realization covers if , and .
The paper's algorithm runs in each round the partial covering algorithm ParCA with parameter , where is the residual value still to be covered and the number of rounds left. ParCA builds a list greedily by a score (1) that averages relative marginal gains over the random outcomes of the items already listed. It then probes the list until exceeds .
There is an absolute constant such that for every feasible instance and every integer some -round-adaptive solution covers almost surely and satisfies
The goal leaves the constant unspecified and does not assert polynomial running time.
The result. The bound is independent of the number of items and of the costs, and for it gives an -approximation in rounds, which is best possible up to constants unless P = NP, even for fully adaptive algorithms. At it bounds the adaptivity gap of stochastic set cover by , which settles the question of Goemans and Vondrák up to a factor. The analysis of a greedy list against an adaptive benchmark, phase by phase, through an adaptivity-gap result for the maximization problem, is reusable for other stochastic covering problems.
Formalizing it. The result is proved on paper. As far as is known, none of it has a machine-checked proof, and the platform holds no prior formalization of stochastic probing, adaptive policies or adaptivity gaps. The work is to formalize the known proof. It also fixes three boundary points the printed argument leaves open: the equality case in Lemma 4.1, the reading of at , and the summation of per-round costs in Theorem 3.2, where the printed induction is loose for large . The Lean statements are written so that the theorem holds as stated.
The obvious argument compares the greedy list directly with , item by item. This fails because the list is fixed in advance while branches. No single list resembles on more than a small fraction of outcomes, so a per-path comparison gives nothing. The score (1) therefore averages over the outcomes of the items already listed, and the comparison has to be made in expectation, separately for each scale of residual coverage, through the adaptivity gap of a maximization problem. The second obstacle is quantitative. A naive charging loses a factor , and removing it requires the harmonic-sum bound of Lemma 4.5 and the geometric phase recursion of Lemma 3.3.
Fin m and the ground set is a Fintype. Each item has a law p i : U → ℝ (non-negative, summing to ). The items are independent, so a joint realization has probability , and every expectation is a finite sum. Costs are natural numbers , and is -valued, monotone and submodular. Submodularity is the published NonmonotoneSubmod.Shared.Submodular.harmonic_tail_lt_log is proved). The adaptivity-gap theorem [BSZ19] is reusable well beyond this mission; contributions proving it, or the scale lemmas, are welcome.Job offers, purchase offers and admission offers usually come as a package: a size (salary, price, bonus) and a deadline after which the offer lapses. An exploding offer is one with a zero deadline: it must be accepted on the spot. Exploding offers are common in practice, in law-clerk hiring, in real-estate contracts, in flash sales, and they are often criticised. Z. Hu and W. Tang ask when an organisation that is competing with a market of alternatives should make an exploding offer and when it should give the candidate time, and how the answer changes when the candidate's alternatives get better (Hu and Tang, Management Science, 2021; SSRN 3143414).
The model sits in the tradition of sequential search with recall-free offers (Lippman and McCall, 1976; Van den Berg, 1990) and of offer deadlines in search (W. Tang, Bearden and Tsetlin, 2009; Zorc and Tsetlin, 2020). The paper's contribution is to optimise the size and the deadline jointly and to show that the two interact. This mission formalizes the paper's comparative-statics result: how the optimal package moves when the distribution of alternative offers increases in the mean residual life order.
Time runs over a finite horizon , . At time the proposer makes an offer of size with deadline to the responder. Meanwhile alternative offers reach the responder by a Poisson process of rate ; each alternative offer is exploding, and its size is an independent copy of a nonnegative continuous random variable with support , , , where is allowed, and with finite mean . The proposer receives utility minus if her offer is accepted, and otherwise.
Two functions of the law of drive the analysis:
is the value-to-time operator: is the search time a responder needs to expect a value . It maps onto , and denotes its inverse.
The responder's value-to-go , his expected payoff from continuing the search at time , solves the Hamilton–Jacobi–Bellman system on with and ; Lemma 1 of the paper gives the closed form before the deadline and after it. The responder accepts the proposer's offer at the deadline when .
The proposer's expected surplus is
the second factor being the probability that the responder accepts no alternative offer before the deadline. Problem (7) maximises over , . Two quantities describe its solution: the shortest acceptable deadline , and the size defined by (10): if , solves on if , and if .
The mean residual life of at is (and once ); means for every .
Let and let be an optimal package against . Then
Each part excludes the boundary case , for the distribution whose package it concludes about (see Formalization scope).
In attack order: below and is a strictly increasing bijection (proof of Lemma 8); Lemma 1 (the closed form solves the HJB system and is its only solution, ); the identity of eqs. (5)–(6); Proposition 1 (the deadline is optimal for a fixed size); well-posedness of and ; Theorem 2 (quasi-concavity, and , is the optimal package); Lemma 4 (i)–(ii) (the mrl order gives , and ); and the two order steps of the proof of Theorem 3 (, , ).
Theorem 3 answers the managerial question the paper poses. When the candidate's market improves in the mean residual life order, a proposer who was giving time keeps giving time, with a smaller offer and a longer deadline; a proposer who makes an exploding offer against the better market also makes one, of smaller size, against the worse market. In this model, therefore, exploding offers are the response to weak outside options, not to strong ones. Theorem 2, a milestone here, is the paper's other main result: the optimum is either an exploding offer matching the responder's value-to-go or an offer of size with a positive deadline, and size and deadline cannot be chosen separately.
The results are proved in the paper; none is formalized. The formal development produces a reusable layer: the value-to-time operator of a continuous offer law and its inverse, existence and uniqueness for the search HJB equation, and the comparison under the mrl order (the stop-loss part of Shaked and Shanthikumar's Theorem 4.A.26), which the platform's stochastic-orders library does not yet have. Formalization also exposes an unstated boundary case of Theorem 2 (below).
The value-to-go is defined by an ODE whose right-hand side vanishes at ; showing that solutions stay below and that is onto is a statement about the behaviour of near , which differs between bounded and unbounded . The surplus is defined through a time integral of ; its closed form holds only along the solution of the ODE. The proposer's problem is not concave, and the optimal package is pinned down only through the quasi-concavity of the reduced surplus . Finally, the comparative statics need the mrl order to transfer to the stop-loss transforms on all of , which is a genuine stochastic-ordering theorem, not a pointwise comparison of the defining ratios.
All values are real, except the upper end of the support, which is an extended real b : EReal; it is only compared with real numbers, never used in arithmetic. The offer law is a measure μ on ℝ with the bundled predicate OfferDist μ a b: a probability measure without atoms, no mass below or above , positive mass on every open subinterval of (this is what support means), , , , and finite mean. The hypotheses , and the finite mean are added to the page's model; is the paper's. "Increasing" and "decreasing" are weak (footnote 3, p. 8).
Conventions: is the supremum of the with , shown to be the inverse by a milestone; is evaluated only below or through , which is for . The HJB terminal condition is imposed only when , because the printed system is contradictory at . In (10) the case is put with ; both give . The mrl order is the platform's MrlOrder applied to the identity random variables, which agrees with the paper's definition on this class of laws. Lemma 2 and Lemma 4 (iii) are not formalized.
The surplus is defined by the no-acceptance probability, not by the ratio (6), and the goal quantifies over arbitrary optimal solutions of problem (7). Substituting the closed form of Theorem 2 for the optimal packages would reduce the goal to the order steps plus min algebra; that formalization is ruled out.
One correction is made. Theorem 2 reads as uniqueness of the optimal package, but when and the reduced surplus is constant on and every size there is optimal; for uniform on and , Theorem 3 (i) fails as printed. Uniqueness in Theorem 2, and each part of Theorem 3, therefore assume or for the relevant distribution.
A complete development needs uniqueness for the search HJB equation, integration along its solution, and the mrl-to-stop-loss comparison. That comparison is reusable beyond this mission, and contributions of it, as a standalone stochastic-orders theorem, are welcome.
Many problems in control, robust semidefinite programming and risk management ask for a decision that keeps a matrix positive semidefinite for every value of an uncertain parameter in a set . Examples include robust polynomial SDPs (Scherer and Hol, 2006), Lyapunov-type conditions that must hold on a region of the state space, and robust correlation stress testing. When the data are polynomial, such a problem has infinitely many polynomial matrix inequality (PMI) constraints, one per point of , and even its deterministic special case, minimizing a polynomial subject to one PMI, is hard in general.
Guo and Wang (arXiv:2304.12628, Mathematics of Operations Research, 2025) build a moment-sum-of-squares (moment-SOS) hierarchy of semidefinite programs for this problem under SOS-convexity, and show that its optimal values converge to the robust optimum and that its solutions yield global minimizers.
Timeline. Lasserre (2001) introduced the moment-SOS hierarchy for scalar polynomial optimization. Helton and Nie (2010) defined SOS-convexity, a semidefinite-checkable strengthening of convexity, and Lasserre (2009) showed that convex problems with SOS-convex data are solved by a single SOS relaxation and satisfy a Jensen inequality for truncated moment sequences. Scherer and Hol (2006) proved a Positivstellensatz for polynomial matrices and used it for robust polynomial SDPs that are affine in the decision variable. Henrion and Lasserre (2006) gave a moment hierarchy for deterministic PMI problems. Guo and Wang (2023–2025) treat robust PMI constraints that are nonlinear in the decision variable.
Let be the decision variable and the uncertain parameter. The data are a polynomial , polynomials in , a symmetric polynomial matrix and an symmetric polynomial matrix . With and , the problem is
It is assumed throughout that (RPMIO) has an optimal solution.
A symmetric polynomial matrix is an SOS matrix if for a polynomial matrix . A polynomial is SOS-convex if its Hessian is an SOS matrix, and a polynomial matrix is PSD-SOS-convex if is SOS-convex for every . Assumption 1 asks that be SOS-convex, that be PSD-SOS-convex for every , and that be compact. Assumption 2 asks for and an SOS matrix with a sum of squares. Assumption 3 is Slater's condition: some has for all and on .
The hierarchy uses two cones. The truncated matrix quadratic module consists of with SOS matrices and both terms of degree at most , where . Its dual consists of sequences of symmetric matrices whose moment matrix and localizing matrix are positive semidefinite, with . For and the diagonal matrix of the these give the scalar sets and . With the Riesz functional , the linear functional , and the degrees (in ) and (in ) of the data, the relaxation of order is
Write for the first-order moments of .
Under Assumptions 1–3,
and if minimizes (4.5) at each order, the limit along any convergent subsequence is a global minimizer of (RPMIO); if the minimizer is unique, converges to it.
In the order the proof uses them:
The result. Theorem 4.9 turns a problem with a continuum of matrix constraints into a sequence of finite semidefinite programs whose values decrease to the exact robust optimum, and whose solutions converge to robust minimizers when the minimizer is unique. Both bounds approach from above, unlike the scalar Lasserre hierarchy, which bounds from below. The paper's further results build on it: finite convergence under a flat extension condition (Theorem 4.11), the robust polynomial SDP case (Theorems 4.17, 4.18) and extensions beyond SOS-convexity (Section 5).
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. No part of the matrix-valued moment-SOS machinery has been machine-checked: there is no formal SOS matrix, matrix quadratic module, matrix-valued moment sequence or SOS-convex Jensen inequality in Mathlib or on this platform. The mission produces these definitions and a checked proof of the convergence theorem. The cited ingredients (Scherer–Hol, Lasserre's Jensen inequality) are reusable well beyond this paper.
The monotonicity in Proposition 4.6 is close to the definitions. The difficulty lies in the two limits. For the dual values, one must show that the moment vector of a nearly optimal strictly feasible point becomes feasible for (4.5) at some finite order. This needs the matrix Positivstellensatz of Scherer and Hol, whose proof rests on a matrix version of Putinar's theorem and is the deepest ingredient. For the primal values, a fixed atomic multiplier measure must exist (Proposition 4.1). Its existence uses a reduction of a convex semi-infinite program to finitely many constraints, which needs compactness of the unit sphere and Slater's condition, and then a Lagrange multiplier theorem. The natural first idea, weak duality at each fixed , is delicate here: the degree bound in is on , not on , so the pairing of a moment sequence with a module element is not obviously nonnegative at a fixed order. Part (ii) also needs a Jensen inequality valid for pseudo-moment sequences, not only for measures.
Polynomials are MvPolynomial (Fin ℓ) ℝ (in ) and MvPolynomial (Fin n) ℝ (in ). is a matrix over MvPolynomial (Fin ℓ ⊕ Fin n) ℝ, with Sum.inl the variables. Its coefficient matrices are read off through MvPolynomial.sumAlgEquiv. Symmetry of and , implicit in the paper's notation , is a hypothesis. Moment sequences are total functions on all exponents, but every object reads only the entries the paper's truncation contains, so the optimal values are those of the paper. Multi-indices of degree at most form a finite set that indexes the block moment and localizing matrices. The optimal values (4.4), (4.5) are extended reals, so an infeasible or unbounded relaxation is , not a junk . is a real infimum and every theorem assumes, as the paper does on p. 2, that (RPMIO) has a minimizer. Finitely atomic measures are explicit lists of points and PSD weights. Corollary 2.14 is formalized only for them, the case the proof uses.
Two encodings would trivialize the goal, and both are ruled out. Dropping the degree bound from would make constant in . Dropping the localizing condition from would forget altogether. A sorry-free sanity file exhibits data (, , , ) satisfying every hypothesis of the goal, so the goal is not vacuous.
A complete development needs: Hessians and SOS-convexity of multivariate polynomials, with convexity of SOS-convex polynomials; the Scherer–Hol matrix Positivstellensatz; Lasserre's Jensen inequality for SOS-convex polynomials and pseudo-moments; Lasserre's representation theorem for SOS-convex programs (used in Proposition 4.6); a reduction theorem for convex semi-infinite programs and the Lagrange multiplier theorem; and positive semidefiniteness of principal submatrices and Kronecker products. The SOS, moment-matrix and Jensen layers are reusable for any scalar or matrix moment-SOS mission. Proofs of the cited results as separate theorems are welcome.
Condition-based maintenance replaces a component on the basis of its observed state rather than its age alone. In many applications degradation accumulates in discrete events: a component sustains shocks, each of which adds a random amount of damage, and it fails once the accumulated damage reaches a threshold. Drent, Drent, Arts and Kapodistria (MSOM 25(1), 2023) study this setting when the parameters of the degradation process differ from component to component and are unknown. The decision maker observes the damage signal of the component in service in real time, learns its parameters by Bayesian updating, and must decide at each decision epoch whether to replace the component preventively. The application in the paper is a component of an interventional X-ray system, and the structural question it answers is classical in maintenance optimization: is the optimal policy a control-limit policy, and how does the limit move as the learner becomes more confident?
Damages are integer valued. Fix base weights . The natural parameter space is , the log-partition function is , and one shock causes damage with probability
a natural exponential family with sufficient statistic (geometric, Poisson and negative binomial damages are instances). Write for its -fold convolution.
Shocks arrive as a Poisson process with rate . The parameters of a new component are drawn from independent priors: with shape and rate , and has the conjugate density on , with normaliser . After a period in which shocks with total damage are observed, the hyperparameters update as . Hence the information state of a component is the triple , where is the degradation level, the number of shocks and the age, and its hyperparameters are .
Let , where and are the damage and the number of shocks in the next period under the predictive law at state , and let . With failure threshold , costs for preventive and corrective replacement, and discount factor , the value function satisfies the Bellman equation (10):
Preventive replacement is optimal at with when the first term of the minimum is at most the second, which is (19).
There are control limits such that, for every ,
and is non-decreasing for every . No numerical value of the limit is fixed; the theorem asserts only its existence and monotonicity.
The theorem reduces an infinite-horizon Bayesian replacement problem to a family of thresholds indexed by the shock count and the age, so an optimal policy can be stored as a table and computed by value iteration on a three-dimensional integer lattice. The monotonicity in formalizes an operational intuition: a component that has aged without failing is evidence of a slowly degrading unit, and the policy should tolerate more damage before replacing it. The paper also shows, by Example 5, that no such monotonicity holds in in general, so the result isolates the coordinates in which structure exists.
The result is proved in the paper; none of it has a machine-checked proof. Formalization adds two things. First, a complete development of conjugate Bayesian updating for a Gamma–Poisson rate jointly with a natural exponential family on , which is reusable for other compound Poisson learning models. Second, a verified answer to Lemma 2(i): the published proof of that lemma is incomplete (see below), so a formal proof would be the first complete argument for the age monotonicity on which the second half of Theorem 1 rests.
Conjugacy (Proposition 1) and the Gamma–Poisson mixture (Lemma 1) are calculations, but they involve integrals over and over with real-valued shape parameters. The structural results need stochastic orderings of mixtures and random sums, preserved through value iteration on a countable state space with an unbounded transition support.
The central difficulty is Lemma 2(i). The obvious argument is induction on value iteration: if is non-increasing in and the next-period increment is stochastically decreasing in , then is non-increasing in . That closure step requires the integrand to be monotone in every coordinate that moves, including the shock count , and is not monotone in , as the paper itself notes before Lemma 2. As grows the law of the shock count shifts down, so the step needs the conditional expectation of given to be monotone in , which nothing in the paper establishes. Numerical value iteration on several instances shows no violation, but a correct proof must use more than the one-step argument.
The Lean development fixes the following conventions.
The standing hypotheses of every theorem are , , , , , and one hypothesis the paper leaves implicit: for every the conjugate kernel at is integrable on with positive integral. It is imposed at every , reachable or not, because is defined on all of . It holds for geometric, Poisson and negative binomial damages; it excludes binomial damages and every damage law with (for such laws the kernel is not integrable at once is large relative to ). Proposition 1 additionally assumes for each observed damage.
Trivializing formalizations are ruled out: the kernel is not defined by its closed form, is the constructed value-iteration limit rather than any solution of (10), is the log-partition function, and the control limit must satisfy the equivalence in both directions for every .
A complete development needs Gamma integrals, Fubini on , convolution of pmfs on , the usual stochastic order and its closure under mixtures and random sums, and a contraction argument for the Bellman operator in the sup norm on bounded functions on . The exponential-family and stochastic-order layers are reusable beyond this mission. Proofs of individual milestones are welcome, as is a disproof of Lemma 2(i) if one exists.
Exploratory data analysis often summarizes a large data set by a small number of representative regions: histogram bins, the leaves of a density estimation tree, balls around cluster centres, or the regions chosen by a covering or -center optimization. Estes, Ball and Lovell (SSRN 3005997; Mathematics of Operations Research, 2021, doi:10.1287/moor.2020.1115) treat all of these as instances of one abstraction, the representative region selection (RRS) method, motivated by summarizing air-traffic ground-delay programs at Newark airport. The first half of their paper proposes axioms for the quality of such summaries. The second half (§6) asks a statistical question: when the data are an i.i.d. sample, do the summaries converge to the population they describe? This mission formalizes that convergence theory, culminating in the consistency of the density estimate that any RRS method induces.
Let be a set. An RRS method on is a pair : is a class of allowed regions, and maps every finite set to a finite set . The coverage region is . The method is sample-covering if , and sample-intersecting if every contains a point of .
Now let be a metric space with a σ-algebra containing every closed ball, and let be i.i.d. -valued random variables with law . Write , , and for the fraction of the first observations lying in . The support of is the set of points all of whose closed balls of positive radius have positive probability.
Regularity is imposed on the class, not on the method. A scalable class writes every region as with a shape parameter and a scale , non-decreasing in . It is uniform-scale if increasing the scale by swells every region by a closed ball of a radius that does not depend on the region, and uniformly continuous with respect to if changing the scale by changes the probability of every region by at most .
A family is arbitrarily precise if, for every , all methods far enough along the family eventually (almost surely, as grows) output regions of diameter at most . A method is uniformly positive with respect to a reference measure if its regions have -measure bounded below, and has asymptotically-bounded cardinality if it eventually outputs at most regions. When has a density with respect to , the RRS density estimate at averages over the chosen regions that contain :
and when no chosen region covers .
If the support of is compact with , is continuous, some closed neighbourhood of has finite -measure, and is an arbitrarily precise family over a uniform-scale class that is uniformly continuous with respect to , with each sample-covering, sample-intersecting, of asymptotically-bounded cardinality and uniformly positive, then almost surely
The goal shows that one estimator, defined uniformly from any RRS method, is -consistent under conditions that are checked once for the class of regions and once for the method. Histograms, density estimation trees, and the paper's own minimum-dominating-set and -center summaries (Corollaries 7.1 and 7.2) all become consistent density estimators as soon as they satisfy those conditions. Theorem 6.1 is of independent interest: it is a Glivenko–Cantelli theorem whose hypotheses are geometric and measure-theoretic rather than combinatorial, applying to classes for which no finite VC dimension is known.
The results are proved on paper; none is machine-checked. The mission produces a formal layer for region-based empirical processes (RRS methods, uniform-scale classes, the region-average density estimate) and machine-checked versions of the convergence chain. The formal statements also repair two places where the printed hypotheses are too weak (see Formalization scope), so a completed development certifies corrected theorems, not merely transcribed ones.
The regions an RRS method selects depend on the sample, so the law of large numbers cannot be applied region by region: there are uncountably many candidate regions and no fixed finite family to which the strong law applies. The uniform convergence of Theorem 6.1 must instead come from a finite approximation of the whole class, combining compactness of the support with the uniform-scale and uniform-continuity hypotheses, and the approximation has to work at every scale, including scales smaller than the approximation step. The goal adds a second limit: the error splits into a part on the coverage region, governed by the uniform estimate of Theorem 6.4, and a part on the uncovered portion of the support where the estimate is zero, governed by Corollary 6.2. The two limits ( inside, outside) and the almost-sure quantifier must be interleaved correctly, with countably many null sets collected over .
All statements live in the namespace RepRegion.Density, with one definitions file RepRegion.Density.Model. is a metric space with an arbitrary σ-algebra in which every closed ball is measurable (no Borel assumption); is a probability space; the observations are X : ℕ → Ω → M, measurable, mutually independent (iIndepFun) and identically distributed, indexed from . is P.map (X 0). The reference measure is an arbitrary measure on . Regions are Set M, a method is Finset M → Finset (Set M), and the scale map is R : Θ → ℝ → Set M, read only at positive scales.
Committed conventions:
A formalization in which the error is a Bochner integral, a supremum is a real sSup, or a diameter is Metric.diam would make the conclusions hold for junk reasons on non-integrable or unbounded inputs; those encodings are ruled out.
A complete development needs the strong law of large numbers for indicators (in Mathlib), finite nets of compact metric sets, and almost-sure hitting arguments for balls of positive probability. The region-based Glivenko–Cantelli theorem and the coverage results are reusable for any later mission on partition-based estimators. Proofs of the individual milestones, alternative arguments, and a version of the goal under continuity of on alone are all welcome.
Schur–Weyl duality says that on the tensor power of the natural representation of , the symmetric group acting by place permutations generates the full commutant of . It is the bridge between representations of general linear groups and of symmetric groups. Two extensions matter in representation theory and in the theory of tensor categories:
Brundan and Stroppel (arXiv:1107.0999) prove the combination: mixed Schur–Weyl duality for . It is the first step towards their main result, a Morita equivalence between and an idempotent truncation of Khovanov's generalized arc algebra , from which they derive that is Koszul for . Comes and Wilson obtained the same duality independently (arXiv:1108.0652); Shader and Moon had a partial result earlier (Commun. Algebra 30, 2002).
Timeline:
Fix integers and put . Let , with parity for and for . Let have basis with of parity , and the dual basis . The Lie superalgebra is , spanned by matrix units of parity , acting by
It acts on , with basis for , through and the sign rule . The super-commutant is the space of all linear maps , not necessarily homogeneous, annihilated by the action of every .
A walled Brauer diagram pairs the vertices on the top and bottom edges of a rectangle, with a wall after position : a vertical strand joins vertices on the same side of the wall and a horizontal strand joins vertices on opposite sides. These diagrams are a basis of ; the product puts under and multiplies by for removed circles. Colouring the bottom vertices by and the top vertices by , the weight is unless every strand has equally coloured ends, and otherwise raised to the sum of over the crossings of strands of colours plus over the bottom horizontal strands of colour (7.5). The right action
defines (7.12). For the permutation diagrams give (7.11).
For all ,
Theorem 7.8 identifies with the full super-commutant of mixed tensor space. Brundan and Stroppel use this to compare with a graded algebra built from Khovanov's arc algebra (Corollary 8.2, Theorem 8.10), which yields a grading on , its Koszulity for , and descriptions of the indecomposable summands of . The injectivity range says exactly when the walled Brauer algebra is faithfully realized on tensor space.
All statements are proved in the literature; none has a machine-checked proof that we are aware of. A complete formalization would need classical and super Schur–Weyl duality (Theorem 7.5 is the deep input, proved in the paper only by citation), the weight calculus of diagrams, and the sign bookkeeping of Lemma 7.7, which the authors call tricky.
Surjectivity onto a commutant is a double-centralizer statement, and the obvious route through semisimplicity fails: for the tensor space is in general not semisimple as a -supermodule. Theorem 7.5 instead rests on Berele and Regev's analysis of hook Young diagrams. Mixed tensor space adds a second obstacle: enters with signs both in its -action and in the dualities , and the reduction to via works only when every sign convention (crossings, bottom caps, the sign rule, the dual map) is matched exactly.
Fin (m + n), odd iff . A tensor space is given by a slot pattern Fin N → Bool (true = ); operators are complex matrices indexed by Fin N → Fin (m + n), with column = input basis vector.Fin N ⊕ Fin N (Sum.inl = top), reusing the published WalledBrauer.Blocks.WalledDiagram, its composition comp and its loop count loops. Crossings are counted by interleaving of endpoints along the boundary, which is the crossing set of a reduced drawing; Lemma 7.2 (isotopy invariance) is thereby absorbed.The following would trivialize or falsify the statement and are ruled out: a commutant of only, or one that drops the odd part or the signs; an unsigned slotwise action; a range statement with only one inclusion; an injectivity statement with only one direction. Not formalized: the paper's general Lemma 7.6 for arbitrary supermodules (no supermodule category in Mathlib), and everything involving . Contributions of a reusable Lie-superalgebra tensor layer and of Berele–Regev's hook-partition theory are welcome.
An insurance contract comes with a product disclosure statement (PDS): a document that groups the possible accidents into sections ("fire", "water damage", "theft") and lets the client choose a deductible in each. Standard expected-utility theory says the grouping is irrelevant: the client sees the same states, the same prices and the same probabilities however they are listed. Experimental and field evidence on framing and partition dependence says otherwise, and the subjectively aggregated subjective expected utility (SASEU) model of Burkovskaya (2019; axiomatized in the work cited in footnote 9 of the source paper) captures it: the consumer first computes an expected utility inside each section and then aggregates the sections with a second, concave function.
Burkovskaya and Li ask what this means for the insurer. When an insurer merges several sections of its PDS into one, how do the clients' deductibles move, and does the insurer's expected loss go up or down? Their answer, Theorem 1 of the paper, is a clean sign result under constant absolute risk aversion: merging sections whose probability-adjusted price is at least that of the no-accident state strictly raises the insurer's expected loss. The practical reading is that expensive sections should be kept separate.
There are finitely many states ; is the state in which no accident occurs. State has probability , Arrow price and loss ; the prices are normalized so that , and the consumer has income . For an event write , , and for its probability-adjusted price; .
A PDS is a partition of the states in which is a block of its own. The consumer chooses consumption in the default state and a deductible in each state , , subject to the budget ; deductibles may be negative. Writing for consumption in state (), the value of an event is and the SASEU utility is
Here with (Assumption 1, CARA), and , defined on , is increasing and strictly concave with non-increasing absolute aggregation aversion (Assumption 2, CARA or DARA). The solution of the demand problem (DP-) determines the insurer's expected loss .
A one-step aggregation replaces a family of at least two events of (not ) by their union , giving a coarser PDS with solution . The paper splits the change through an intermediate problem (DP-B): keep consumption off and the expenditure on fixed, and re-optimize inside ; call the solution . The aggregation effect is and the event-smoothing effect is .
If the merged events do not all have the same price and
then
The theorem turns a behavioral preference model into a prediction about a quantity the insurer controls and observes: the sign of the change in expected loss after a redesign of the disclosure statement depends only on prices and probabilities ( and ), not on the unobserved functions and beyond their qualitative shape. Lemma 1 makes the ranking of events observable, and the two-step decomposition, modeled on the Slutsky decomposition, separates the redistribution inside the merged section from the redistribution across sections. The paper uses these results to derive necessary features of an optimal PDS.
The results are proved on paper and, to the best of current knowledge, not formalized anywhere. A formal development adds a checked version of a comparative-statics argument whose printed form contains approximations: the closed forms of Lemma 2 and of the middle of Proposition 1 are first-order expansions printed as equalities, and the exact statements here avoid them. It also pins down the hypothesis , which the printed theorem omits.
The decision problem is a strictly concave program on a hyperplane, and its first-order conditions are explicit; the difficulty is comparative statics across three such programs, none of which has a closed-form solution. The sign of the event-smoothing effect is harder: it requires comparing the multiplier of (DP-B) with those of (DP-) and (DP-), which depends on the third-order behavior of (CARA or DARA), and then weighting state-by-state deductible changes by , whose signs are not uniform. A naive argument that "both effects move insurance from expensive to cheap states, so the loss rises" fails: when the weight on the default state's consumption change has the wrong sign. With four equiprobable states, , , , , , the finest PDS and , one has , but , so the printed "moreover" clause of Theorem 1, which assumes only , is false; the paper's own proof uses .
States form a Fintype with a distinguished default state; a PDS is a Finpartition of the whole state set with among its parts. Everything is real-valued. The consumer's choice is encoded by the consumption bundle with and , as the paper itself does; budget and loss are written in the paper's form. The utility index is a parameter of the model and Assumption 1 is the hypothesis CARA with ; all hypotheses on are imposed on the open set , and Assumption 2 includes (the paper's aggregation aversion, used in the proof of Lemma 1). The p. 17 phrase "non-decreasing absolute aggregation aversion" is read as non-increasing , which is what CARA or DARA means.
Solutions are hypothesized maximizers (IsDemand, IsIntermediate) and multipliers are any reals satisfying the first-order conditions; the well-posedness and FOC milestones guarantee that they exist, so no result is vacuous. Two hypotheses are added and disclosed in every affected item: in Theorem 1, and that the merged events do not all share one price (otherwise and no strict inequality holds). Proposition 1 enters without its approximate middle expression. Defining solutions by closed forms, hard-coding CARA into the utility, replacing (DP-B) by its first-order conditions, or pre-simplifying the budget would trivialize or alter the statements and is ruled out.
Not formalized: Lemma 2 and the approximation lemmas of §4.3 and the appendix (Lemmas 7–12, 16), Corollary 1 on the optimal PDS, and the monotone-PDS analysis of §4.2. Contributions that prove the milestones — in particular the exact multiplier comparison of Lemma 3 and the sign argument of Proposition 2 — are welcome, as are reusable lemmas on strictly concave maximization over a hyperplane and on CARA first-order conditions.
Fair division of indivisible goods asks how to split a set of items among agents who value them differently, with no money changing hands. Many allocation problems are not symmetric: partners in a venture hold different stakes, heirs inherit different fractions of an estate, and countries or departments receive budgets in proportion to size. Such settings are modelled by entitlements with , the share of the whole that agent is owed.
With divisible goods the proportional share is the natural target. With indivisible goods it can be unattainable (one item, two agents), and the literature replaces it with weaker share notions. For equal entitlements the standard one is the maximin share (Budish 2011), and constant-factor approximations of it are known. For arbitrary entitlements no share notion was known to admit any constant-factor guarantee for all agents simultaneously.
Babaioff, Ezra and Feige (arXiv:2103.04304, Mathematics of Operations Research, 2024) introduce the AnyPrice share and prove that it can be approximated within a constant factor for agents with additive valuations and arbitrary entitlements.
There is a set of indivisible items and agents. Agent has an additive valuation: a non-negative value for each item , and for a bundle . Agent has entitlement , and . An allocation partitions all items into bundles , some of which may be empty.
The AnyPrice share (Definition 1.1) is the value an agent can guarantee herself when the items are priced adversarially with total price and she buys her favourite bundle within budget :
An equivalent packing form (Definition 3.1) is the largest such that there is a probability distribution over bundles of value at least in which every item has total probability at most .
The Truncated Proportional Share (Definition 4.1) of an additive valuation is
the proportional share once every item value is capped at that same value.
The Bidding Game (p. 14) is a mechanism. Each agent starts with budget . In every round all agents bid an amount between and their remaining budget. A highest bidder (ties broken arbitrarily) takes any non-empty set of remaining items she can afford, paying her bid per item. The game ends when no items remain.
For every instance there is an allocation such that for every agent
In the Bidding Game every agent has a strategy that, whatever the others do, secures the largest of , and the value of her -ranked item.
The milestones are the paper's numbered results on the route to the goal, in attack order:
The result. Theorem 1.3 is the first guarantee of a constant fraction of any share for agents with arbitrary entitlements. The AnyPrice share is at least the maximin share and at least the pessimistic share. The guarantee therefore transfers to those notions, and it approaches the full AnyPrice share as . Because the Bidding Game is a concrete mechanism and the guarantee holds whatever the others do, every equilibrium of the game gives every agent at least that fraction. For three or more agents a constant factor is the best possible, since exact maximin-share allocations need not exist.
Formalizing it. The theorem is proved in the paper; to our knowledge none of it has been machine-checked. A complete development formalizes the two definitions of the APS and their LP-duality equivalence, the TPS and its comparison with the APS, and the Bidding Game together with the semantics of a strategy guarantee against arbitrary opponents. It also formalizes the two strategy analyses behind the constants and . The share definitions and the game-and-guarantee layer can be reused for other share notions and other bidding mechanisms.
The natural strategy, bidding one's normalized value for the best remaining item, secures only half of the TPS. It fails because an opponent can take items that the agent values close to the share threshold, and then her budget no longer translates into value at the original rate. The bound needs a two-stage strategy whose last stage is run on a rescaled sub-instance. Its analysis must show that the APS of the sub-instance, at half the rescaled entitlement, has not dropped by more than a factor . That argument rebuilds a feasible packing from the original one after the adversary's purchases. The bound needs an induction on the number of items that tracks the invariant through every possible behaviour of the other agents.
Items are Fin m and agents Fin n. Values are real, non-negative item values, with . Entitlements are a real vector with and as hypotheses. Every share takes its item set explicitly, so Lemma D.1 can be stated on . An allocation is a map from items to agents, so every item is allocated.
Three trivializing encodings are ruled out. The legality clause excludes illegal strategies, which would satisfy a guarantee vacuously because no play is consistent with them. The APS is never a junk sInf ∅ on a nonempty item set, and the TPS and the packing-form APS are suprema of nonempty, bounded-above sets.
Contributions of any milestone are welcome, as are lemmas about plays: suffixes of plays, budget non-negativity, and existence of a complete play when every agent follows a legal strategy.
Firms that develop technology in generations face a recurring choice: sell the product they already have, or hold it back while the next generation is developed. Selling it earns revenue now, but once the advanced product arrives, the earlier product cannibalizes part of its market. An established firm makes this choice by weighing development risk against cannibalization. A cash-constrained start-up faces a third pressure: it can only keep developing while it can pay for development, and selling the on-hand product is also a way to finance the next period.
Bhaskaran, Erzurumlu and Ramachandran (SSRN 3255345; Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0895) model both firms as infinite-horizon dynamic programs and compare their optimal strategies. For the established firm, the answer is governed by two thresholds on the per-period probability of development success. For the start-up, the paper relates its strategy to the same thresholds and to its cash. This mission formalizes the start-up's strategy in the low and intermediate success-probability regimes, together with the established-firm benchmark it is built on.
A firm holds an on-hand product that pays per period once launched, and develops an advanced product that pays per period once developed. Each period of development costs and succeeds with probability . Payoffs are discounted by , so the lifetime values are and . If the advanced product is launched after the on-hand product, it earns only per period, where is the cannibalization factor.
In each period the firm chooses among three actions: launch the on-hand product and stop development (LS), launch it and continue development (LC), or defer its launch and continue development (DC). Once the on-hand product is launched, only LS and LC remain.
Established firm. Its values (on-hand product not yet launched) and (launched) satisfy equations (1)–(2):
with , and .
Start-up. It holds cash , and unused cash earns interest at rate . After a period of development, its cash is if it deferred the launch and if it launched. Its value functions of the cash level satisfy equations (3)–(5):
and when , and when .
The established firm's thresholds (Proposition 1) are defined by its strategy: launch and stop for , launch and continue for , and defer and continue for .
For every cash level :
Proposition 2 answers the managerial question the paper poses: a cash-constrained start-up should behave like the established firm when development is unlikely to succeed, and must stop when it cannot fund the current period. In the intermediate regime it, too, should launch the on-hand product and keep developing. The established firm's thresholds of Proposition 1 therefore also organize the start-up's decision, and the start-up's cash enters only through whether development can be funded.
The paper also states a third part: above , a cash threshold below which the start-up launches. This part is false: with , , , , and , deferring is strictly optimal at and and launching at . Lemma 2, the route the paper takes to (iii), fails for the same instance. Lemma 1(ii) as printed also fails: when , launching and continuing need not beat launching and stopping. The mission states the corrected forms, so a machine-checked proof here settles exactly which parts of the characterization hold. No part of this paper has a machine-checked proof.
The start-up's equations are a functional fixed-point problem in which the action sets depend on the state: the defer option changes form at and launching-and-continuing requires , so and have jumps. Comparisons between actions therefore cannot be read off a single closed form. They must hold uniformly along the cash trajectories and , which shrink below the interest break-even and grow above it.
The paper's own argument for (ii) goes through Lemma 2, a single-crossing property of in the cash level, and that property is false. A proof of (ii) must instead show directly that deferral never beats launch-and-continue below , at every cash level, including those where the start-up can afford only a few periods of development. The threshold itself is defined by the established firm, so one must also relate the start-up's finite-horizon comparisons to the established firm's infinite-horizon ones.
Everything is real-valued. The expectations in (1)–(5) are explicit two-outcome sums, and no probability or MDP library is used. The parameters form a structure with the standing assumptions , , and , and . The paper allows , but needs ; is also assumed.
Trivializing formalizations are ruled out: and are not given by closed forms, launch-and-continue is not available without funding, (i) asserts strict optimality, and (ii) asserts continuation at every later funded cash level, not only at the current one.
Not formalized: Proposition 1(iv) (comparative statics of ), Proposition 2(iii) and Lemma 2 (false), Propositions 3–6 (built on the threshold or on approximations), and the extensions of §5. Contributions welcome: proofs of the milestones. The well-posedness milestone concerns a generic two-state discounted recursion with a state-dependent action set, and its proof is reusable beyond this paper.
The incremental knapsack problem is a multi-period extension of the binary knapsack problem. Items are inserted over a planning horizon whose capacity grows over time, and an item, once inserted, stays. Sharp (2007) and Hartline (2008) introduced it in their theses on incremental optimization. It models resource allocation in which the available budget grows predictably, such as investing a growing income or selecting bonds (Faenza–Malinovic 2018), and is related to assortment optimization over time.
Timeline.
An instance has items, item with profit and weight . It also has periods, period with a coefficient and a capacity , where and . A solution is a nested sequence of item sets with for every . The item is introduced in period . The objective is
and .
The algorithm of Section 3 of the paper fixes an accuracy and proceeds in four steps.
The subroutine is the λ⁺-bounded scheme of Section 2 (Theorem 3). Section 3 uses only two properties of it: the returned weight is at most the optimum (super-optimality, equation (8)), and the returned profit is at least .
The statement holds for every admissible profit grid, every subroutine with the two properties above, and every traceback. depends on alone.
The result. Theorem 1 settles the approximability of incremental knapsack up to the PTAS barrier. Strong NP-hardness excludes an FPTAS, so a PTAS is the best possible guarantee unless P = NP. It answers the open question of Bienstock et al. (2013, §5) in the strongest form. Its reduction to sub-problems with bounded ratios of values is a template for related multi-period problems; compare the generalized incremental knapsack problem of Faenza, Segev and Zhang (arXiv:2009.07248).
Formalizing it. The theorem is proved on paper; no machine-checked proof exists. A formalization checks a chain of eleven quantitative steps with explicit constants (, , , ). It also records the corrections the printed argument needs, listed under Formalization scope: the printed profit grid (7) is too short for Lemma 11 (with , one period and 20 unit items, the algorithm with grid (7) returns at most 3 items against ), and the single-cluster profit has to be read with the full-horizon . The model layer (nested solutions, item contributions, clusters) is reusable for other incremental optimization problems.
The obvious argument fails in two places.
First, a single dynamic program over all periods cannot use the Section-2 subroutine, whose running time depends polynomially on the ratio between extreme values. That ratio is unbounded in general. Clustering bounds within a cluster, but items introduced in the dropped bad intervals are lost. The loss is controlled only on average over the shift (Lemma 7), not for each shift.
Second, a near-optimal solution can spread one profit class over several clusters, which would couple the single-cluster sub-problems. Lemma 8 shows that after filtering negligible items, the classes form stars ordered across clusters. Its proof uses the gap of a factor that a bad interval creates between clusters.
The remaining steps are discretization arguments. Claim 3 is an induction comparing with . It works only because the profit requirement absorbs the grid rounding, and because super-optimality lets a smaller carry over. Claim 2 telescopes the resulting losses.
All declarations live in the namespace IncrKnapsack.PTAS, and one definitions file holds the whole model.
Representation.
Fin T, 0-based: the paper's period is t - 1.Fin n → Option (Fin T), the introduction period of each item; nestedness is built in.⊤ : WithTop ℝ, and minima over finite sets are Finset.inf.j = ℓ + 1.Additions and corrections, all disclosed in the items.
IsProfitGrid. It requires property (15) of p. 35 on , the range p. 22 gives , guarded by so that it is satisfiable on every instance.IsSubroutine, the guarantee of Theorem 3, met by the exact single-cluster optimum. The traceback may choose any minimizer.Everything else is constructed, not assumed: rounding, intervals, clusters, , and the glued output .
Ruled out. A trivializing formalization would assert that some feasible solution has , which the optimum itself satisfies. The goal is instead about the constructed output , and nothing about it is assumed.
Not formalized.
Contributions welcome. Proofs of any milestone, and a general existence lemma for admissible grids and tracebacks.
A routing decision can have a known immediate cost while its consequences depend on uncertain weather. A controller observes the current state, chooses an action, and then faces a random next state. A policy optimized for one estimated transition model may perform poorly when those estimates change. Chapter 13 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization studies this issue through finite-state control problems and illustrates it with aircraft routing. The mathematical target here is the finite-horizon theorem that evaluates and optimizes policies against admissible changes in transition probabilities.
The uncertainty model matters. Requiring nature to use one fixed transition matrix throughout the horizon couples its choices across time. Allowing each time, state and action to have its own admissible probability row gives a different problem. The latter is the setting of this mission and of the chapter's robust Bellman recursion. No assertion of exact solution of the stationary-uncertainty problem is included.
Let the state space be a finite nonempty set , and let the action space be a finite nonempty set , available in every state. The decision times are , with terminal time . A deterministic Markov policy assigns an action to every time and state . The stage cost and terminal cost are real numbers; they need not be nonnegative. The initial state has a given probability distribution .
A transition row gives the probabilities of the next state, conditional on time , current state , and action . For fixed policies, distributions evolve according to
The expected total cost is defined from these forward distributions:
For robust control, every row belongs to a nonempty closed set in the probability simplex. Rectangular uncertainty means that nature's admissible policies are the entire product of these sets: choices at different times, states and actions are independent constraints. The sets themselves may depend on time and need not be convex. These are the standing assumptions of Sections 13.2–13.3 of the book.
The first supporting target is Theorem 13.1.2. For a fixed controller and fixed transition rows, the expected cost equals the attained maximum of the linear program with terminal vector and inequalities
whose objective is . The second target, Theorem 13.1.4, is the nominal Bellman theorem: the recursion that minimizes the corresponding one-step expression over actions gives the optimal remaining cost at every time and state, and greedy policies for its values are optimal.
The goal is the full Theorem 13.3.1. With , define
Then is the minimum worst-case remaining expected cost starting at state at time , and
The target includes existence of controller policies choosing the displayed minimizing actions and nature policies choosing maximizing rows. Every such controller is optimal, and corresponding maximizing rows realize its worst cost. For any fixed controller , the separate evaluation recursion
must give its attained worst expected remaining cost, including the total value .
These statements connect three different objects: a forward stochastic evolution, optimization over complete policies, and backward value calculations. The robust theorem supplies both an optimal decision rule and an evaluation of uncertainty for a prescribed rule. Keeping the initial distribution arbitrary retains the distinction between statewise values and the value of the original control problem.
The results are established mathematics in the source; the work requested is their formal verification. A related proved robust-DP theorem uses time-independent uncertainty sets, nonnegative stage costs and a fixed initial state. This mission preserves the book's different data and attainment conclusions. Its local statements are open proof targets, not completed Lean proofs.
The central issue is relating the independent forward cost to the policy optimization and preserving all attainments. Choosing an individually favorable action does not by itself establish optimality over complete policies. Likewise, replacing a maximum by a real supremum leaves the existence of a maximizing nature policy unresolved. Closedness of the row sets and their probability constraints are substantive assumptions here. The fixed-policy and optimizing recursions must also be distinguished: nature's worst choices for an arbitrary controller need not be the rows selected from the optimal value function.
States, actions and decision times use finite index types, with nonempty state and action spaces. All costs and probabilities are real. Probability vectors have nonnegative coordinates summing to one. The model retains arbitrary initial distributions, time-dependent uncertainty sets and terminal costs. A zero horizon has no decisions and yields terminal expected cost.
The definition bundle includes forward distributions, expected costs, both Bellman recursions, the independent worst-cost function, and the policy-selection predicates. The theorems compare these independently defined quantities, rather than defining expected cost to be the desired Bellman value. Extrema use attained order predicates, with internal suprema restricted to the admissible nature policies. Full-horizon policies encode suffix policies by ignoring coordinates before the starting time.
Formalization Note Each theorem carries its needed concrete definitions in a separate namespace so it compiles without importing unpublished drafts. The definition item records the common reusable interface. Equation (13.1.3) supplies the forward-distribution definition rather than a tautological milestone. The nominal LP Theorem 13.1.3 is not a dependency in this selected route; its printed index and arbitrary-optimizer issues are recorded locally. No corrected or strengthened variant is posed.
A quantum circuit normally applies a sequence of gates to a prepared state. Verstraete, Wolf and Cirac proposed a different physical route: couple a quantum system to a memoryless environment so that dissipation drives it toward a state recording the circuit's computation. Their dissipative quantum computation construction places a clock beside the computational qubits and makes the circuit history a stationary state of a time independent master equation. A useful process must have a well identified stationary state and a rate of relaxation that does not collapse with the number of qubits or with the chosen gates. The paper argues for these properties in its DQC section and its efficiency appendix (Verstraete, Wolf and Cirac, 2008, pp. 1–2, 4–5).
The printed spectral gap formula and part of its supporting clock block do not describe the slowest decay of the stated generator. Direct finite dimensional calculations reveal a slower coherence sector. This mission therefore targets the stated stationary state and a corrected, explicitly ranged version of the paper's lower bound. The discrepancies and boundary cases are recorded in the formalization scope so that the target is a mathematical claim about the displayed Lindblad operators rather than an unchecked transcription.
Fix qubits and circuit steps. A computational basis string is a function from the qubit positions to . The clock register has basis for . A family of unitary gates acts on the qubit register. Its history vectors are and .
A jump operator resets qubit only when the clock is at zero: . For each neighboring clock pair, another jump operator moves in both directions, applying the relevant gate on the forward move and its adjoint on the reverse move. The Lindblad generator is the linear map on matrices
There is no Hamiltonian term. The proposed history state is the normalized density matrix
These are equations (1)–(4) of the paper, with the clock step index repaired as described below. The appendix introduces a gate removal unitary , a connected clock path matrix , and clock blocks with a penalty at time zero. Their spectra lead to the uniqueness and decay claims (paper, pp. 2, 4–5).
For every , , and family of unitary gates, prove that , that is positive semidefinite with trace one, and that the full kernel of consists of scalar multiples of . For , prove additionally that every nonzero eigenvalue satisfies
The bound applies uniformly across the number of qubits and the circuit gates. It is the corrected form of the efficiency conclusion on p. 5. The goal does not assert the printed formula , which is contradicted by the slowest coherence sector (paper, pp. 2, 5).
The milestones first establish stationarity and removal of the circuit gates by . They then target the one dimensional fixed space for identity gates, the first nonzero eigenvalue of the connected clock path, the penalized clock blocks, and the full generator's bound for identity gates. This follows the sequence of reductions described in the efficiency appendix while retaining the paper's exact clock constants where they are valid (paper, pp. 4–5).
The kernel statement identifies every stationary matrix, a stronger assertion than merely finding one stationary density matrix. The eigenvalue bound supplies a uniform spectral scale for the finite dimensional generator, independent of the circuit content. Together these make precise the part of dissipative computation that says the intended history is singled out and spectrally separated from other modes. A convergence time theorem would also have to control Jordan blocks or the operator semigroup and is outside this target; the paper itself notes this separate issue on p. 5 (paper, p. 5).
Formalizing the corrected claim creates a reusable finite matrix representation of a Lindblad generator and a circuit clock, plus independently usable path and boundary penalty spectral statements. The paper result is known in physics prose; these exact Lean statements are open proof goals in this proposal. The correction also prevents later arguments from importing a spectral equality that does not hold for the displayed process.
The gate operators couple the qubit register to the clock, so diagonalizing a clock matrix alone does not describe the generator. Even after the gates are removed, the Liouvillian acts on matrices, including coherences between two qubit states and two clock times. The decay of a one sided coherence at clock zero carries half the penalty of a population term. Reading every nonzero sector as if it had the population penalty produces the printed gap value and misses the slowest mode. The clock path also has to retain the first edge and its endpoint diagonal entries; omitting that edge changes the spectrum.
Lean uses matrices indexed by bit strings paired with the finite clock , and a complex linear endomorphism on those matrices. Gates are quantified as unitary matrices; they may act on all qubits, whereas the paper starts with nearest neighbor gates. The appendix's spectral argument is independent of that locality, so this is a disclosed generalization. The model also permits . Gates use zero based indexing: Lean's is the paper's and acts on the step . This repairs equation (3), which otherwise calls for both an undefined and an out of range clock state .
Uniqueness is restricted to : at an additional clock coherence is stationary. The strict bound is restricted to : direct diagonalization shows it fails for . The paper's printed corner coefficient is correct for a population sector, but a one sided coherence has coefficient . A milestone states the valid printed matrix fact and the corrected bound for all clock zero penalties . The connected path matrix follows the displayed spectral formula rather than the printed tridiagonal sum whose range omits the first edge.
The generator is defined from the jump operators by equation (1). It is not defined from the desired block decomposition or eigenvalues. The spectral assertion quantifies over actual nonzero complex eigenvalues and compares their real parts directly; no default valued infimum defines a gap. Work toward the mission may supply matrix identities, unitary covariance, tridiagonal spectra, or a direct finite dimensional analysis of the generator. The generic finite matrix Lindblad definition can be reused independently of this circuit model.
Banks hold capital against the risk of their trading books, and the amount is computed by a risk measure: a functional that assigns a real number to each random loss . For two decades the regulatory standard was the Value-at-Risk , a quantile of the loss. The Fundamental Review of the Trading Book of the Basel Committee (BCBS, 2019) replaced it by the Expected Shortfall , the average of the quantiles beyond level . The academic case for ES rested mostly on coherence (Artzner, Delbaen, Eber and Heath, 1999), that is, on subadditivity, a property that the regulator's documents do not take as their starting point.
Wang and Zitikis (SSRN 3423042; Management Science, 2021, doi:10.1287/mnsc.2020.3617) give an axiomatic answer in the regulator's own terms. Besides three basic requirements (monotonicity, law invariance, prudence), they ask that a portfolio whose components all suffer their largest losses in the same stress scenario receive no diversification benefit. They prove that these four axioms characterize exactly the family . Earlier characterizations of ES (Kusuoka, 2001; Acerbi and Tasche, 2002) start from coherence or comonotonic additivity; this one does not assume convexity, subadditivity or translation invariance.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. A random variable is a measurable ; a positive value is a loss. is the set of integrable random variables, its non-negative part, and , , the random variables with finite -th moment. means that and have the same distribution function.
For ,
A tail event of is an event with such that for almost all and ; a -tail event is a tail event of probability . A vector is -concentrated if its components share a -tail event. A functional on a domain may satisfy:
is -additive if whenever and share a -tail event.
For with ,
and in the forward direction for every stress event , uniquely.
The theorem identifies ES as the only normalized risk measure on meeting four requirements that can be checked one by one, three of which every risk measure in practice satisfies. It shows that the passage from VaR to ES in the Basel framework follows from a no-diversification-benefit principle for concentrated portfolios, independently of the coherence argument. Theorem 5 describes the dependence structures for which ES is additive, which is a statement about worst-case aggregation of ES with fixed marginals. Example 1 shows that VaR fails the same requirement.
The results are proved in the paper. None of them is machine-checked. The Lean library has no quantile-based Expected Shortfall on a general probability space, no notion of tail event, and no characterization of law-invariant linear functionals. A completed mission would supply all three, together with the first formal axiomatic characterization of a regulatory risk measure.
Each axiom is weak on its own. Additivity is required only for pairs sharing one fixed stress event, and nothing is assumed about other pairs. The obvious approach, extending additivity from the stress event to all comonotonic pairs and then invoking Kusuoka's representation, fails because pairs sharing a single tail event are far from comonotonic. The real work is in Lemma A.2: building from a -additive, law-invariant, monotone functional a linear functional on , which needs re-couplings on the atomless conditional spaces of and . Then come the identification of law-invariant linear functionals (Lemma A.1) and a monotonicity argument that excludes the mixtures with . On the ES side, Lemma A.7 and Theorem 5 need the dual representation of ES and a careful treatment of quantile ties, where and differ.
TailRiskSharing.VaRConv.IsAtomless (every measurable set of positive mass splits), the published cdf distFn and left quantile VaRL, all from the definition module TailRiskSharing_VaRConv_Setting. The paper's is VaRL P (1 - p). Atomlessness is stated on every theorem that uses it; Proposition 1 and Example 1 do not.Ω → ℝ, not a.e. classes. A risk measure is any ρ : (Ω → ℝ) → ℝ constrained only on its domain. Axiom M is the sure order and Axiom P pointwise convergence at every scenario, the weakest forms in the paper's Remark 1. Law invariance makes constant on a.s.-equal functions.VaRL (monotonicity, quantile transforms of a uniform variable), the dual representation of ES, existence of couplings with prescribed joint law on atomless spaces, and the representation of law-invariant linear functionals on . Each is useful beyond this mission, and contributions of any of them as separate lemmas are welcome.Many constructions in differential topology and infinite-dimensional Lie theory start from a continuous object and need a smooth one: a continuous section of a smooth bundle, a continuous map into a manifold, a continuous homotopy between smooth maps. Steenrod's approximation theorem (Steenrod 1951, §6.7) says that, for finite-dimensional bundles, a continuous section can be smoothed by a small homotopy through sections, without changing it where it is already smooth. Hirsch's textbook (Hirsch 1976, Ch. 2) gives the relative version for maps between finite-dimensional manifolds.
Gauge theory and the study of principal bundles whose structure group is an infinite-dimensional Lie group (current groups, diffeomorphism groups, gauge groups) need the same statement when the typical fibre is infinite-dimensional. C. Wockel (arXiv:math/0610252, 2006) proves it for a finite-dimensional base with corners and a fibre that is a manifold modelled on a locally convex space, combining Steenrod's argument with Neeb's approximation results for maps into locally convex spaces (Neeb 2002, App. A.3). The consequences in the paper are that smooth and continuous homotopy classes of sections, and of maps from a finite-dimensional manifold into a locally convex manifold, coincide; this is used in bundle theory for infinite-dimensional structure groups (Müller–Wockel 2006, cited as [MW06] in the paper).
A manifold with corners is a Hausdorff paracompact space with charts onto open subsets of the quadrant and smooth coordinate changes. A locally convex manifold is a Hausdorff space with charts onto open subsets of a locally convex space and smooth coordinate changes, where smoothness of means that all iterated directional derivatives exist and are continuous (Definition 0.1 of the paper).
A map is a locally trivial smooth bundle with typical fibre if every point of has an open neighbourhood and a diffeomorphism with . A section is a continuous map with . A map is smooth on a neighbourhood of a set if it is smooth on some open set containing .
For spaces , is the space of continuous maps with the compact-open topology, generated by the sets with compact and open.
Let be finite-dimensional and connected, a locally trivial smooth bundle with typical fibre , a continuous section, closed, open, and smooth on a neighbourhood of . Then for every open there are a section and a homotopy with
The result. The theorem turns continuous sections into smooth ones by homotopies that are small (they stay in any prescribed open set around the section) and relative (fixed where nothing needs changing). It yields that is dense in for the graph and compact-open topologies (Corollary 0.12), that every continuous section is homotopic to a smooth one and continuously homotopic smooth sections are smoothly homotopic (Proposition 0.13), and that smooth and continuous homotopy classes agree (Corollary 0.14). These are the statements needed to compare smooth and topological classification of bundles with infinite-dimensional structure groups.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. Mathlib has smooth partitions of unity on finite-dimensional manifolds with corners and local-to-global smoothing for maps into convex sets, but no density of in for the compact-open topology, no relative smoothing lemma, and no smoothing of sections of non-vector bundles. A formalization would supply these as reusable statements about Mathlib's ContMDiff, Bundle.Trivialization and C(M, Y).
The obvious argument glues local smoothings with a partition of unity, as for real-valued functions. This fails for sections of a non-linear bundle: convex combinations of points of , or of , are meaningless, so a partition-of-unity average of local smoothings is not a section, and the smoothing cannot be done in one global step. Any stepwise replacement must keep the section inside the prescribed open set , must not destroy smoothness already achieved near earlier parts of , and must avoid convergence arguments, since infinitely many steps are needed on a non-compact . The homotopy has to be continuous at the end where infinitely many steps accumulate. Finally, an infinite-dimensional is not locally compact, so all compactness must come from ; this is why the base is finite-dimensional while the fibre is not.
ContMDiff … ∞ (not the analytic ω). This is the one specialisation of the paper; non-normable locally convex fibres are out of scope.[T2Space M], and [ParacompactSpace M] (Theorem 0.11, Remark 0.4, milestone 6) or [SigmaCompactSpace M] (Proposition 0.7, Corollary 0.8, Lemmas 0.9, 0.10), as Definition 0.3 and the statements require; Theorem 0.11 adds [ConnectedSpace M]. is [T2Space N].SmoothNear), not smoothness on itself. Spaces for or are maps into the subtype with the compact-open topology, so neighbourhoods are taken in . A bundle is given by smooth Bundle.Trivializations covering ; " diffeomorphic to an open convex subset of " is a partial diffeomorphism with source and convex target. The homotopy is indexed by unitInterval and runs from at to at . "Support" is the closed support tsupport.A firm that can lower its unit production cost must usually spend money before it sells anything. That payment improves the margin on future sales but leaves less cash to fund production. If the firm borrows the shortfall, the investment can therefore change both its operating return and the cost of financing. Tanrisever, Joglekar, Erzurumlu and Lévesque (2021) study this tension in a two-stage model of a capital-constrained producer facing uncertain demand. Their Proposition 4 asks when the producer gains more from the investment in a market with bankruptcy costs than in a frictionless capital market.
The question matters for a production decision made before demand is known. A cost reduction may permit a larger production quantity and increase the return on each sale. It may also reduce the size and risk of the required loan, although paying for the investment consumes capital first. The paper isolates these effects so that the sign of the financing contribution can be examined separately from the direct operating gain. This mission covers that analytic comparison in §3 of the published paper, not its later numerical experiments or uncertain-investment extension.
The firm sells each unit for . It chooses a nonnegative production quantity before demand is realized; demand is uniform on with . Revenue is . The firm starts with unit production cost and capital . It may invest to reduce unit cost by , where is cost reduction per dollar. Its post-investment cost and capital are and . Without investment, the corresponding pair remains . These are the objects introduced on p. 91 of the paper.
For a generic cost-capital pair , production requires an external loan when . A competitive bank lends the shortfall and chooses a face value so that its expected receipt equals the loan principal. If sales revenue falls below the face value, the firm defaults; the bank recovers revenue less a proportion lost to bankruptcy, where . The bank's zero-profit equation is equation (2), and Assumptions 2–3 require the adjusted face value to be below and the face value to be below . A self-financed quantity has no loan. The firm's expected bankruptcy cost is the expected lost proportion of revenue in default. Its expected operating profit before the investment payment is
An equilibrium production quantity is any feasible that maximizes over every feasible nonnegative quantity. The mission compares equilibria for and at the same , then repeats the comparison at . Ties, if any, are allowed. The investment's net benefit is invested operating profit minus minus noninvested operating profit. The model and profit definition follow equations (1)–(4) on p. 92 of the paper.
The paper separates the net benefit into an operational effect , independent of , and a friction effect :
Here compares the perfect-market operating profits. Proposition 2 gives in the positive-margin regime. Proposition 3 defines by four integrals of the marginal rate of return and marginal cost of external funds . In particular, is an explicit quantity derived from the two production and financing curves; it is not defined from the difference between and . These formulas appear on pp. 93–95 of the paper.
The goal is Proposition 4. For any positive , at equilibrium quantities under friction and at their perfect-market counterparts, it states
The milestone list follows the paper's supporting claims: competitive pricing of the loan, properties of bankruptcy cost and marginal financing cost, the equilibrium equations, the positive operational effect, the area description of profit, and the decomposition of . Each claim is stated over the same model. The goal makes no assertion that every parameter choice produces a positive friction effect; it identifies the consequence when the integral in equation (8) is positive.
A positive means the investment's change to production and financing improves its value relative to a perfect capital market. Proposition 4 turns that model-specific sign into a comparison of two net benefits, each evaluated at its own equilibrium quantities. Without the financing calculation, the direct reduction in unit cost alone says only that the operational effect is positive; it does not determine how market frictions change the investment's value. The distinction is the paper's contribution in §3 Tanrisever et al. (2021).
The result is proved in the published paper; its proofs are assigned there to Online Appendix A, which is not included in this mission's canonical PDF. This formalization sets up an open Lean proof problem for that known result. It also gives reusable, explicit definitions for competitive zero-profit loan pricing under uniform demand, proportional bankruptcy loss, feasible production, and equilibrium profit. Those definitions can support later formalizations of the paper's threshold and comparative-statics results. The local proposal contains statements and compiled definitions, while the milestone theorems and goal remain proof obligations.
The comparison in Proposition 4 depends on an identity between two descriptions of profit. Equation (4) defines profit through expected revenue and the bankruptcy-cost expectation. Figures 2–3 and equation (8) express the same quantities through areas under marginal curves. Identifying the area with the expected-profit expression requires control of the loan face value as production varies and of the transition between borrowing and self-financed production. Merely subtracting the two profit formulas does not yield equation (8). The equilibrium quantity is also chosen over feasible production quantities determined by the bank's lending restrictions, so a stationary marginal equation needs justification as an equilibrium characterization. These are the main obligations represented by the earlier milestones.
Lean uses real-valued parameters and a normalized interval integral, , for every expectation under . The parameter record holds ; a standing predicate requires their stated positivity, , and . The friction proportion remains a variable in . Quantities are nonnegative with no imposed upper bound. Lending feasibility enforces Assumptions 2–3; self-financed quantities require no loan. Equilibrium quantities are hypotheses quantified over all feasible competitors, avoiding a default-valued supremum or a manufactured maximizer.
Two conventions are stated explicitly. First, is added for Propositions 2–4: with , the first upper limit in the paper's equation (8) can be negative, and its displayed implication fails. Second, and where . On the positive-loan branch, is the lower closed-form root of the bank's equation (2), and agrees with the printed formula. The paper usually assumes capital is insufficient for production; this proposal also allows self-financed production, with the convention disclosed in the statements. The definition of is the four-integral equation (8), rather than , and expected profit remains equation (4), rather than an area definition.
The development needs interval integration, real square roots and derivatives, convexity, and optimization over feasible real quantities from Mathlib. The definitions and theorems use the main text of the published article; proofs in its online appendices and the later numerical and stochastic extensions are outside the present scope.
The Lie superalgebra , a central extension of the Lie superalgebra of infinite matrices of finite support, appears in the representation theory of the vertex algebra and in Howe-type dualities with (Kac–Radul; Cheng–Lam). Its irreducible quasi-finite highest weight modules of positive integral level are indexed by generalized partitions , and their characters had been computed by Cheng and Lam in terms of hook Schur functions and Littlewood–Richardson coefficients.
J.-H. Kwon (arXiv:math/0605005) gave these characters a tableau model. He introduced A/B-semistandard tableaux, pairs of super-semistandard tableaux attached to a generalized partition, showed that their generating function is the character in question (Theorem 5.2), and developed an insertion scheme that yields an RSK correspondence, a Littlewood–Richardson rule, and a Jacobi–Trudi type determinant formula (Theorem 4.5). The paper notes that this determinant formula for the characters of -modules had not been observed before. The combinatorics rests on Stembridge's rational semistandard tableaux (1987), which model the rational representations of , and on Berele–Regev's hook Schur functions (1987).
Let and be linearly ordered, at most countable sets, each split into even and odd letters, .
A filling of a skew Young diagram with letters of is -semistandard if its entries weakly increase along rows and down columns, even letters strictly increase down columns, and odd letters strictly increase along rows. The weight of records how many times each letter occurs, and .
A generalized partition of level is . It is drawn against a vertical line: row has boxes to the right of the line if and boxes to the left if .
An A/B-semistandard tableau of shape is a pair with and for some and partition , . Both tableaux are drawn against the line of , so enlarging by one and by a full column gives the same pair. The character is
a power series in the symbols and . At level one, is defined for every , negative included.
A rational -semistandard tableau of shape fills the diagram of with right of the line and left of it, rows weakly and columns strictly increasing, subject to Stembridge's compatibility condition between columns and . Its content has , and counts the tableaux of shape and content .
For infinite , and every , ,
The entries are level-one A/B-characters, not complete symmetric functions. Unlike , they do not vanish for .
The result. Theorem 4.5 is the super, rational analogue of the Jacobi–Trudi identity. Through Theorem 5.2 it becomes a determinant formula for the characters of the irreducible quasi-finite -modules of positive level (Corollary 5.4). Specialising and recovers formulas for and for the Howe duality. Milestones 2–6 develop the rational Kostka theory along the way: its shift invariance, its triangularity, and its role in an RSK correspondence for A/B-tableaux.
Formalizing it. The theorem is proved in the paper; nothing in it has a machine-checked proof. Mathlib has semistandard Young tableaux and symmetric polynomials, but no Schur polynomials as tableau generating functions, no Kostka numbers, no RSK, and no classical Jacobi–Trudi identity. Milestone 6 is therefore new to formal mathematics in its own right, and it is a prerequisite for the goal's proof.
The obvious attack proves the classical Jacobi–Trudi identity once and then transfers it. That fails here for two reasons. The entries with are nonzero, so the classical vanishing that truncates the determinant is unavailable. And the expansion is an infinite sum over generalized partitions, so the comparison with (4.5) leaves an error term supported on . Killing it requires both the shift invariance of the rational Kostka numbers and the uniqueness of coefficients in infinite combinations (Corollary 3.23). The combinatorial input, Corollary 4.4, is a weight-preserving insertion bijection for pairs of super tableaux, built from row and column insertion, rectangular complements and Stroomer's theorem. Each of these is substantial to formalize.
SuperTableaux.JacobiTrudi, with one definitions item.LinearOrder and Countable; the grading is a function odd : A → Bool, where true means odd.MvPowerSeries (A ⊕ B) ℤ. The variable Sum.inl a is and Sum.inr b is the symbol , which is literally the ring . The coefficient at a monomial is Nat.card of the set of tableaux of that weight; milestone 1 proves that set finite.toLex, which is the paper's "reverse lexicographic ordering" of p. 23.HasSum/Summable in the coefficientwise topology, never tsum.A formalization that defines by a determinant or product formula, sums over without the identification (every coefficient becomes Nat.card of an infinite set, i.e. ), or drops the parity conditions trivializes the goal; the definitions here are the tableau generating functions of (3.13)–(3.14).
A complete development needs Kostka numbers, Schur polynomials as tableau generating functions, the classical Jacobi–Trudi identity, RSK for super tableaux, and coefficientwise convergence in multivariate power series. All of these are reusable beyond this mission. Contributions are welcome on any milestone, and on intermediate lemmas such as the classical Jacobi–Trudi identity.
In the fluid queuing model (Vickrey's model) of flows over time, a continuum of infinitesimal particles travels from a source to a sink through a network whose arcs have capacities and transit times. Each particle picks a route that minimizes its own arrival time, and a dynamic equilibrium (a Nash flow over time) is a flow in which no particle can arrive earlier by deviating. Dynamic equilibria are a basic model of congestion in road traffic and communication networks.
Koch and Skutella (2011) showed that the derivatives of a dynamic equilibrium are normalized thin flows with resetting, and Cominetti, Correa and Larré (2015) proved that such thin flows always exist, which gives existence of equilibria. Computing a thin flow, however, was known to be efficient only in the two extreme cases where no arc or every arc is resetting. Kaiser (2022) casts thin flows as a linear complementarity problem, studies how they depend on the flow value, and shows that on two-terminal series-parallel networks the whole family of thin flows, for all flow values at once, can be computed in polynomial time. The key quantitative fact behind that algorithm is a bound on the number of breakpoints of the thin-flow labels as a function of the flow value. This mission formalizes that bound and the chain of results it rests on.
A network is a finite directed multigraph with vertex set , arc set and two vertices . It is a shortest path graph if is acyclic and every vertex is reachable from . Fix a set of resetting arcs and capacities . A static –-flow of value is a vector on the arcs that is conserved at every vertex other than and has net outflow at .
Along an arc a label is propagated by
Labels correspond to the flow if for every and on every arc with ; such an is a normalized thin flow with resetting (Definition 4).
The label function maps each flow value to the corresponding labels, with label at , of a normalized thin flow of value . A breakpoint of is a value around which some component of is not affine.
A two-terminal series-parallel multigraph is built from single arcs by series composition (sink of glued to source of ) and parallel composition (sources glued, sinks glued).
For a two-terminal series-parallel multigraph , any and any capacities : the label function exists, is continuous on , has finitely many breakpoints, and
The milestones follow the paper's proof path.
The bound is what makes the recursive computation of along a series-parallel decomposition run in time polynomial in the size of the network. Each composition step is linear in the number of pieces, and Theorem 31 keeps the number of pieces linear in . Combined with the paper's §5, the result computes dynamic equilibria in series-parallel networks for piecewise constant, and more generally right-monotone, inflow rates. For general graphs the complexity of computing a thin flow with resetting is open: the problem lies in PPAD, and no polynomial algorithm is known. The bound is attained already for a single non-resetting arc, whose label at is .
The results are proved in the paper. None of them has been formalized: there is no machine-checked theory of flows over time, thin flows or directed series-parallel graphs. A formalization adds three things. It gives a checked LCP formulation of thin flows, which is reusable for any equilibrium computation in this model. It gives a checked parametric analysis (existence, uniqueness, monotonicity and piecewise linearity of the labels). And it gives a complete account of the counting argument for parallel composition, which the paper extends from the sink's label to the whole label vector only in outline ("Repeating the counting more carefully…").
Existence (Theorem 13) is not elementary. It combines a principal-minor computation for a block matrix with a theorem from LCP theory: a -matrix whose LCP has only the trivial solution at zero data has a solution for every right-hand side. Mathlib has neither. Piecewise linearity (Proposition 17) likewise uses that solution sets of an LCP are finite unions of polyhedra.
The breakpoint count is subtle in the parallel case. Splitting the flow between the two parts is generally not unique, so is not simply a composition of and . The proof constructs a piecewise linear selection of the split and counts where its pieces can change. A tempting shortcut is to bound only the breakpoints of the sink's label . That is weaker than what is claimed, which is a bound for the entire label vector.
Net) with arc types and tail/head maps, so parallel arcs are first-class.Finset of arcs and capacities are real with .IsLeast, never sInf.T.toNet of terms T : SPTerm built from arc, series and par. Every member of Definition 28's class is isomorphic to such a graph, and all quantities here are isomorphism-invariant.Set.encard in Lemmas 29–30 and with Set.ncard plus finiteness in the goal.A complete development needs:
The LCP layer and the network and series-parallel layer are reusable beyond this mission. Contributions to either are welcome, as are proofs of the elementary milestones (Lemma 7, Lemma 11, Theorem 14, Corollary 15) independently of the rest.
Statistical decision theory compares two experiments by asking which one is more useful: one experiment is deficient with respect to another if, in every decision problem, it achieves nearly the same payoff. The randomization criterion turns this operational comparison into a structural one: an experiment is -deficient exactly when a Markov kernel (a randomization) maps the better experiment to within of the worse one in -distance. Its exact case, the Blackwell–Sherman–Stein theorem, is a standard tool in statistics and economics, and the approximate version is the basis of Le Cam's theory of comparison of experiments (Strasser 1985; Torgersen 1991).
Quantum information asks the same question for quantum devices: when can one channel be simulated from another by further processing, and how is that detected by tasks? A short timeline of the results this mission builds on:
This mission formalizes the central result of the last paper: the randomization theorem for post-processings of channels (Theorem 3, p. 15).
All spaces are finite-dimensional. A Hilbert space is with its standard basis and is the algebra of complex matrices. A C-algebra* is a block-diagonal algebra with ; full matrix algebras and the diagonal (classical) algebras are the extreme cases. is the set of density matrices in .
is the real space of Hermitian linear maps from to , paired with by , where is the trace of a map on matrices.
An admissible family of positive cones (Definition 1) assigns a closed convex cone of Hermitian maps to every pair of spaces, with , and . Here , and are the positive, completely positive and entanglement-breaking maps. Examples are , , and the -positive maps. Restricted to algebras, is a cone in , and is the dual of under the pairing. A -channel is a trace-preserving element of ; they form . is the replacement map .
The two norms on are
where and are the orders of and . For , is the usual diamond norm.
Given channels and , a decision algebra , decision rules and payoff maps , is -post-processing deficient with respect to , written , if every payoff achievable from is achievable from up to (Definition 3).
For the following are equivalent:
Moreover, if , then (all decision algebras) iff .
Lemma 1 (trace property of ); identity (1); (proof of Lemma 2); (p. 8); Corollary 8 (ii) for ; the dual formula (4) for ; Corollary 8 (iii) for channels; and Lemma 4, monotonicity of both norms under channels.
Theorem 3 says that a channel is approximately worse than another in every post-processing decision task exactly when every post-processing of the better channel can be approximated, in the (-)diamond norm, by a post-processing of the worse one. It contains the classical randomization criterion (classical algebras, ) and Matsumoto's quantum criterion (cq-channels, ) as special cases. Through the Moreover clause, it reduces deficiency over all decision algebras to a single one, the output algebra. Because is arbitrary, the same statement covers positive, -positive and completely positive simulation.
The paper gives complete proofs, and the result is not open. No machine-checked version of it, of the base-section norms, or of admissible cone families exists on the platform or in Mathlib. A complete development gives a reusable, Mathlib-only layer for Hermitian maps between block algebras, their trace pairing, cone families, and the diamond norm defined relative to a cone; and a formal proof of a quantum decision-theoretic equivalence that relies on a minimax theorem.
The equivalence (i)⇔(ii) and the implication (iv)⇒(i) are short once the norm duality is available: Corollary 8 (ii) and (iii), which identify norms of positive elements and differences of channels with suprema of payoffs. Formalizing those duality statements is the first obstacle. They rest on the appendix theory of base sections, including the fact (Theorem 8) that and are dual norms, which uses an extension theorem for positive functionals and closedness of the cones.
The step (iii)⇒(iv) is where the argument cannot be done pointwise. Condition (iii) gives, for each payoff separately, a decision rule depending on ; condition (iv) needs one that works for all at once. Exchanging the two quantifiers requires a minimax theorem on the compact convex sets (the unit ball of ) and , followed by formula (4). Compactness of needs closedness of .
All definitions are in one module, ChannelRandomization.PostProc.Setting, and depend only on Mathlib.
sInf/sSup. Their sets are nonempty and bounded when the dimensions are positive, and in dimension 0 both sides of every statement are 0.List.TFAE) together with the Moreover clause. "" means that the identity of lies in for every .The structure of admissible families is not vacuous: the positive maps form an instance, constructed sorry-free in a separate verification file. A formalization that defines the norms by the supremum formulas, fixes , drops the closedness of the cones, or restricts the decision algebra to one kind proves a different statement and does not count.
Out of scope are the pre-processing theorem (Theorem 5, whose proof the paper omits as "practically the same as the proof of Theorem 3"), the cq- and qc-channel specializations of §3.2.1–3.2.3, the pointwise deficiency results, and the Choi-matrix formula of Theorem 1.
Contributions are welcome at every level: proofs of the milestones, a general Lean theory of base sections and their norms (Theorem 8, Corollary 8 in abstract form) that would serve other ordered-vector-space arguments, and alternative proofs of (iii)⇒(iv) using Mathlib's minimax theorem.
In the standard model of costly sequential search, a consumer knows from the start which products exist and pays to learn how much each is worth. Weitzman (Econometrica 1979) solved this problem with a single number per product, the reservation value: inspect in decreasing order of reservation values, and stop as soon as the best product found is worth more than every remaining reservation value. This rule underlies most structural models of online search in marketing and industrial organization.
In many markets, though, consumers do not know every option at the start. On a retail platform they scroll through results a page at a time, and each page shows only partial information (price, picture, rating) about the products it reveals. Learning the full value of a product requires clicking on it. The consumer therefore chooses among three kinds of action: buy, inspect a product already seen, or discover more products. R. P. Greminger, Optimal Search and Discovery (Management Science, 2022), shows that this richer problem is still solved by comparing reservation values, now three kinds of them.
Timeline. Weitzman (1979) treats inspection with a known set of products. Keller and Oldale (JET 2003) prove that a Gittins index policy is optimal for branching bandits, in which taking an action creates new actions. Choi, Dai and Kim (Econometrica 2018) give the eventual purchase theorem for Weitzman's problem. Greminger (arXiv 2019, journal 2022) adds the discovery action and characterizes the optimal policy.
A risk-neutral consumer gets utility from buying product . The partial valuation is visible as soon as the product is discovered. The rest of the value, , is revealed only by inspection. The pairs are independent draws of , where and .
In period the consumer has a consideration set of inspected products (valuation known), which also contains an outside option worth , and an awareness set of discovered products for which only is known. The available actions are:
With probability , the consumer believes, a discovery is the last one. Recall is free, payoffs are not discounted, and the objective is the expected purchase value minus the total costs paid.
The three reservation values are defined against a hypothetical outside option . The search value is the root of
The purchase value is . The discovery value is the root of
where is the optimal value of the reduced problem whose only products are the outside option and the newly discovered ones.
Let and . Every policy that obeys
is feasible and attains the largest expected payoff among all feasible policies, from every initial state.
The theorem turns a dynamic program over an infinite state space into comparisons of three reservation values. The discovery value still requires optimizing inspection among the products in one newly discovered batch. The paper builds on the result in several directions. Its second main result, an eventual purchase theorem under limited awareness (Theorem 2), is derived from Theorem 1. So are its closed-form expected payoff, its comparisons with random and directed search, and the claim that the discovery value, and hence the optimal policy, does not depend on the belief .
Formalizing it gives the first machine-checked statement of a Weitzman-type optimality theorem with an outside option, partial information and a branching action. As far as a search of the Prove2Me catalog shows, Weitzman's rule itself is not formalized for undiscounted search with an outside option, so the milestones on the search value and on the closed form of are new formalizations in their own right. The paper's proof relies on two external results, Keller and Oldale's branching bandit theorem and Choi, Dai and Kim's Corollary 1. A complete formal development either proves these or replaces them with a direct argument.
The obvious argument is to treat the problem as a multi-armed bandit and apply the Gittins index theorem. It does not apply as stated. Discovery creates new arms, the problem is undiscounted and ends at a purchase, and the number of future discoveries is random. The branching bandit theory that covers creating arms is stated for discounted rewards and in a derivative form, , which needs almost-everywhere differentiability of value functions in the outside option. The step specific to this paper is to show that the index of discovery does not depend on whether later discoveries are possible. That needs the index to be non-increasing along search, which the paper derives from stationarity. Finally, the rule policy must be shown to stop almost surely with an integrable payoff even when infinitely many products can be discovered ().
All objects live in the namespace SearchDiscovery.Reservation. A model SDModel carries , the kernel κ (), cs, cd, nd and . Its standing assumptions are , , finite second moments of and of each κ x, and a finite unconditional mean of (footnote 36). An information state lists the purchase values of (the outside option is one entry), the partial valuations of , and whether discovery is available. A run is driven by an explicit probability space: the hidden of each initial awareness product, and for each discovery i.i.d. pairs together with an independent Bernoulli() flag saying whether the discovery was the last.
The formalization commits to the following readings:
Several shortcuts would make the statements trivial, and the formalization rules them out:
FollowsRules is not vacuous;A complete development needs:
The Weitzman/Pandora layer (search values, the closed form of the reduced problem) is reusable well beyond this paper. Contributions to any milestone are welcome, as are alternative proofs that avoid the derivative form of the branching bandit theorem.
Traffic and packet networks are congested over time, not only on average. The fluid queuing model (Vickrey's bottleneck model on a network) captures this: every arc of a network is a bottleneck queue followed by a link of fixed length. Users entering at a source choose routes so as to arrive at the destination as early as possible, given the queues that the other users create. The resulting dynamic equilibrium (also called a Nash flow over time) is the dynamic analogue of a Wardrop equilibrium and a standard object in dynamic traffic assignment.
A basic question about any such dynamics is its long-run behaviour. When a constant inflow enters forever, do queues grow without bound, oscillate, or settle down? Cominetti, Correa and Olver (arXiv:2112.10412, Operations Research 70(1), 2022) answer this: if the inflow rate does not exceed the minimum cut capacity of the network, every dynamic equilibrium reaches a steady state after finite time, in which all queues are constant.
Timeline.
A fluid queuing network is a finite directed multigraph with a source and a terminal . Each arc has a capacity and a delay . A constant inflow rate enters at . Every node is assumed reachable from .
A flow over time consists of measurable, locally integrable inflow rates and queue lengths with , governed by the queue dynamics
The queue releases flow at rate while it is nonempty, and the released flow leaves the arc time units later. Flow is conserved at every node other than , with external inflow at .
A particle entering arc at time leaves it at . The earliest arrival label is the minimum over – paths of . An arc is active at if , i.e. it lies on a currently fastest route. A flow over time is a dynamic equilibrium if, for almost every time , flow enters an arc at time only if for some at which is active. It attains a steady state if there is with for every arc and every .
The potential of the paper is
for every dynamic equilibrium. No bound on is asserted.
The result. Theorem 3 shows that, under the min-cut condition, the equilibrium dynamics settles. Queues freeze, so travel times become constant. The limit regime is described by the linear program (P), a min-cost flow, and its dual (D). Without the theorem it would be unknown whether congestion can oscillate forever in a network with enough capacity. The condition is sharp: if exceeds the minimum cut capacity , the arcs of a minimum cut grow unbounded queues (p. 4). The result is a prerequisite for the paper's convergence-time bounds and for its constructions of long transient phases.
Formalizing it. The result is proved on paper; to our knowledge, no part of the theory of flows over time with queues has been formalized. The mission produces a Lean model of fluid queuing networks and dynamic equilibria for general measurable inflows. Its definitions (queue dynamics, earliest arrival labels, active arcs, thin flows with resetting) can be reused for the other results of this literature (existence of equilibria, the price of anarchy over time, convergence-time bounds). The paper's own proofs of the §2.3 facts cite earlier work, so a complete development also formalizes parts of Koch–Skutella (2011) and Cominetti–Correa–Larré (2015).
The potential argument is short once its ingredients exist, but each ingredient is analytic. The labels are minima of compositions of exit-time functions that depend on the queues. The queues depend on the inflows, and the inflows are constrained by the labels. Absolute continuity and almost-everywhere differentiability of the labels, and the identification of their derivatives with a thin flow, need the regularity theory of this fixed point.
The step "there are only finitely many possible derivatives, hence a uniform " is the delicate point. It relies on the thin-flow system determining from the pair (active arcs, queuing arcs). As printed ("for all subsets "), that uniqueness fails when contains a cycle of zero-delay arcs carrying no flow. A proof must therefore use the structure of the active-arc sets that actually occur. The bound needs max-flow/min-cut and LP weak duality in the network's own encoding.
Everything lives in the namespace NashFlowLT.SteadyState. The network is a structure with tail, head : E → V over finite types, so parallel arcs are allowed, as in the paper's Example 1. Its data are nu, tau, u0, s, t.
The standing assumptions , , , and reachability of every node from form Network.Standing. The last two are added to the page: is implicit in a source–sink pair, and reachability is needed so the minimum defining is over a nonempty set.
Flows over time carry the inflows fin and the queues z as data. The queue equation is imposed in integrated form from , inflows are measurable, nonnegative and integrable on bounded intervals (an added hypothesis), and conservation holds almost everywhere. All functions of time are real-valued on , and only matters.
Labels are minima over simple paths (lists of arcs visiting distinct nodes), never solutions of the Bellman equations. With zero-delay cycles those equations admit spurious solutions.
The min-cut hypothesis is stated as " is at most the capacity of every – cut". The bound is stated against every feasible point of (P), so no infimum is defined. The equality case of Theorem 2 and the thin-flow characterization are posed for almost every ; the nonnegativity of holds at every point of differentiability.
The goal quantifies over all dynamic equilibria. It must not be replaced by a statement about one constructed equilibrium, by the label condition of Lemma 1, or by a hypothesis that is bounded or that there are finitely many phases. A sanity file exhibits a one-arc instance that satisfies every hypothesis and is a dynamic equilibrium.
Contributions welcome: proofs of the milestones, a proof of the thin-flow characterization, a max-flow/min-cut bridge to the platform's existing LinearOptimization.max_flow_min_cut, and the uniqueness of for the active-arc sets that occur in equilibria.
An ordinary Lie algebra has a vector space and an antisymmetric bracket satisfying the Jacobi identity. In a Lie 2-algebra, the vectors become the objects of a linear category, and the Jacobi identity is witnessed by a morphism called the Jacobiator. This lets the Jacobi identity hold coherently rather than as a strict equation. Baez and Crans developed this notion to make the relation between categorified Lie algebra structures and short chain complexes precise (Baez–Crans, §§3–4). The result of interest here is their equivalence between semistrict Lie 2-algebras and two-term -algebras, Theorem 36.
A 2-vector space is a category internal to vector spaces over a field : its objects and morphisms are vector spaces; source , target , identity , and composition are linear. Composition is read in diagrammatic order, so means first , then . The identity laws require . Lemma 6 shows that linearity forces the composition of composable and to be
The arrow part of is . It remembers the displacement of after its source is translated to zero. A 2-vector space can therefore be compared with the two-term complex . Conversely, a complex gives arrows with source , target , and identity (Baez–Crans, Proposition 8).
A semistrict Lie 2-algebra is a 2-vector space with a skew-symmetric bilinear bracket functor and a completely antisymmetric trilinear natural isomorphism
The Jacobiator obeys the Jacobiator identity, an equality between two composites of morphisms through the octagon in Definition 22. A homomorphism is a linear functor equipped with a bilinear natural transformation satisfying Definition 23’s square. The resulting one-cell category is (Baez–Crans, pp. 18–21).
A 2-term -algebra has vector spaces , a differential , brackets of degrees adding to at most one, and a trilinear map . Its equations are precisely (a)–(i) of Lemma 33. In particular, measures the failure of the ordinary Jacobi identity, and equation (i) is its four-input coherence law. Homomorphisms are chain maps with a skew bilinear comparison map satisfying all three equations of Definition 34. They form (Baez–Crans, pp. 28–30).
The goal is Theorem 36, an equivalence of the two one-cell categories:
The milestone path begins with Lemma 6’s forced composition law. Proposition 8 states the underlying linear equivalence , and the 2-cell part of Theorem 12 identifies linear natural transformations between linear functors with chain homotopies between the corresponding chain maps, through their arrow parts. Propositions 25 and 35 establish identity, composition, and associativity for the homomorphisms on each side. Equation (3) reconciles the two expressions for the bracket of morphisms under the construction . The proof of Theorem 36 then supplies on objects and morphisms and the reverse construction . The goal additionally requires functoriality and natural isomorphisms, which the paper asks the reader to check or construct (Baez–Crans, pp. 30–36).
The equivalence says that the categorical and chain-complex descriptions carry the same one-cell algebraic information. It permits constructions expressed with morphisms, functors, and a Jacobiator to be studied with a differential and higher brackets, and conversely. Later classifications of skeletal Lie 2-algebras in the paper use the two-term viewpoint (Baez–Crans, §§5–6).
Theorem 36 is proved in the cited paper; the machine-checked proof is the work this mission seeks. The local files compile the definitions and open theorem statements, and a sorry-free check exhibits nonzero carriers satisfying the principal structures. The milestones expose the individual obligations that a complete Lean proof must discharge. This mission does not claim a formal proof of the result or of the stronger 2-categorical statement.
A bilinear bracket on objects and morphisms is not enough to define a bracket functor: it must preserve source, target, identity, and simultaneous composition. In the direction, two ways of decomposing a pair of morphisms suggest different bracket formulas. Their equality is equation (3), using Lemma 33(f). In the direction, the interaction of two degree-one elements comes from the bracket functor’s preservation of a commuting square. The Jacobiator’s naturality and octagon must then correspond to the remaining identities. Finally, the constructions must act on homomorphisms and yield natural isomorphisms of functors (Baez–Crans, pp. 31–36).
The field has characteristic different from two in Theorem 36 and its §4.3 milestones, matching the standing assumption on p. 27. The §3 and §4.1 results retain the paper’s broader field convention. All vector spaces are unrestricted in dimension. A 2-vector space stores and defines its composition by Lemma 6. A 2-term -algebra is represented directly by Lemma 33(a)–(i), with and ; the general graded Definition 32 is outside scope.
The two categories are represented by raw object and morphism data with explicit predicates for lawful homomorphisms. An equivalence consists of functors preserving lawful morphisms, identities, and composites, together with natural isomorphisms in both directions. This representation keeps Propositions 25 and 35 as proof obligations and expresses the one-categorical content of Theorem 36. The stronger Theorem 39 asserts a 2-equivalence, but its 2-cell work is left without proof in the source and is not the goal here.
The Lie 2-algebra side retains the bracket’s functoriality on composable morphisms, the full naturality square, and the Jacobiator octagon. Its coherence is not replaced by Lemma 33’s equations: doing so would collapse the goal into a comparison of two copies of the same definition. The infrastructure for two-term complexes, 2-vector spaces, raw categories, curried multilinear maps, and their homomorphisms is reusable. Of Theorem 12 only the 2-cell correspondence is stated; the 2-functoriality of and the 2-naturality of the comparison isomorphisms are not. Of Proposition 25 only the one-cell category laws are stated; the 2-homomorphisms of Definition 24 are not. A formalization in which the Lie 2-algebra side is defined by arrow-part equations, or in which the equivalence omits the natural isomorphisms or the category laws, would trivialize the goal and is excluded. Contributions proving the displayed category laws, the and constructions, their functoriality, and the two natural isomorphisms are welcome.
Quantum mechanics is usually written in linear-algebraic terms: states are vectors of a complex Hilbert space, observables are Hermitian operators, and expectation values pair the two. Classical mechanics is written geometrically: states form a symplectic manifold, observables are functions on it, and dynamics is a Hamiltonian flow. A line of work starting with Kibble (1979) and continued by Cirelli, Lanzavecchia, Heslot, Ashtekar–Schilling (arXiv:gr-qc/9706069) and Brody–Hughston (arXiv:quant-ph/9906086) recasts quantum mechanics in the classical language: the Hilbert space, seen as a real manifold, carries a Kähler structure (a symplectic form, a Euclidean metric and a compatible complex structure), and observables become real quadratic functions on it.
Cariñena, Clemente-Gallardo and Marmo (arXiv:math-ph/0701053v2) organise this correspondence around one map, the momentum map of the unitary group acting on Hilbert space. The algebra of observables carries two products, a Lie product (the commutator) and a Jordan product (the anticommutator). The paper's Proposition 5 states that the momentum map carries both products, read as tensors on the dual of the unitary Lie algebra, to the symplectic and Euclidean parts of the Kähler structure of Hilbert space. This mission formalizes that statement in finite dimension.
Fix and let , with . The space of observables is the real vector space of Hermitian complex matrices. On it the paper defines:
Through (4), the dual is identified with Hermitian matrices . Each observable gives a linear function . On the paper defines the Lie–Poisson tensor (11), , and the Jordan tensor (12), .
On the Hilbert space side, use real coordinates . Every complex matrix defines the quadratic function . The canonical Poisson bracket is , and the contravariant Euclidean structure is . The momentum map is
For Hermitian and every :
In the paper's notation: , and .
In attack order:
Proposition 5 says that the algebra of observables can be read off Hilbert space geometrically:
This is the dictionary behind geometric treatments of the Schrödinger equation as a Hamiltonian flow. It also underlies variance and uncertainty relations written through the metric, and the reduction to projective space and density states that the paper discusses in §§2.5 and 4. The paper presents it as an alternative to the GNS construction for pure states.
The paper's proof is "Direct verification", and Lemmas 1–3 and Proposition 1 are classical facts about Hermitian matrices. No step is open. What the mission adds is a machine-checked version with every normalisation pinned, as listed in Formalization scope:
The paper uses both the Hermitian picture (3), (4), (6) and the anti-Hermitian picture (5), (11). The formal statement fixes the signs and factors needed to read their relation precisely. The prior-art search for this mission found no published Prove2Me statement with the same finite-dimensional objects and conclusion.
The algebraic milestones are short computations once the definitions are unfolded. The work concentrates in the goal, whose two sides live in different worlds.
The left side is built from real partial derivatives of real-valued functions on , viewed as . Its derivatives must be computed in the directions and and then recombined into complex inner products.
The right side is a trace of a product of matrices with the rank-one matrix .
The difficulty is that the derivative formulas use real coordinates while the tensor formulas use complex matrix products and traces. Their normalizations and sign conventions must agree at the level of the full identity, including the in and the factors of in the quadratic functions.
Replacing the derivative-defined brackets by their closed forms would make the goal trivial and is not permitted, see below.
All objects are defined in one definitions module in the namespace GeomQM.MomentumMap, over Mathlib's Matrix (Fin n) (Fin n) ℂ and vectors Fin n → ℂ.
Committed conventions.
IsHermitian hypothesis. Lemma 5 is about an arbitrary complex matrix, and equivariance needs no hypothesis. is allowed, since every statement then holds trivially, as in the paper.fderiv ℝ applied to Pi.single k 1 and Pi.single k I. This is the paper's .Ruled out. The brackets on are defined through real derivatives of arbitrary functions, never as or . The tensors on are trace formulas, never rewritten as quadratic functions of . Either shortcut would make bullets 2 and 3 hold by definition.
Not in scope. The following are not formalized:
Welcome contributions. Proofs of the milestones and of the goal, and general lemmas that would be reusable beyond this mission:
Fin n → ℂ;Integrable spin chains with a Lie superalgebra symmetry are lattice regularizations of two-dimensional field theories with target-space supersymmetry, such as the Gross–Neveu models and sigma models on superspaces, which appear in the study of disordered systems, polymers and the AdS/CFT correspondence. Their spectra are described by the nested Bethe ansatz: each eigenvalue of the transfer matrix corresponds to a family of complex numbers, the Bethe roots, solving a system of algebraic equations, the Bethe ansatz equations (BAE). The nested algebraic Bethe ansatz for general closed chains was carried out by Belliard and Ragoucy (arXiv:0804.2822).
C. Candu, Continuum Limit of gl(M|N) Spin Chains (arXiv:1012.0050), studies the antiferromagnetic chain of alternating fundamental and dual representations. Its §4 shows that a class of solutions of the BAE is fully characterized by solutions of the BAE, which embeds the spectrum into the spectrum. This is the algebraic counterpart of cohomological reduction (Candu–Creutzig–Mitev–Schomerus, arXiv:1001.1344), in which the chain is the cohomology of an odd nilpotent element acting on the chain. The paper uses this relation to compare all chains with fixed, and concludes that their continuum limits share the Gross–Neveu-like particle content.
This mission formalizes that restriction and lift of Bethe ansatz equations.
Let and . A grading assigns to each position a parity and a sign ; counts the even and the odd positions. The loop weight is . The simple roots are , ; is odd when .
For a chain of length the source terms are
For each type let be a finite set of pairwise distinct complex numbers and , with . The BAE (2.9) state that for every and every root ,
With (2.11), the energy (2.18) of a solution is
The paper works throughout under .
Fix with A1 ( odd) and A2 ( has no source term, ). R1 identifies the roots of types and . The reduced system deletes grading positions and root types : it is the BAE of a chain with simple roots .
Under A1, A2, R1 and non-degeneracy of the roots,
and . The forward direction is the restriction R1–R2; the backward direction is the reduction of the lift to "a solution … to either eq. (4.2) or eq. (4.4)".
The restriction gives an explicit map from Bethe solutions to Bethe solutions that preserves the energy. Iterated, it relates every chain to the chain, which is how the paper identifies the vacuum and the massive excitations of the chains in the continuum limit (§5–§6). It is also a concrete, equation-level check of cohomological reduction.
The result is proved in the paper by direct algebra. The result is not formalized anywhere on Prove2Me, which has no Bethe ansatz equations of any kind. This mission produces a precise statement of the nested BAE with their grading-dependent signs, shifts and boundary conventions, and a verified version of the restriction, including the bookkeeping that the paper leaves implicit: the reindexing of types, the change of the source terms of the reduced chain, and the invariance of the energy.
Each step is elementary algebra; the difficulty is bookkeeping. The sign , the shifts , and the boundary cases differ between the original and the reduced system: after deletion, the neighbour of type is type , and the last source term and the partial sums in (2.11) are those of a different grading. A naive argument that matches equations by position, or that treats the reduced system with the original source terms, misses these shifts. The backward direction needs non-degeneracy, because recovering (4.4) from (4.6) and (4.2) requires dividing by the two sides of (4.2).
Everything is in the namespace SuperBAE.Restriction and works over . Positions and types are natural numbers, and a grading is a Boolean function (true = odd), with . Root sets are Finset ℂ, which encodes the paper's requirement that no two roots of the same type coincide. equals outside . Only the homogeneous chain is modelled. The BAE are in division form, so every theorem carries a regularity hypothesis: at each root of type , the values , , , and are nonzero. This is the non-degeneracy the division form presupposes; it is imposed on the original system only. The standing assumption is kept as , although the algebra of §4 does not use it. A1 is the Boolean condition , and A2 is , .
The reduced system is the same BAE predicate applied to the deleted grading on positions and the reindexed roots, with its own source terms and its own loop weight. A formalization that writes the reduced equations by hand, or passes to the reduced chain as a parameter, is trivializing and is ruled out. Without the regularity hypothesis, Lean's convention would make degenerate configurations satisfy (2.9) vacuously; regularity excludes this, and a verification file checks that the hypotheses of the goal are jointly satisfiable and that regularity is not vacuous.
Out of scope: the Yang–Baxter and Yangian structure, the walled Brauer algebra, the weight constraints (4.1) and (4.8), existence and uniqueness of lifted type- roots, inhomogeneous chains, the boundary case of §4.3, and the thermodynamic limit. Proofs of the milestones are welcome, as are lemmas that put the finite-product manipulations of -polynomials into a reusable form.