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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Classical Bayesian mechanism design assumes that the designer knows the agents' beliefs about each other: typically a commonly known prior over independent private values. Wilson's critique (1987) observed that mechanisms tuned to such a prior can depend on details that no designer knows, and a literature on robust mechanism design replaced the fixed prior by a large family of possible beliefs. Chapter 10 of Börgers, An Introduction to the Theory of Mechanism Design (OUP 2015), develops this programme in the framework of Bergemann and Morris (2001, 2005): agents' information is described by a type space, the designer is uncertain which beliefs agents hold, and mechanisms are compared across all type profiles at once.
Timeline of the results formalized here:
There are finitely many agents , and agent has a set of payoff types. An outcome gives agent the utility , which may depend on all payoff types. A type space consists of nonempty sets of types, a payoff type map and a belief map , where . Different types may share a payoff type and differ only in their beliefs, and vice versa. A common prior is a distribution on from which every type's belief is obtained by conditioning. A type space has a large variety of certainties if for every and some type with payoff type is certain that the others' payoff types are . The space of finite types collects every infinite hierarchy of beliefs ("I believe that you believe that …") that is generated by a type of some finite type space.
A mechanism has strategy sets and an outcome rule . Strategies form a Bayesian equilibrium if each type maximizes expected utility under its own belief; it is belief-independent if types with equal payoff types play alike, and ex post if each type's choice stays optimal when it becomes certain of the others' types. A direct mechanism asks agents for their types, a reduced direct mechanism only for their payoff types. In the quasi-linear case outcomes are and , with paid by agent ; a direct mechanism is .
On a finite type space with quasi-linear utilities, suppose that for every agent no belief in is a convex combination of the others, and that in the direct mechanism no type wants to imitate another type with the same belief. Then there is a direct mechanism in which truth telling is a Bayesian equilibrium, with
The goal fixes neither the transfers nor any bound on them; it asserts the existence of a truthful mechanism with the same alternatives and the same interim payments.
The other fourteen numbered results of the chapter: conditional independence of payoff types under a full-support common prior (10.1); three revelation principles (10.2–10.4); existence of Bayesian equilibria of finite mechanisms on (10.5); betting between agents with inconsistent beliefs (10.7); ex post implementation of unique equilibrium outcomes and alternatives (10.8, 10.9); emptiness of the set of undominated auctions under interim Pareto welfare and under ex post revenue (10.10, 10.11); Hylland's characterization of random dictatorship (10.12); and three comparisons of random dictatorship with random dictatorship with compromise (10.13–10.15).
Proposition 10.6 reduces the design problem on a finite type space to incentive constraints among types with the same beliefs: belief types can always be elicited by side payments that leave interim utilities unchanged. With a common prior and Proposition 10.1 this yields optimal mechanisms by solving an independent-types problem for each profile of belief types (§10.8; Farinha Luz 2013 carries this out for auctions). Proposition 10.7 and its consequences 10.10–10.11 show why the same construction cannot be used without a common prior: inconsistent beliefs allow unbounded bets, so interim or revenue criteria admit no undominated mechanism. Propositions 10.12–10.15 show that relaxing belief independence escapes Hylland's impossibility result in the voting problem.
None of these results is formalized elsewhere to our knowledge. The book proves only some of them (10.1, 10.5, 10.8, 10.9, 10.13–10.15 are proved or outlined; 10.6 is sketched; the proofs of 10.2–10.4 are omitted as standard; 10.7 and 10.10–10.12 are stated without proof), so formalization also produces complete proofs of results the book leaves informal. Two printed statements are corrected (see Formalization scope).
The obvious approach to Proposition 10.6 applies the Crémer–McLean construction type by type. This fails because several types may share a belief: a side payment that depends on the reported belief cannot separate them, and the convex-independence condition concerns the set of distinct beliefs rather than the indexed family of types.
For the results on , a type is an infinite belief hierarchy, and a strategy must be one function on all finite types simultaneously. Existence (10.5) cannot be obtained by applying Nash's theorem to a single finite type space, because a type belongs to many finite type spaces and must play the same strategy in all of them. Hylland's theorem (10.12) requires a full characterization of strategy-proof random rules on a cardinal preference domain.
PMF X); expected utilities are sums. The book leaves the measure structure of type spaces unspecified (p.179, note 3); finite type spaces, and point beliefs are covered exactly. A Bayesian equilibrium requires every type's expected utility to exist (absolute summability) under every mixed strategy.Fin 2, candidates , strict private vNM utilities with every strict utility attained; mechanisms map to lotteries over candidates; rankings are bijections C ≃ Fin 3.Welcome contributions: a finite Farkas/separation lemma in the form needed for 10.6 (the platform has Polyhedral.farkas_lemma), basic API for PMF-valued type spaces (products of mixed strategies, conditioning), and the hierarchy map of finite type spaces, which all milestones share.
Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.
This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.
Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.
There is a finite set of agents and a finite set of alternatives. Each agent has a preference relation over ; reads " is weakly preferred to ". Every is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is . The set of all linear orders over is , and a profile is . is the profile obtained from by replacing agent 's preference with .
A direct mechanism is a function (Definition 8.1). It is
"The range of is " means that every alternative is chosen at some profile.
For §8.3 the alternatives are labelled . A preference is single-peaked if it has a top alternative and declines monotonically to the right and to the left of it. is the set of single-peaked preferences, and on the restricted domain DSIC and dictatorship are read with all profiles and deviations taken from .
This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.
The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.
Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.
Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses cannot succeed. Formally, each "move just below in agent 's ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.
LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. is a Fintype. "The range of is " is Function.Surjective f, and is 3 ≤ Fintype.card A.∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.lab : A ≃ Fin K (labels ). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.A group of agents must choose one alternative from a set (whether to build a public project, who receives an object, which of several policies to adopt). Each agent privately knows how much each alternative is worth to them, and money can be transferred. A designer who wants the welfare-maximizing alternative must ask the agents for their valuations, and must set payments so that no agent gains by misreporting, whatever the others report. This requirement, dominant strategy incentive compatibility, does not depend on what agents believe about one another, which is why it is the standard robustness benchmark in public economics, auction design and algorithmic game theory.
The Vickrey–Clarke–Groves (VCG) mechanisms solve this problem for every efficient decision rule. The central question of Chapter 7 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), is whether they are the only solution, and what can be implemented in dominant strategies at all.
Timeline:
There is a finite set of agents and a set of alternatives. Agent has a type from an abstract set . If alternative is chosen and agent pays , agent 's utility is . A type vector is ; omits agent , and replaces agent 's type by .
A direct mechanism consists of a decision rule and transfer rules . It is dominant strategy incentive-compatible (DSIC) if for all , and ,
A decision rule is efficient if maximizes over at every . A mechanism is VCG if is efficient and every agent's transfer has the form
for some function of the other agents' types. The chapter also uses positive association of differences (PAD: if and every agent's utility advantage of over every other alternative strictly increases from to , then ), flexibility (the range has at least three elements), ex post individual rationality and ex post budget balance ().
If every is a convex subset of a Euclidean space and every is convex and continuous on , then every DSIC mechanism with an efficient is a VCG mechanism: for each there is with
The goal leaves , the number of agents and the dimensions free; it asserts only the form of the transfers.
Every numbered result of Chapter 7 except Proposition 7.6 (see Formalization scope):
Corollary 7.1 turns the VCG construction from one solution into the complete answer. Any question about efficient dominant-strategy mechanisms (revenue, budget balance, individual rationality) reduces to a question about the functions . With Proposition 7.10 it gives a necessary and sufficient condition for efficient, budget-balanced dominant-strategy implementation. That condition fails in bilateral trade, and the failure does not use individual rationality. Roberts' theorem plays the same role for inefficient rules: on unrestricted domains, weighted welfare maximization is essentially all that can be implemented.
All of these results are proved in the literature, and none is formalized. The platform has VCG incentive compatibility and weak monotonicity for valuation-based types (the Algorithmic Game Theory IV mission). It has no uniqueness theorem, no revenue equivalence for multidimensional convex types, no Rochet theorem and no Roberts theorem. The book proves Corollary 7.1 from Proposition 7.3, but proves 7.3 itself only by reference to Krishna and Maenner. It states Roberts' theorem without proof.
The uniqueness claim does not follow from incentive compatibility alone. With finitely many types it is false, because any transfers inside the gaps left by the incentive constraints work (Börgers §5.8). The work lies in showing that, along every segment in the convex type set, an agent's equilibrium utility is pinned down by the decision rule. The equilibrium utility is a pointwise supremum of convex functions, one for each report, and the chosen alternative can change at uncountably many points of the segment. A differentiable envelope argument is therefore not directly available. At the boundary of the type set, convexity alone does not prevent upward jumps, which is why continuity is part of the hypotheses. Roberts' theorem needs a separate, combinatorial analysis of the sets of utility differences at which each alternative is chosen, and flexibility is essential there.
Agents form a finite type ι with decidable equality. Types are arbitrary types Θ i, and utilities are u : ∀ i, A → Θ i → ℝ. The profile is Function.update θ i θ'. is the product Others Θ i over j ≠ i, so each and is a function of the others' types only; a constant or a function of the full profile would change the theorem. In the goal and Proposition 7.3, is a convex set S i in EuclideanSpace ℝ (Fin (d i)).
Deviations from the page, each forced by a counterexample recorded in the item's natural-language statement:
The trivializing formalization to avoid is proving Proposition 7.4 (VCG DSIC) in place of the goal (DSIC efficient VCG). A development that proves the goal needs reusable infrastructure: convex functions restricted to segments, absolute continuity of continuous convex functions on compact intervals, and an envelope theorem for suprema of convex functions. Proofs of Rochet's and Roberts' theorems in this abstract setting are also welcome.
Almost every screening, auction and regulation model asks the same preliminary question: which allocation rules can be made incentive-compatible by some choice of payments? In the one-dimensional models of auction theory and nonlinear pricing the answer is monotonicity: higher types must receive higher allocations. Many applications are not one-dimensional, though. Examples are multi-object auctions, multi-product pricing, and lotteries over several outcomes. For those, a characterization that uses no structure at all is needed. Rochet (1987) gave one: an allocation rule is implementable exactly when it is cyclically monotone, a condition that originates in Rockafellar's characterization of subdifferentials of convex functions. Later work on dominant-strategy implementation, the "weak monotonicity" literature of algorithmic mechanism design, and revenue equivalence all build on it.
This mission formalizes Chapter 5 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): all nine numbered results of the chapter.
Timeline. Rockafellar (1970, Theorem 24.8) characterized the cyclically monotone maps between vector spaces as the subgradient selections of convex functions. Rochet (1987) extended the idea to arbitrary alternatives and types with quasi-linear utility and proved that implementability is exactly cyclical monotonicity. Krishna and Maenner (2001) proved revenue equivalence on convex type spaces with utilities convex in the type. Bikhchandani, Chatterji, Lavi, Mu'alem, Nisan and Sen (2006) showed that for finitely many alternatives, weak monotonicity (the two-type case of cyclical monotonicity) already suffices on rich, order-based domains. Saks and Yu (2005) proved the same on convex domains.
A designer and one agent choose an alternative from a set . The agent has a type in a nonempty set . With utility function , her payoff from when she pays is . Neither nor carries any structure.
A direct mechanism is a decision rule and a transfer rule . It is incentive-compatible if for all . A decision rule is implementable if some makes it incentive-compatible. It is weakly monotone if for all pairs of types. It is cyclically monotone if for every finite sequence of types with ,
A complete and transitive order of induces a partial order on types: if values every -higher alternative strictly more, relative to an -lower one, than does, and neither type distinguishes -indifferent alternatives. The type set is one-dimensional if any two distinct types are -comparable, and bounded if all utility differences lie in for some . It is rich if, for some reflexive and transitive relation , every function with is some type's utility function. A mechanism is individually rational with outside option if every type does at least as well as with and no payment.
for arbitrary , nonempty and .
Rochet's theorem turns the existence of payments, an infinite system of linear inequalities in unknowns , into a condition on the decision rule alone. It underlies the characterization of implementable rules in multidimensional screening, the taxation principle, and the dominant-strategy characterizations of Chapter 7 (applied agent by agent). Propositions 5.4–5.6 recover the "monotone allocation" results of the one-dimensional chapters from it. Proposition 5.8 is the general form of the payoff-equivalence lemmas used for optimal auctions.
All results are classical and proved on paper, except Propositions 5.7 and 5.8, whose proofs the book omits and refers to the literature. None of them is formalized on Prove2Me. The platform's algorithmic-game-theory series has the weak-monotonicity half in a multi-agent valuation model (types are valuations ), not the abstract-type statement, and has no cyclical-monotonicity or Rochet result.
Necessity is a two-line telescoping argument. Sufficiency needs a transfer rule built from the decision rule, and the first idea fails: prices attached to alternatives chosen pair by pair (which weak monotonicity supplies) need not be globally consistent. Figure 5.1 of the book gives a three-type example that is weakly monotone but not implementable. The transfer must come from a supremum over all finite chains of types starting at a fixed type. The supremum is finite only because of cyclical monotonicity, and no finiteness, compactness or boundedness is available. Proposition 5.8 needs an envelope argument along segments in without differentiability. Proposition 5.7 needs a combinatorial argument that uses richness of the domain.
Alternatives and types are arbitrary Lean types A, Θ with Nonempty Θ, and the utility is u : A → Θ → ℝ. A cycle of length is a map Fin (m+1) → Θ with equal first and last entries, and its summands are indexed by Fin m. Relations are predicates A → A → Prop. For Propositions 5.3 and 5.8, types form a subset S of Ω → ℝ (resp. Fin n → ℝ) used as a subtype. Lotteries are stdSimplex ℝ Ω, and the subgradient inequality is required only at points of S.
The explicit statements are fixed as follows:
Two statements are corrected from the page, each with a counterexample to the literal version recorded in its item:
Both directions of Rochet's theorem are required. The necessity half alone, or a version with finite , finite or bounded utilities, is a different and much weaker theorem and does not close the goal.
The development needs finite telescoping sums, suprema of sets of reals (sSup with an explicit bounded-above argument), convex functions on sets and one-dimensional convex analysis (Proposition 5.8). The definitions file is reusable for Chapters 6–8 of the series. Contributions of alternative proofs, for example Proposition 5.6 through Rochet's theorem, are welcome.
Bayesian mechanism design assumes that the designer knows a common prior from which every agent's beliefs about the others are derived. Chapter 4 of Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, DOI 10.1093/acprof:oso/9780199734023.001.0001) drops that assumption. The designer is unwilling to rely on anything about what agents believe about each other, and therefore requires that truth telling be optimal for every type whatever the other agents report (dominant strategy incentive compatibility) and that participation be worthwhile after all reports are known (ex post individual rationality). The chapter revisits the three examples of Chapter 3 (single unit auctions, public goods, bilateral trade) and asks which mechanisms survive these requirements.
The answer differs sharply between examples. In auctions nothing is lost: an expected-revenue-maximizing auction can be implemented in dominant strategies. With a budget constraint, the class collapses. For a public good shared by two agents, the only dominant-strategy, ex post individually rational mechanisms that exactly balance the budget are fixed cost shares; in bilateral trade they are fixed-price mechanisms. These results go back to the dominant-strategy literature on public goods (Serizawa 1999, Econometrica) and on bilateral trade (Hagerty and Rogerson 1987, Journal of Economic Theory), as the book's §4.5 records (p.93), and they explain why simple posted-price and cost-sharing rules are common in practice.
Every agent has a type in an interval. In the auction and the public good examples the interval is with ; is the set of type vectors, and is without its -th entry. A direct mechanism asks every agent to report a type and maps the reports to an outcome.
A mechanism is dominant strategy incentive-compatible if for every agent, every true type, every false report and every report profile of the others, truthful reporting yields at least as much utility. It is ex post individually rational if every type's utility at every type vector is at least its outside option: for buyers and public good agents, (keeping the good) for the seller. A canonical mechanism (Definitions 4.3–4.5) allocates according to strictly increasing continuous scores and charges each agent the smallest report with which the outcome would have been the same.
For and a decision rule whose production set is closed, a direct public good mechanism is dominant strategy incentive-compatible, ex post individually rational and ex post budget balanced if and only if there are with and, for all ,
Both directions are part of the goal; the "only if" direction is the content.
Proposition 4.4 shows that the optimal auctions of Chapter 3 remain available without any assumption on beliefs, while Propositions 4.8 and 4.12 show that under exact budget balance, dominant strategy implementation forces rules that ignore reported valuations except through a yes/no participation decision. Together they mark the boundary between settings where the Bayesian and the belief-free approaches coincide and settings where the belief-free requirement is severe. This contrast motivates the robust mechanism design of Chapter 10.
These results are proved in the book: Propositions 4.5 and 4.8 in full, the others with proofs omitted or "analogous". No machine-checked proof of them appears on the platform or in Mathlib. The platform has a single-parameter characterization in a different model (AGT.single_parameter_characterization: valuation profiles, win sets, normalized losers' payments) and the second-price dominance fact; neither covers public goods, bilateral trade, budget balance or randomized allocations. The mission would add a machine-checked belief-free counterpart of Chapter 3, including the two characterization theorems whose printed proofs leave cases to the reader.
The characterizations (Propositions 4.2, 4.5, 4.9) are standard single-agent arguments applied to every profile of the others. The goal is harder. Proposition 4.5 describes each agent's incentives separately, for each report of the other agent, with thresholds and payments that may vary with that report. Budget balance couples the two agents' payments at every type vector. The step that fails when attempted naively is going from "a threshold for each " to "one fixed threshold for each agent": the thresholds may lie outside the type interval, several degenerate configurations occur (an agent whose report never matters, a good that is always or never produced), and the printed proof treats the degenerate cases by assuming and leaves one of them "analogous". The closedness hypothesis is what makes the relevant minimal types exist; without it the boundary of the production set is not determined. Proposition 4.12 has the same structure with the seller's orientation reversed.
Fin 2 for the goal, and a pair (θS, θB) : ℝ × ℝ for bilateral trade. A deviation is Function.update θ i x for θ ∈ Θ; quantifying over θ ∈ Θ quantifies over .sInf/sSup of sets that are nonempty and closed whenever they are used.Contributions welcome: proofs of the characterization milestones (4.2, 4.5, 4.9), which the goal and Proposition 4.12 use; a proof of the goal covering the degenerate cases the book leaves to the reader; and the three-agent counterexample of p.90 as a separate statement.
Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.
This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.
Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.
A seller owns one indivisible good; a buyer may buy it. The seller's value has distribution with density on ; the buyer's value has distribution with density on . The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is if she sells for and if she keeps the good and receives ; the buyer's is if he buys and pays , and otherwise.
A direct mechanism is a trading rule on and transfers (received by the seller) and (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities , the interim transfers , and the interim utilities and . The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if and for all types, ex post budget balanced if for every , and ex ante budget balanced if . A first-best trading rule trades when and not when , with any choice at ties. The seller's virtual cost is and the buyer's virtual valuation is ; the distributions are regular if both are increasing.
An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if
for some , exact budget balance , and the incentive-compatible payments with binding participation of and .
The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.
All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.
The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.
A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on with density . Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in on (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: , , are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.
Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter , the exact budget equation of Proposition 3.13 (ii), the payment formulas and , the profit rule , and the thresholds and .
The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality . Dropping budget balance, weakening it to , or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all " characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to : under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.
Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.
Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.
This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.
A community of agents , , decides whether to produce an indivisible, nonexcludable public good, , at cost . Agent pays a transfer and obtains utility . Her type is private information, drawn independently across agents from a distribution with density , strictly positive on the common support , . The type space is and .
A direct mechanism is a decision rule and transfer rules . For agent reporting , is the probability of production and the expected transfer, taken over the other agents' types, and . The mechanism is incentive compatible (IC) if for all , and individually rational (IR) if for all . It is ex post budget balanced if for every , and ex ante budget balanced if this inequality holds after integrating both sides against .
Welfare is . The first best decision rule is if and otherwise; a first best mechanism uses and transfers that add up to exactly in every state. The pivot mechanism uses and
The virtual valuation is , and is regular if is strictly increasing.
In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.
the budget binds, , and . 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff , with the same formula for . 7. Proposition 3.10 (Example 3.3: , uniform types on , ): the second best produces iff , where is the unique root in of if , and if . 8. Proposition 3.11 (same example): the profit maximizer produces iff .
Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.
All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.
The naive argument for the goal fails at the first step: a mechanism that implements with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.
Agents are Fin N with ; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures on , which encodes independence. and integrate the decision and transfer rules against this distribution with agent 's coordinate overwritten by her report. Decision rules are deterministic, with values in on , as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.
The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires and each to be Borel measurable, each integrable, and each conditional expectation of given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every , is sufficient; necessity holds for almost every , since changing on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier and the binding budget identity; ; the cubic for ; for ; and for the profit maximizer.
A trivializing formalization of the goal takes "first best" to mean only the decision rule ; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly in every state.
Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.
A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.
This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.
Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).
There are potential buyers . Buyer values the good at ; if he receives it and pays his utility is , and otherwise . The seller's utility is . The valuations are independent; has cumulative distribution function and density with on the common support , where . The type space is and the joint density is .
A direct mechanism asks buyers to report their types and consists of an allocation rule , where , and payment rules . Its interim quantities are the expected allocation probability, payment and utility of buyer conditional on his own type:
The mechanism is incentive-compatible if for all (truth-telling is a Bayesian Nash equilibrium) and individually rational if for all . The virtual valuation of buyer is
and the distribution is regular if is strictly increasing.
Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue exactly when, for every buyer ,
the allocation identity holding for almost every ; and such a mechanism exists.
The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.
The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end , Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on .
The obvious argument maximizes the virtual surplus pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every ; the pointwise maximizer is feasible only because regularity makes increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of , with care at the endpoints of the type interval.
Buyers form a finite type with at least two elements. The prior is the measure on with density on and no mass outside it; each is measurable, strictly positive on and integrates to ; . Allocation and payment rules are total functions whose values on are constrained, and , are prior expectations with the -th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of on (Assumption 3.1).
The following conventions are committed to:
The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.
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.
Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of states, or the stocks of commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation
and, in the limit of small time steps, to differential equations of the form and, when two opposing controllers act, .
These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).
Fix . Row of the matrix carries its own control , ranging over a set ; the joint control is in , and . Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over is then taken row by row.
The Perron root is the characteristic root of of largest absolute value, the spectral radius of as a complex matrix. The conditions (10.3) of the chapter are:
For the continuous processes, and , and a solution of , , on is a continuous with , which is the book's "satisfying the equation almost everywhere". The successive approximations are , .
Under (10.3) there is exactly one for which
has a solution with all . That solution is unique up to a positive factor, and
Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration : after normalization by the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.
The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.
The map is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each , including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in and Lipschitz in with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.
Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row 's control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume ; for every would qualify.
Conventions and repairs:
Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for with an integrable Lipschitz constant, each reusable well beyond this mission.
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 IX of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) recasts problems of the calculus of variations with constraints as dynamic programming processes. A variational problem with an inequality constraint on the control, such as , is awkward for the classical Euler–Lagrange theory: the optimal control switches between the constraint boundary and the interior, and the number and location of the switches are unknown in advance. Bellman's proposal is to replace the continuous problem by a discrete-time one and to solve that by the recurrence relations of dynamic programming, a procedure he describes as the more reliable computational one "in cases treated to date" (§ 11, p. 260).
That proposal is sound only if the discrete values converge to the continuous value as the time step goes to zero. Chapter IX states one such convergence result, Theorem 2 of § 12, and proves it through an Euler-scheme error estimate. The same chapter works through an example (§§ 10–11) whose discrete version is described by Theorem 1. Both are the subject of this mission. The convergence of time-discretized dynamic programming to the continuous value function has since become a standard topic of numerical optimal control (for example the semi-Lagrangian schemes analysed by Capuzzo-Dolcetta and Falcone), and Bellman's § 12 is an early rigorous instance of it.
A state evolves on a horizon under a control with , a running reward and dynamics
Writing with a fractional control turns and into and (phiForm). The continuous value is
over measurable with values in , where solves on (IsTrajectory, contValue).
For the discrete problem uses step and steps (horizonSteps): for ,
and (eulerTraj, discretePayoff, discreteValue). A discrete control defines the step control on (stepControl).
The example of §§ 10–11 has a gain function with , , , as , (IsGainFunction; is one), and value functions (uSeq)
Assume (11): (a) and have continuous second partial derivatives; (b) for , ; (c) throughout that region, or throughout. Then for all , , the set of continuous payoffs is nonempty and bounded above, and
Milestones 3–5 are stated for , as in the book's proof ("Given and "); the goal is stated for , as in the theorem.
Theorem 2 says that the value of a constrained continuous-time control problem can be computed, to any accuracy, by the finite recurrence of dynamic programming on a time grid. Its upper half (12.14) gives a rate: the discrete value never exceeds the continuous one by more than . The lower half (12.17) needs no rate and holds because measurable controls are approximated by step controls. Theorem 1 is a discrete counterpart of the transition curve computed in § 10: below the threshold the whole state is invested, above it an interior amount, and the thresholds increase with the number of remaining stages.
As far as the mission's author could establish, none of these results has a machine-checked proof. The Euler error estimate is classical and has a Gronwall-type proof; Mathlib contains Gronwall's inequality (Analysis/ODE/Gronwall) and Picard–Lindelöf for continuous right-hand sides, but no convergence theory for the value of discretized control problems. The book leaves the proof of Theorem 1 to the reader.
The upper bound (12.14) follows from the Lemma once the continuous and the discrete trajectories are known to stay in a common bounded strip ; that uniform bound is what assumption (11b) provides and must be established first. The lower bound is where the obvious argument fails: an arbitrary measurable control is not a step control on the grid , and passing to a step control changes the trajectory, so the payoff must be shown continuous under almost-everywhere convergence of controls. This uses the trajectory's dependence on the control in , not only on the initial value. Solutions exist in the Carathéodory sense only, so the integral form of the equation is required. For Theorem 1 the induction must carry concavity of and a strict comparison of marginal values across , and is not differentiable at , where .
States, controls and rewards are real; (or ), with the hypotheses imposed where the book imposes them. The conventions:
A trivializing formalization is ruled out: the discrete and continuous values are defined from and by the book's recursions and integrals, not assumed as hypotheses, and the corrected step count is not a free parameter.
Needed infrastructure: Carathéodory existence and uniqueness for Lipschitz right-hand sides with measurable controls, Gronwall estimates for the Euler scheme, and approximation of measurable controls by step functions. All three are reusable beyond this mission, and contributions of any of them 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.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.
The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.
Theorem 3.3.1 (p.211) is the one that says when the two views coincide.
This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the
θ_t-framework.
E⁰_A[f(Z(0))] = E[f(Z(0))] (3.3.1)
for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f,
whenever A admits the constant F_t-intensity λ; and, under ergodicity,
lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds . (3.3.2)
The "some care" is the word predictable. PASTA is false without it: an arrival that changes the
state it then observes does not see the time average, and that is exactly what predictability —
measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a —
rules out.
The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two
are equivalent, but that equivalence is a remark on the page and not part of this theorem.
§3.4 derives formulas from conservation equations. Applying the rate conservation principle of
Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula
iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) , (3.4.44)
an identity between a stationary expectation and a Palm expectation of the workload just before
an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the
arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and
E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) , (3.4.45)
the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.
§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.
§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a
countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its
two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes
Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by
thinnings of the entrance processes of two disjoint sets.
§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.
Nothing here is on the platform or in Mathlib. The nearest platform item,
queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring
disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the
Palm identity for a stationary ergodic marked point process, derived from the inversion formula
(1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a
pathwise limit. Different framework, different hypotheses, and neither implies the other.
Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.
(3.3.1) is an equality in [0, ∞] for every non-negative
measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one
common limit, so both limits exist. Predictability is measurability for the predictable σ-field
P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis,
because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity,
E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".u, and for
u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under
P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a
measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for
{W(t−)}, and it asserts that its denominator is non-zero.E_α R. The chain is irreducible, F is non-empty,
and hitting times are counted from time 0.E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is
flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is
the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞].
Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?
The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked
point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the
service still owed by the server, obeys Lindley's equation between arrivals:
W(t) = (W(T_n−) + σ_n − (t − T_n))⁺, t ∈ [T_n, T_{n+1}). (2.1.6)
Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The
answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].
Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under
ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and
it is given explicitly by the Loynes supremum
W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ , (2.1.12)
with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If
ρ > 1 there is no finite stationary workload process at all.
Each half earns its place. The supremum is what "the Loynes construction" means: look back from the
origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and
maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient
condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there
"may or may not" be a stationary workload — and is deliberately absent from the statement.
§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.
Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with
Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it
forces that difference to be invariant, and ergodicity then forces it to be zero.
Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form
lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ], P⁰-a.s.
Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.
The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is
the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes
E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space
with a whole interval of stationary solutions. What survives is that the solution set is bracketed
— M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).
Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a
sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges
in variation to the stationary trajectory's. The proof is one inequality,
|P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.
The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible
random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum
W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book
claiming no uniqueness here.
ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and
falls under the non-existence half rather than being read as ρ = 0.E⁰[σ]/E⁰[τ] of Theorem
2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).θ_t-compatible workload processes; maximality
in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a
random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would
trivialize the goal and is ruled out.None of it is on the platform or in Mathlib. The nearest platform item,
single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves
two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it
unique, gives it in closed form, and adds the non-existence half. Different conclusion, different
generality, different Mathlib revision.
Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field on a closed manifold is Anosov when the tangent bundle splits as , with uniformly contracted and uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.
The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.
A plug is a compact 3-manifold with boundary and a nonsingular C¹ vector field transverse to . The boundary splits into the entrance boundary (where points inwards) and the exit boundary . The maximal invariant set consists of the points whose orbit stays in for all times. The plug is hyperbolic if is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination and the exit lamination are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of (and of ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.
A diffeomorphism is a strongly transverse gluing map if and are transverse and cut into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold with an induced vector field . Two triples and are strongly isotopic if they are joined by a continuous path of such data.
Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.
The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).
EuclideanHalfSpace 3 with a structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.flowMap X t x is when the orbit is undefined.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).