Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.
Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).
The buyer's type is his valuation for the good. His utility is if he receives the good and pays , and if he only pays . The seller's belief about is a cumulative distribution function with density on an interval , , with throughout and .
A direct mechanism is a pair , : the buyer reports a type , receives the good with probability and pays . Write . The mechanism is incentive-compatible if for all , and individually rational if for all . The seller's expected revenue is .
For the extreme-point argument, denotes the space of functions on with the norm, and the set of increasing functions with values in . A point of a convex set is an extreme point if for every at least one of , lies outside .
In the nonlinear pricing model of §2.3 the good is divisible, quantity costs the seller with , and the buyer's utility is , with , , , and . The seller maximizes expected profit . The distribution is regular if the virtual valuation is increasing.
If , then the mechanism
maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule with values in ; the statement fixes no distribution and no constant.
Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.
All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.
The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing with values in may do better than every deterministic threshold rule unless one shows that expected revenue is linear in and that its maximum over the infinite-dimensional set is attained at an extreme point. That step needs compactness of in and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.
Types are real numbers; every function of the type is a total function and every condition quantifies over only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density , positive and integrable on with total mass , and tied to it by . No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes monotone and bounded and measurable, so every expected revenue is a genuine integral.
The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with ; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; in Lemma 2.5; and in Proposition 2.6 the two-case rule for and the payment . The goal fixes , for existence and quantifies over every incentive-compatible, individually rational completion at the tie.
The space is of almost-everywhere classes, because the book's "norm" on bounded functions vanishes on null functions; is the set of classes with an increasing -valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.
A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with valued in .
Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in , and the maximum principle for linear functions on compact convex sets. Contributions to any of these are welcome.
Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.
A logical context is represented by its set of possible truth assignments, and a statement (up to logical equivalence) by its truth set . Negation, conjunction and disjunction are complement, intersection and union; the certainty is and the impossibility is ; " is narrower than " means , and are compatible when .
An experimental domain is a family of statements that contains and , is closed under finite conjunction and countable disjunction, and has a countable basis : every element of is obtained from by finite conjunctions and countable disjunctions. Its theoretical domain is the closure of under negation, finite conjunction and countable disjunction. A possibility is a non-impossible that, for every , is either narrower than or incompatible with it; denotes the set of possibilities. The verifiable set of a statement is , and the natural topology on is the topology generated by . A domain is decidable if it is closed under negation.
The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the axiom are thereby derived rather than assumed, and the cardinality bound limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.
The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of ; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.
Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family . Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction and the empty disjunction ; generation with negation (NegFinConjCountDisj) includes . Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.
Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.
It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.
Mine A holds units of gold and mine B holds . At time a proportion of the machine's effort goes to A and to B (Eq. (7.3)). With the gold remaining, the probability that the machine still works and the expected gold mined, the process is defined by Eq. (7.2):
with , , , . The mining rates and the failure rates are positive. The objective is the expected total gold .
In the three-choice problem (§ 12) a third decision removes gold from A at rate and from B at rate , and fails at rate . A control is a triple with (Eq. (12.2)). For a horizon , the switching functions of Eq. (12.5) are computed along a control. For instance,
They measure the first-order gain from shifting effort towards each decision at time . The linear forms
and the quantity (Eqs. (13.2)–(13.3)) organize the analysis.
For the two-choice process, the maximum of is attained by the policy
The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes over all measurable controls with values in .
Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope , and on the line it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: means that removes gold at a higher failure cost than an equivalent mixture of and .
On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.
The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and is preferred near the -axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into " on the interval".
0, 1, 2 for .Useful infrastructure: the derivative formulas (13.1) for the , a first-variation lemma for under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.
The optimal inventory problem asks how much of an item to stock when demand is random, ordering costs money, and running short costs more. Arrow, Harris and Marschak formulated it as a sequential decision problem in 1951 (Optimal inventory policy, Econometrica 19), and Dvoretzky, Kiefer and Wolfowitz studied its structure in 1952–53. Chapter V of Richard Bellman's Dynamic Programming (1957) treats the problem through a single functional equation for the minimal expected discounted cost. It shows that when ordering and shortage costs are proportional to quantity, the optimal policy is described by one number, a constant stock level , computed from the demand distribution alone.
This result is an early form of the base-stock (order-up-to) policy. Base-stock policies are the standard structure in periodic-review inventory theory: Karlin (1958), Scarf's theorem (1960) and Veinott (1965) extend it. Chapter V is also a worked example of a point the book makes throughout: the method of successive approximations determines the shape of an optimal policy, and not only its existence.
A single item is stocked over an unbounded sequence of periods. At the start of a period the stock is . The decision maker orders up to a level , at cost with . A demand then arrives, with probability density : for , , and . If , the next period starts with stock . If , the excess is bought at the penalty rate and the next period starts with stock . Costs one period ahead are multiplied by a discount factor .
Write for the minimal expected discounted cost from stock . Enumerating the cases gives Bellman's equation (5.1):
A policy assigns an order-up-to level to each stock . It is optimal when attains the minimum. The mission takes the equation itself as the model; no stochastic process is built.
The equation has exactly one solution among measurable functions bounded on . If , the equation
has exactly one root , and for every the minimum is attained at
If , the minimum is attained at : never order.
is its absolute minimum.
The theorem reduces an infinite-horizon stochastic control problem to a scalar equation. Rewriting it as gives the critical-fractile form familiar from the newsvendor problem, with the discount factor entering the fractile. The level depends on the demand law only through its distribution function, and the policy does not depend on the current stock except through . This is what makes the policy implementable and its parameters estimable from data, the point Bellman makes in § 1. Theorem 3 shows the same structure over a finite horizon, with levels that rise as more periods remain. Theorem 4 marks where the structure starts to depend on the demand density.
As far as a search of the platform shows (queries recorded in the mission files), none of these results has a machine-checked proof. Base-stock theorems on the platform, Veinott's multi-product theorem and Gallego–Özer's advance-demand model, use discrete periods, different excess-demand conventions and different state spaces. They do not cover a continuous-demand, lost-sales-at-penalty, discounted functional equation. Formalizing Chapter V would produce an explicit solution of a nonlinear integral equation of renewal type, a uniqueness theorem for that equation, and a Lean treatment of the renewal equation that other applied-probability missions can reuse.
Two steps resist the obvious argument. First, the minimization is over the unbounded set , and the unknown enters through a convolution with . The operator is a contraction on bounded functions, which settles uniqueness in the bounded class. Uniqueness among functions bounded only on finite intervals (Chapter IV's class) is not a contraction statement, because the minimization reaches arbitrarily far to the right. Second, optimality of for requires to be nondecreasing on . There is defined only implicitly, as the solution of a renewal-type equation, and this monotonicity is a positivity statement about that solution, not a consequence of the first-order condition. Checking that the first-order condition holds at is not enough, and neither is checking that the candidate function satisfies the equation at the single level .
Functions are ℝ → ℝ; only their values on enter. Integrals over are Lebesgue integrals and are interval integrals. The equation is stated with an infimum (IsGLB), as Chapter IV writes it, and every policy statement asserts that the minimum is attained (IsLeast) at the stated level. Uniqueness is asserted on (Set.EqOn … (Set.Ici 0)). Solution classes require measurability. This is the standing convention that makes meaningful; without it a non-measurable function would make the integral default to . "" is read as positivity on .
Conventions and corrections, each stated in the items:
A trivializing formalization is ruled out. The goal does not assume the stated policy is optimal, does not assume is given, and does not take as a hypothesis. It asserts the existence of the root, the existence and uniqueness of the solution, and attainment of the minimum at for every .
Theorems 2 (two items, joint density), 5 (one-period delivery lag) and 6 (strictly convex ordering cost) are not part of this mission. Theorem 2 is printed with a sign error in (6) and garbled marginals. Theorem 5 states no hypotheses. Theorem 6's (9b) contradicts itself at . Welcome contributions include a Lean library for the renewal equation (existence by successive approximation, positivity, differentiation under the convolution), which Theorem 9 needs and which is independent of inventory theory, and the contraction estimate for on bounded measurable functions.
A multi-stage decision process is summarized by its optimal return function , which satisfies a functional equation. In Chapters I and II of Dynamic Programming (Princeton University Press, 1957), Richard Bellman proves existence and uniqueness for particular processes: allocation of resources, gold mining. Chapter IV abstracts these arguments into theorems about whole classes of equations. The same scheme reappears in later chapters (multi-stage games, the calculus of variations) and in every later treatment of dynamic programming.
Two points explain why the chapter is still worth formalizing. First, uniqueness is always claimed within a stated function class, and the choice of class is part of the theorem: an equation of this kind can have many solutions, and only one of them lies in the class that the process singles out. Second, the chapter covers equations that are not contractions in the supremum norm, in particular Type One, where the shrinking happens in the state rather than in the function values.
Let carry the Euclidean norm , let be a nonempty set of decisions, and let and . The general equation (1.1) is
Here is the one-stage return, the next state and a multiplier: a discount factor or a survival probability.
An equation is of Type One with constant under the following conditions. contains the null vector . is bounded on bounded parts of , uniformly in , and . . . Finally, with , the series converges for every .
It is of Type Two under the following conditions. is bounded on bounded parts of . On each bounded part, for some . maps into , and either or is bounded.
The successive approximations are and .
The equation of the third type of § 8 lives on the probability simplex of distributions , with vertices . It reads
Each maps into itself, and the -th coordinate of is never . is the minimal expected time to drive a system into state with certainty, by observing the state (cost , then continuing from the observed vertex) or by applying one of the operations (cost ).
For a Type One equation there is exactly one solution on , among functions continuous at and zero there, of
It is the pointwise limit of the successive approximations from , and also from any that is continuous and zero at and bounded on bounded parts of . If , and are continuous in on bounded portions of , uniformly in , the solution is continuous on every bounded portion of .
Theorem 1 guarantees that the optimal return of a process whose decisions shrink the state is well defined and computable by iteration. It applies without assuming that the supremum over decisions is attained and without regularity of the maximizing decision. Theorems 3 and 4 give quantitative continuous dependence of the solution on the reward. This is what justifies approximating a process by a simpler one. Theorem 5 is a uniqueness result for an undiscounted minimum-time problem, where no contraction in the supremum norm is available.
All of these results are classical and proved in the book. None is formalized: the platform's related statements treat finite state spaces with a fixed policy (FoundationsML.ReinforcementLearning.bellman_equations_unique_solution), or Karlin's compact-decision-set setting with nonnegative rewards and an explicit vanishing-tail hypothesis (KarlinDP.Deterministic.unique_solution_of_vanishing_tail), or finite-state stochastic shortest paths (BertsekasDP.ssp_main_theorem). This mission adds machine-checked versions over a continuum of states and an arbitrary decision set, with the function classes stated exactly.
For Type One, the natural idea is to apply the Banach fixed-point theorem in the space of bounded functions. That fails: allows no contraction in the supremum norm, and the solution need not be bounded on . Contraction happens only along trajectories, , so every estimate must be localized to balls and summed along radii . Uniqueness then rests on continuity at rather than on a global norm.
The suprema over an arbitrary, possibly infinite, decision set are not attained in general, so no argument may select a maximizing decision. For the third-type equation, neither a contraction nor a shrinking of the state is available: the operations need not move towards . Uniqueness among bounded solutions requires controlling how long a solution can keep choosing an operation other than observation.
The state space is EuclideanSpace ℝ (Fin N), is a Set, the decision set is a nonempty type S, and functions are total, EuclideanSpace ℝ (Fin N) → ℝ. Only their values on matter, and uniqueness is asserted on . The equation is encoded with IsLUB, so the supremum is genuine and has no junk value. The successive approximations and the radii , use real iSup/sSup, evaluated only where the book's boundedness conditions hold. "Continuous at " is continuity within .
Conventions and corrections:
Fin M.A trivializing formalization would state uniqueness among all solutions of the equation, which is false because constants solve it when and . Equally trivializing would be to encode the supremum with a junk-valued sSup, so that unbounded return sets pass for solutions. Both are excluded: the class is part of each statement, and the equation is an IsLUB.
Theorem 6 of the chapter (the optimal inventory equation) is not part of this mission; it is treated in the inventory mission of the series. Welcome contributions include a reusable library for localized successive approximations and the equicontinuity lemmas that the continuity statements need.
Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) treats the stochastic gold-mining process, the first stochastic multi-stage decision process of the book whose optimal policy can be written down in closed form. There Bellman introduces decision regions, the sets of states at which a given first choice is optimal, and where he obtains an index rule: at every state, compute one number per alternative and choose the largest. The same kind of rule was later developed in general form as the Gittins index for multi-armed bandits (Gittins 1979), and the gold-mining process is an early instance of what that literature calls a deteriorating bandit, in which each alternative's index can only decrease when it is used.
Bellman first described the process in his 1954 survey The theory of dynamic programming, with the two-mine index rule stated as Eq. (8.3), and it appears on Prove2Me in a mission on that paper. The book gives the full chapter: existence and uniqueness, the rule for two mines, its extension to several outcomes per use and to any number of mines, the finite-horizon process, and a stability estimate.
Two mines, Anaconda and Bonanza, hold amounts of gold and . A single machine is used in one mine at a time. Used in Anaconda, it mines the fraction of the gold there and stays in working order with probability , or is destroyed without mining anything with probability . Bonanza has the corresponding data and . Before each use the operator chooses a mine (choice A or B), and the process stops when the machine is destroyed. The aim is to maximize the expected total amount of gold mined.
The expected return under an optimal policy satisfies the functional equation
where is the return of an A-choice followed by optimal continuation and that of a B-choice. The -stage returns are and . The A-region of a value function is the set of points of the closed quadrant where the A-branch attains the maximum; the B-region is defined in the same way.
In the generalization, a use of mine has outcomes: outcome occurs with probability , yields and leaves in the mine, and is the probability that the machine is destroyed. With mines the equation is
"The solution" of an equation always means its unique solution in the class of functions bounded in every rectangle , (or every box ), per Bellman's footnote 7.
Under , , , , equation (4) has a unique solution bounded on boxes, and at every state any index maximizing
attains the maximum in (4). Ties among the maximizers may be broken arbitrarily.
The index rule reduces the choice among mines to computing numbers. Each one depends only on its own mine, as the ratio of immediate expected gain to immediate expected loss. Without the theorem, an optimal policy for the -stage process is a word in letters whose number of candidates grows like . The finite-horizon theorems show that the same rule is exactly optimal for every horizon beyond a finite , and the stability theorem bounds how much the solution moves when the equation is perturbed.
Theorem 2's content is also the target of the 1954-paper mission, where it is stated for the supremum of expected returns over choice sequences. Those statements (BellmanTheoryDP.GoldMining.gold_mining_decision_rule, …optimal_return_functional_equation) are included here as reference items. They concern a different object: the book's theorems are about the unique bounded solution of (5.1), and the two coincide once (5.1) is known to characterize the optimal return. None of the chapter's results has a machine-checked proof on the platform yet. The -mine rule (Theorem 4) and the finite-horizon results (Theorems 5 and 6) are not stated anywhere on the platform.
The equation for the boundary between the regions involves the unknown function , so equating the two branches of (5.1) does not by itself locate the boundary. Comparing the orders "A then B" and "B then A" determines the index line, but only on the assumption that there are just two regions. Bellman's Figure 1 shows why that assumption carries real content: homogeneity alone only makes the regions unions of sectors, which could alternate. The assumption is not automatic either. In § 13 a third, compromise choice is added, and a counterexample shows that the three-choice problem need not have the analogous three-sector structure. For the finite-horizon process the boundary ray of generally differs from the index line, and Theorems 5 and 6 are statements about how it differs.
Namespace BellmanDP.GoldMining. Values are real functions ℝ → ℝ → ℝ (two mines) or (Fin n → ℝ) → ℝ (n mines); equations are imposed only on the closed quadrant or orthant, and uniqueness means agreement there. Mines are Fin n with added (with no mine the maximum in (4) is empty). Outcomes are Fin K (Theorem 3's ). A maximum over two branches is max, and a maximum over mines is encoded as "every alternative is at most and one equals it". The class "bounded in any rectangle" is BoundedOnRectangles, and for mines it is BoundedOnBoxes. The -stage returns are goldIter N, with goldIter 0 = 0 so that goldIter 1 is the book's .
Choices made explicit:
A statement of the index rule that assumes the index policy's return satisfies (5.1) and calls it "the solution" without the bounded-class uniqueness would prove nothing about optimality. Here every theorem is about solutions in the bounded class, whose uniqueness is Theorem 1 (and part of the goal).
Contraction estimates on rectangles (Theorems 1 and 7) are reusable across the other functional-equation chapters of this series. Proofs of the goal via general index theory are welcome, provided they discharge the statements as written.
Many optimization routines contain an inner step that maximizes a function of one variable whose values are expensive to compute: a line search inside a multivariate method, a tuning parameter chosen by simulation, a stage of a dynamic program in which each evaluation requires solving a subproblem. When the only structural information is that the function has a single peak, the natural question is how to place the evaluations so that the peak is pinned down as tightly as possible with a fixed budget. Richard Bellman's Dynamic Programming (1957) takes up this question in Chapter I, § 22, as an illustration of the functional-equation method, and answers it with the Fibonacci numbers.
Timeline.
Let . A function is strictly unimodal with maximum at if is strictly increasing on and strictly decreasing on . No continuity is assumed, and the peak may sit at an endpoint. The point is then the unique maximizer of .
A search procedure is a finite decision tree. At each internal node it names a point at which is evaluated and moves to a subtree chosen by the observed value ; at a leaf it announces a closed interval . The -th evaluation point may depend on all values seen so far, but on nothing else about . The cost of the procedure on is the number of evaluations along the path that determines.
The procedure locates the maximum on within unit length using at most values if, for every strictly unimodal on with maximum at , it evaluates at most times and announces with and . Write for the set of lengths for which such a procedure exists, and following Bellman's Eq. (22.1),
The book's Fibonacci numbers are , for (in Lean, bookFib).
In the discrete version, is defined on the points , strictly increasing up to its maximizer and strictly decreasing after it. is the largest for which some procedure evaluates at most values and then names exactly, for every such .
The supremum is not attained once (with two evaluations every length is searchable, the length is not), which is why the statement is about the supremum rather than a maximum.
The result. Theorem 11 is an exact minimax statement: evaluations shrink the interval of uncertainty for the peak of a unimodal function by a factor of at most , and no adaptive rule, however clever, does better. It certifies Fibonacci search as optimal and golden-section search as asymptotically optimal, which is the reason these methods are the default line searches when derivatives are unavailable. Eq. (22.4) quantifies the rate: twenty evaluations give four decimal digits.
Formalizing it. The theorem has been proved since 1953; the work here is a machine-checked proof of the full minimax statement over all adaptive procedures, including the lower bound. That half is a statement about every decision tree and requires an adversary argument, which is exactly the kind of reasoning that is informal in the book and easy to get wrong. The discrete Theorem 12 is misprinted in the book (see below), so a formal proof also settles the correct values. We are not aware of an existing formalization of the optimality of Fibonacci search in Lean or another proof assistant. The Binet formula and the ratio limit are in Mathlib for Mathlib's indexing (Real.coe_fib_eq, tendsto_fib_succ_div_fib_atTop); milestone 6 only transfers them to the book's indexing.
The upper bound must hold for every procedure, not only for procedures that follow the "compare two points, discard a piece, keep the surviving point" pattern of the book's figures. A procedure may place its second point depending on the first value, may re-evaluate points, may evaluate outside , and may branch on the exact values rather than on their order. The book's argument tacitly restricts to that pattern, so the lower bound has to be established for arbitrary trees, where the information carried by exact values, repeated or wasted evaluations and branch-dependent placements all have to be accounted for. The bookkeeping is delicate because the surviving sets are half-open or open intervals, and whether the endpoints are included decides that the supremum is not attained.
The naive attempt of proving a bound only for "one new point per step inside the current bracket" procedures does not prove the goal: the goal quantifies over all decision trees.
ℝ → ℝ, constrained only on ; evaluations outside are allowed and useless.bookFib with ; in Mathlib's indexing is Nat.fib (n + 1). The goal is stated for every ; the book calls a convention, and in this model agrees with it.IsLUB, never as "a procedure exists for ", which is false for . Theorem 12 is stated with IsGreatest, which asserts that the maximum exists.Chapter I of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) opens the book with a multi-stage allocation process: a resource is divided, stage after stage, between two activities, each of which yields an immediate return and leaves behind a depleted remainder that is re-divided at the next stage. The chapter uses this process as its prototype for "a number of multi-stage processes, of diverse origin, but similar analytic structure" (§ 8, p. 11), and the techniques it introduces here — the functional equation of the infinite process, successive approximations, approximation in policy space, transfer of convexity and concavity through the recurrence, and a stability estimate — reappear throughout the book and in the later theory of Markov decision processes.
When the number of stages is large, Bellman replaces the finite sequence of recurrences by a single equation for the infinite process. As the book stresses (p. 11), this replacement is only useful once one knows that the equation has a solution and possesses "no extraneous solutions". This mission formalizes that existence and uniqueness theorem and the chapter's main structural results that rest on it.
A quantity is split into , assigned to a first activity with return , and , assigned to a second activity with return . After the stage the first allocation has been reduced to and the second to , and the process continues with the quantity . Writing
the total return of the infinite process satisfies the allocation equation (Bellman's (8.1))
The standing hypotheses of Chapter I, Theorem 1 are:
The successive approximations from an initial function are . A policy is a function with ; its return is the total of the stage returns obtained by using at every stage.
In Lean all objects live in the namespace BellmanDP.Allocation: allocT is , allocM is , AllocationHyp g h a b bundles the three hypotheses, IsAllocationSolution g h a b f is the equation with the maximum attained, allocIter is the sequence , and policyReturn is the return of a policy.
Under the three hypotheses, there is a function with
this is continuous on , and every solution continuous at with value there coincides with on .
Theorem 1 is what gives meaning to "the solution" of the allocation equation, which every later result of the chapter refers to. Without the side condition at uniqueness fails: when , every constant function and the indicator of solve the equation. Theorems 2 and 3 turn the existence proof into computational procedures (value iteration and policy improvement), and Theorem 3's monotonicity is the prototype of the policy-improvement property. Theorems 4 and 5 are the first structural results on optimal policies — all-or-nothing allocation under convex returns, a unique interior-or-boundary allocation under strictly concave returns — and Theorem 9 bounds the error made by replacing a return function with a simpler approximation.
These are classical results with published proofs in the book. No machine-checked version of any of them is known to this mission; the work is to formalize the proofs, building reusable infrastructure for functional equations of the form with a contracting transition .
The equation is not a contraction in the supremum norm on : and may be unbounded, so no global Banach fixed-point argument applies. Control comes instead from the shrinking of the argument, , which propagates a local estimate near out to every finite interval, and the summability hypothesis (1b) is what makes the resulting series converge uniformly on bounded sets. Uniqueness cannot come from a norm estimate either; it rests on continuity at alone. The maximum in the equation must be shown to be attained, which requires continuity of the limit function; the book notes (p. 13) that the monotone argument for nonnegative gives only a supremum. For Theorems 4 and 5, convexity and concavity must be carried through each approximation and preserved in the limit, and strict concavity must be recovered for the limit, where a pointwise limit of strictly concave functions is only concave.
ℝ → ℝ; only their values on enter any hypothesis or conclusion. Continuity at is one-sided (ContinuousWithinAt f (Set.Ici 0) 0), and uniqueness is equality on .IsGreatest of , so a solution attains its maximum at every . The maxima inside definitions (, , the triangle maximum of Theorem 9) are real suprema (sSup) of images of compact nonempty sets of continuous functions, which equal the book's maxima under the stated hypotheses.Welcome contributions: a general existence-and-uniqueness theorem for equations with , and a lemma that parametric maxima over of continuous functions are continuous in .
This is the fourth mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing the axiomatic core of Part II, Chapter 4, "Ensemble spaces". The chapter proposes three physically motivated axioms (ensemble, mixture, entropy) that every space of statistical states should satisfy, covering classical probability distributions and quantum density operators alike, and derives from them structure that is usually postulated, for example that mixtures can be "un-mixed" (cancellativity). That is the first step towards embedding ensembles in a vector space. Unlike missions II and III, this mission does not depend on earlier missions.
An ensemble space is a , second countable topological space with a continuous mixing operation (, ) that is idempotent, commutative and associative, and a continuous entropy . The entropy is strictly concave, with equality iff , and bounded above by for a universal function . Two ensembles are orthogonal, , when this bound is saturated, and mixtures preserve orthogonality. An ensemble is a component of if with ; two ensembles are separate if they have no common component. The mixing entropy is .
Cancellativity is what allows affine combinations with negative coefficients, the origin, in this framework, of the vector-space embedding of ensembles (Theorem 4.94) and of negative quasi-probabilities such as Wigner functions. It holds in classical and quantum statistics, and here it is derived from continuity and strict concavity of the entropy instead of being postulated. The results are proved informally in the book; no machine-checked formalization is known to the drafters.
The convex-space axioms are stated in a two-sided associativity form, so every rearrangement of mixtures must be derived from it. The book's proof of cancellativity first propagates the equality from one coefficient to all of by an iteration , and then uses a limit together with continuity of mixing and of the entropy. Strict concavity has to be applied only to non-trivial coefficients.
The structure EnsembleSpace I E bundles Axioms 4.4, 4.7 and 4.55 for a topological space E; mixing coefficients are elements of Mathlib's unitInterval. Real coefficient expressions in the associativity axiom pass through clampI, the projection , and lie in on the stated domain. The universal function is a parameter. Orthogonality is saturation of the upper bound for every . Strict concavity is required for only, since at equality is automatic. The book's Proposition 4.67 uses for , which follows from universality of (any space with two distinct ensembles forces it); the milestone carries this as an explicit hypothesis. Items 3 and 4 of Proposition 4.116 in the book use the normalization from Theorem 4.59; item 3 is stated with and item 4 is omitted. Hull operators, the vector-space embedding (Theorem 4.94), boundedness of lines (Theorem 4.105), the entropic geometry and the standard classical/quantum models (Propositions 4.5, 4.9, 4.56) are left for later missions.
Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level . A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.
The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.
A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate . An order is for units with probability , where and the mean order size is finite (compound Poisson demand; simple Poisson demand is ). Resupply times have mean . The steady-state probability that units are in resupply is
where is the probability that orders total units. In this mission is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is , and the book also writes .
For a stock level :
Forward differences are and ; discrete convexity means .
With items, unit costs and budget , Problem 4 (3.40) is
For a multiplier , the item-wise criterion defines as the least with , and .
For every , each exists and
for every vector of nonnegative integer stock levels. That is, is optimal for Problem 4 at budget . This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.
The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, , is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.
All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.
The algebra of first differences is elementary; the difficulties are elsewhere. is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying with , requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every is concave; dropping the floor constraints makes it false.
Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields , an order-size distribution with , , , and summable (the finite mean is added: without it is infinite). Expected on-hand inventory is the finite sum . Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).
Pinnings and deviations, each stated in the item's Formalization Note:
A trivializing formalization is ruled out: the goal is stated for the book's own backorder function built from the compound Poisson law, not for an arbitrary convex function nor for a defined through its differences.
Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.
The Euclidean projection of a vector onto the simplex — the nonnegative vectors whose entries sum to a fixed radius — is a subroutine of first-order methods whose iterates must stay probability vectors or nonnegative budgets: portfolio optimization, multispectral unmixing, image segmentation, constrained least squares and many machine-learning models. Through a classical reduction the same routine projects onto the ball, the feasible set of -constrained sparse regression. Because the projection is called once per iteration, often on vectors of millions of entries, the exact algorithms that compute it have been studied for half a century.
A short timeline. Held, Wolfe and Crowder (1974) gave the sorting-based method: sort the entries, find the number of active entries, compute a threshold. Michelot (1986) gave a variable-fixing method that repeatedly averages the surviving entries and discards those below the average, without sorting. Kiwiel (2008) and Duchi, Shalev-Shwartz, Singer and Chandra (2008) popularized partition-based methods with expected linear time. Condat (Math. Program. 2016) proposed a Gauss–Seidel-like variant of Michelot's method that updates the threshold after every entry read instead of after every full pass; it is exact, needs no sorting and is empirically the fastest of the family. Its correctness is argued in one paragraph of the paper; the argument has not been machine-checked.
Fix an integer , a vector and a real . The simplex of radius is
and the ball of radius is . The Euclidean projections are and , where is the Euclidean norm. In Lean, "" is the predicate IsSimplexProjection a y x: and for every ; IsL1Projection is the same for .
The projection onto has the thresholding form for a unique real , so computing amounts to computing .
Condat's Proposed Algorithm (Fig. 2 of the paper) keeps a list of candidate entries, an auxiliary list and a running value :
In Lean this is the total function condatAlgorithm a (List.ofFn y), returning .
For every , , , if the algorithm returns then
No assumption is made on the order or distinctness of the entries of .
The goal certifies a routine used inside many optimization solvers: for every real input, the algorithm returns the exact projection, and the reported is the size of its support. The milestones are reusable facts about simplex and -ball projection in their own right — the thresholding characterization (Proposition 2.2), the bracket and monotonicity of the root function, and the two reductions between and — on which the correctness of the sorting, heap, partition and Michelot methods reviewed in the paper also rests.
All of these results are proved on paper (Propositions 2.1 and 2.2 are classical and cited by the author; the algorithm's correctness is argued in Sect. 3). None of them is formalized in Mathlib, which has the standard simplex (radius 1, as a set) and the abstract Hilbert-space projection theorem but no thresholding formula and no projection algorithm. The mission turns the paper's argument into a checked proof about a transcription of Fig. 2 that can be read line by line against the figure.
The algorithm mixes three different updates of — an incremental mean when an entry is added (with counted before the addition in step 2.1 and after it in step 3.1), a reset to , and a removal update — and a loop whose termination depends on strictly decreasing. The paper's argument relies on invariants that are stated informally: equals outside the reset, never exceeds , is a sub-multiset of that contains every entry larger than once the cleanup pass is done, and at every division. The first idea, to argue directly that the first pass already finds , fails: in general it does not, and the reset of step 2.3 temporarily breaks the mean invariant, which is exactly why step 3 exists. The thresholding characterization itself needs the optimality conditions of a constrained quadratic problem, available in Mathlib only as the abstract variational inequality for projections onto closed convex sets.
Vectors are Fin N → ℝ, and the squared Euclidean distance is the explicit sum (Mathlib's norm on Fin N → ℝ is the sup norm and is not used). Every theorem assumes exactly the paper's standing hypotheses and . Projections are predicates, not chosen minimizers. The algorithm reads as the list ; lists keep repeated values; step 4's loop is a do-while encoded by well-founded recursion on , so the function is total without an iteration bound and termination is part of the definition. is compared with the number of indices with . The only placeholder is the empty input (), which the paper excludes and every theorem excludes by hypothesis.
A formalization in which the algorithm's output is defined as "the of Proposition 2.2", or as a sorting method or Michelot's method instead of Fig. 2, or in which the loop is cut off by a fuel bound, would make the goal trivial or different; the definition here transcribes Fig. 2 step by step, and the goal quantifies over every input.
A complete development needs: the thresholding characterization via first-order optimality conditions on ; elementary facts about the piecewise-linear function ; and loop invariants for the three passes of the algorithm, stated on lists with multiplicity. The simplex and -ball facts are reusable for any later mission on projection algorithms (sorting, heap, partition, Michelot). Contributions welcome: proofs of any milestone, lemmas relating List.ofFn sub-multisets to index sets, and invariant lemmas for the individual steps of Fig. 2.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest
of the book runs on. Its subject is the relation between two ways of looking at the same stationary
system: from a clock fixed in time, and from a customer arriving into it. The two are not the same
— the interval a random instant falls into is longer than a typical interval, a fact every
queueing student meets as the inspection paradox — and the object that makes the difference precise
is the Palm probability P⁰_N.
The chapter defines P⁰_N by the Matthes definition in terms of counting,
λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ], (1.2.1)
and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried
in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make
Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the
inversion formula and the goal theorem would inherit that emptiness.
From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift
(1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell
formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from
P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4),
which relates two point processes stationary for the same flow; and the Miyazawa rate
conservation principle (1.3.10), which balances the drift of a process between its jumps against
the rate at which it jumps.
§1.3.7 then collects all of them into one identity. Its name is the book's own:
Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.
Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A,
departures {τ_n} with counting measure D — not assumed ordered — sojourn times
W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with
X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative
process {Z(t)}, all compatible with a measurable flow under which P is invariant:
λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ]. (1.3.28)
Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law,
here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other
choices give the inversion formula, the Miyazawa conservation principle and the rate conservation
law.
P⁰_NOne milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of
P⁰_N as "what an arriving customer sees":
lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0. (1.5.3)
The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.
Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.
{θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a
point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely
many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is
axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula
would make the milestones and the goal trivial and is ruled out.[0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded
or integrable ones.{B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails);
it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the
Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.δ for every A).Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.
Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.
Let be a real matrix, , . The primal problem is to maximize subject to , ; the dual is to minimize subject to , . A primal–dual point is a quadruple with , ; it is strictly positive, , if every component is. Write for the diagonal matrices of and for the all-ones vector. The norms are and .
At a point the three measures of progress are the primal infeasibility , the dual infeasibility , and the complementarity . Fix parameters and . One iteration of the method, from a strictly positive point, sets , takes any solution of the Newton system
computes the step length
(with when all ratios vanish), and moves to . This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts denote the quantities at the -th iterate, and is the step length computed there.
If , is real, and for all one has , , , then for all , with ,
The one-step identities for the infeasibilities, (18.8) and (18.9); the one-step complementarity estimate
under ; and the recursion (18.11). Two unnumbered statements complete the picture: every iteration has and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies (§18.5.3).
Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor per iteration while the complementarity, and hence (by the duality-gap estimate) the gap , falls only by . The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.
All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.
The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term that has no sign. Bounding it requires relating the size of the step to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon is what makes the statement non-trivial.
Vectors are Fin n → ℝ and Fin m → ℝ, is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case when all ratios vanish, since Lean's r / 0 = 0 would otherwise give . An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current direction. The hypotheses , (pp. 272–273) are stated in every theorem; is an arbitrary real number and a natural number. As in the book, the hypotheses of Theorem 18.1 range over , so the iteration from index is part of the data.
Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant ". Because is fixed, that existential is satisfied trivially by , and a statement with would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): . Eq. (18.11) is stated with the book's written out.
The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.
Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.
The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).
A network has a finite set of nodes and a set of directed arcs . Node carries a supply (negative values are demands) with , and arc carries a cost . The flow on arc is the decision variable. The node–arc incidence matrix has in the column of an entry in row , in row , and elsewhere. The network flow problem (14.1) is
A flow satisfying is balanced; a balanced flow with is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of and without directions, is connected and has no cycle. Fixing a root node and deleting its row gives the matrix . A set of arcs is a basis if its columns form an invertible square submatrix of , and a basic feasible solution is a feasible flow vanishing off some basis.
For maximum flow, a source , a sink and finite upper bounds are given; all and an extra arc of infinite capacity is added. A feasible flow satisfies , and flow balance. A cut is a node set with , , and its capacity is .
If girls and boys are such that every girl knows exactly boys and every boy knows exactly girls (knowing being symmetric), then there is a bijection from girls to boys with
both extrema attained.
The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).
König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.
All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention , bases as square submatrices of with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.
The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.
Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.Fin n, knowing is one relation between girls and boys, and is a hypothesis: the book's proof divides by , and for the claim is false. No connectedness is assumed.A formalization of the goal as a matching of size in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the girls and the boys using only acquainted pairs.
Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.
Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set and redistribute the probability of leaving back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.
A Markov chain with costs on a denumerable state space has transition probabilities with and a finite nonnegative cost at each state. For a set and a start , is the first passage time to . The taboo probability is the probability of moving from to in steps with no intermediate state in . The expected visits count the visits to at times . The mean first passage time is , infinite when is missed with positive probability. The first passage cost is . A state is positive recurrent when , and the steady state probability is . On a positive recurrent class the average cost is . The chain is standard when and for every . Such a chain has one positive recurrent class with , and every other state is transient.
An approximating sequence (AS) consists of increasing nonempty finite sets with and, for each , a chain on with the same costs and transition probabilities . The quantities of are written , , and . An AS is conforming (for a standard ) if, for large , is unichain with in its positive recurrent class, and and for all . It is conforming on if and on .
An augmentation type approximating sequence (ATAS) keeps the original probabilities inside and redistributes the probability of each excluded target according to an augmentation distribution on :
It sends excess probability to if every is concentrated on .
For a standard chain and a finite nonempty ,
and if it is also conforming on . No rate of convergence and no constants are involved, and need not contain .
The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple with . First passage costs can converge to the wrong value even when the steady state probabilities converge.
Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between bounds and limits in explicit, and produces a reusable library of first passage quantities for countable chains.
The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in , a first passage that leaves is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: may have several recurrent classes, or a recurrent class not containing , and ruling this out is part of the conclusion rather than an assumption.
The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, , , and are defined as sums in . is infinite whenever is missed with positive probability. The average cost is the of the Cesàro cost averages.
An AS is a structure carrying , the finite sets (as Finset S) and . is built as an MC on the subtype of , and a set is read in as . Quantities of are lifted to functions of and of states of with the value where they are undefined ( or a state outside ). For fixed states this affects finitely many , and all statements are limits, s or eventual equalities. All convergence is in . The conformity predicate includes the standing assumption that is standard. The positive recurrent class of a standard chain is the communicating class of .
A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class excludes , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce exactly by (C.27).
A complete development needs first passage decompositions for countable chains, the renewal-reward identity , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.
Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.
Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the -person game becomes unmanageable as grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.
The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition ; and every splitting set is a union of blocks of . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.
Let be a finite set of players. A characteristic function is a real number for every subset (every coalition, including the empty set and ). Write . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying
For with complement , the game is decomposable with respect to and if there are constant-sum games on the players and on the players with for all — formula (41:3). The -constituent is the game on with for (41:4).
A splitting set (43.1) is a satisfying (41:6),
The game is indecomposable if and are its only splitting sets (43.3.1). A minimal splitting set is a splitting set none of whose proper subsets is splitting (43.3.2), and is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. for all , for some reals (the transformation (42:5)).
For every satisfying (42:6:a)–(42:6:c):
The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that is a partition.
In attack order: the criterion (42:G) (decomposability (41:6) (41:7)); the closure properties (43:A) (complements), (43:B) (, ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( splits iff every block of lies inside or outside ); and the two extreme cases (43:J) ( = all singletons iff the game is inessential) and (43:K) ( iff the game is indecomposable).
The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.
The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.
The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that is splitting one cannot simply add the identities (41:6) for and for , since a pair , is not of the form those identities control, and may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of (players of the constituent) and subsets of .
ι with decidable equality (the book's ; in Chapter IX players are also named ). Coalitions are Finset ι, and are the complement Sᶜ in , and is a function Finset ι → ℝ.IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes nonempty ([Nonempty ι], the book's ); every other statement holds without it. (43:E) assumes , since the book's constituent is a game and has at least one player.↥J, ↥Jᶜ; the -constituent is restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives .Finset ι and their atoms, which would shorten (43:F)–(43:H).Consider the classical error-correcting problem. An input vector (the plaintext) is encoded as by a coding matrix with , and an unknown, arbitrary vector of errors corrupts the result, so that only is observed. Can be recovered exactly, and by an algorithm whose running time is polynomial in ? Candès and Tao (2005) answer both questions at once: if a matrix annihilating satisfies a restricted orthonormality condition, then is the unique solution of the convex program , which is a linear program, whenever at most entries of are corrupted, whatever their positions and values. Read for the matrix alone, the same theorem says that minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.
Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of and minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition , sharpened the sufficient condition; those later results are not part of this mission.
Let be a real matrix with columns , and let be the linear span of these columns. For an index set and real coefficients , write . A vector is supported on when for all ; with this convention is just the product . Norms are the Euclidean norm and the norm .
Definition 1.1. For an integer , the -restricted isometry constant is the smallest quantity such that
for all of cardinality at most and all real coefficients . The -restricted orthogonality constant is the smallest quantity such that
for all disjoint with and . The paper writes for . These numbers measure how far the columns of are from an orthonormal system when only linear combinations of at most columns are considered.
The two optimization problems are
A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.
Let be a real matrix of full rank with , and a real matrix with . Let satisfy
If where is supported on a set of size at most , then is the unique minimizer of .
Let satisfy (1.10) for , and let be supported on a set with . Then is the unique minimizer of with .
Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the numbers control the numbers), Lemma 1.3 (uniqueness of sparse representations under ), and the two dual sparse reconstruction properties, Lemma 2.1 ( version) and Lemma 2.2 ( version).
The result. The guarantee is deterministic and uniform: one condition on , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.
Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of and exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.
The whole proof rests on a dual certificate: a vector with for and for . Given such a , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is ; this interpolates the signs on and, by restricted orthogonality, its inner products off are small in an sense, but not in the sense required. That is exactly Lemma 2.1: the bound holds only outside an exceptional set of at most indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on fixed, and summing a geometrically convergent series.
Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to () at each step, while the per-step factors it quotes, , are what Lemma 2.1 gives for a set of size ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with in its bound on the exceptional set, while the inequality (2.3) its proof establishes gives ; the mission states the lemma with , which coincides with the printed form in the case used by Lemma 2.2.
Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on is a vector in Fin m → ℝ supported on the finite set , and is F.mulVec c. The Euclidean and norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. is the span of the columns.
The constants and are the infimum of the set of nonnegative (resp. ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as . The definitions are total in , and each theorem carries the paper's domain conditions (, and , or as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has , so none of the statements is vacuous.
"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the matrix with is injectivity of ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant depending only on " is a positive function of the real number , quantified before all other data.
Out of scope, with the reason for each: Theorem 1.6 refers to a threshold "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for and "large enough", with an unspecified threshold and an term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.
Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix and its inverse under , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to ) belong to a separate mission.
In a Walrasian pure exchange economy, agents trade a fixed stock of commodities, and a price vector is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).
Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.
There are commodities and agents. Prices are vectors , and the paper's implicit summation is written . Agent has an expenditure function (minimal cost of reaching a fixed utility level), and the market weighs agents with constants ; the aggregate expenditure is
The economy controls the price velocity and minimizes the cost functional (eq. (7))
whose value function is . The Hamiltonian (eq. (8)) is
the optimal policy (eq. (9)) is , and the HJB equation (eq. (10)) reads
Here always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent with . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: .
If is and solves the time-reversed HJB equation, and the price path follows the optimal policy , then on any interval on which
the function is strictly decreasing; if moreover , it is strictly positive on .
The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.
Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.
All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption is kept; positivity of and is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. , , with small on a bounded interval), so the goal is not vacuous.
This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever .
The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).
Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group with piecewise maps of the line with rational breakpoints (p. 2). Whether is amenable is a notorious open problem, and whether is amenable is Monod's Problem 12 (p. 2).
The projective line is OnePoint ℝ, on which acts through by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring of (A : Subring ℝ; is ⊥, is ⊤), P A is , the set of fixed points of hyperbolic elements (trace of absolute value greater than ).
A homeomorphism of is piecewise in with breakpoints in (IsPiecewiseProjOn A E f) when, off some finite subset of , it agrees near every point with a Möbius transformation from . Monod's (Gpp) is the group generated by the homeomorphisms piecewise in , with breakpoints anywhere, and (Hpp) is its stabilizer of (fixInf). For a subring , (G A) is the subgroup of generated by its elements that are piecewise in with breakpoints in (IsPiecewiseProj A), and (H A) is its stabilizer of ; is H ⊥. GRat is the subgroup of generated by its elements piecewise in with breakpoints in , and HRat its stabilizer of : the rational-breakpoint variants of and (p. 2).
Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.
A relation is amenable for a measure (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on to functions on , linear up to -null sets and invariant under the partial transformations of . volP1 is the Lebesgue measure class on .
The goal is Theorem 1, "The group is non-amenable if " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring of , compares the orbits of and on (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of on is not.
The milestones are, in the paper's order: consists exactly of the elements of piecewise in with breakpoints in ; ; preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of on is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of and with and .
The result. Theorem 1 and Theorem 2 together make , for instance , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).
Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's and (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.
The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of on is not amenable for countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in that contradicts an invariant mean directly.
OnePoint ℝ and acts through Matrix.SpecialLinearGroup (Fin 2) A; since acts trivially the orbits are those of .OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that is exactly its set of such maps and that .volP1).This mission formalizes Geoghegan's conjecture that Thompson's group is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.
A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.
Timeline.
Let UI be the unit interval . Thompson's group (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational and every slope a power of . It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).
A mean on a set is a function from the subsets of to with , for disjoint , and . A group is amenable (Garrido.IsAmenable G) when it carries a mean with for all and , where . This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in .
The milestones use four further notions, defined precisely in the definitions item and in their own statements:
The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.
The milestones are results from the literature, stated as their sources state them: has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of ; Kaimanovich's theorem that random walks on with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of as extensive amenability of its action on the dyadic rationals; Stankov's embedding of into Monod's ; Monod's theorem that is not co-amenable in ; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.
Monod's Problem 12 asks whether is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of , namely ; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).
The result. A proof of the conjecture would make a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.
Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.
The obstructions to amenability that settle the question for most groups are absent here: has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.
Lean representation and conventions.
UI; and are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, ; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.What is left out.
What a development needs. Thompson's group and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.
The Thomson problem asks for the configuration of electrons, constrained to the surface of the unit sphere and repelling each other according to Coulomb's law, that minimises the total electrostatic potential energy. J. J. Thomson posed it in 1904 in connection with his "plum pudding" atomic model. The same energy-minimisation question reappears in the arrangement of protein subunits in spherical virus shells, in colloidosomes, in fullerene patterns and in multi-electron bubbles, and it is a special case () of the Riesz -energy problem on the sphere; the logarithmic variant is Smale's 7th problem.
Despite its elementary statement, the minimum is rigorously known only for a handful of values of .
Timeline of exact solutions (as reported in the source).
A configuration of points is a map . It is admissible if every point lies on the unit sphere, , and the points are pairwise distinct. In units with and its Coulomb energy is
An admissible is an energy minimiser (solves the Thomson problem for ) if for every admissible -point configuration .
Explicit candidate configurations are fixed in the definitions file: the antipodal pair (), an equatorial equilateral triangle (), the regular tetrahedron (), the triangular bipyramid (), the regular octahedron (), the pentagonal bipyramid (: the two poles plus a regular pentagon on the equator) and the regular icosahedron ().
This asserts admissibility of the seven points and the inequality against every admissible seven-point configuration . It fixes no numerical value of the minimum and does not assert uniqueness.
The result. Among the values of listed in the source, is the smallest one whose optimum was, until the 2026 claim, supported only by numerical computation; the cases and were settled earlier. Settling extends the short list of rigorously known Thomson minimisers.
Formalizing it. The result reported in the source is recent and described there as a claimed Lean-kernel-checked proof; a formalization on this platform against a public, reviewed statement would corroborate it independently. For the milestones, the source attributes the cases to published proofs (Föppl 1912, Schwartz 2013, Yudin 1992, Andreev 1996); the source does not describe machine-checked proofs of these, and each is a self-contained formalization target.
The energy is a non-convex function on the configuration space with many critical points, so numerical minimisation — which is how most entries of the source's table of smallest known energies were obtained — does not certify global optimality. The case, the most recent classical entry before , was resolved only with a computer-assisted proof (Schwartz 2013).
Points live in EuclideanSpace ℝ (Fin 3); configurations are functions Fin N → EuclideanSpace ℝ (Fin 3). Admissibility requires unit norm and injectivity (distinct points), matching the source's " distinct points". The energy sums over ; Lean's convention is harmless because coincident points are excluded by admissibility. The candidate configurations are fixed in one particular orientation; since the energy is invariant under orthogonal maps and relabelling, this is no loss of generality. The statement " is an energy minimiser" includes admissibility of itself, so the goal cannot be satisfied by a degenerate candidate.
Reusable infrastructure welcome: energy invariance under isometries and permutations, existence of minimisers by compactness, linear-programming (Delsarte–Yudin) bounds on the sphere, and interval-arithmetic tooling for certified numerical bounds.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission extends the best possible constant for complex diagonal matrices from to every real . The result is proved in Lean. The constant and its formula are unchanged from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. For each exponent, it works for every triple of diagonal matrices, whatever their size, and no smaller constant does.
The mission started from a supplied pen-and-paper proof. Lowering the cutoff took more than replacing 256 with 90: several estimates in the original argument had to be strengthened. The research note proves the bound for real entries first, then transfers it to complex entries and shows that the constant cannot be improved. The goal theorem below gives the exact formula and statement.
This is the second step of the sharp diagonal Hlawka campaign, and it reuses the foundation's definitions and supporting results. The campaign invites further improvements below 90, keeping the same formula.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms for a Metropolis–Hastings sampler can combine them in two ways. Either each drives its own Metropolis–Hastings kernel and the sampler picks kernel with probability at each step, or the mixture is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target invariant, so the choice is about efficiency.
Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).
Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.
Let be a measurable space and a probability measure on it, the target. A proposal kernel is a Markov kernel on . Given a measurable acceptance probability , the Metropolis–Hastings kernel is
where is the point mass at (mhKernel Q α).
Put and . With and (canonDensity), let
(canonR, canonRatio). The set is symmetric, and are mutually absolutely continuous on and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is
(alphaMH π Q), and the kernel with is the maximal Metropolis–Hastings kernel for (maxMHKernel π Q).
For kernels on , dominates off the diagonal, (OffDiagDominates π P₁ P₂), if for -almost every , for all . For a countable family of kernels and weights , the mixture is the kernel (mixKernel β K).
Let be a finite or countable family of proposal kernels and with . Let be the maximal Metropolis–Hastings kernel for and the maximal Metropolis–Hastings kernel for . Then
Both sides use maximal kernels: uses of the mixture proposal, each its own , and the same weights form both mixtures.
A companion item states the maximality of (§3, p. 7): every measurable acceptance probability whose kernel is reversible satisfies -a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.
The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function with finite variance the asymptotic variance of under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.
Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that , defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on passes to the kernel-level statement with one null set for all ; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of , or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.
The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare of sums with sums of minima. On a general state space there is no common reference measure given in advance, and is only defined up to -null sets, through a Radon–Nikodym derivative with respect to , a measure that differs for and for each . The step that needs care is relating these different versions: the densities of the against a common symmetric , the density of , and the transpose densities , which are densities of only because is symmetric.
The second difficulty is the passage from measures to kernels. The inequality between measures on gives, for each fixed , the kernel inequality for -almost every , with a null set that depends on . The order requires one null set for all , and the diagonal must be removed, which needs the diagonal to be measurable.
The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in (ℝ≥0∞); a general is assumed measurable with . is π ⊗ₘ Q, its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.
Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's and ), on the goal and the maximality companion; and, on the goal only, the σ-algebra of is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in uniform over in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.
is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with , not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio is set to 1 on the null subset of where is infinite, so that and hold everywhere, as Proposition 1 asks.
Trivializations ruled out: is the indicator of times , never an arbitrary acceptance function or a single shared by all components; compares , not (on the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on = Bool with uniform, two proposals and and weights .
Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, , and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.
The discrete logarithm problem modulo a prime asks, given a prime , a generator of the multiplicative group modulo , and a nonzero residue , for the exponent with . Its presumed classical hardness underlies Diffie–Hellman key exchange, ElGamal encryption and the Digital Signature Algorithm. The best classical algorithm known when Shor wrote, Gordon's adaptation of the number field sieve, runs in time .
In §6 of Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (SIAM J. Comput. 26(5), 1997; doi:10.1137/S0097539795293172, arXiv:quant-ph/9508027), Shor gave a quantum algorithm that uses two modular exponentiations and two quantum Fourier transforms and outputs, with constant probability, a pair from which can be computed. The quantitative core of that analysis is a single number: the circuit produces a "good" output with probability at least . This mission formalizes that bound and the three estimates it is assembled from.
Let be a prime and a generator of , so that are all the nonzero residues. Fix the unknown with and put . Let be the power of with .
The Fourier matrix is the matrix with entries for (§4, eq. (4.1)). Rows index input basis vectors and columns output basis vectors.
The algorithm uses three registers: two holding numbers and one holding a nonzero residue modulo . It starts from the state
(preFourierState), applies to each of the first two registers (finalState), and measures all three registers. The probability of observing is the squared modulus of its amplitude (outcomeProb).
For integers and , the symmetric residue is the residue of modulo in (symmRes). Put
An observed state is good (IsGood) when
Goodness depends only on .
The constant is the one the page carries forward. The goal fixes no threshold on : it is stated for every prime that admits a power of two strictly between and .
The result. The bound is what turns the circuit into an algorithm. Repeating the circuit times in expectation yields a good output, and from a good pair one reads off an equation that determines modulo divisors of (§6, eqs. (6.18)–(6.20)). Together with the quantum Fourier transform circuit and reversible modular exponentiation, this places the discrete logarithm modulo a prime in quantum polynomial time. Every later analysis of quantum attacks on discrete-logarithm cryptography starts from this success probability or a sharpened version of it.
Formalizing it. The result has been proved since 1994–1997 and is textbook material; it is not open. As far as is known, no machine-checked proof of Shor's discrete-logarithm analysis exists. The paper's proof of eq. (6.17) replaces a sum by an integral with an error term whose constant is not given, yet states for every prime. A formal proof must therefore either control that error explicitly or find another argument, and so settles a point the paper leaves informal. Numerically, the smallest value of over good states is about for all primes , so the unconditional claim is not in doubt for small . The page also contains two small slips, recorded under Formalization scope; a complete development pins down exactly what is true.
The exponential sum (6.4) runs over pairs satisfying a congruence modulo , while the phases are taken modulo . The two moduli are unrelated: is a power of two and is arbitrary. Eliminating through the congruence introduces a floor function , and the resulting phase is not linear in . The obvious estimate treats the sum as a geometric series in and bounds it by its first-order phase; this fails because the floor term perturbs every phase by an amount of size up to . Condition (6.11) only keeps this perturbation within of the main phase; it does not remove it. The per-state bound must survive this perturbation uniformly in , and , including small primes where the paper's integral approximation gives no explicit control.
The count of good pairs needs a separate argument about how often a multiple lies within of a multiple of when is large.
Fin q × Fin q × (ZMod p)ˣ → ℂ. The first two registers range over ; the third over the units modulo .finalState is defined this way from (6.1) and . It is not typed in as the closed form (6.3) or (6.4). A formalization that defined the final state by (6.4) directly would make milestone 1 trivial, and is ruled out.Fact p.Prime). The generator is encoded as orderOf g = p - 1. is a parameter, with . is given by q = 2 ^ l together with . No large- threshold is added anywhere.x⁻¹ ^ b in the unit group. is computed in and inside and the congruences, and as natural-number subtraction only where makes it exact. is real.Needed infrastructure: finite exponential sums and their modulus, the symmetric residue and its basic properties, and counting multiples in residue classes of . The exponential-sum estimates of milestones 1 and 2 are reusable in the order-finding analysis of §5 of the same paper. Proofs of any milestone, of the normalization , and of auxiliary lemmas about symmRes are welcome.
Many problems in statistics, signal processing and machine learning minimize a sum of a smooth loss and a nonsmooth regularizer: least squares with an or penalty, and constrained problems in which the regularizer is the indicator of a nonconvex set. The proximal gradient method (also called forward–backward splitting) is the standard first-order algorithm for such problems. Each step takes a gradient step on the smooth part and then applies the proximal mapping of the nonsmooth part, which for many nonconvex regularizers (hard thresholding, projection onto sparse vectors) has a closed form.
For a smooth part whose gradient is -Lipschitz, the classical analysis allows any constant step size , and every cluster point of the iterates is stationary; Li and Pong cite Bredies and Lorenz (Minimization of non-convex, non-smooth functionals by iterative thresholding, preprint, 2009) for this. Attouch, Bolte and Svaiter (Math. Program., 2013) added convergence of the whole sequence when has the Kurdyka–Łojasiewicz property. When is nonconvex, however, is governed by the most negative curvature of as much as by the most positive one, and the admissible step sizes can be much smaller than the convex part of alone would require.
Li and Pong (SIAM J. Optim., 2015; preprint arXiv:1407.0753v6) show that the concave part of imposes no restriction on the step size: it suffices to bound the curvature of after it has been offset by a convex function. This mission formalizes that result, Theorem 4 of their paper. It is the fourth mission of a series on the paper; the first three treat its results on the alternating direction method of multipliers.
Work in with the Euclidean inner product and norm . The problem is
under the paper's standing assumptions: is twice continuously differentiable with a bounded Hessian ; is proper (never , finite somewhere) and closed (lower semicontinuous); and for every and the proximal problem has a minimizer. Neither nor is assumed convex.
A vector is a regular subgradient of at (with ) if for all near , for every . The limiting subdifferential collects the limits of regular subgradients at points with . A point is stationary if
Given a step size and an arbitrary starting point , the proximal gradient method generates by
Any minimizer may be selected. A cluster point of is the limit of a subsequence .
The step-size condition involves a convex function and a constant with
where is the Loewner order on symmetric linear maps.
Suppose is twice continuously differentiable and convex, , (44) holds, and is generated by (43) with . Then
and every cluster point of , if one exists, satisfies .
The goal does not assert that a cluster point exists, nor that the whole sequence converges; both are false without further assumptions.
In the order of the paper's proof:
The result. For a difference of convex functions with being -Lipschitz, (44) holds with and , so the step size may be taken in whatever the curvature of . For an indefinite quadratic the admissible range becomes instead of , and for a concave quadratic every positive step size is admissible. Because the method is a descent method under this rule, its iterates stay in a sublevel set of , so the sequence is bounded whenever is coercive. The same estimates feed the whole-sequence convergence argument for Kurdyka–Łojasiewicz functions.
Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it requires the limiting subdifferential of an extended-real-valued function, its closedness property (3), and a Fermat rule for a smooth-plus-nonsmooth sum, none of which is in Mathlib. These are reusable for any nonconvex first-order method analysed through cluster points.
The descent part rests on (45), a descent inequality for whose Lipschitz constant is read off from a two-sided Hessian bound; the familiar descent lemma is stated for alone and does not apply, since may have a much larger Lipschitz constant than .
The stationarity part is where the naive argument fails. Passing to the limit in (47) needs not only but also , because the limiting subdifferential is closed only under -attentive convergence. Lower semicontinuity gives one inequality; the other must come from the minimizing property (43) compared against . The objective may be at , so summability of the steps has to be extracted without assuming a finite starting value.
The space is EuclideanSpace ℝ (Fin n). and are real-valued; takes values in EReal, and every objective value is compared in EReal, never through EReal.toReal. The Hessian is the derivative of the gradient map, a continuous linear self-map; the Loewner order is Mathlib's partial order A ≤ B ↔ (B - A).IsPositive, and both sides of (44) are kept. The regular subgradient is encoded in its -neighbourhood form, and the limiting subdifferential requires all three convergences , , . Stationarity is . The update (43) is a relation on sequences: minimizes the bracket over all of , with no uniqueness and a free starting point. A cluster point is the limit of for a strictly increasing .
Trivializing formalizations are ruled out: (44) is not replaced by " is -Lipschitz", which is the classical special case ; , boundedness of the sequence and existence of a cluster point are not assumed; and a limiting subdifferential without is not used, since that would make stationarity a weaker statement.
Contributions welcome: the closedness (3) and the Fermat rule behind (47) for the limiting subdifferential, a descent lemma from a two-sided Hessian bound, and the telescoping and limit arguments of the proof.