All missions

Motivation

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: $n$ processors, at most $m$ 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 $n \ge 3m+1$ when messages can be forged in relay, and possible for every $n \ge m$ 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 $3m+1$ 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 $n\ge 3m+1$ processors in $m+1$ rounds of message exchange.

Setting

Let $P$ be a finite set of $n = |P|$ processors and $V$ a set of values. A string over a set $S$ is a finite sequence $p_1p_2\cdots p_r$ of elements of $S$, repetitions allowed. For $k\ge 1$ a $k$-level scenario is a map $\sigma$ from the nonempty strings over $P$ of length at most $k+1$ to $V$. The value $\sigma(p)$ is $p$'s private value $V_p$; for $r\ge 2$, $\sigma(p_1p_2\cdots p_r)$ is the value $p_2$ tells $p_1$ that $p_3$ told $p_2$ … that $p_r$ told $p_{r-1}$ is $p_r$'s private value. A $k$-level scenario records the outcome of $k$ rounds of message exchange.

Faults are modeled by a set $N\subseteq P$ of nonfaulty processors, unknown to the processors. Nonfaulty processors relay truthfully, so $\sigma$ is consistent with $N$ when

$$\sigma(pqw) = \sigma(qw)\qquad (q\in N,\ p\in P,\ w \text{ a string over } P,\ |pqw|\le k+1).$$

Faulty processors are otherwise unconstrained. A processor $p$ sees only its view $\sigma_p$, the restriction of $\sigma$ to strings beginning with $p$.

The procedure (p. 230). Processor $p$ computes the entry for processor $q$ as follows, with $n$ and $m$ the current processor count and fault bound:

1. If some $Q\subseteq P$ with $|Q|>(n+m)/2$ and some $v$ satisfy $\sigma_p(pwq)=v$ for every string $w$ over $Q$ of length $\le m$, record $v$.
2. Otherwise apply the procedure for $m-1$, $n-1$ to the processor set $P-\{q\}$ and the view $\hat\sigma_p(pw)=\sigma_p(pwq)$, obtaining a vector of $n-1$ entries. If at least $\lfloor (n+m)/2\rfloor$ of them agree, record the common value; otherwise record NIL.

In Lean this is InteractiveConsistency.OralAlgorithm.record m P τ q with τ = fun w => σ (p :: w), values in Option V with none for NIL.

Formalization targets

Goal: the procedure assures interactive consistency

For $n\ge 3m+1$, for every $N\subseteq P$ with $|N|\ge n-m$ and every $(m+1)$-level scenario $\sigma$ consistent with $N$,

$$\mathrm{record}(m,P,\sigma_p,q)=\sigma(q)\quad(p,q\in N),\qquad \mathrm{record}(m,P,\sigma_p,r)=\mathrm{record}(m,P,\sigma_{p'},r)\quad(p,p'\in N,\ r\in P).$$

This is procedure_assures_ic. It is the paper's claim about this procedure, not an existence statement.

Milestones, in the order the paper's proof uses them

1. Nonfaulty $q$ (p. 231): for $p,q\in N$, step (1) succeeds and $p$ records $V_q$.
2. Two step-(1) quorums agree (p. 231): if $p,p'\in N$ find quorums $Q_1,Q_2$ with values $v,v'$, then $v=v'$.
3. The subscenario (p. 230): for faulty $q$, $\hat\sigma(w)=\sigma(wq)$ is an $m$-level scenario on $P-\{q\}$ consistent with $N$, and $|N|\ge (n-1)-(m-1)$.
4. The $\hat Q$ claim (p. 231): if $Q,v$ satisfy step (1) for $p'$ and $q$, then $\hat Q=Q-\{q\}$ has at least $\lfloor(n+m)/2\rfloor$ members and $\hat Q, v$ satisfy step (1) of the recursive call for every $q'\in\hat Q$.

Significance

The theorem is the upper bound in the tight characterization $n\ge 3m+1$ 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 $\mathrm{OM}(m)$ of the Byzantine generals paper, and its quorum arithmetic ($|Q|>(n+m)/2$, 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 $\mathrm{OM}(m)$ 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.

Difficulty

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 $q$, the fault bound drops by one, and the scenario becomes $\hat\sigma(w)=\sigma(wq)$ 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 $q$ is faulty nothing forces either value to be $q$'s private value. The thresholds are exact: $|Q|>(n+m)/2$ in step (1) and $\lfloor(n+m)/2\rfloor$ agreeing entries in step (2), both in the current $n$ and $m$; 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.

Formalization scope

Processors form a Finset α with decidable equality; strings are List α, read left to right (the receiver first, the originator last), so $\sigma_p(pwq)$ is σ (p :: (w ++ [q])). A scenario is a total function List α → V; consistency with $N$ (ConsistentUpTo P N (m + 1) σ) constrains it only on strings over $P$ of length at most $m+2$, the domain of an $(m+1)$-level scenario and all the procedure reads. The procedure receives only the view fun w => σ (p :: w), never $\sigma$ or $N$. The fault hypothesis $|N|\ge n-m$ is P.card ≤ N.card + m; $m=0$ is included.

Explicit readings of the paper's prose: "size $>(n+m)/2$" is P.card + m < 2 * Q.card; $\lfloor(n+m)/2\rfloor$ is natural-number division; "strings over $Q$ of length $\le m$" includes the empty string and allows repetitions; the step-(2) vector is indexed by P.erase q and includes $p$'s own entry; the recorded value in step (1) is $\sigma_p(pq)$ (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 $m=0$ a failing step (1) records NIL (never reached under the hypotheses). Two printed slips are corrected in the Lean: "records $V_q$ and $q$" (for "for $q$") and "$\sigma_{p'}(p'wq')$" (for $\hat\sigma_{p'}$).

Trivializing formalizations are ruled out: the procedure never sees $\sigma$ itself (with it, recording $\sigma(q)$ would be trivial), consistency constrains only relays by nonfaulty processors, and $N$ ranges over every subset of size at least $n-m$.

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 $m$, 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 $n\le 3m$ (Section 4), and mission 3 the authenticated-message procedure for every $n\ge m$ (Section 5).

Selected references

• M. Pease, R. Shostak, L. Lamport, Reaching agreement in the presence of faults, Journal of the ACM 27(2), 1980, 228–234. https://doi.org/10.1145/322186.322188
• L. Lamport, R. Shostak, M. Pease, The Byzantine generals problem, ACM Transactions on Programming Languages and Systems 4(3), 1982, 382–401. https://doi.org/10.1145/357172.357176
• J. H. Wensley et al., SIFT: Design and analysis of a fault-tolerant computer for aircraft control, Proceedings of the IEEE 66(10), 1978, 1240–1255. https://doi.org/10.1109/PROC.1978.11114

Why a nonsmooth implicit-function theorem

The classical implicit-function theorem solves an equation $F(x, y) = 0$ for $x$ as a function of a parameter $y$ near a known solution $(x_0, y_0)$, provided $F$ is (strongly) Fréchet differentiable in $x$ 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 $\min$, 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 $f$ 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.

Setting

Let $X$, $Y$, $Z$ be real normed linear spaces, with $X$ complete. Fix $x_0 \in X$, $y_0 \in Y$, a neighborhood $\Xi$ of $x_0$ and a neighborhood $H$ of $y_0$. Let $F$ map $\Xi \times H$ to $Z$, with $F(x_0, y_0) = 0$, and let $f$ map $\Xi$ to $Z$, with $f(x_0) = 0$. $B(x, \rho)$ denotes the closed ball of radius $\rho$ about $x$.

Expansion modulus. For a map $f$ between metric spaces and a set $S$,

$$\delta(f, S) = \inf\left\{ \frac{\|f(x_1) - f(x_2)\|}{\|x_1 - x_2\|} : x_1 \ne x_2,\ x_1, x_2 \in S \right\}.$$

If $\delta(f,S) > 0$, then $f$ is one-to-one on $S$ and its inverse is Lipschitzian with modulus $\delta(f,S)^{-1}$. In Lean the mission works with lower bounds: ExpansionAtLeast f S d says $d\,\|x_1 - x_2\| \le \|f(x_1) - f(x_2)\|$ on $S$, i.e. $d \le \delta(f,S)$.

Strong approximation (Definition 2.4). $f$ strongly approximates $F$ in $x$ at $(x_0, y_0)$, written $f \approx_x F$ (Lean: StronglyApproxInX f F x₀ y₀), if for each $\varepsilon > 0$ there are neighborhoods $U$ of $x_0$ and $V$ of $y_0$ with

$$\big\|[F(x, y) - f(x)] - [F(x', y) - f(x')]\big\| \le \varepsilon \|x - x'\| \qquad (x, x' \in U,\ y \in V).$$

When $f$ is the partial derivative map $x \mapsto F_x(x_0,y_0)(x - x_0)$ this is strong partial Fréchet differentiability; in general $f$ may be piecewise linear or any map with a Lipschitzian inverse.

Formalization targets

Goal: Theorem 3.2 (p. 299)

Assume (a) $f \approx_x F$ at $(x_0, y_0)$; (b) for each $x \in \Xi$, $F(x, \cdot)$ is Lipschitzian on $H$ with modulus $\varphi$; (c) $f(\Xi)$ is a neighborhood of $0$ in $Z$; (d) $\delta(f, \Xi) =: d_0 > 0$. Then for each $\lambda > d_0^{-1}\varphi$ there are neighborhoods $U \subseteq \Xi$ of $x_0$, $V \subseteq H$ of $y_0$ and a function $x : V \to U$ with

$$x(y_0) = x_0, \qquad \|x(y_1) - x(y_2)\| \le \lambda \|y_1 - y_2\| \ (y_1, y_2 \in V), \qquad \{\xi \in U : F(\xi, y) = 0\} = \{x(y)\} \ (y \in V).$$

Every $\lambda$ strictly above $\varphi/d_0$ is claimed; $\lambda = \varphi/d_0$ is not.

Milestones

1. Lemma 3.1 (p. 298), the Lipschitz perturbation lemma: if $f$ maps $\Omega$ onto a ball $B(y_0, \alpha)$, $h$ is Lipschitzian with modulus $\eta < \delta := \delta(f, \Omega)$, $\Omega \supseteq B(x_0, \delta^{-1}\alpha)$ and $\theta := (1 - \eta\delta^{-1})\alpha - \|h(x_0)\| \ge 0$, then

$$(f + h)\big(B(x_0, \delta^{-1}\alpha)\big) \supseteq B(y_0, \theta), \qquad \delta(f + h, \Omega) \ge \delta - \eta > 0.$$

2. (3.1)–(3.2) in the proof of Theorem 3.2 (p. 300): for every $\varepsilon \in (0, d_0)$ there are $\alpha, \kappa > 0$ and a neighborhood $V \subseteq H$ of $y_0$ with $\Omega = B(x_0, d_0^{-1}\alpha) \subseteq \Xi$ such that for each $y \in V$

$$\delta(F(\cdot, y), \Omega) \ge d_0 - \varepsilon, \qquad F(\cdot, y)(\Omega) \supseteq B(0, \theta(y)) \supseteq B(0, \kappa),$$

where $\theta(y) = (1 - \varepsilon d_0^{-1})\alpha - \|F(x_0, y)\|$.

Significance

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 $\varphi/d_0$. 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.

Difficulty

The obvious approach, differentiate and invert, is unavailable: $f$ need not have a derivative anywhere near $x_0$, so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of $F(\cdot, y)$ onto a ball uniformly in $y$ from information about $f$ alone. Injectivity transfers directly from $f$ through the small Lipschitz modulus of $F(\cdot, y) - f$; surjectivity does not, because $f$ carries no information about $F(\cdot, y)$ 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 $y$. Completeness of $X$ is essential (the paper stresses this on p. 306) and is not available for $Y$ and $Z$.

Formalization scope

All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:

• Scalars are real; $X$ is a complete normed space ([CompleteSpace X]); $Y$, $Z$ are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.
• $\delta(f, S)$ via lower bounds. Every statement takes a real $d$ with ExpansionAtLeast f S d in place of "$d = \delta(f,S)$", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be $0$ on sets with fewer than two points.
• Total functions. $F$ is a curried total function F : X → Y → Z and $f : X \to Z$; hypotheses constrain them on $\Xi \times H$ only, and the conclusions keep the implicit function inside the domain: $U \subseteq \Xi$, $V \subseteq H$, $x(V) \subseteq U$. This makes explicit what the paper leaves implicit (its $F$ is only defined on $\Xi \times H$). Likewise $\Omega \subseteq \Xi$, used implicitly in the paper's proof, is a conclusion of milestone 2.
• Closed balls (Metric.closedBall), radii $\delta^{-1}\alpha$ written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.
• Lemma 3.1 keeps the paper's hypothesis that $\Omega$ is open, although Theorem 3.2's proof applies it to a closed ball.
• Milestone 2 states as an existence claim, for every $\varepsilon \in (0, d_0)$, the choices the paper makes at the start of its proof.

A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at $y = y_0$), in which $V$ may shrink to $\{y_0\}$, $\lambda$ is existential, or uniqueness is asserted outside $\Xi$, 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.

Selected references

• S. M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, 292–309. https://doi.org/10.1287/moor.16.2.292
• S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 1980, 43–62. https://doi.org/10.1287/moor.5.1.43
• A. V. Dmitruk, A. A. Milyutin, N. P. Osmolovskii, Lyusternik's theorem and the theory of extrema, Russian Mathematical Surveys 1980, No. 6, 11–51 (as cited in Robinson 1991, p. 298).
• L. V. Kantorovich, G. P. Akilov, Functional Analysis, cited in Robinson 1991 as [17].

Motivation

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:

• 1953. Shapley defines the Shapley value $\varphi$ for transferable-utility games by efficiency, symmetry, a carrier axiom and additivity (Shapley 1953).
• 1976–1977. Myerson introduces cooperation graphs, the fairness (equal gains from each link) condition, proves existence and uniqueness of the fair allocation rule, identifies it as the Shapley value of the graph-restricted game, proves its total stability for superadditive games, and extends existence and uniqueness to games without transferable utility in graph function form.

Setting

Let $N$ be a nonempty finite set of players and $CL$ the set of nonempty coalitions $S\subseteq N$. A game in characteristic function form is a vector $v\in\mathbb R^{CL}$; $v_S$ is the transferable wealth coalition $S$ can divide.

A link $n{:}m$ is an unordered pair of distinct players and a graph $g$ is a set of links; $GR$ is the set of all graphs, $\bar g^N$ the complete graph, $g\setminus n{:}m$ the graph with one link removed, and $|g|$ the number of links. Players $a,b$ are connected in $S$ by $g$ if $a=b\in S$ or a path of links of $g$ joins them through players of $S$ only; the classes form the partition $S/g$ of $S$, and $N/g$ is the set of connected components of $g$. The graph-restricted game is

$$(v/g)_S=\sum_{T\in S/g}v_T .$$

An allocation rule is a function $Y:GR\to\mathbb R^N$, with $Y_n(g)$ the payoff of player $n$ under cooperation structure $g$. It is a fair allocation rule for $v$ if

1. (efficiency, (7)) $\sum_{n\in S}Y_n(g)=v_S$ for every $g$ and every component $S\in N/g$, and
2. (equity, (10)) $Y_n(g)-Y_n(g\setminus n{:}m)=Y_m(g)-Y_m(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$.

$Y$ is totally stable if $Y_n(g)\ge Y_n(g\setminus n{:}m)$ for every $g$ and every link $n{:}m\in g$, and $v$ is superadditive if $v_{S\cup T}\ge v_S+v_T$ for disjoint $S,T\in CL$.

A game in graph function form assigns to every pair $(S,g)$ with $S\in N/g$ a closed, comprehensive (closed under decreasing coordinates), proper ($\emptyset\ne W\ne\mathbb R^S$) set $w(S,g)\subseteq\mathbb R^S$ of feasible payoffs; its fair allocation rule replaces (7) by (14), $(Y_n(g))_{n\in S}\in\partial w(S,g)$.

Formalization targets

Goal: Theorem 3 (p. 8)

If $v$ is superadditive, then the fair allocation rule $Y$ for $v$ is totally stable:

$$Y_n(g)\ge Y_n(g\setminus n{:}m)\qquad\text{for all } g\in GR,\ n{:}m\in g .$$

Theorem 1 (p. 7) and Theorem 4 (p. 10)

Every $v\in\mathbb R^{CL}$ has a unique fair allocation rule; every game $w$ in graph function form has a unique $Y$ satisfying (14) and (10).

Theorem 2 (p. 8)

The fair allocation rule is

$$Y(g)=\varphi(v/g)\quad\text{for all }g\in GR,\qquad\text{in particular } Y(\bar g^N)=\varphi(v).$$

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 $v/g$ and the efficiency and equity of $\varphi(v/g)$ (proof of Theorem 2), Theorem 2, and the monotonicity of $v/g$ and $\varphi(v/g)$ 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.

Significance

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.

Difficulty

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 $2^{|\bar g^N|}$ 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 $w(S,g)$.

Identifying the rule with $\varphi(v/g)$ requires the efficiency of the Shapley value on each component of $g$, which is not the efficiency of $\varphi$ on $N$, and equity requires tracking how the partitions $S/g$ 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.

Formalization scope

Players are Fin n, with $0<n$ in every theorem as the paper assumes $N$ nonempty; the paper's player $k$ is index $k-1$. The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): $\bar g^N$ is ⊤, the empty graph ⊥, $h\subseteq g$ is h ≤ g and $h\subset g$ is h < g. A game is a function Finset (Fin n) → ℝ; its value at $\emptyset$ is a junk coordinate that no definition reads, and no theorem assumes $v_\emptyset=0$. Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at $\emptyset$ to $0$. $\mathbb R^S$ is ↥S → ℝ with the product topology, and $\partial$ is the topological frontier.

Explicit readings of the typescript:

• The printed definition of "connected in $S$ by $g$" (p. 3) asks $n^i\in S$ only for $i\ge1$; the formalization requires every vertex of the path, including the start, to lie in $S$, which makes $S/g$ the partition of $S$ the paper describes.
• Comprehensiveness (p. 10) prints "$\forall n\in N$" for coordinates of vectors in $\mathbb R^S$; read as $n\in S$.
• Display (17) writes $Y_n(h)$ under the index $m\in S$; read as $Y_m(h)$, as in (18b).
• The proof headed "PROOF OF THEOREM 4." on p. 13 is the proof of Theorem 3.
• "The unique fair allocation rule" in Theorems 2 and 3 is stated for every fair allocation rule; existence and uniqueness are Theorem 1.
• The paper's $N$ is nonempty; every theorem carries the corresponding hypothesis $0<n$.

The equity and stability conditions quantify over links of $g$ 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 $w(S,g)$.

Contributions welcome: general lemmas on the partitions $S/g$ (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.

Selected references

• R. B. Myerson, Graphs and Cooperation in Games, Discussion Paper No. 246, CMS-EMS, Northwestern University, September 1976; published in Mathematics of Operations Research 2(3):225–229, 1977. https://doi.org/10.1287/moor.2.3.225
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
• M. O. Jackson and A. Wolinsky, A Strategic Model of Social and Economic Networks, Journal of Economic Theory 71(1):44–74, 1996. https://doi.org/10.1006/jeth.1996.0108

Why a threshold rule matters

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

Observations and threshold rules

Let $n\ge1$, and let $X_1,\ldots,X_n$ be independent, nonnegative real random variables. Write $X_n^*=\max(X_1,\ldots,X_n)$. For a threshold $c\ge0$, the weak threshold rule $t(c)$ takes the first $X_i$ with $i<n$ and $X_i\ge c$; the strict threshold rule $s(c)$ uses $X_i>c$. If no earlier observation qualifies, either rule takes $X_n$, even when $X_n$ 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,

$$E^+X_{t(c)}=E[X_{t(c)}\mathbf1_{\{X_{t(c)}\ge c\}}], \qquad E^+X_{s(c)}=E[X_{s(c)}\mathbf1_{\{X_{s(c)}>c\}}].$$

The last forced observation may contribute to $E X_{t(c)}$ or $E X_{s(c)}$ while contributing zero to $E^+X_{t(c)}$ or $E^+X_{s(c)}$. This difference is essential to the theorem's middle bounds. A median $m$ of $X_n^*$ means both $P(X_n^*<m)\le\tfrac12$ and $P(X_n^*>m)\le\tfrac12$. Define the excess sum $\beta=\sum_{i=1}^n E(X_i-m)^+$, where $x^+=\max(x,0)$. The two median inequalities allow an atom at $m$, and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)

Formalization targets

Theorem 1: a median threshold

For every median $m$, the goal retains both of the paper's conditional conclusions:

$$\begin{aligned} \beta\ge m&\Longrightarrow E X_n^*\le2E^+X_{s(m)}\le2E X_{s(m)},\\ \beta\le m&\Longrightarrow E X_n^*\le2E^+X_{t(m)}\le2E X_{t(m)}. \end{aligned}$$

At equality $\beta=m$, 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 $a^*=E(X_n^*-a^*)^+$ and $b^*=\sum_iE(X_i-b^*)^+$, then every $a^*\le c\le b^*$ satisfies the same chain with $t(c)$. Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215

What the result gives

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 $E X_n^*\le2E X_\tau$. For a reward distribution with atoms, the theorem says exactly when to use $>$ and when to use $\ge$. 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.

Where the formal proof is delicate

The event that a rule reaches index $i$ depends on the observations before $i$. Establishing its independence from the excess of $X_i$ requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at $n$ 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)

Formalization scope

Lean indexes the $n$ observations by Fin $n$ with $n>0$. Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop $n$. The rules are the least qualifying index or that final index. The paper's $s(m)>i-1$ and $t(m)>i-1$ therefore become $i\le s(m)$ and $i\le t(m)$. 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 $[0,\infty]$. 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 $m\ge0$ directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds $a^*$ and $b^*$ 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 $E^+X_\tau$ with $E X_\tau$, 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.

Selected references

• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, The Annals of Probability 12(4), 1213–1216, 1984. DOI: 10.1214/aop/1176993150

Motivation

A production process deteriorates over time, and the state it is in cannot be observed directly. Each period the operator chooses among three actions: produce without looking, produce and inspect the item (which reveals the current state at a cost), or revise the process back to its good state. This is one of the earliest partially observed Markov decision problems with a costly observation action, and it is the prototype of the inspection and machine-replacement models that followed in operations research and maintenance theory. Ross (Management Science 17(9), 1971) set it up for a countable state space, reduced it to a fully observed problem on beliefs, and determined the structure of an optimal policy for two states.

Intuition suggests a three-region policy for two states: produce while the probability of the bad state is small, inspect at intermediate probabilities, revise when it is large. Ross showed that the true structure has up to four regions: produce, inspect, produce again, revise. This mission formalizes that structure theorem and the general results it rests on.

Setting

The underlying process has a countable set of states $0,1,2,\dots$, with transition probabilities $P_{ij}$ from state $i$ at the end of a period to state $j$ at the beginning of the next. In state $i$, producing without inspection costs $C_i$, producing with inspection costs $I_i$, and revising costs $R_i$; costs are bounded, and future costs are discounted by $\beta\in(0,1)$. A revision puts the process in state $0$.

The decision maker tracks a belief $P=(P_0,P_1,\dots)$, a probability vector on the states, ranging over

$$S=\Big\{P: P_i\ge0,\ \sum_iP_i=1\Big\}.$$

Producing without inspection moves the belief to $TP$, with $(TP)_i=\sum_jP_jP_{ji}$. Inspecting reveals the state; if it is $i$, the next belief is the row $e^i=(P_{i0},P_{i1},\dots)$. Revising leads to $e^0$.

The $\beta$-discounted optimal cost $V_\beta$ is the limit of value iteration: $V^0=0$ and

$$V^{n+1}(P)=\min\Big\{\sum_iP_iC_i+\beta V^n(TP);\ \sum_iP_iI_i+\beta\sum_iP_iV^n(e^i);\ \sum_iP_iR_i+\beta V^n(e^0)\Big\}.$$

The three terms with $V^n$ replaced by $V_\beta$ form the right side of the optimality equation (1). The $\beta$-optimal produce, inspect and revise regions are the sets of beliefs at which the corresponding term equals $V_\beta(P)$, and a stationary rule is $\beta$-optimal when it always selects an action attaining the minimum.

In the two-state process of §3, state $0$ is good and state $1$ is bad: $P_{00}=1-\pi$, $P_{11}=1$, $C_0=0$, $C_1=C$, $I_0=I_1=I$, $R_0=R_1=R$, with $C<I<R$. The belief is a number $P\in[0,1]$, the probability of the bad state, $TP=P+\pi-\pi P$, and the optimality equation becomes

$$V_\beta(P)=\min\{CP+\beta V_\beta(TP);\ I+\beta PV_\beta(1)+\beta(1-P)V_\beta(\pi);\ R+\beta V_\beta(\pi)\}.\tag{3}$$

Formalization targets

Goal: Theorem 3.3, the four-region structure

There are thresholds $\pi\le P_1\le P_2\le P_3$ with $P_2\le1$ such that the rule

$$\text{produce on }[0,P_1),\quad\text{inspect on }[P_1,P_2),\quad\text{produce on }[P_2,P_3),\quad\text{revise on }[P_3,1]$$

is $\beta$-optimal, and $P_3\le1$ whenever revising is $\beta$-optimal at some belief. Degenerate thresholds (empty intervals) are allowed, so the statement fixes only the order of the regions, not their number.

Milestones

1. (1): value iteration converges on $S$, $V_\beta$ is bounded, solves (1), and is its unique bounded solution.
2. Lemma 2.1: $V_\beta$ is concave on $S$.
3. Theorem 2.2: the $\beta$-optimal inspect and revise regions are convex.
4. (3): the two-state optimality equation, as an instance of (1).
5. Lemma 3.1: in the two-state model $V_\beta$ is nondecreasing on $[0,1]$.
6. Lemma 3.2: for $0\le P\le\pi$, producing is strictly better than inspecting and than revising.

Significance

Theorem 3.3 reduces the search for an optimal policy in the two-state problem to the choice of three numbers, and it fixes the order of the regions: there is never a revise region below an inspect region, and inspection never occurs below the deterioration probability $\pi$. Together with Theorems 3.4 and 3.7 of the same paper (separate missions in this series), it is the basis for computing optimal inspection policies by searching over thresholds. Theorem 2.2 holds for any countable state space and is the general form of the observation that, in partially observed problems with linear-in-belief action costs, the regions of the "information" and "reset" actions are convex while the region of the passive action need not be.

The results are proved in the paper. As far as a search of the Prove2Me library shows (October 2026), none of them is formalized. Related formal work treats other models: belief-state reductions of finite POMDPs, and abstract contraction models for discounted dynamic programming. The mission produces machine-checked versions of the general model's optimality equation, the concavity of its value function, the convexity of two of its regions, and the two-state structure theorem.

Difficulty

The paper's proofs are short and lean on facts quoted from the literature. Theorem 3.3's proof is two sentences long. Filling it in requires several facts that the paper leaves implicit. The revise region of the two-state model is a closed right-hand interval. The inspect region meets $[0,1]$ in an interval, through the affine embedding $P\mapsto(1-P,P)$ of $[0,1]$ into $S$. The half-open endpoints of the rule select optimal actions. That last point needs continuity of $V_\beta$ inside $(0,1)$, a consequence of concavity, and Lemma 3.2 at the left end. The naive reading of the printed theorem, with all three thresholds in $[0,1]$, is false in general (see below), so the threshold bookkeeping cannot be skipped.

On the general side, the optimality equation (1) is quoted from Blackwell. Here it must be proved for value iteration on the belief simplex of a countable state space, where the inspect term is an infinite series of values at the rows $e^i$. Its convergence and the contraction estimates use the boundedness of the costs.

Formalization scope

The general model is a structure over a type ι with [Countable ι], a distinguished state i₀, a transition matrix Pm, costs C I R : ι → ℝ and β. A separate predicate Model.Valid requires nonnegative entries, rows with HasSum (Pm i) 1, bounded costs and 0 < β < 1. The simplex uses HasSum P 1, never tsum, so it consists of genuine probability vectors. $V_\beta$ is defined as limUnder atTop of value iteration from $V^0=0$, which is the paper's own characterization in the proof of Lemma 2.1. It is not an arbitrary function assumed to satisfy (1). The paper's definition as an infimum over measurable policies is not formalized; the policy class would be a separate mission. Regions are subsets of $S$.

The two-state model is the instance ι = Fin 2 with $P_{00}=1-\pi$, $P_{01}=\pi$, $P_{10}=0$, $P_{11}=1$, and its value at the scalar belief $P$ is the general $V_\beta$ at $(1-P,P)$. The general Lemma 2.1 and Theorem 2.2 therefore apply to it without restatement. Standing hypotheses of §3 are $0<\beta<1$, $0\le\pi\le1$ and $0<C<I<R$. $0<C$ is implicit in the paper, where the good state costs $0$ and the bad state $C$. "$\beta$-optimal rule" means a rule selecting a minimizer of the right side of (3) at every $P\in[0,1]$, the criterion the paper quotes on p. 588. "Every $\beta$-optimal policy produces" (Lemma 3.2) means that producing is the unique minimizer.

Threshold repair. The paper prints $\pi\le P_1\le P_2\le P_3\le1$. This is false when revising is never optimal, for instance when $R>C/(1-\beta(1-\pi))$: then always producing is optimal and revising at $P=1$ is strictly worse, so no rule revising on a nonempty $[P_3,1]$ is optimal. The goal keeps $P_3\le1$ exactly when the $\beta$-optimal revise region is nonempty and otherwise allows $P_3>1$; the rest of the printed chain, $\pi\le P_1\le P_2\le1$, is kept. Adding the hypothesis $R<C/(1-\beta(1-\pi))$ instead would drop a case the paper covers.

The statement admits no trivializing reading. The thresholds are quantified existentially, but the rule must be optimal at every belief in $[0,1]$, $V_\beta$ is pinned down by its definition, and the paper's numbers ($C=4$, $\pi=0.1$, $I=6$, $R=10$, $\beta=0.9$) satisfy all hypotheses.

Infrastructure needed: tsum manipulations on the belief simplex (linearity of $T$, summability of $\sum_iP_iV(e^i)$ for bounded $V$), a sup-norm contraction argument for value iteration, and closure of concavity under minima and pointwise limits. The value-iteration and contraction lemmas are reusable for any discounted model with bounded costs. Contributions of intermediate lemmas, such as continuity of the two-state $V_\beta$ on $(0,1]$ or the bridge identities $T(1-P,P)=(1-TP,TP)$, are welcome.

Selected references

• S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9):587–596, 1971. https://doi.org/10.1287/mnsc.17.9.587
• D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X