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.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.
Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.
Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.
A committee of individuals chooses from a finite set of alternatives. A strong order on is a complete, transitive relation with no indifference between distinct alternatives; denotes strict preference. Let be the set of strong orders and the set of strict ballot sets .
Arrow's conditions on : CS—for all some gives ; IIA—if for all then ; NNR—raising an alternative in individual ballots, with the order of the other alternatives unchanged, never lowers against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for over yields .
For and there is a bijection
with for every and every .
The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.
On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.
The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation does this, but proving that is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.
A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.
A, ι with decidable equality; , throughout.ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.Set.range v = Set.univ.Equiv together with " underlies " for every . A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.Reusable beyond this mission: the strict-preference vocabulary (strong orders, , Arrow's conditions in the paper's form) and Gibbard's construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.
A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.
Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.
Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.
Timeline.
A committee of individuals ranks a finite set of alternatives. A weak order on is a complete, transitive relation, and reads " is preferred or indifferent to ". Its strict part is : and not . The weak orders form . A strong order is a weak order with no indifference between distinct alternatives, and the strong orders form . A ballot set is .
A social welfare function assigns to every ballot set a social ordering . A strict social welfare function is defined only on strong ballot sets and takes values in . For , is the set of -best elements of , and is the restriction of to .
A tie-breaking function maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order .
For , and any social welfare function on weak ballot sets,
The converse is false with indifference, so the goal is one-directional.
Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').
All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.
Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.
A and ι with decidable equality. = Fintype.card ι, = Fintype.card A, and , are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.
Axiomatic bargaining theory asks which rule should divide a set of feasible utility vectors among a group of agents, and answers by listing properties a reasonable rule must have and determining the rules that have them. Nash's solution (Nash 1950) and the Kalai–Smorodinsky solution (Kalai and Smorodinsky 1975) are the two classical answers for a fixed set of two agents. Both characterizations take the number of agents as given.
In many division problems the group is not fixed: a supply of goods that was to be shared among some agents must later be shared among more. Thomson (1983) (Math. Oper. Res. 8:319–326) introduced a framework in which the population varies and a solution is a family of rules, one for each finite group. He proposed an axiom tying the rules for different groups together: when new agents arrive and the resources stay fixed, none of the original agents should gain (population monotonicity). The paper shows that this axiom, combined with four standard ones, singles out the Kalai–Smorodinsky solution.
Timeline.
The agents are the natural numbers, and a group is a nonempty finite set of agents. For a group , is the space of real vectors indexed by , and its nonnegative orthant. For vectors, means for every , means for every , and means with .
A division problem for is a set that is compact, convex, contains a strictly positive vector, and is comprehensive: if and , then . The class of these problems is . The subclass also requires that whenever and , some satisfies .
A solution chooses a point for every group and every . The ideal point of is , with . The Kalai–Smorodinsky solution selects the largest point of on the segment from the origin to :
The axioms on a solution are:
For every solution ,
Two further statements accompany the goal. Corollary 2 says that no solution satisfies PO, An, S. Inv and Mon. Lemma 1 says that some solution other than satisfies WPO, An, S. Inv and Mon.
The theorem identifies the Kalai–Smorodinsky solution as the only rule, among those treating agents symmetrically and ignoring utility units, under which an arrival of new claimants never benefits existing ones. Corollary 2 shows that weak Pareto-optimality cannot be strengthened to Pareto-optimality. Lemma 1 shows that continuity cannot be dropped. Together they fix the logical boundary of the result. The replica construction of the appendix is a reusable device: a problem in which every agent of a larger group faces an exact copy of one agent's situation.
The result has been proved since 1983. It has not been machine-checked, and to our knowledge no proof assistant library contains bargaining problems, solutions or the Kalai–Smorodinsky solution. The mission produces these definitions and checks the full argument, including two steps the paper asserts without proof. One is that the replica problem has the required slices. The other is that problems satisfying condition (c) are dense in the Hausdorff metric. Formalizing the paper also exposes a printed slip: Theorem 2 is stated as an equivalence, but only one direction is true and proved, and only that direction is stated here.
Theorem 1 asks for routine but real convex analysis. Continuity of requires the ideal point and the maximal scalar to move continuously with in the Hausdorff metric. Comprehensiveness and the strictly positive vector are what make this work.
The substance is in Theorem 2. The first thought is to compare with inside alone, using only WPO, An and S. Inv. That cannot work: Lemma 1 exhibits a solution satisfying all four axioms that differs from , so the argument must leave the group . The proof builds a larger problem in which every member of an enlarged group faces a copy of the worst-treated agent's position. Mon then caps each agent's payoff in , and WPO fails at the diagonal point . Choosing the groups and bijections, and verifying that each slice of the convex comprehensive hull is exactly the intended copy, is the delicate part. The paper dismisses it as "clear".
Theorem 3 needs the density of in . An approximating problem must lose every flat face on its weak Pareto boundary while staying compact, convex and comprehensive.
Agents are ℕ, where the paper uses ; this relabelling is harmless. Groups are nonempty: for the empty group, is a point and WPO would hold for no solution, so the page's "finite subsets" is read as nonempty finite subsets. A group is a Finset ℕ, and is the function type P → ℝ, whose metric is the sup metric. Hausdorff convergence uses Mathlib's extended Hausdorff distance Metric.hausdorffEDist. Convergence in it is equivalent to Euclidean Hausdorff convergence, because the norms are equivalent.
A solution is a total function on all sets, together with the hypothesis IsSolution F that for . Every axiom quantifies over problems in only, and " is the Kalai–Smorodinsky solution" means agreement on every . Two formalizations of the goal would be trivial or false, and the statements here rule out both: one that equates and as functions, and one that drops IsSolution.
The remaining conventions are these.
sSup. Both suprema are attained on .P ≃ P'.Deviation from the page. Theorem 2's printed "if" direction is false, so only "only if" is stated. For example, choosing on and elsewhere gives a solution with that violates S. Inv. The replica milestone states the appendix construction existentially, for a generic agent instead of agent 1.
Out of scope: Theorem 4 (solutions defined on only, whose necessity proof is a sketch), and the remarks of §4.2–§4.4.
A complete development needs Hausdorff-metric continuity of maxima over compact sets and the convex comprehensive hull. It also needs elementary facts about slices and relabellings of comprehensive sets. All of these are reusable for other bargaining and fair-division formalizations. Contributions are welcome on any milestone, and on lemmas about that several milestones share.
The logarithm of a share price is commonly modelled as a Brownian motion with drift, . The Black–Scholes option pricing formula needs the volatility but not the drift , so a practitioner must estimate from data. Observing the whole path would give exactly through its quadratic variation, but a real observer sees far less. The most readily available daily information is the opening and closing prices together with the day's high and low.
Parkinson (1980) proposed an estimator from the high–low range, and Garman and Klass (1980) found the minimum-variance estimator among a class of quadratic functions of high, low and close. Both were derived assuming zero drift, , and the Garman–Klass estimator is biased when . Rogers and Satchell (Ann. Appl. Probab. 1 (1991) 504–512) proposed the estimator
which is unbiased for every drift. Their estimator is now a standard tool in empirical finance for range-based volatility measurement.
Fix a probability space carrying a standard Brownian motion : , its increments over disjoint intervals are independent and Gaussian with variance equal to the length of the interval, and every sample path is continuous. Fix a drift and a volatility . The log-price is
and, for a trading period , the running maximum and running minimum are
Thus , and are the high, the low and the close of the log-price (with the open normalized to ). In Lean these are logPrice σ c B t ω, runMax σ c B t ω and runMin σ c B t ω in the namespace RogersSatchell.Unbiased.
The proof in the paper passes through an exponential time: a random variable with (rate , mean ), independent of the whole path . For the rates
appear, in Lean alpha σ c lam and beta σ c lam.
For every , every and every , is integrable and
At this is the unbiasedness of of display (2). The statement quantifies over all drifts; the absence of on the right-hand side is the content.
The goal certifies a drift-free unbiased volatility estimator built from four numbers per trading day. Because only enters the Black–Scholes formula, an estimator whose mean does not depend on the nuisance parameter is exactly what is needed. Milestone 7 complements this with a drift-uniform bound on its variance, , while the exact value quoted in the paper is only available at .
On the formalization side, the results are classical and proved; none is machine-checked as far as the platform's catalog shows. A complete development would give the first formal treatment of the joint law of the running maximum of drifted Brownian motion at an exponential time, of the Wiener–Hopf splitting at the maximum, and of a Laplace-inversion argument for a moment function of the time horizon. All three are reusable well beyond volatility estimation: in ruin theory, queueing (reflected Brownian motion), and the pricing of lookback and barrier options.
The obvious approach, computing directly from the joint density of for drifted Brownian motion, requires the reflection principle combined with a Girsanov change of measure, followed by a double integral involving Gaussian tails, done separately for each sign of . The cancellation that makes the drift disappear is not visible in that computation, and a statement specialized to (where the reflection principle alone suffices) does not carry over. Every step of the milestone list rests on path properties of Brownian motion (the strong Markov property, the law of the running maximum, splitting at the maximum) that Mathlib does not yet provide for IsBrownianReal, and the passage from milestone 4 to milestone 5 needs uniqueness of the Laplace transform.
ProbabilityTheory.IsBrownianReal B P with B : ℝ≥0 → Ω → ℝ, plus the hypothesis that every sample path is continuous (the standard choice of a continuous version). Time is ℝ≥0.sSup/sInf of the path over the interval ; with continuous paths they are attained. The supremum is never taken over all times or in extended reals.HasLaw T (expMeasure λ) P; "parameter " is read as rate . "Independent of " is independence from the path-valued random variable with the product σ-algebra. is evaluated at truncated to .A formalization that specializes to , takes the supremum over all of , or omits the integrability conjuncts is not the statement of this mission.
Infrastructure that a complete development needs: the reflection principle or the strong Markov property for Brownian motion, the exponential-time law of the running maximum of a Lévy process, and uniqueness of Laplace transforms for continuous functions. All of these are reusable; contributions of any of them are welcome. Related platform items cover other objects and are credited here: running maxima and exit problems for spectrally negative Lévy processes (Avram2004.Exit.reflected), a drifted Brownian motion in characteristic-function form in a queueing-network setting (Reiman84.QueueLength.Paths), and a GI/G/1 Wiener–Hopf transform identity (QueueingFundamentals.GG1.wiener_hopf_transform).
The method of multipliers (augmented Lagrangian method), proposed independently by Hestenes and Powell in 1969, solves a constrained optimization problem by a sequence of unconstrained minimizations of a penalized Lagrangian, updating a multiplier estimate between them. It became one of the standard algorithms of nonlinear programming and is the ancestor of ADMM and of the proximal-point view of dual methods. Rockafellar's 1973 paper (Math. Programming 5, 354–373) extended the method to inequality constraints with the penalty Lagrangian and reinterpreted it as unconstrained maximization of a smooth concave dual function . Its §4 shows that primal points recovered from any maximizing dual sequence are asymptotically minimizing; its §5, the subject of this mission, asks how fast they converge.
Timeline. 1969: Hestenes and Powell introduce multiplier methods for equality constraints. 1973: Rockafellar treats inequality constraints in the convex case through and its dual (this paper), and in the same year applies the multiplier method of Hestenes and Powell to convex programming (J. Optim. Theory Appl. 12). 1976: Rockafellar's "Augmented Lagrangians and applications of the proximal point algorithm in convex programming" (Math. Oper. Res. 1) gives the general convergence theory.
Let be convex and convex. The problem is
With and a parameter , the penalty Lagrangian is
and the dual problem maximizes over all ; is its supremum. A maximizing sequence is a sequence with . The dual method of Theorem 4.1 takes a bounded maximizing sequence and, for each , a point that minimizes to within a tolerance :
The standing assumptions of §5 concern a point that is an optimal solution of (P), near which are twice continuously differentiable, and a multiplier vector satisfying with the Kuhn–Tucker conditions (, , , and minimizes over ). With the active set and , they are: (i) for ; (ii) the , , are linearly independent; (iii) for every nonzero with for all .
Under the standing assumptions, with as in (4.7), if for some
then there is a constant with
No rate for is fixed: the statement compares the primal error with the dual error, whatever method produces the dual sequence.
Corollary 5.3 is the paper's answer to the practical question of how accurately each inner minimization must be done. A tolerance proportional to the current dual gap costs nothing in the order of convergence: the primal iterates then converge at least as fast as the dual ones. Since is with a negative definite Hessian near (Theorem 5.1 (v)), any locally linearly or superlinearly convergent unconstrained method applied to yields a primal sequence with the same rate. The estimates (5.15)–(5.17) are the quantitative bridge between inner accuracy, dual error and primal error, and reappear in later analyses of inexact augmented Lagrangian methods.
The results are proved in the paper (1973) and in textbook treatments; none of them has a machine-checked proof on this platform or in Mathlib. The mission produces a formal statement of the second-order theory of the penalty Lagrangian: the local smooth structure of and , the implicit minimizer map , and the rate comparison. Complete formal proofs of each milestone are the remaining work.
The obvious argument linearizes everything at , but is only globally: has a kink in its second derivative, so smoothness of must first be established on a neighborhood of , using complementary slackness and strict complementarity (i) to fix which branch of (2.4) each constraint follows. The sequence is not assumed to converge; localizing it into that neighborhood requires the uniform statement of Theorem 5.1 (i) (with chosen after ) and the uniqueness of and . The minimizer map then comes from the implicit function theorem applied to , and the formula for needs the derivative of the envelope .
EuclideanSpace ℝ (Fin n), multipliers in EuclideanSpace ℝ (Fin m); constraint indices are Fin m (0-based), and is a separate argument.ConvexOn ℝ X, an explicit hypothesis of every theorem, the paper's standing assumption of p. 358), and twice continuous differentiability only on a neighborhood of . Smoothness of and is always a conclusion, never a hypothesis.EReal, so (4.7), (5.2), (5.3) and (5.18) are differences in ; is explicit for the penalty Lagrangian, while is defined separately.Analysis/Calculus/Implicit), second derivatives of compositions, envelope differentiation, and the quadratic-growth estimates of a function with definite Hessian. Results on Hessian forms and on strict complementarity are reusable beyond this mission. Proofs of individual milestones are welcome independently.Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility than the close alone. Rogers and Satchell (1991) propose an estimator, , that is unbiased for whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.
Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at times. The sampled maximum falls short of the true maximum by an amount , and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,
enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.
Fix a volatility and a sampling mesh (in the paper ). For a level define
The factor is the probability that a Brownian bridge of duration and volatility climbs above level . The factor is a probability density on . Since and decreases continuously to , it is the survival function of a law on . This law is the paper's display (9).
A real random variable has distribution (9) if it is measurable and for every . In the paper, is the overshoot of the continuous maximum over the sampled maximum in the sampling interval to the left of the time at which is attained, and is the overshoot in the interval to the right. The paper then assumes (p. 508) that and are independent, each with distribution (9), and approximates by . Write .
In Lean, overshootSurvival σ h α is , HasOvershootLaw P σ h Z is " has distribution (9) under ", and constA, constB are and .
For and independent with distribution (9), the variables and are integrable, and
The goal combines milestones 2–5 through , which the paper uses in (11).
The result. The two identities are the coefficients of the corrected estimator (5): replacing and by and turns the high–low estimator into an equation whose positive root largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for and the correction has no concrete form.
Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes ). To our knowledge none of these identities has been formalized before.
The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights on an unbounded domain. The minimum of and couples two such integrals, and the resulting kernels and have to be integrated in closed form over the unit square. Matching and exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is .
(Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels : the formula is even in , and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. and are max and min.Integrable, or MemLp … 2 for second moments). The conditioning "" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "" in (13) is read as , as its first line shows. The integrals in (9) run over and .survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.A convex minimization problem comes with a dual maximization problem, and the dual value never exceeds the primal value. When the two values differ, a duality gap occurs. Dual bounds, Lagrangian relaxations and optimality certificates are then weaker than hoped. Conditions that rule the gap out are constraint qualifications such as Slater's condition and Rockafellar's notion of a stably set problem. Such conditions say when the gap vanishes, but not what the dual value is when it does not.
R. T. Rockafellar's 1967 paper answers that question for the Fenchel-type pair of problems built from a convex function, a concave function and a continuous linear map between infinite-dimensional spaces. Its Theorem 6 (§6, "Weak duality theorems", pp. 179–180) "explains the exact way in which inf (P) and sup (P*) can fail to be equal", by expressing the dual value through the primal problem alone: the dual supremum is the lower limit of the optimal values of slightly perturbed primal problems. This perturbational view of duality was later developed in Rockafellar's Conjugate Duality and Optimization (1974). It underlies the modern treatment of value functions in convex optimization.
Two real vector spaces and are topologically paired when each carries a locally convex Hausdorff topology, they are in duality under a bilinear form that is continuous in each variable, and every continuous linear functional on either space is the pairing with exactly one element of the other. Let and be two such pairs. Let be continuous linear and its adjoint, the continuous linear map with .
A function is convex when its epigraph is convex in . It is proper when it never takes and is finite somewhere. A function is proper concave when is convex, never takes , and is finite somewhere. The standing hypotheses are that is lower semicontinuous proper convex on and is upper semicontinuous proper concave on . Their conjugates are
The primal problem (P) is to minimize over . The dual problem (P*) is to maximize over . For the perturbed problem (P()) is to minimize . Its value defines the perturbation function
The lower semicontinuous hull of is , where is allowed, so that . All infima and suprema are taken in .
valid except in the trivial case where the left side is and the right side is . No consistency, constraint qualification or attainment is assumed, and neither side need be finite. The exception is exactly the stated conjunction. A version assuming (P) consistent would be weaker, since an inconsistent (P), with , may still have a finite lower limit.
The paper's Lemma 2 (convexity of ) is used by the first claim. It is a milestone of the companion mission on Theorem 3 of the same paper and is not restated here.
Theorem 6 reduces every question about the dual value to a question about the primal value function near the origin. Strong duality holds exactly when is lower semicontinuous at (outside the trivial case). A duality gap is exactly a downward jump of at . The dual of (P*) obeys the same formula, which the paper uses to derive Theorem 7 on normal problems. An integer-lattice analogue appears in discrete convex analysis (Murota, Theorem 8.53, whose duality relation is already stated on Prove2Me as DiscreteConvex.ConjugacyDualityD.general_duality_relations). That statement has no topology and is not the same theorem.
The result is classical and its proof is published. As far as the platform's index shows, no machine-checked statement of it exists in the paper's generality, nor a statement of extended-real biconjugation on general paired locally convex spaces. The value of the mission is a formal proof in the paper's setting: arbitrary topologically paired spaces, extended-real-valued functions, and both the proper and the improper case of the hull. The biconjugation milestone (6.2) and the hull lemma are reusable for other perturbational duality results.
The obvious argument compares with the dual objective directly. It cannot give the theorem, because may jump at , and the dual objective does not detect the value of at a single point: the target is a lower limit, not a value. In infinite dimensions, conjugacy recovers a function only when it is lower semicontinuous and convex for a topology compatible with the pairing, so the statement depends on the full compatibility of the pairing on , not on a norm. The usual statements of biconjugation cover proper functions only, whereas here the lower limit may take both values , and both cases of the theorem must be covered. Finally, extended-real arithmetic must be tracked so that the dual objective, defined from , and , is matched in every infinite case.
Values lie in EReal. Infima and suprema are complete-lattice ⨅ and ⨆, so an empty or unbounded family gives as in the paper. The lower limit is Filter.liminf h (nhds y) over the full neighbourhood filter: a punctured limit would change the theorem. Convexity is epigraph convexity in , and properness is the paper's two-sided condition. A topological pairing is a structure holding a bilinear map, separate continuity, and existence and uniqueness of representing elements in both directions. No norm, inner product or finite dimension is assumed. The adjoint is continuous linear data satisfying the adjoint identity. The conjugates , are defined by the paper's formulas from , , so their regularity is a consequence, not a hypothesis. Properness of and excludes the form from and from . No statement is repaired relative to the page.
The dual value is the supremum of the maximand built from , and as on p. 172. Defining through (for instance as the biconjugate of at ) would make Theorem 6 true by definition and is ruled out.
A complete development needs extended-real conjugates on paired spaces, the lower semicontinuous hull and the closure of a convex epigraph, and Fenchel–Moreau for proper lower semicontinuous convex functions on a locally convex space. All of these are reusable beyond this mission. Proofs of the milestones, and lemmas toward Fenchel–Moreau in this generality, are welcome contributions.
Constrained convex programs are routinely solved by turning them into a sequence of unconstrained problems. The classical route is the ordinary Lagrangian , whose dual function is in general nonsmooth and equal to off the orthant , so maximizing it requires a constrained, nonsmooth method. In 1969 Hestenes (JOTA 4, 1969) and Powell (in Optimization, ed. Fletcher, Academic Press, 1969) proposed the method of multipliers for equality constraints, which adds a quadratic penalty to the Lagrangian. Rockafellar's paper (Math. Programming 5, 1973) gives the inequality-constrained version, the penalty Lagrangian , and shows that for convex programs its dual is a smooth, unconstrained, concave maximization problem with the same solutions and value as the ordinary dual. The method of multipliers built on this Lagrangian, now called the augmented Lagrangian method, underlies ADMM and many large-scale solvers.
Timeline. Hestenes and Powell (1969): multiplier method for equality constraints. Rockafellar (1973, this paper; and JOTA 12, 1973): the inequality-constrained penalty Lagrangian, its duality theory, and convergence of the multiplier method for convex programs. Rockafellar (Math. Oper. Res. 1, 1976): the method of multipliers identified as the proximal point algorithm applied to the dual. Bertsekas (Constrained Optimization and Lagrange Multiplier Methods, 1982): the general nonconvex theory.
This mission covers the first half of the paper: the duality theory of (§3) and the theorem that maximizing the penalty dual yields asymptotically optimal primal sequences (§4, Theorem 4.1).
Let be a nonempty convex subset of a real vector space and convex real functions on . The problem is
Multipliers range over , with Euclidean norm and inner product . With and a parameter , the penalty Lagrangian is
defined for all with no sign restriction. The dual function is , and the dual problem maximizes over ; and are the same with , and is the dual optimal value. In Lean these objects are Lr, L0, gr, g0, dualValue, and Fr is the perturbed objective if , otherwise.
A sequence in is asymptotically feasible if for every . The asymptotic optimal value (asympValue) is the infimum of over asymptotically feasible sequences, and a sequence attaining it is asymptotically minimizing (IsAsympMinimizing). A maximizing sequence for is a sequence with .
Suppose the asymptotic optimal value in (P) is finite, , is a bounded maximizing sequence for , and satisfies
Then is asymptotically minimizing for (P).
Theorem 4.1 says that any procedure that drives the smooth, unconstrained dual to its supremum, while computing -minimizers only approximately, produces an asymptotically optimal primal sequence. It needs no constraint qualification, no existence of a dual or primal optimal solution, and not even feasibility of (P): only that the asymptotic optimal value is finite. Together with Theorem 3.2 it justifies the multiplier method as a dual ascent on a concave function with Lipschitz gradient, and it is the starting point of the convergence theory of augmented Lagrangian methods.
None of these statements is formalized on Prove2Me or in Mathlib, which has Lagrangian duality only in special forms and no theory of the penalty Lagrangian or of asymptotic optimal values. The Qi–Sun augmented Lagrangian items on the platform (NonsmoothNewton.AugLagrangian.*) use the -scaled function on and concern smoothness in , not the dual function. The results of this paper are classical and proved; this mission formalizes them.
The obvious argument compares the primal iterates with a saddle point: if is a dual optimal solution and (P) is normal, approximate minimizers of are approximately optimal. Theorem 4.1 assumes neither. The function need not attain its supremum, (P) need not be normal or even feasible, and there may be no Kuhn–Tucker vector, so there is no saddle point to compare with; the only data are the dual values , the boundedness of and the tolerances . The difficulty is to obtain primal feasibility and optimality information from dual convergence alone, measured against the asymptotic optimal value rather than the infimum in (P). Every ingredient is extended-real-valued: is off the orthant, may be identically , and the asymptotic optimal value may be . Mathlib does not package this part of convex analysis (partial conjugates, envelopes of extended-real concave functions, the asymptotic duality theorem).
is a bare real vector space (AddCommGroup E, Module ℝ E) with no topology, as in the paper. The functions are total functions assumed convex on ; only their values on enter. Constraint indices are Fin m (0-based) and is a separate argument. Multipliers live in EuclideanSpace ℝ (Fin m). The standing assumption of §3 ( nonempty convex, all convex) is a hypothesis of every theorem.
Explicit choices:
EReal, so are represented and no infimum is replaced by a junk real value.EReal, equivalent to the printed difference; only is assumed.The goal must not be replaced by " and ": that is the special case of normal problems with feasible solutions. Nor may it assume a Slater point, a Kuhn–Tucker vector, or feasibility of (P), each of which makes it a special case.
A complete development needs extended-real convex analysis on (partial conjugates, Moreau envelopes of concave functions, the asymptotic duality theorem), which is reusable beyond this mission. Contributions proving any milestone, or general lemmas on Moreau envelopes of extended-real concave functions, are welcome.
In convex optimization, a dual problem supplies a bound on what a primal minimization problem can achieve. The bound can be useful even when no minimizer is known, but an equality of the primal and dual values says more: it certifies that the bound is exact. In applications, one also wants a dual variable that actually attains the bound, since that variable can act as a multiplier or a sensitivity certificate. Rockafellar's 1967 paper asks when such an attained equality follows from the behavior of the primal value under small changes to the problem Rockafellar 1967.
The paper works with locally convex spaces paired with their continuous duals, rather than limiting the question to finite-dimensional vectors or normed spaces. In this setting, ordinary finite-dimensional constraint qualifications need not describe the relevant behavior. Theorem 3 gives a criterion in terms of the perturbation function itself. It also states the corresponding criterion with the primal and dual roles reversed Rockafellar 1967, §5.
Let and be real locally convex Hausdorff spaces in topological duality, with pairing . Let and be another such pair. Each pairing represents every continuous linear functional on either member uniquely by a point of the other member. Let be continuous linear, and let its continuous adjoint satisfy .
The primal data are a lower semicontinuous proper convex function and an upper semicontinuous proper concave function . Here proper means that never takes and is finite somewhere, while never takes and is finite somewhere. Convexity means convexity of the real epigraph, and concavity means convexity of . Their conjugates are and Rockafellar 1967, §2.
The primal problem minimizes over . Its dual maximizes over . A translation changes the primal objective to , giving
The primal problem is stably set when it is consistent, meaning , and when directional rates of change of at zero cannot be arbitrarily negative in every neighborhood of zero. The instability test is made only when is finite. Consequently counts as stable, as the paper explicitly observes Rockafellar 1967, §4–5. The dual stability condition is the same definition applied to the dual's minimization form , with perturbations in .
The goal is both directions of Theorem 3, including the dual statement:
The symbols and assert that the stated value is attained. A statement equating only an infimum and a supremum would omit part of the theorem. The mission's milestones are the convexity of (Lemma 2), the equivalence between stability and a nonempty subdifferential , the criterion linking a subgradient to inequality (5.1), and weak duality (Lemma 1). Each is a claim stated in the paper's proof or as a numbered lemma Rockafellar 1967, pp. 174, 178–179.
The theorem turns a local property of the optimal-value function into an exact, attained duality statement. A dual optimum has operational meaning: its point is a continuous linear response to perturbations , expressed through . The converse says that attained exact duality already forces the same stability property. The dual half adds a symmetric criterion for attainment of the primal minimum Rockafellar 1967, Theorem 3.
The 1967 result is proved in the cited paper; this mission asks for its Lean formalization. A complete development would give reusable definitions for paired locally convex spaces, extended-real conjugates, epigraph convexity, and perturbation-based stability. The milestone statements expose the intermediate mathematical claims separately, so later formalizations can use the parts they need without importing the entire theorem.
Weak duality by itself gives only an inequality. It does not supply a dual point achieving the primal infimum, and equality of two extended-real lattice values does not establish attainment. The central issue is that a perturbation function can have a finite value at zero yet fall at arbitrarily steep rates in nearby directions; then no continuous linear support at zero need exist. Infinite primal values bring two additional cases: inconsistency when , and the paper's stable case when . The dual half requires the topology on because the translated dual problem is perturbed there Rockafellar 1967, §§4–5.
The Lean representation uses EReal for all objective and conjugate values; its complete lattice gives the paper's values for unbounded or empty extrema. Spaces are arbitrary locally convex Hausdorff real topological vector spaces equipped with a pairing that identifies each space with the continuous linear dual of the other. The adjoint is continuous linear data constrained by the pairing identity. Properness rules out endpoint arithmetic of the form in the primal and dual objectives. The conjugates are defined from and ; their regularity is not assumed separately.
Stability is encoded using the positive one-sided lower limit of directional difference quotients, which equals the paper's limit for convex . It requires consistency and excludes arbitrarily negative rates in every neighborhood. It is not defined by : that equivalence is an independent milestone. Attained extrema are represented by greatest and least elements of the ranges of the objective functions, rather than by equality of lattice values alone. The formalization includes both halves of Theorem 3 and all four listed milestones. Contributions toward general convex analysis on paired spaces and toward the extended-real endpoint cases are useful beyond this mission.
Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.
A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.
The world is a continuous-time Markov chain on a countable set with generator , , and bounded rates , . While , unit demands arrive at rate , all demand is backlogged, and orders arrive after a random lead time that is independent of the world and the demand. Costs are discounted at rate . With the unit order cost , holding rate and penalty rate , set and
where is the demand during a lead time when the world starts in . Uniformizing at a rate with and , the myopic cost is . The linear-cost model () is solved by value iteration from :
, with limits and . The myopic level , the finite-horizon levels and the optimal level are the smallest minimizers of , and , and . Throughout, (Assumption 1).
The world states carry a partial order . The chain is stochastically partial-monotone (display (14)) if for every there is a probability space carrying copies of started at and at whose paths satisfy for all almost surely. Condition 1 requires this together with nondecreasing in .
Under Condition 1, the three families of levels exist and are nondecreasing along :
Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal parameters are monotone, and instead bound them between monotone functions.
All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.
The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term , which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain is monotone for every . As printed, this is false at : for two states with , swaps the states. A complete proof cannot rely on that lemma as printed.
A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits , must be justified by Lemma 4's uniform bounds.
The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law and the world transition function are defined by uniformization at the model's rate , the paper's own device. The lead-time law is a probability measure on , and is the series of display (16). uses an infimum over integers , and , are suprema over , which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in is Monotone/Antitone with respect to . Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on .
Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.
Lemma 7 is not included because it is false as printed. A guarded version (for instance with ) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on . Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.
Processors in a distributed system may hold separate readings of a sensor, clock, or diagnostic result while some processors give misleading reports. The aim of interactive consistency is for every functioning processor to compute the same vector of reported values and to put each functioning processor's actual private value in its corresponding position. A shared vector can then be used for a common decision. Pease, Shostak, and Lamport formulated this problem for isolated processors communicating by two-party messages; their paper discusses clock synchronization, input stabilization, and diagnostic tests as concrete applications Pease–Shostak–Lamport 1980.
In the paper's oral-message model, faulty processors can invent reports about values they received from others. The other two missions in this series formalize the recursive majority procedure for and the matching impossibility result below that bound. Section 5 changes the communication assumption: a faulty processor may refuse to pass on a received value but cannot pass on an altered value as if it came from its original sender. Under that assumption, the authors give a procedure for every , including configurations outside the oral-message threshold Pease–Shostak–Lamport 1980, §§3–5.
Let be a finite set of processors and a type of private values. Each processor has a value . A scenario records the values reported along chains of processors. A string is read from receiver to originator: receives a report ultimately attributed to . A recorded value may be NIL, meaning that no authenticated value is available. The view available to receiver is its -scenario, the restriction ; it contains no report that begins with a different receiver.
Choose a set of nonfaulty processors. At most processors may be faulty, expressed as . An authenticated scenario consistent with obeys two conditions whenever the displayed strings are in the -level scenario. If and , the report made by nonfaulty relay is truthful: . For any prefix , a chain passing through nonfaulty carries either the value at or NIL: . The second condition allows omission by later relays while excluding a changed value falsely attributed to Pease–Shostak–Lamport 1980, p. 233.
For each receiver and originator , the procedure forms , the set of all non-NIL values in 's view on strings . The intermediate string has at most distinct letters, all in . Receiver records the sole value in when this set is a singleton; otherwise it records NIL. The resulting entries, one for each , form 's proposed consistency vector Pease–Shostak–Lamport 1980, p. 233.
The first milestone covers a nonfaulty originator : every nonfaulty receiver sees exactly its true value. The second covers a faulty originator: the set of non-NIL values seen by one nonfaulty receiver is contained in the set seen by another. The same statement with the receivers exchanged gives equality of their sets.
The goal is the procedure's full interactive-consistency guarantee, for every choice of and every authenticated scenario satisfying the conditions above:
Here is the optional value recorded by processor for processor . Both clauses matter: agreement alone could be achieved by always recording NIL, while correct nonfaulty entries alone would leave faulty entries inconsistent.
The result identifies an exact communication assumption under which the paper's oral-message bound no longer governs the procedure. Even if a faulty originator gives conflicting values, nonfaulty receivers finish with identical entries for that originator; if an originator is nonfaulty, they retain its actual value. The paper describes authenticators as a practical approximation to the assumption, but the guarantee here is a mathematical statement about scenarios satisfying its two conditions, not a probability claim about a cryptographic implementation Pease–Shostak–Lamport 1980, §5.
Formalizing this result supplies precise interfaces for authenticated scenario consistency, local views, the set , and the recording rule. The paper proves the result on pp. 233–234; this mission asks for a machine-checked proof of those statements in Lean. The scenario and local-view definitions can support later formalizations of message-passing protocols with truthful or omissible relays. Contributions that establish the two source milestones and the final guarantee, or develop reusable list and finite-set facts needed by them, are within scope.
The case of a faulty originator is the central difficulty. Its private value has no required relationship to what different nonfaulty receivers hear, so simply asserting that every receiver obtains the same direct report is unjustified. A faulty relay may also omit a report, which makes equality of raw scenario entries too strong. The target must compare sets of non-NIL values obtained along admissible relay chains. At the longest allowed chain, the length bound prevents adding another relay, and the number of faulty processors is needed to establish that an admissible nonfaulty relay occurs in the chain Pease–Shostak–Lamport 1980, p. 234.
Lean represents processors by a finite set P : Finset α, values by a type V, strings by List α, and NIL by none : Option V. A scenario is a total function from strings to optional values. Only strings over of length at most are constrained by authenticated consistency, matching the -level scenario that the procedure reads. A single-letter string has a non-NIL private value for every processor in . Conditions (i) and (ii) constrain nonfaulty relays only; condition (ii) allows either the original value or NIL for every prefix over , including an empty prefix.
The procedure is applied only to 's view , so it has no access to the full scenario or to . Its intermediate strings are repetition-free, exclude both and , and have length at most . The set contains values in , not NIL; an empty set and a set with multiple values both cause a NIL record. The formal theorem retains the printed condition, although it is not needed in the proof of the stated set relationships. It also covers , , and empty or singleton processor sets when their quantified conditions apply. These conventions rule out an always-NIL decision rule and the trivial rule that reads from outside the receiver's view.
The cryptographic maps , their message encodings, and the paper's assertion that practical authenticators can meet the assumption with arbitrarily high probability are outside scope. The formal result assumes the two exact authenticated-scenario conditions. A complete development needs finite-set cardinality and list facts, especially about distinct relay strings and bounded concatenation; these facts can be reused for other authenticated relay models.
A fault-tolerant system built from several processors must let its working processors act on the same data, even though some processors may have failed in ways nobody can predict: a failed processor may stop relaying information, relay something it invented, or tell different processors different things. Pease, Shostak and Lamport (J. ACM 27 (1980) 228–234) isolated the core question in the setting of the SIFT aircraft-control computer: each of processors holds a private value, at most processors are faulty, and processors communicate only by two-party messages. Can the nonfaulty processors each compute a vector of values, one entry per processor, such that all nonfaulty processors compute the same vector and the entry of each nonfaulty processor is its true private value? This requirement is called interactive consistency.
The paper answers with a sharp threshold. Interactive consistency can be achieved when (Section 3), and it cannot be achieved when , however many rounds of message exchange are allowed (Section 4). With unforgeable signatures it can be achieved for every (Section 5). The impossibility half is the origin of the "" bound that appears throughout Byzantine fault tolerance, popularised two years later as the Byzantine Generals Problem (Lamport, Shostak, Pease, ACM TOPLAS 4 (1982)). This mission is the impossibility theorem.
Timeline:
Let be a finite set of processors and a set of values. Write for the set of strings over (the empty string included) and for the nonempty strings. A string is read as a chain of reports: was told by that was told by that 's private value is the recorded value.
A scenario is a map . The value is processor 's private value, and is the value received for the chain . For , the -scenario is the restriction of to the strings beginning with : everything ever learns.
For a set of nonfaulty processors, is consistent with if
that is, every nonfaulty processor reports truthfully what it knows or hears. Faulty processors are unconstrained.
A decision family assigns to each a map that takes a -scenario and a processor and returns a value : the entry computes for . The family assures interactive consistency for faults if for every with and every scenario consistent with ,
In the Lean development these are InteractiveConsistency.Impossibility.ConsistentWith P N σ and AssuresIC P m F, with restrict σ p the -scenario.
If and
then no family assures interactive consistency for faults. Since scenarios are defined on strings of every length, no bound on the number of rounds is assumed.
The theorem shows that the algorithm of Section 3 is optimal in its fault tolerance: with oral messages, processors are not only sufficient but necessary. Every later lower bound for Byzantine agreement, Byzantine broadcast and approximate agreement with unauthenticated messages rests on this bound or a variant of its argument, and it is the reason replicated state machines tolerating Byzantine faults use replicas. It also explains why Section 5 needs authentication: the argument depends on faulty processors being able to relay fabricated values.
The result has been proved since 1980; what is open here is its formalization. Nothing on Prove2Me models message-passing agreement, and this mission states the theorem in the paper's own model: scenarios on unbounded strings and decision functions of a single -scenario. The mission produces a reusable vocabulary (scenarios, consistency, interactive consistency) and the explicit three-scenario construction.
The obvious attempt is to argue round by round about what a processor can know after rounds; with unboundedly many rounds this never terminates in a contradiction. The paper's argument instead needs three entire scenarios, each a legitimate behaviour for a different set of faulty processors, that two processors cannot tell apart from their own views. Writing these scenarios down so that consistency holds on every string while the indistinguishability survives on every string is the delicate part: the faulty set of each scenario must relay exactly the values that keep the other scenario's view intact, and one of the defining equations () looks like a misprint but is what the argument requires. The counting step is elementary but carries the hypothesis that the printed theorem leaves implicit.
Processors are a Finset P in a type with decidable equality; strings are lists read left to right ( is the head of the list); a scenario is a total function List α → V whose values on the empty list and on lists with a letter outside carry no meaning: every condition quantifies only over strings whose letters lie in . Decision functions have type α → (List α → V) → α → V and are applied only to the -scenario fun w => σ (p :: w), never to ; giving the whole scenario would make the problem trivial (output ). Consistency with constrains only relays by members of , and includes the empty . The quorum is written , which avoids truncated subtraction on . is the existence of two distinct values.
Explicit readings of the page:
A complete development needs only finite sets and lists from Mathlib. The vocabulary of p. 232 is shared with the other two missions of this series, Reaching Agreement in the Presence of Faults 1 (the algorithm for ) and 3 (authenticated messages, ), each of which defines it in its own namespace. Proofs of the milestones and of the goal are welcome, as is a proof of the goal by a different route.
Section 4 of Herbert Robbins's 1952 address Some aspects of the sequential design of experiments (Bull. Amer. Math. Soc. 58, 527–535, doi:10.1090/S0002-9904-1952-09620-8) isolates a problem that every user of significance tests meets: if the sample size is not fixed in advance, an experimenter can keep sampling until the test rejects. Robbins shows that a fixed-sample test then loses all control of its error probability, and he proposes the compromise of allowing the sample size to range over a window , with an explicit bound on the resulting error.
The question is still current. "Optional stopping" and "peeking" at accumulating data are a standard concern in clinical trials and online A/B testing, and the modern theory of always-valid inference and confidence sequences (for example Howard, Ramdas, McAuliffe and Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), arXiv:1810.08240) answers exactly the question Robbins raises: how large is the probability that a running statistic crosses a boundary at some time in a range. The earlier treatment Robbins cites is Feller's 1940 discussion of the statistics of ESP experiments.
Let be independent real random variables on a probability space , each normal with mean and variance . This is the null hypothesis for observations that are normal with unknown mean and unit variance; the alternative is . Write
The fixed-sample test of size rejects if and only if
for a real constant . (In this mission always denotes this test constant; in Section 2 of the paper the same letter is the mean of a coin.) The standard normal distribution function is
For integers the window probability is
and . In Lean these are Phi, S X n ω = ∑ i ∈ Finset.range n, X i ω and g P X n₁ n₂ α, in the namespace RobbinsSeqDesign.OptionalStopping.
For integers and every real , with ,
The inequality is strict, as printed, and holds for every real , not only the large values of practical interest.
For every and real ,
For every real , with probability the inequality holds for infinitely many .
The results. (22) says that the fixed-sample test has error probability whatever is. The infinitely-often statement says that this guarantee is void under unrestricted optional stopping: sampling until (21) holds rejects a true with probability one, however large is. The goal (25) quantifies the compromise: if the stopping time is confined to , the error probability is at most the fixed-sample error divided by , where depends only on the window's ratio. For large and moderate this keeps the error of the same order as the fixed-sample error; Robbins notes that it is useful when is not too large and that sharper inequalities can be devised.
Formalizing it. The three statements are classical and their proofs are short on paper, but none is machine-checked for Gaussian partial sums. The goal needs stopping-time machinery for discrete-time Gaussian random walks; the infinitely-often statement is a consequence of the lower half of the law of the iterated logarithm, which Mathlib does not contain. On the platform, DurrettProbability.brownian_limsup_sqrt (proved) gives for Brownian motion, a different process, and AzumaWeightedSums.IteratedLog.theorem2_limsup_le_one gives an upper iterated-logarithm bound for weighted sums, the opposite direction; neither states any of the targets here, but both are related infrastructure.
The goal is a maximal inequality over a window of times. The obvious argument, a union bound over , gives , which grows with the window length instead of depending on alone, and exceeds for long windows. The events for different are strongly dependent, and the boundary is curved, so the bound has to account for when, inside the window, the boundary is first crossed; this requires stopping-time arguments for a discrete-time walk that are not yet available for Gaussian random walks in Mathlib. The strictness of the inequality also has to be tracked through the argument. The infinitely-often statement cannot be obtained from the central limit theorem alone, which gives only ; upgrading this to probability one needs a zero–one law or the law of the iterated logarithm.
The observations are X : ℕ → Ω → ℝ on a probability space (Ω, P) with [IsProbabilityMeasure P], iIndepFun X P and ∀ i, HasLaw (X i) (gaussianReal 0 1) P; the paper's is X (i - 1). The explicit readings committed to are:
cdf (gaussianReal 0 1)).P.real of the event; (22) is stated for .∀ᵐ ω ∂P, ∃ᶠ n in atTop, α * √n < S X n ω, for every real .A trivializing formalization is ruled out: is the probability of the union over the whole window (not the event at alone), is the fixed standard normal distribution function (not an arbitrary monotone function), and the parameter range excludes , where Lean's convention would replace the right side by .
A complete development needs the law of a sum of independent Gaussians, the strong Markov property of a Gaussian random walk at a stopping time (or an equivalent first-passage decomposition), and, for the infinitely-often milestone, either the lower law of the iterated logarithm for Gaussian walks or the Hewitt–Savage/Kolmogorov zero–one law combined with the central limit theorem. These pieces are reusable well beyond this mission; contributions of any of them, as separate lemmas, are welcome.
A linear program subject to , assumes that the constraint matrix is known exactly. In practice the columns of — the activity vectors, describing how much of each resource one unit of activity consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.
The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.
Fix integers . Vectors in are compared componentwise. For a set and a scalar , , and the sum of sets is Minkowski addition, .
Let be nonempty convex activity sets and a nonempty convex resource set. Problem (I) is
and denotes its set of feasible . Problem (Ib) is the special case for a right-hand side .
The support functional of a set is , a value in . With the -th unit vector, the auxiliary matrix is the matrix with entries
defined when all of these are finite, and LP is the linear program subject to , . Finally is the set of matrices whose -th column lies in .
In the application, the activity sets are Euclidean balls around nominal columns of a matrix , with radii .
Assume every is nonempty and convex and for all . Then
and for every objective , the optimal solutions of (Ib) and of LP coincide.
The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in , of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column is inflated by the full radius , which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.
The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.
The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every " to uses that the supremum of a sum of independent terms is the sum of suprema, which needs every nonempty and the scalars nonnegative; with an empty activity set the Minkowski sum is empty and every becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.
Fin m → ℝ and Fin n → ℝ, with indices in place of ; the order on vectors is componentwise.(∑ j, x j • K j) ⊆ R (pointwise set operations) together with . It is not defined as "for every choice ", which would make milestones 1 and 5 trivial, and is constructed from the , not an arbitrary matrix dominating , which would make the goal trivial.EReal. The entries of are its real conversions, so every statement mentioning assumes and , the paper's standing assumptions (pp. 1154–1156). Convexity of the is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of ).EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii .FenchelRobust.Counterpart.supportFun with the same body.EReal statement equating the optimal values, are welcome.An inventory controller must decide how much to order while demand changes with an observed external condition. A single demand rate misses that dependence: the same inventory position can justify different orders when the condition changes. Song and Zipkin's 1993 study asks whether a simple policy remains optimal when the condition follows a continuous-time Markov chain and orders arrive after a random lead time. The answer for linear ordering costs is a world-dependent basestock policy: each world state has one target inventory position, and an order raises the current position to that target when it lies below it.
The policy claim concerns an infinite horizon. It is stronger than showing that a particular collection of target levels performs well or that such a policy minimizes a one-step cost. Theorem 2 of Song and Zipkin identifies the targets through a limiting value function and establishes optimality for the full discounted problem. This mission formalizes that theorem and the finite-stage results the authors use to state its limit precisely.
The world state belongs to a nonempty countable set . The world evolves according to a conservative continuous-time Markov generator , with exit rate . When the world is in state , customers demand individual units at rate . The exit rates and demand rates are bounded above. Inventory is fully backlogged: a negative inventory level records unmet demand. The controller observes the world state and the inventory position , which includes outstanding orders, and chooses an order-up-to position .
An order has actual unit cost and may have fixed cost . This mission takes the linear-cost case, so the discounted fixed cost is . The lead time is a finite nonnegative random time, independent of the world and demand process. Its Laplace transform discounts the ordering costs to , where is the discount rate. Holding one unit costs per unit time; backlogging one unit costs .
Write for the number of demands during the lead time conditional on initial world state . The cost rate of an inventory level is for and otherwise. The lead-time cost and myopic cost are
where is a uniformization rate at least , , and . The paper's Assumption 1, , applies to the later results. It ensures the myopic cost has finite nonnegative minimizers. The smallest such minimizer in world state is , and .
With zero fixed cost and zero terminal cost, the -stage transformed cost minimizes the auxiliary cost over . Each combines the myopic cost with the expected discounted continuation after a demand, a world-state jump, or a self-loop. Let and denote their pointwise limits. A basestock policy orders to in state ; it never cancels an outstanding order.
The main target is the finite, smallest global minimizer of for each world state, with the inequalities of Theorem 2(c):
Here is the limit of the smallest finite-stage minimizers . Theorem 2(e) then asserts that has minimum infinite-horizon expected discounted cost from every state among all feasible policies. The milestone list states Lemmas 1, 2 and 4, Corollaries 1 and 2, all parts of Theorem 1 as identified by the paper's internal references, and the limit and optimality-equation clauses of Theorem 2. Together they fix the finite-stage and limiting objects used by the goal.
The theorem reduces a decision at every integer inventory position to one integer target for each observed world state. It gives an exact policy structure for a model with a changing demand rate and random lead time, rather than an approximation derived from a constant-demand model. The limiting inequalities also locate an optimal target relative to the myopic target and the finite-stage targets, giving a mathematically specified range for policy computation. These claims are the linear-cost part of Song and Zipkin's analysis; the paper proves the result but supplies no Lean proof.
Formalization will leave reusable definitions for countable-state uniformization with a demand counter, integer convexity of inventory cost functions, and discounted costs of history-dependent policies. The mission's theorem statements compile as open goals. The remaining work is to verify the analytic properties of the lead-time demand law, the finite-stage inequalities, convergence, and the infinite-horizon policy comparison. The fixed-order-cost and monotone-world-state results of the paper are separate missions.
The world can have countably many states, so a continuation value includes a series over possible world jumps. The stage cost grows with inventory position, so a bounded-cost finite-state dynamic-programming theorem does not directly cover the model. The minimization is over an unbounded set of integers, and the minimizers themselves change with the stage number. Convexity of a one-stage cost alone does not establish that the limiting policy beats policies that use the entire observation history. These are the specific gaps the paper's bound, ordered-difference, and limit results address.
World states are a nonempty countable Lean type, inventory positions and order-up-to levels are integers, and costs are real until policy evaluation. The lead-time law is a probability measure on finite nonnegative real times, independent of world and demand. The demand-count law is defined by exact Poisson uniformization at rate , with demand, world-jump, and self-loop branches. The infinite-horizon policy cost uses extended nonnegative reals and a supremum of finite-horizon costs, so it can express an infinite expected cost without a default real value. Policies may depend on all past observed states; the goal compares its basestock policy against every feasible deterministic policy in this class. Randomized policies are omitted because they cannot improve expected nonnegative costs on this countable state space.
Assumption 1 is attached only to the results that use it. The linear-cost recursion has and . Integer convexity means nondecreasing forward differences. Smallest minimizers and the minimum across world states are asserted to exist; neither is encoded by an integer infimum that returns a default on an empty or unbounded set. The goal requires an actual optimal policy cost comparison from every state, so solving the limiting optimality equation only within basestock policies cannot close it. Contributions to the lead-time mixture, integer convexity, boundedness of the real series and infima, and unrestricted policy comparison all fit this scope.
A fault-tolerant system often replicates a computation on several processors and needs the nonfaulty ones to act on the same data, even though some processors may fail in arbitrary ways: send wrong values, send different values to different recipients, or lie about what they were told. Pease, Shostak and Lamport posed the question in 1980, motivated by the SIFT fault-tolerant aircraft-control computer under development at SRI (Wensley et al. 1978), where it arises in clock synchronization among other places: processors, at most of them faulty, communicate by two-party messages whose sender is always identifiable, and each holds a private value. Can the nonfaulty processors all compute the same vector of values, one entry per processor, whose entry for every nonfaulty processor is that processor's true value? The paper (J. ACM 27 (1980) 228–234) calls this interactive consistency and settles it: possible if and only if when messages can be forged in relay, and possible for every when they cannot. The same problem, under the name Byzantine generals, became the standard model of arbitrary ("Byzantine") failures in distributed computing (Lamport, Shostak & Pease 1982); the bound underlies the quorum sizes of later replication protocols.
This mission covers the positive half of the paper's characterization: Section 3's recursive procedure, which achieves interactive consistency with processors in rounds of message exchange.
Let be a finite set of processors and a set of values. A string over a set is a finite sequence of elements of , repetitions allowed. For a -level scenario is a map from the nonempty strings over of length at most to . The value is 's private value ; for , is the value tells that told … that told is 's private value. A -level scenario records the outcome of rounds of message exchange.
Faults are modeled by a set of nonfaulty processors, unknown to the processors. Nonfaulty processors relay truthfully, so is consistent with when
Faulty processors are otherwise unconstrained. A processor sees only its view , the restriction of to strings beginning with .
The procedure (p. 230). Processor computes the entry for processor as follows, with and the current processor count and fault bound:
In Lean this is InteractiveConsistency.OralAlgorithm.record m P τ q with τ = fun w => σ (p :: w), values in Option V with none for NIL.
For , for every with and every -level scenario consistent with ,
This is procedure_assures_ic. It is the paper's claim about this procedure, not an existence statement.
The theorem is the upper bound in the tight characterization of when interactive consistency is achievable with unauthenticated messages; the matching impossibility (the paper's Section 4 THEOREM) shows that no procedure, with any number of rounds, does better. The procedure is the ancestor of the "oral messages" algorithm of the Byzantine generals paper, and its quorum arithmetic (, intersections of two quorums containing a nonfaulty member) recurs throughout Byzantine fault-tolerant replication.
The result is proved in the paper, in a half-page induction. What this mission adds is a machine-checked proof against an explicit model of scenarios, views and consistency with a bounded number of rounds. Machine-checked proofs exist for the related algorithm of the later Byzantine generals paper in other proof systems; this procedure, with its quorum-based step (1), has to our knowledge not been formalized in Lean, and nothing on message-passing agreement exists on this platform.
Each step of the paper's proof is short, but the bookkeeping is where an argument breaks. The recursion changes three things at once: the processor set loses , the fault bound drops by one, and the scenario becomes of one level less. The induction hypothesis must therefore be stated for every finite processor set and every scenario, and applied to a subscenario whose consistency is inherited only for strings of the right length. The mixed case, where one nonfaulty processor exits at step (1) and another recurses, is the delicate one: the two processors' computations take different branches, and since is faulty nothing forces either value to be 's private value. The thresholds are exact: in step (1) and agreeing entries in step (2), both in the current and ; off-by-one changes in either break the case analysis. Finally, step (2)'s majority value must be shown unique, so that two processors with the same vector record the same value.
Processors form a Finset α with decidable equality; strings are List α, read left to right (the receiver first, the originator last), so is σ (p :: (w ++ [q])). A scenario is a total function List α → V; consistency with (ConsistentUpTo P N (m + 1) σ) constrains it only on strings over of length at most , the domain of an -level scenario and all the procedure reads. The procedure receives only the view fun w => σ (p :: w), never or . The fault hypothesis is P.card ≤ N.card + m; is included.
Explicit readings of the paper's prose: "size " is P.card + m < 2 * Q.card; is natural-number division; "strings over of length " includes the empty string and allows repetitions; the step-(2) vector is indexed by P.erase q and includes 's own entry; the recorded value in step (1) is (the empty string forces it); when several values reach the step-(2) threshold one is chosen deterministically from the vector (under the goal's hypotheses at most one does); for a failing step (1) records NIL (never reached under the hypotheses). Two printed slips are corrected in the Lean: "records and " (for "for ") and "" (for ).
Trivializing formalizations are ruled out: the procedure never sees itself (with it, recording would be trivial), consistency constrains only relays by nonfaulty processors, and ranges over every subset of size at least .
The development needs only finite sets and lists; no library beyond Mathlib is required. The quorum-intersection lemmas and the subscenario construction are reusable for other oral-message protocols. Contributions welcome: proofs of the four milestones, the goal by induction on , and a computable version of the procedure for concrete instances. This is mission 1 of a series of three on this paper; mission 2 formalizes the impossibility THEOREM for (Section 4), and mission 3 the authenticated-message procedure for every (Section 5).
The classical implicit-function theorem solves an equation for as a function of a parameter near a known solution , provided is (strongly) Fréchet differentiable in with an invertible partial derivative. Much of optimization does not meet that hypothesis. Optimality conditions of constrained problems, complementarity problems and variational inequalities are routinely rewritten as equations involving the projection onto a convex set, the componentwise , or the normal map of a polyhedron. These maps are Lipschitzian and piecewise smooth, but not differentiable. Sensitivity analysis asks whether the solution of such a system moves Lipschitz-continuously with the problem data, and the classical theorem cannot answer it.
Stephen M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, pp. 292–309, gives a theorem with the same shape as the classical one, in which differentiability is replaced by strong approximation by a function whose inverse is Lipschitzian. The paper's §4 applies it to parametric variational inequalities over polyhedral sets through the normal map.
Timeline. Robinson's Strongly regular generalized equations (Math. Oper. Res. 5, 1980) proved an implicit-function theorem for generalized equations under a linearization hypothesis called strong regularity. The 1991 paper reformulates that idea for single-valued nonsmooth equations: the approximating function need not be linear. Lemma 3.1 extends the Banach perturbation lemma for linear operators (Kantorovich–Akilov, Functional Analysis, Th. 4(2.V)) to Lipschitzian functions; after acceptance, A. Ioffe pointed the author to closely related results of Dmitruk, Milyutin and Osmolovskii (Lyusternik's theorem and the theory of extrema, Russian Math. Surveys, 1980, Theorems 1.2, 1.3), credited in the paper's footnote.
Let , , be real normed linear spaces, with complete. Fix , , a neighborhood of and a neighborhood of . Let map to , with , and let map to , with . denotes the closed ball of radius about .
Expansion modulus. For a map between metric spaces and a set ,
If , then is one-to-one on and its inverse is Lipschitzian with modulus . In Lean the mission works with lower bounds: ExpansionAtLeast f S d says on , i.e. .
Strong approximation (Definition 2.4). strongly approximates in at , written (Lean: StronglyApproxInX f F x₀ y₀), if for each there are neighborhoods of and of with
When is the partial derivative map this is strong partial Fréchet differentiability; in general may be piecewise linear or any map with a Lipschitzian inverse.
Assume (a) at ; (b) for each , is Lipschitzian on with modulus ; (c) is a neighborhood of in ; (d) . Then for each there are neighborhoods of , of and a function with
Every strictly above is claimed; is not.
where .
The result. Theorem 3.2 yields existence, local uniqueness and Lipschitz dependence of solutions of parametrized nonsmooth equations, with an explicit Lipschitz modulus arbitrarily close to . In the paper it underlies Theorem 3.3 and Corollary 3.4 (approximation and B-differentiation of the implicit function) and the sensitivity results of §4 for parametric variational inequalities over polyhedral convex sets. The same template, an equation approximated by a map with Lipschitzian inverse, is the basis of later strong-regularity and semismooth-Newton analyses in nonlinear programming and complementarity.
Formalizing it. The theorem is proved in the paper; it has not been machine-checked. The platform has the smooth implicit-function theorem (FamousTheorems.implicit_function_theorem, Rudin.ch09_implicit_function) and Mathlib has the contraction mapping principle, but there is no Lipschitz-inverse perturbation result and no notion of strong approximation. The mission produces both, together with the formal Theorem 3.2 that a follow-on mission (Theorem 3.3, Corollary 3.4, §4) would reference.
The obvious approach, differentiate and invert, is unavailable: need not have a derivative anywhere near , so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of onto a ball uniformly in from information about alone. Injectivity transfers directly from through the small Lipschitz modulus of ; surjectivity does not, because carries no information about beyond the small Lipschitz modulus of the difference, and the domain ball, the image ball and the parameter neighborhood must be chosen once for all . Completeness of is essential (the paper stresses this on p. 306) and is not available for and .
All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:
[CompleteSpace X]); , are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.ExpansionAtLeast f S d in place of "", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be on sets with fewer than two points.F : X → Y → Z and ; hypotheses constrain them on only, and the conclusions keep the implicit function inside the domain: , , . This makes explicit what the paper leaves implicit (its is only defined on ). Likewise , used implicitly in the paper's proof, is a conclusion of milestone 2.Metric.closedBall), radii written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at ), in which may shrink to , is existential, or uniqueness is asserted outside , would be a different and trivial or false statement; the statements here rule these out.
Needed infrastructure: the contraction mapping principle on a closed subset of a complete space (Mathlib's ContractingWith), Lipschitz estimates on sets, and the two definitions of this mission. Lemma 3.1 is reusable for any Lipschitz-perturbation argument. Proofs of either milestone, or a direct proof of the goal, are welcome.
A connected network survives the failure of any single link exactly when it has no bridge, but a stronger and more useful property is to carry several edge-disjoint spanning trees: each tree can broadcast to every node on its own, so such trees give independent routing or broadcast structures, and the network stays connected after any link failures. The question of when a graph contains edge-disjoint spanning trees was answered in 1961, simultaneously and independently, by W. T. Tutte (On the problem of decomposing a graph into n connected factors) and C. St.J. A. Nash-Williams (Edge-disjoint spanning trees of finite graphs). The answer is a min-max condition over vertex partitions, now called the Tutte–Nash-Williams tree-packing theorem. It is a standard result in combinatorial optimization and the graphic case of Edmonds's matroid base-packing theorem (1965).
Timeline:
A graph here is a finite unoriented multigraph in which every edge joins two distinct vertices; two vertices may be joined by several edges. Write for its vertex set and for its edge set. A tree on a non-empty vertex set is an edge set , all of whose edges have both ends in , containing no cycle (two parallel edges count as a cycle), such that any two vertices of are joined by a path of -edges. A spanning tree of is a tree on all of using edges of . Spanning trees are edge-disjoint if no two share an edge.
A partition of is a set of non-empty, pairwise disjoint subsets of whose union is ; is the number of its members. The crossing edges are the edges whose two ends lie in different members of , counted with multiplicity. Throughout, is a fixed positive integer. For , is the set of edges with both ends in , , and
The theorem gives an exact, checkable certificate in both directions: a family of trees certifies the packing, and a single partition violating (1) certifies that no packing exists. Corollaries include that every -edge-connected graph has edge-disjoint spanning trees, and that the maximum number of edge-disjoint spanning trees (the strength-type parameter used in network reliability and in Nagamochi–Ibaraki style connectivity algorithms) is the minimum of over partitions with . The partition condition is also the prototype of the rank condition in matroid base packing.
The result itself is classical and fully proved. What this mission adds is a machine-checked version in a multigraph setting. Mathlib has trees and spanning trees for simple graphs (SimpleGraph.IsTree, SimpleGraph.Connected.exists_isTree_le), but not edge-disjoint tree packing, and its simple graphs cannot express the parallel edges that the theorem and its proof need. Related items on the platform include the multigraph layer NagamochiIbaraki.EdgeConn.Multigraph (reused here), the Keller–Trotter spanning-forest count for simple graphs, and Edmonds's matroid partition theorem with Nash-Williams's covering corollary. Covering and packing are different statements, so none of these yields Theorem 1 directly. Formalizing Tutte's alternative proof, or deriving Theorem 1 from a formalized matroid union theorem, would also be welcome.
Necessity is a counting argument. The difficulty lies in sufficiency. The obvious induction deletes an edge or contracts a set of vertices, but deleting an edge can destroy (1), and contracting changes the vertex set, so neither reduction preserves the hypothesis on its own. The hardest case is a graph in which only the partition into singletons is critical. There a vertex of degree less than has to be removed while (1) is preserved on the remaining graph, and the trees found there have to be converted back into trees of the original graph. Both steps need careful bookkeeping of edges incident with that vertex. A simple-graph development cannot carry the argument, because the edges that the reduction adds among the neighbours of the removed vertex may be parallel to existing ones.
V, an edge type E (both finite, in Type), and ends : E → Sym2 V, the published encoding of NagamochiIbaraki.EdgeConn. Loops are excluded by the hypothesis ∀ e, ¬ (ends e).IsDiag. Parallel edges are allowed, and simplicity is never assumed. A subgraph is a pair (W : Finset V, F : Finset E).IsForest: every edge is a bridge) and connected. is Lemma 1, not part of the definition. " edge-disjoint spanning trees" is a family Fin k → Finset E of pairwise disjoint spanning trees.Finpartition (Finset.univ : Finset V). (1) is required for every partition, including the one-part partition and the singletons. All counts involving subtraction (, (1), criticality, ) are in .E ⊕ Fin s, so the added edges always exist; none of them may be a loop. A fusion uses a given fresh edge ρ : E in an ambient edge type, and a sequence of fusions is a list, each valid on the graph produced by the later ones ( applies first). In (†) and Lemma 4, "is a tree" means "is a spanning tree of ", since the vertex set is all of . Lemma 6 carries the paper's inductive hypothesis as an explicit hypothesis: Theorem 1 (admissible implies trees) for all loopless multigraphs with smaller .An arbitrator choosing an outcome for several people can ask them about their preferences, but the answer to that question may affect the outcome. A person who expects to gain from a false report may give one. Roger Myerson's 1979 paper puts this incentive problem inside a bargaining model: the arbitrator may randomize over collective choices, and an allocation is considered feasible only if some mechanism makes truthful reporting an equilibrium. The paper then applies a weighted Nash bargaining criterion to the resulting set of feasible interim payoffs. The mission formalizes the existence and uniqueness result for that criterion, along with the finite Bayesian model on which it depends.
The issue matters whenever an agreement is selected using information known privately to its participants. If the arbitrator evaluates a payoff vector that can arise only when somebody has a reason to lie, that vector cannot serve as a credible bargaining alternative under the model's own behavior assumption. Myerson's feasible set keeps the behavioral constraint visible when the group compares agreements. This mission addresses the paper's Theorems 1 and 3 and the claims between them that establish the relevant sets and their reference point.
Let be a nonempty finite set of players. Player has a nonempty finite type set , and the group has a nonempty finite set of possible choices. A type profile is . The utility is player 's payoff when choice occurs and is the true profile. A nonnegative function on type profiles, summing to one, is the common prior. Write for the probability that player has type , and for the posterior probability of conditional on that type. Every is positive, so the conditional probabilities are defined.
A choice mechanism asks each player for a response and assigns a probability to each choice at each response profile . For the direct mechanisms used here, the response set of player is : a response is a claimed type. The probabilities are nonnegative and sum to one for each response profile. If a player whose true type is instead reports , while the others report truthfully, the player's conditional expected utility is . The posterior weights true profiles; the mechanism sees the profile with only coordinate replaced by ; and utility is evaluated at the true profile .
The mechanism is Bayesian incentive-compatible when for every player and pair of types. Its interim payoff vector has one coordinate for every player-type pair. The set contains the vectors attained by all direct choice mechanisms; contains those attained by Bayesian incentive-compatible direct choice mechanisms. Theorem 1 says is nonempty, convex, compact, and contained in . The nonemptiness claim includes the mechanism that selects each choice with probability , independent of all reports.
Fix a conflict outcome : the choice that occurs if bargaining fails. Its conflict payoff vector gives each player type the conditional expected utility from that fixed choice. A constant mechanism selects regardless of reports. It is incentive-compatible and generates , so . The individually rational incentive-feasible set is
For , the generalized Nash product of equation (18) is
A bargaining solution is a vector in that maximizes over that set. Myerson's Theorem 3, the goal of this mission, says that if the constant conflict mechanism is not incentive-efficient—that is, an incentive-compatible mechanism strictly improves every player-type payoff over it—then exactly one such vector exists:
The milestones follow the paper's claims: the uniform mechanism is incentive-compatible; has the four properties in Theorem 1; the conflict vector belongs to ; every Nash-product maximizer strictly improves each conflict payoff when such improvement is feasible; and every implementing mechanism is incentive-efficient. The final claim concerns a mechanism that realizes the maximizing vector. It does not assert uniqueness of that mechanism.
Theorem 1 supplies a feasible set that respects truthful reporting. Theorem 3 selects a unique interim payoff vector from that set after a conflict outcome is specified. It thereby gives a well-defined allocation criterion for the paper's finite Bayesian collective choice problems. Myerson also observes that several mechanisms may implement the same solution. The allocation, rather than a unique mechanism, is the object selected by the theorem.
The result was proved in the 1979 paper. The work here is a machine-checked statement and, for solvers, a proof of that known result and its supporting claims in Lean. The mission's statements are open proof targets; the source paper's proof is not claimed to have been formalized already. A related platform item on Nash's two-player axiomatic characterization concerns a solution function on compact convex subsets of . It is a distinct result and supplies neither this paper's Bayesian model nor Theorem 3.
The set of all real-valued functions on choices and reports is much larger than the set of mechanisms: probabilities must be nonnegative and sum to one at every report profile. Bayesian incentive compatibility adds inequalities involving the true and reported type in different positions. Theorem 1 requires these constraints to give the compact, convex set of attainable interim payoffs, rather than merely a formal collection of payoff functions.
The Nash product also has a boundary: an individually rational vector may match the conflict payoff in one coordinate, making its product zero. Theorem 3's hypothesis has to rule out a zero maximum before uniqueness of an interior maximum can be concluded. The weights matter in that uniqueness statement, and the result ranges over all player-type coordinates, not only one aggregate payoff per player. Restricting the maximization to an arbitrary small subset, fixing two players, or assuming a positive maximum would change the theorem.
Lean represents players, each type set, and choices as finite nonempty types. Type profiles are dependent functions ; interim vectors are real functions on the disjoint union , with the product topology. A mechanism is a real function subject to explicit nonnegativity and sum-to-one constraints. Both and quantify only over functions satisfying those constraints. Conditional beliefs use the common prior in equations (3)–(4), and positive marginal probabilities make every denominator meaningful without requiring positive probability for each full profile. The positivity of every is an assumption the paper makes implicitly by dividing by it in (3); it is a field of the problem structure, not a hypothesis of the theorems. The subjective reading of and that the paper permits on p. 63, the response-plan equilibria of Section 3, and the numerical example of Section 6 are outside this mission.
Strict dominance means a strict gain for every player type. The constant mechanism, conflict vector, and individually rational set are defined from the problem data. The conflict vector is defined by equation (16), while its equality with the constant mechanism's payoff is a theorem item. The product uses real powers with the paper's marginal weights and is compared only on , where each base is nonnegative. A solution is a maximizer property; it is not chosen in advance or supplied as a theorem hypothesis. These choices exclude vacuous encodings of incentive efficiency, unrestricted mechanisms, and a maximization domain that already contains only a nominated winner.
A complete proof development needs finite sums and products, continuous and convex maps on finite-dimensional real spaces, compactness of the constrained mechanism set, and facts about positive weighted real powers or logarithms on the strictly positive region. The model definitions can be reused for the paper's separate revelation-principle mission; this mission also welcomes proofs of the explicit claims about the uniform mechanism, the conflict mechanism, and product maximizers.
Manufacturers of perishable goods must decide how much inventory risk to leave with retailers. A retailer who pays for every ordered unit may order less than is best for the manufacturer and retailer together; a generous return policy changes that incentive. Pasternack studies this question in a single-period setting, with a fixed selling price, uncertain demand and goodwill costs when customers cannot be served. The article identifies two familiar endpoint policies that fail: no returns, and unlimited returns reimbursed at the full wholesale price. It then investigates partial credit as a way to align the order decisions. Pasternack (1985)
The target here is the article's paired Theorems 1 and 2. They concern one retailer and one manufacturer, and their conclusion is about the order quantity the retailer chooses. The model does not ask the retailer to choose the selling price, nor does it compare realized profits for one particular demand outcome. The value of the result lies in ruling out two whole classes of pricing and return terms before considering how to divide the gains from a coordinated channel. Pasternack (1985), pp. 169–171
A manufacturer produces at unit cost and charges the retailer a wholesale price . The retailer orders units before observing demand , then sells at a fixed retail price . Unsold units have salvage value . A return policy gives the retailer a credit for a fraction of the order: permits no returns and permits returns of every leftover unit. The retailer incurs goodwill cost for each unmet unit of demand; the manufacturer bears the additional cost , and is the total goodwill cost. The paper assumes and . Pasternack (1985), pp. 169–170, (1)–(2)
Demand is described by a density on the nonnegative reals and distribution function . From the same order and demand outcome, the paper computes three expected profits: for an integrated company store, for the independent retailer, and for the manufacturer. Their definitions are equations (3), (6) and (8). An optimal order maximizes the relevant expected profit over nonnegative . The paper calls the channel coordinated when the retailer chooses a system-optimal order, as if the manufacturer operated the store directly. The formal model compares the sets of all such optimal orders, so it also handles a distribution whose CDF is flat over an interval. Pasternack (1985), pp. 170–171, (3), (6), (8)–(10)
The integrated company's optimal-order equation (5) supplies the benchmark:
The retailer's optimal-order equation (7) includes both and . Substituting the integrated benchmark gives equation (10), the common comparison used for the two endpoint policies. The first three milestones formalize these conditions, including existence of an integrated optimum. The last two milestones record the separate calculations in the appendix for full-credit returns and no returns. Pasternack (1985), pp. 170–171, 175
The mission goal combines Theorems 1 and 2 as the article does immediately after stating them. With or with , every system-optimal order fails to be retailer-optimal:
The disjointness claim is read separately for each endpoint policy. It says more than merely finding one order on which the firms disagree: neither endpoint policy can induce the retailer to choose a system optimum. Pasternack (1985), Theorems 1–2 and following paragraph, p. 171
The result separates a policy that reimburses all unsold stock at full wholesale price from one that offers no return option. Both may be simple to administer, but neither aligns the retailer's stocking choice with the integrated company's choice under the article's cost ordering. The result makes the paper's subsequent search for partial-credit terms substantive: the coordinating policy lies away from these two endpoints. It does not say that either endpoint always gives a loss, or that a retailer cannot make a profit. The claim concerns the order that maximizes expected channel profit. Pasternack (1985), pp. 171–172
The known result is proved in the article, but its definitions and theorem statements have not been machine-checked as part of this mission. Formalization gives a reusable account of the paper's piecewise expected profits, feasible order quantities and return fraction, and makes explicit the conditions under which the endpoint conclusions hold. Related proved platform statements include Snyder and Shen's wholesale coordination and wholesale under-ordering. They are not imported: their contract data require , while Pasternack's retailer has no separate own unit cost and the article does not require nonnegative salvage value.
The claim is sensitive to the demand model. If demand is deterministic, its CDF has a jump, and an order exactly equal to demand can be optimal under both the integrated profit and unlimited full-credit returns. The paper assumes a demand density; continuity of the CDF is therefore material to Theorem 1. Flat parts of a continuous CDF pose a different issue: a theorem identifying just one optimum would lose some orders, so the milestone conditions identify whole sets of maximizers. Pasternack (1985), p. 170, definition of and (4)–(7)
The no-return case also depends on the meaning of the manufacturer's additional goodwill cost. The paper names as a cost but does not print a separate nonnegativity inequality. If it were allowed to be negative, the appendix's contradiction with could disappear. The formalization states , along with , and identifies this convention openly. Pasternack (1985), pp. 170, 175
Lean uses a probability measure supported on with finite first moment in place of a named density . The theorems assume that has no atoms, giving the continuous CDF needed by the paper's first order conditions. The profit definitions retain the piecewise formulas of (3), (6) and (8), including the thresholds and . Adjacent pieces agree at their boundaries. The fixed retail price and the fraction match the paper's setting. The cost ordering is split between fixed costs and an admissible policy, because the theorem compares particular policy choices.
Only is feasible. An optimal-order predicate includes this membership as well as maximality, and coordination compares complete argmax sets. The goal explicitly asserts that a system optimum exists, preventing a vacuous conclusion about orders when there are none. At the retailer profit is independent of , so the goal quantifies over every credit without imposing an unused bound on it. The denominator is positive under and . Contributions that develop the optimal-order characterizations, the substitution identity, or the endpoint contradictions within these conventions directly support the goal.
A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.
Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.
A manufacturer produces at unit cost . A retailer sells at the fixed retail price . Leftover units are salvaged at per unit. Each unit of unmet demand costs the retailer a goodwill penalty and the manufacturer an additional penalty ; write . The data satisfy .
The manufacturer chooses a policy : the retailer pays per unit ordered and may return up to the fraction of its order for a credit per unit. The paper assumes
Demand is random with distribution function . Three expected profits are defined as functions of the order : , equation (3), the profit of a company store in which the manufacturer sells directly; , equation (6), the independent retailer's profit under the policy; and , equation (8), the manufacturer's profit when the retailer orders . An optimal order for a profit function is a maximizing it over . The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.
The Lean development uses the same letters: Costs carries ; Costs.Admissible K c1 c2 R is (1)–(2) with ; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; is cdf D for a demand law D.
A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of and . Precisely, for every price with there is a credit with
such that the policy coordinates the channel for every continuous demand distribution on with finite mean. The credit is chosen before, and independently of, the demand law.
The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.
Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for establishes only , which suffices only when , although the claim holds for all . And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost , which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.
The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on , including the boundary . Coordination is a statement about sets of maximizers, not about one first-order condition: when is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where increases. The naive reading "both first-order conditions hold at " proves one inclusion only.
Demand is a probability measure D on with D (Iio 0) = 0 and finite mean (IsDemand), and is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy , implicit in the paper. is a fraction in . Optimal orders are maximizers over that are themselves . Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator is positive under these assumptions, so no division is degenerate.
The goal is not the algebraic statement "there is solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of .
A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.
Decisions under uncertainty are often modelled by a finite set of scenarios: possible futures with weights , each with its own optimization problem. Solving every scenario separately is easy but useless in practice, because the decision taken today cannot depend on which scenario will be revealed tomorrow. Progressive hedging, introduced by Rockafellar and Wets in Scenarios and policy aggregation in optimization under uncertainty (IIASA Working Paper WP-87-119, 1987; Mathematics of Operations Research 16(1), 1991), restores this nonanticipativity by iterating between scenario-wise solves and an averaging step, guided by price systems that act as multipliers. It is the standard decomposition method for multistage stochastic programs and is implemented in widely used software such as PySP/mpi-sppy. This mission formalizes the paper's convergence theorem in the convex case, Theorem 5.1, together with the duality theory of §4 and the proof steps of §5 it rests on.
Let be a finite set of scenarios with weights , . For each the scenario subproblem is to minimize over , where is nonempty and closed and is locally Lipschitz with bounded level sets . The convex case is when every and is convex.
A decision vector is split by time, . A policy is a map ; the policy space carries the inner product and norm . At each time the scenarios are partitioned into bundles of scenarios that cannot yet be told apart. The aggregation replaces by its -weighted average over the bundle of at time , and . The implementable policies are constant on each , the price systems are , and the admissible policies are . With the problem is
Its Lagrangian is on , the dual is : maximize over with .
The progressive hedging algorithm fixes , starts from any and any , and in iteration sets , lets minimize
for every scenario, and updates .
In the convex case with exact minimization, the sequences and are bounded if and only if (P) and (D) have optimal solutions. In that case there are optimal for (P) and for (D) with
and, with ,
for all , strictly unless , and the step lengths are nonincreasing from on.
Theorem 5.1 is the guarantee behind progressive hedging in the convex case: solving only small scenario problems and averaging, the method finds a nonanticipative optimal policy and an optimal price system whenever these exist, with a distance to the solution that never increases. The dual sequence converges to a solution of (D), which gives the prices of information that the paper interprets economically. Boundedness of the iterates is an exact test for solvability.
The result is classical and fully proved on paper; its proof reduces the algorithm to Rockafellar's proximal point algorithm for a maximal monotone operator. No machine-checked version is known to exist. The mission produces a formal statement and, eventually, a proof of the full chain from scenario data to convergence, including the duality theorem of §4, which is of independent use for scenario-based stochastic programming. A related platform mission in this series treats the nonconvex case (limits of the algorithm satisfy first-order conditions).
The algorithm is not a proximal point method in the variable : it acts on the pair , and the averaged policy is in general not admissible while is in general not implementable. The step that fails in a direct attempt is showing that the map is firmly nonexpansive, which requires recognizing it as the resolvent of the monotone operator of a saddle function restricted to , in the rescaled norm rather than in the original product norm. A second difficulty is duality: identifying the fixed points of the iteration with optimal pairs of (P) and (D) needs the convex duality theory of §4 for an extended-real-valued perturbation function without any constraint qualification.
is EuclideanSpace ℝ (Fin n); policies are functions S → EuclideanSpace ℝ (Fin n) with S a Fintype. Time periods are a monotone map assigning each coordinate to its period, and each is a Setoid S; no refinement between periods is assumed. The standing assumptions of §3 are fields of the model structure, and the convex case is a separate hypothesis.
The inner product (2.2), norm (2.3) and (5.2) are explicit weighted sums. Mathlib's norm on a function type is the sup norm; it is used only for topology (boundedness, convergence, local Lipschitz continuity, compactness), which coincides with that of (2.3) in finite dimension. Stating (5.3) or (5.26) with Mathlib's sup norm would change the inequalities and is ruled out. Optimal values , , , , and are EReal infima and suprema, so that infeasibility gives and an unbounded dual objective gives ; real-valued sInf would silently return there. A solution of (D) must have . The algorithm is a predicate on sequences, with arbitrary and ; Proposition 3.2 shows the predicate is satisfiable.
Subgradients and normal cones are those of convex analysis; the normal cone is the published definition FirstOrderOpt.ConvexTheory.normalCone. Not formalized: the nonconvex (Clarke) parts of §4, the linear-quadratic case and its rate result, and inexact minimization.
A complete development needs: separable minimization over product sets, finite-dimensional compactness arguments, convex duality for a perturbation function on a subspace, and the convergence of the proximal point algorithm for maximal monotone operators (Rockafellar 1976, Theorem 1 and Proposition 1). The last two are reusable well beyond this mission; contributions of either as standalone results are welcome.
Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as when the base is near (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base- digits of a fraction written backwards, so the period of the generator is the period of a repeating base- expansion, i.e. the multiplicative order of modulo .
Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.
Fix a base and two lags and with . A state (or seed vector) is
where each is a base- digit and is the carry bit. The digit is the oldest one. The add-with-carry map (p. 465) is
and the generated sequence of a seed is . Reading off the last digit of each state gives a digit stream obeying , with the carry updated at each step. The two trivial seeds are and . The modulus of the generator is
For and , the -th base- digit of after the point is . The order is the least with , and is a primitive root of a prime when .
Let be prime, and let be any seed other than the two trivial seeds. Then is a periodic point of and
This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular , , and does not assume that is a primitive root. When it is, the period is , the value announced in §2.
The result. The goal reduces the period of the generator, a property of a dynamical system on states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses : search for primes and check the order of . Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus . Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.
Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base- expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.
The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: is not linear over , and the state does not live in a group in any evident way. The link to the order of modulo goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed , whose digits are those of , has to be excluded.
A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.
CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of and . A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so holds by typing. Lean index is the paper's : x 0 is (the digit the step drops), and the partner digit is index . step is defined directly from the two-case formula of p. 465, not through . The digit stream out is one-based: the seed digits for , then the last digit of . digit b m k j is the exact integer formula above, used for only.Function.minimalPeriod. It is at non-periodic points, so the goal's equation with the positive also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period " is stated as " is a period iff ".minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.Classical cooperative game theory assumes that any coalition of players can form and coordinate. In many settings cooperation is mediated by pairwise relationships: communication lines, contracts, alliances, or trade links. Roger Myerson's discussion paper Graphs and Cooperation in Games (Northwestern University, 1976; published in Mathematics of Operations Research 2(3), 1977, doi:10.1287/moor.2.3.225) models such a cooperation structure as a graph on the set of players and asks how the players should share the worth of the game when only linked players can coordinate directly.
The answer, now called the Myerson value, is the starting point of the literature on communication situations and network games. It underlies later work on network formation (Jackson and Wolinsky, A strategic model of social and economic networks, JET 1996) and on allocation rules for networks, and it is a standard textbook example of an axiomatic solution concept.
Timeline:
Let be a nonempty finite set of players and the set of nonempty coalitions . A game in characteristic function form is a vector ; is the transferable wealth coalition can divide.
A link is an unordered pair of distinct players and a graph is a set of links; is the set of all graphs, the complete graph, the graph with one link removed, and the number of links. Players are connected in by if or a path of links of joins them through players of only; the classes form the partition of , and is the set of connected components of . The graph-restricted game is
An allocation rule is a function , with the payoff of player under cooperation structure . It is a fair allocation rule for if
is totally stable if for every and every link , and is superadditive if for disjoint .
A game in graph function form assigns to every pair with a closed, comprehensive (closed under decreasing coordinates), proper () set of feasible payoffs; its fair allocation rule replaces (7) by (14), .
If is superadditive, then the fair allocation rule for is totally stable:
Every has a unique fair allocation rule; every game in graph function form has a unique satisfying (14) and (10).
The fair allocation rule is
The milestones follow the paper's Section 7: the steps of the proof of Theorem 4 (displays (15)–(17)), Theorem 4, Theorem 1, the decomposition of and the efficiency and equity of (proof of Theorem 2), Theorem 2, and the monotonicity of and in a link (proof of Theorem 3). Theorem 3 is the goal because its proof uses the formula of Theorem 2, whose proof uses the uniqueness of Theorem 1, which is the transferable-utility case of Theorem 4: all four numbered results lie on one path.
The theorems give an axiomatic foundation for allocation in networks: two natural requirements, component-wise efficiency and equal gains from each link, single out one rule, and that rule is an explicit formula built from the Shapley value. At the complete graph it recovers the Shapley value itself, so the result is also a new characterization of the Shapley value. Total stability says that, for superadditive games, no player has an incentive to break a link, which connects the allocation rule to the question of which networks form.
The results are proved in the paper. A search of the platform found no formalization of cooperation graphs, the graph-restricted game, the Myerson value or total stability; the Shapley value is available as a platform definition and is reused. This mission produces machine-checked statements of all four theorems and of the intermediate steps of their proofs, together with a reusable definition layer for communication situations.
The equity condition (10) relates the payoff at a graph to the payoff at a graph with one fewer link, and it constrains only pairs of linked players; it is not evident that these conditions, together with efficiency on components, determine the rule at every graph, nor that they are consistent. Uniqueness and existence must hold simultaneously for all graphs, and the constraints couple each graph to all of its subgraphs and each player to every other player of its component. In the graph function form, efficiency becomes a boundary condition on a closed comprehensive set, and the existence and uniqueness of the relevant extremal point depend on all three properties of .
Identifying the rule with requires the efficiency of the Shapley value on each component of , which is not the efficiency of on , and equity requires tracking how the partitions change when a link is removed. Total stability is false for general games: without superadditivity a player can gain by cutting a link, so the hypothesis cannot be dropped.
Players are Fin n, with in every theorem as the paper assumes nonempty; the paper's player is index . The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): is ⊤, the empty graph ⊥, is h ≤ g and is h < g. A game is a function Finset (Fin n) → ℝ; its value at is a junk coordinate that no definition reads, and no theorem assumes . Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at to . is ↥S → ℝ with the product topology, and is the topological frontier.
Explicit readings of the typescript:
The equity and stability conditions quantify over links of only. Quantifying over all pairs of players would make Theorem 1 false and the goal vacuous, so that reading is ruled out. Likewise (14) is boundary membership, not membership in .
Contributions welcome: general lemmas on the partitions (refinement under link deletion, restriction to components), Möbius inversion over the subgraph lattice of a finite simple graph, the carrier and null-player properties of the Shapley value, and the extremal-point lemma for closed comprehensive sets. These are reusable beyond this mission.
In a finite stopping problem, a decision maker observes rewards one at a time and must accept one without seeing the future. A fully informed observer takes the maximum. This comparison is often called a prophet inequality. The abstract bound that an optimal stopping rule can secure at least half the expected maximum does not say how to choose a simple rule. Samuel-Cahn showed that a threshold chosen from a median of the maximum already gives this guarantee, even when the rewards are independent but differently distributed. The rule requires one number fixed before observations begin. Samuel-Cahn, 1984
The paper builds on earlier comparisons between the maximum and the best stopping value, then narrows attention to rules that accept an observation when it crosses a fixed threshold. This mission isolates its first main result, Theorem 1, and the two cases that determine whether the crossing test is strict or weak. The paper's second main result, concerning the sharpness of the constant for identically distributed rewards, belongs to the next mission in this series. Samuel-Cahn, 1984, pp. 1213–1215
Let , and let be independent, nonnegative real random variables. Write . For a threshold , the weak threshold rule takes the first with and ; the strict threshold rule uses . If no earlier observation qualifies, either rule takes , even when is below the threshold. Hence every rule returns exactly one observed reward.
The paper distinguishes the full stopped reward from its positive threshold reward. In its notation,
The last forced observation may contribute to or while contributing zero to or . This difference is essential to the theorem's middle bounds. A median of means both and . Define the excess sum , where . The two median inequalities allow an atom at , and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)
For every median , the goal retains both of the paper's conditional conclusions:
At equality , both conclusions apply. The attack path follows the expected maximum bound (1.3), the displayed identities and probability bound in (1.4), and the companion weak threshold display. Each milestone points to an actual line of the paper. The NOTE and ASSERTION give a further interval of working thresholds: if and , then every satisfies the same chain with . Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215
Theorem 1 replaces the unspecified best stopping policy with a specific threshold chosen from the distribution of the maximum. It also shows that the thresholded part of the stopped reward alone meets the factor two bound. That stronger middle statement distinguishes the theorem from an outer comparison . For a reward distribution with atoms, the theorem says exactly when to use and when to use . Its companion ASSERTION shows that a median is not the only useful threshold choice. Samuel-Cahn, 1984, p. 1214
The result is proved in the paper; the work here is to express its assumptions, boundary behavior, and all displayed inequalities as Lean statements that solvers can prove. The milestones expose reusable facts about positive parts, forced stopping, and independence of a current observation from the event that the rule has survived earlier ones. No machine checked proof of these drafted statements is claimed. The second mission can use the completed theorem to formalize why the factor two cannot be improved uniformly over threshold rules, even for identically distributed observations.
The event that a rule reaches index depends on the observations before . Establishing its independence from the excess of requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at also makes the positive threshold reward smaller than the full stopped reward whenever the last observation misses the threshold. Ignoring that last case would erase one of the theorem's conclusions. Finally, atoms at the median prevent the strict and weak crossing events from being interchanged. Samuel-Cahn, 1984, (1.1)–(1.4)
Lean indexes the observations by Fin with . Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop . The rules are the least qualifying index or that final index. The paper's and therefore become and . Observations are measurable, nonnegative almost surely, and mutually independent under a probability measure.
Expectations use the extended nonnegative integral of the positive part, taking values in . This keeps infinite expected rewards visible without imposing an integrability assumption absent from Theorem 1. The median has both strict tail inequalities from (1.1). The identities for positive stopped rewards state directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds and are parameters satisfying the paper's defining equations, with no extra uniqueness hypothesis in statements that do not use it.
The goal cannot be satisfied by replacing with , by permitting a rule to return no observation, or by making the median predicate empty. Useful contributions include the measurable threshold rule interface, the pathwise excess decomposition, the factorization under mutual independence, and the remaining extended nonnegative arithmetic. Those pieces can also support other finite prophet inequality developments.