The OR Formalization Drive

Motivation

Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit $\gamma \downarrow 0$; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.

Setting

Jobs on parallel machines. There are $n$ jobs with service times $s_i > 0$ and weights $c_i$, and $m$ identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time $C_i$ of a job is the total service time of the jobs on its machine up to and including it; the flow time is $\sum_i C_i$ and the weighted flow time $\sum_i c_i C_i$. The load of a machine is the total service time assigned to it, and $\delta_j$ is its excess over the average $S/m$. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.

The search problem (Problem 3). A stationary object is hidden in one of $n$ boxes, in box $i$ with probability $p_i$. A search of box $i$ costs $c_i$ and finds the object with probability $q_i$ if it is there. A search policy is a sequence of boxes; after $N_i$ unsuccessful searches of box $i$ the posterior probability that the object is there is proportional to $p_i(1-q_i)^{N_i}$, and the search index of the box is $p'_i q_i/c_i$, the current probability of finding the object per unit cost. The expected cost of a policy is $\sum_k c_{\sigma_k}\Pr[\text{not found by the first } k \text{ searches}]$.

Two discount factors. Bandit process $A$ (state space $S_A$, kernel $P_A$, reward $r_A$) discounts at rate $a$ and $B$ at rate $b$; a reward obtained at time $t$ is worth $a^t$ or $b^t$ times its face value according to which process produced it. The cross indices are $\nu_{AB}(x) = \sup_{\tau>0} \mathbb{E}\sum_{t<\tau} a^t r_A(x(t)) \big/ \mathbb{E}[1 - b^\tau]$ and $\nu_{BA}(y)$ with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as $\mathbb{E}\int_0^\tau b^t\,dt$ and compares $\nu_{AB}(x)$ with $\nu_{BA}(y)$ at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union $S_A \oplus S_B$.

Formalization targets

Goal: Theorem 3.6

For prior probabilities $p_i \ge 0$ summing to one, detection probabilities $0 < q_i \le 1$ and costs $c_i > 0$, a search policy is optimal if and only if at every step it searches a box of maximal current index $p'_i q_i / c_i$:

$$\text{optimal}(\sigma) \iff \forall k,\ \forall i:\ \frac{p_i (1-q_i)^{N_i(k)} q_i}{c_i} \le \frac{p_{\sigma_k}(1-q_{\sigma_k})^{N_{\sigma_k}(k)} q_{\sigma_k}}{c_{\sigma_k}}.$$

Milestones

Theorem 3.3, as the identity $\sum_i c_i C_i = \frac{\kappa}{2}\big(\sum_i s_i^2 + S^2/m + \sum_j \delta_j^2\big)$ when $c_i = \kappa s_i$; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time $t$, $A$ when $a^t \nu_{AB}(x) > b^t \nu_{BA}(y)$ and $B$ when $a^t \nu_{AB}(x) < b^t \nu_{BA}(y)$ attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on $m$ machines and that the optimal schedules are exactly those placing the $r$-th block of $m$ longest jobs at level $r$ from the end, for some order of the equal jobs.

Significance

Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time $t$ weighs the indices by $a^t$ and $b^t$, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying $0.18$ ($a = 0.9$) and $1$ ($b = 0.5$) are best played $B, B, B$ and then $A$ forever, which no stationary rule does.

None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.

Difficulty

For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as $\sum_i \ell_i s_i$ with $\ell_i$ the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.

Formalization scope

Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in $[0, \infty]$ of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, $p_i(1-q_i)^{N_i} q_i/c_i$, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an $A$-state by $P_A$ and a $B$-state by $P_B$; the payoff is the round-by-round series $\sum_t (a^t \mathbb{E}[r\mathbf 1\{A_t = A\}] + b^t \mathbb{E}[r\mathbf 1\{A_t = B\}])$, absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: $m \ge 1$, service times positive; $p_i \ge 0$, $\sum p_i = 1$, $0 < q_i \le 1$, $c_i > 0$; countable state spaces, bounded rewards, $a, b \in (0,1)$.

Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by $a^t$, $b^t$. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
• D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
• J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
• K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
• P. Nash, A generalized bandit problem, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01119.x

Motivation

Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.

Setting

There are $N$ job types $E = \{1, \dots, N\}$. A policy $\pi$ has a performance $x^\pi \in \mathbb{R}^N_+$, a vector of expectations; a permutation $\sigma$ of $E$ defines the permutation policy giving $\sigma_N$ highest and $\sigma_1$ lowest priority, and $S_k = \{\sigma_1, \dots, \sigma_k\}$ is the set of the $k$ lowest-priority types. The system satisfies GCL(1) if there are a base function $b : 2^E \to \mathbb{R}_+$ and a matrix $A = (A_i^S)$, positive on $S$ and zero off it, such that for every policy

$$\sum_{i \in S} A_i^S x_i^\pi \ge b(S) \quad (S \subseteq E), \qquad \sum_{i \in E} A_i^E x_i^\pi = b(E),$$

with equality in the first for every permutation policy whose $|S|$ lowest-priority types are $S$. GCL(2) reverses the inequality. The adaptive greedy algorithm $AG(A, r)$ picks $i_N$ maximizing $r_i/A_i^E$, sets $\bar y_E$ to the maximum, removes $i_N$, and repeats with the adjusted rewards $r_i - \sum_{j \ge k} A_i^{S_j}\bar y_{S_j}$ divided by $A_i^{S_{k-1}}$; its outputs are the order $i_1, \dots, i_N$, the dual variables $\bar y_{S_k}$ and the indices $\nu_{i_k} = \sum_{j \ge k} \bar y_{S_j}$.

For the SFABP of Section 5.3, $n$ identical bandit processes on $E$ with kernel $P$ and discount factor $a$ in the model of the Bandit Algorithms series, $x_i^\pi = \mathbb{E}^\pi \sum_t a^t I_i(t)$ is the discounted number of continuations of a bandit in state $i$, $A_i^S = \mathbb{E}[1 + a + \cdots + a^{T_i^S - 1}]$ is the discounted return time to $S$ from $i \in S$, and $b(S)$ is the minimal cost $\sum_{i \in S} A_i^S x_i^\pi$, namely $(1-a)^{-1}\mathbb{E}[a^\tau]$ with $\tau$ the number of continuations needed to bring every bandit into $S$.

Formalization targets

Goal: Theorem 5.5

For a GCL(1) system whose achievable region is convex, and any reward vector $r$: the achievable region is the polytope

$$P(A, b) = \Big\{x \in \mathbb{R}_+^N : \sum_{i \in S} A_i^S x_i \ge b(S),\ S \subset E,\ \sum_{i \in E} A_i^E x_i = b(E)\Big\};$$

its extreme points are performances of permutation policies; $AG(A, r)$ has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes $\sum_i r_i x_i^\pi$ over all policies.

Milestones

Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside $S$); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.

Significance

Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.

None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.

Difficulty

The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except $\bar y_E$ and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from $S$, and the observation that at most $\tau$ slots can be spent on bandits that have never been in $S$; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of $b(S)$ requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets $\{i_1, \dots, i_{k-2}\}$, which lie between $\{\nu < \nu(i_{k-1})\}$ and $\{\nu \le \nu(i_{k-1})\}$; ties make the induction delicate, and the statement is claimed for every tie-breaking.

Formalization scope

GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use $n$ identical bandits on Fin N in the Bandit Algorithms model, the coefficients $A_i^S$ through Mission I's stoppedTime at the return time, and $b(S)$ in the product form $(1-a)^{-1}\prod_{j : k_j \notin S}\mathbb{E}[a^{T^S_{k_j}}]$, which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is $0$ when all bandits start in $S$ where the minimal cost is $1/(1-a)$. Discount factors are in $(0, 1)$ throughout.

Trivializing readings are excluded: $A_i^S > 0$ for $i \in S$ is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 5. doi:10.1002/9780470980033
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2), 1996. doi:10.1287/moor.21.2.257
• P. Tsoucas, The region of achievable performance in a model of Klimov, IBM Research Report RC16543, 1991.
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3), 1980. doi:10.1287/opre.28.3.810
• K. D. Glazebrook, R. Garbe, Almost optimal policies for stochastic systems which almost satisfy conservation laws, Annals of Operations Research 92, 1999. doi:10.1023/A:1018992306696
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and $m$ of $n$ must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy $W$ paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy $W(x)$ at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with $W$, the bandit is indexable and $W(x)$ is its Whittle index; the Whittle index policy activates the $m$ bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as $n$ grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.

Setting

A restless bandit is a Markov decision process with two actions, active ($u = 1$) and passive ($u = 0$), each with its own transition kernel and reward. Under a deterministic stationary Markov policy $g$ with passive subsidy $W$ the reward in state $x$ is $r(x, g(x)) + W(1 - g(x))$, and the average reward from $x$ is the Cesàro limit of the expected rewards. The optimal average reward $g(W)$ is the supremum over such policies and initial states; a policy is optimal if it attains $g(W)$ from every initial state; $E_0(W)$ is the set of states in which some optimal policy is passive; the bandit is indexable if $E_0(W)$ is nondecreasing in $W$; and $W(x) = \inf\{W : x \in E_0(W)\}$.

The spinning plates asset lives on $\{1, \dots, k\}$: active moves $x \to x + 1$ at rate $\lambda(x)$, passive moves $x \to x - 1$ at rate $\mu(x)$, $\lambda(k) = \mu(1) = 0$, and $r(x)$ is earned under both actions, $r$ increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy $(y)$ is passive exactly on $\{x \ge y\}$; under it the asset alternates between $y - 1$ and $y$, spending the fraction $\phi(y) = \lambda(y-1)/(\lambda(y-1) + \mu(y))$ of its time at $y$, so its average reward is $W\phi(y) + R(y)$ with $R(y) = r(y)\phi(y) + r(y-1)(1 - \phi(y))$, and $W^*(x) = (R(x+1) - R(x))/(\phi(x) - \phi(x+1))$. The vigour bandit is the mirror image: active moves down at rate $\nu(x)$ and earns $r(x)$, passive moves up at rate $\rho(x)$ and earns nothing, $\psi(y) = \nu(y)/(\nu(y) + \rho(y-1))$, and $W^{**}(x) = (r(x)(1 - \psi(x)) - r(x+1)(1 - \psi(x+1)))/(\psi(x+1) - \psi(x))$.

Formalization targets

Goal: Theorem 6.4

For the spinning plates asset: (i) if $\phi$ is strictly decreasing over the thresholds $1 \le y \le k + 1$, the asset is indexable; (ii) if additionally $W^*$ is strictly decreasing over the states, the Whittle index is

$$W(x) = W^*(x) = \frac{R(x+1) - R(x)}{\phi(x) - \phi(x+1)}, \qquad 1 \le x \le k.$$

Milestones

Eqs. (6.9)–(6.10): the monotone policy $(y)$ earns $W\phi(y) + R(y)$ from every initial state and $g(W) = \max_y [W\phi(y) + R(y)]$, because a monotone policy always achieves $g(W)$; Theorem 6.5, the same two statements for the vigour bandit with $\psi$ increasing and $W^{**}$ increasing.

Significance

Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value $g(W)$ is the upper envelope of finitely many lines $W\phi(y) + R(y)$ whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.

None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.

Difficulty

The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle $\{z - 1, z\}$ whose average reward is that of the monotone policy $(z)$, so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly $\{x \ge x(W)\}$ for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as $\{0,1\}$-strings. The envelope argument then needs that the smallest maximizer of $\max_y [W\phi(y) + R(y)]$ is nonincreasing in $W$ when $\phi$ is strictly decreasing, and that with $W^*$ strictly decreasing the maximizer is $\le x$ exactly when $W \ge W^*(x)$. Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.

Formalization scope

Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of $\phi$ and $\psi$ (the book's "convenient positive values") replaced by their values $1, 0$ and $0, 1$ at the two extreme thresholds; the model assumptions $\lambda(k) = \mu(1) = 0$, $\nu(1) = \rho(k) = 0$, rates in $[0, 1]$, and $r$ increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict $\psi$ admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires $k \ge 1$ and positive interior rates, which Theorem 6.4's hypothesis (i) implies.

Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary $\{0,1\}$-policy to a monotone one, and the envelope lemma for lines with decreasing slopes.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 6. doi:10.1002/9780470980033
• P. Whittle, Restless bandits: activity allocation in a changing world, Journal of Applied Probability 25(A), 1988. doi:10.2307/3214163
• R. R. Weber, G. Weiss, On an index policy for restless bandits, Journal of Applied Probability 27(3), 1990. doi:10.2307/3214547
• K. D. Glazebrook, C. Kirkbride, D. Ruiz-Hernandez, Spinning plates and squad systems: policies for bi-directional restless bandits, Advances in Applied Probability 38(1), 2006. doi:10.1239/aap/1143936141
• J. Niño-Mora, Restless bandits, partial conservation laws and indexability, Advances in Applied Probability 33(1), 2001. doi:10.1017/S0001867800010661
• C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queueing network control, Mathematics of Operations Research 24(2), 1999. doi:10.1287/moor.24.2.293

Motivation

The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target $T$ (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives $\nu(\bar x, n) = \bar x + \nu(0, n)$, a scale parameter gives $\nu(\bar x, n) = \bar x\,\nu(1, n)$, and for target processes the target can be absorbed into the state, $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$. These identities are what make the tables of Chapter 8 one-dimensional.

Setting

A sampling model consists of a likelihood $f(\cdot \mid \theta)$, a family of priors $\pi(\cdot \mid p)$ on the parameter indexed by the parameters $p$ of a conjugate family, and the Bayes update $p \mapsto p_x$ of those parameters after observing $x$; the family is conjugate if the posterior of $\pi(\cdot \mid p)$ given $X = x$ is $\pi(\cdot \mid p_x)$. The predictive distribution is $f(\cdot \mid p) = \int f(\cdot \mid \theta)\pi(d\theta \mid p)$. The reward process moves from $p$ to $p_x$ with $x \sim f(\cdot \mid p)$ and earns $r(p) = \int x f(x \mid p)dx$. The target process with target $T$ moves to the completion state $C$ if $x \ge T$ and to $p_x$ otherwise, earning the current probability of success $r(p) = f([T, \infty) \mid p)$, and $0$ in $C$. A state $p$ is favourable if $r(p_{x_1 \cdots x_m}) \le r(p)$ for every finite sequence of observations $x_i < T$. For the invariance theorems the parameters are $(\bar x, n)$ with the update $((n\bar x + x)/(n+1), n+1)$; $\mu$ is a location parameter of the likelihood if $f(\cdot \mid \mu + c)$ is $f(\cdot \mid \mu)$ shifted by $c$, and $\bar x$ is a location parameter of the prior family if $\pi(\cdot \mid \bar x + c, n)$ is $\pi(\cdot \mid \bar x, n)$ shifted by $c$; scale parameters are defined with $x \mapsto bx$, $b > 0$. The Gittins index is that of the Bandit Algorithms model on these chains.

Formalization targets

Goal: Theorem 7.9 (in the form of Corollary 7.10)

If $\mu$ is a location parameter of a reward process with a conjugate prior family in which $\bar x$ is a location parameter and the parameters update as the sample mean and count, then for every $n > 0$

$$r(\bar x + c, n) = r(\bar x, n) + c \quad\text{and}\quad \nu(\bar x, n) = \bar x + \nu(0, n),$$

under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.

Milestones

Proposition 7.4 (favourable state: $\nu = r$); Example 7.5 (Bernoulli target process, $\nu(\alpha, \beta) = \alpha/(\alpha + \beta)$); Example 7.6 (normal target process with known variance, $\nu(\bar x, n) = \Phi(\bar x (1 + n^{-1})^{-1/2})$ for $\bar x \ge 0$); Theorem 7.11 (scale parameter: $\nu(\bar x, n) = \bar x\,\nu(1, n)$); Theorem 7.17 (target process with a location parameter: $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$).

Significance

Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of $n$ alone and that of the exponential process as a function of $n$ and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.

None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.

Difficulty

The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by $c$ times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most $r(p)$, which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of $\bar x_m (1 + 1/(n+m))^{-1/2}$ in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that $\alpha/(\alpha + \beta + m)$ decreases.

Formalization scope

The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters $(\bar x, n)$ it is required on $n > 0$ only (IsConjugateOn): a proper prior has $n > 0$, and conjugacy at every $(\bar x, n) \in \mathbb{R}^2$ is impossible with a location parameter, since at $n = -1$ the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: $a \in (0, 1)$; integrable observations and L&S Assumption 35.6 for the reward processes; $n > 0$ for the invariance theorems and $\bar x > 0$ for the scale theorem; $\alpha, \beta > 0$; $\bar x \ge 0$ and $n > 0$ for the normal example.

Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 7. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 1974.
• D. M. Jones, Search Procedures for Industrial Chemical Research, PhD thesis, University of Wales, 1975.
• H. Raiffa, R. Schlaifer, Applied Statistical Decision Theory, Harvard University Press, 1961.
• T. S. Ferguson, Mathematical Statistics: A Decision Theoretic Approach, Academic Press, 1967.
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 34–35. doi:10.1017/9781108571401

Motivation

The free energy principle (FEP) proposes that a self-organizing system — a brain, an organism, an agent — persists by minimizing one quantity: the variational free energy of its sensory states under an internal generative model. Introduced by Karl Friston as a principle of brain function [Friston 2006] and stated in its unified form [Friston 2010], the principle makes a precise mathematical claim at its core: whatever internal state estimate the system holds, the free energy of incoming data is never below the data's surprisal (negative log marginal likelihood), and the excess is exactly the Kullback–Leibler divergence between the system's recognition density and the Bayesian posterior implied by the model. Active inference extends the same functional from perception to action and planning [Friston et al. 2017], and the same bound is known in machine learning as the evidence lower bound (ELBO) of variational inference [Parr et al. 2022].

Timeline of the mathematical content this mission formalizes:

• 2006 — Friston, A free energy principle for the brain (J. Physiol. Paris 100): the bound stated for perception as variational inference on a generative model.
• 2010 — Friston, The free-energy principle: a unified brain theory? (Nat. Rev. Neurosci. 11, 127–138): free energy as an upper bound on surprisal, presented as the core of a unified account.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory (Neural Comput. 29(1), 1–49): the same functional drives policy selection through expected free energy.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): textbook treatment; the posterior-form identity $F = D_{\mathrm{KL}}(Q\,\|\,P(s|o)) - \log P(o)$ as the central equation.
• 2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 Free Energy Principle topics, compiled with zero proof holes against a pinned Mathlib. This mission transcribes the catalogue's core-free-energy chain — topic fep-002 and the foundation module active_inference — onto the platform, turning the first link of the FEP development into solvable community infrastructure.

Setting

Everything is finite, and laws are normalized real mass functions.

A finite law on a finite type $\alpha$ is a function $p : \alpha \to \mathbb{R}$ with $p(x) \ge 0$ for every $x$ and $\sum_x p(x) = 1$. A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row over $\beta$. The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence

$$D_{\mathrm{KL}}(p\,\|\,q) \;=\; \sum_{x} q(x)\cdot \mathrm{klFun}\!\left(\frac{p(x)}{q(x)}\right), \qquad \mathrm{klFun}(x) = x\log x + 1 - x,$$

a totalized real-valued divergence that is finite even at zero-mass atoms (the convention $0 \cdot \log 0 = 0$ via Real.negMulLog) and nonnegative on normalized laws.

A finite generative model for active inference (definition Def_fep_generative_model) over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ consists of: an initial state law $P(s)$; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ and the outcome law $P(o \mid \pi)$. A recognition density is any finite law $Q$ over states — the system's internal estimate. At an outcome $o$ with positive predicted mass, the Bayesian posterior $P(\cdot \mid o, \pi)$ is the exact finite Bayes rule. The outcome surprisal is $-\log P(o \mid \pi)$, and the posterior-form variational free energy of a recognition density $Q$ is

$$F[Q, o, \pi] \;=\; D_{\mathrm{KL}}\big(Q \,\|\, P(\cdot \mid o, \pi)\big) \;-\; \log P(o \mid \pi).$$

Formalization targets

Goal: the variational free-energy bound

For every generative model, every policy $\pi$, every outcome $o$ with $P(o\mid\pi) > 0$, and every recognition density $Q$:

$$-\log P(o \mid \pi) \;\le\; F[Q, o, \pi].$$

The recognition density $Q$ is universally quantified — the bound holds for whatever state estimate the system happens to carry.

Exactness, uniqueness, and the ELBO form

Three companions pin down the equality case, ordered weakest to strongest alongside the milestone list:

• Exactness — the Bayesian posterior attains the bound:

$$F\big[P(\cdot \mid o, \pi),\, o,\, \pi\big] = -\log P(o \mid \pi).$$

• Uniqueness — equality characterizes the posterior, with no full-support assumption:

$$F[Q, o, \pi] = -\log P(o \mid \pi) \iff Q = P(\cdot \mid o, \pi).$$

• ELBO form — negating both sides:

$$-F[Q, o, \pi] \;\le\; \log P(o \mid \pi).$$

Measure-theoretic core

Independently of the finite model, in Mathlib's nonnegative extended reals $\mathbb{R}_{\ge0} \cup \{\infty\}$, with $q$, $p$ measures on any measurable space and $s \in \mathbb{R}_{\ge0} \cup \{\infty\}$:

$$s \;\le\; s + D_{\mathrm{KL}}(q \,\|\, p),$$

the unconditional shape of the bound (topic fep-002 of the source catalogue), with the divergence taken as $\infty$ when the log-likelihood ratio is not integrable.

Significance

The result itself. This inequality is the load-bearing step of the FEP: it converts "minimize free energy" into "move recognition toward the posterior," and it is the exact statement whose continuous, dynamic, and policy-selecting extensions (expected free energy, Markov blankets, non-equilibrium thermodynamics) form the rest of the FEP literature. Without it, the principle's variational step has no mathematical content.

Formalizing it. The mathematics here is classical — Gibbs' inequality — and the source development already proves every row with no proof holes. What the mission adds is faithful, reusable infrastructure: the definitions are published as platform nodes in the shared namespace FreeEnergyPrinciple, so later missions in this programme (expected free energy and policy selection, Markov blankets, Gaussian and continuous-time variants, already proved in the source repository) can import them instead of re-deriving the substrate. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.

Difficulty

The bound itself is a one-line consequence of KL nonnegativity — the naive idea "prove it by simp on the KL sum" is essentially right, and the source proofs are correspondingly short. The actual difficulty is boundary precision, where plausible renderings go silently wrong:

• The positivity premise $P(o \mid \pi) > 0$ is not decoration: the Bayesian posterior is defined only where the evidence has positive mass, and hiding that in a totalized division would change the statement.
• The uniqueness characterization is not a formality: at zero-mass reference atoms the logarithmic cross-entropy identity degenerates, and the proof needs the normalization lemma $D_{\mathrm{KL}}(p\,\|\,q) = 0 \leftrightarrow p = q$, which forces the recognition law's mass to zero wherever the posterior's is zero. A solver who proves the bound but states equality with a full-support hypothesis has proved something different from the source.
• The measure-theoretic core is deliberately unconditional; adding finiteness side conditions to it would weaken the source's point that $\mathbb{R}_{\ge0} \cup \{\infty\}$ absorbs the degenerate cases.

A vacuous formalization — quantifying over a single distinguished recognition law, or taking "posterior" as an arbitrary variable — would trivialize the goal; the targets below rule this out by fixing the exact finite Bayes rule and universally quantifying $Q$.

Formalization scope

Committed conventions of this mission's Lean development:

• All model carriers are finite types (Fintype); laws are $\mathbb{R}$-valued normalized mass functions; kernels are normalized rows. No measure-theoretic machinery below the finite substrate except for the measure-theoretic core milestone.
• KL is the totalized real-valued finite divergence $D_{\mathrm{KL}}(p\,\|\,q) = \sum_x q(x)\cdot \mathrm{klFun}(p(x)/q(x))$; entropy uses Real.negMulLog, so $0 \cdot \log 0 = 0$ exactly, not by exception-handling.
• The posterior is the exact finite Bayes rule FiniteKernel.posterior, taken at the explicit hypothesis $0 < P(o \mid \pi)$.
• One mission-wide namespace FreeEnergyPrinciple; definitions live in the published definition files Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model, and every theorem item imports them. A Free Energy Principle II mission (expected free energy) is expected to reuse the same namespace and definitions.
• The measure-theoretic core uses Mathlib's InformationTheory.klDiv in ℝ≥0∞ with no finiteness hypotheses.
• Contributions welcome: alternative measure-theoretic renderings of the core bound, the Gaussian instantiation of the same identity, and ports of the source repository's subsequent rows (Bayesian model reduction, expected free energy) onto these definitions.

Selected references

• K. Friston, A free energy principle for the brain, Journal of Physiology (Paris) 100 (2006) 70–87. https://doi.org/10.1016/j.jphysparis.2006.10.001
• K. Friston, The free-energy principle: a unified brain theory?, Nature Reviews Neuroscience 11 (2010) 127–138. https://doi.org/10.1038/nrn2787
• K. Friston, T. FitzGerald, F. Rigoli, P. Schwartenbeck, G. Pezzulo, Active inference: a process theory, Neural Computation 29 (2017) 1–49. https://doi.org/10.1162/neco_a_00912
• T. Parr, G. Pezzulo, K. J. Friston, Active Inference: The Free Energy Principle in Mind, Brain, and Behavior, MIT Press (2022). https://mitpress.mit.edu/9780262045354/active-inference/
• D. A. Friedman, fep_formal: Towards Lean 4 Formalization of the Free Energy Principle (v1.2.0), Active Inference Institute (2026), the formal source of truth for this mission. https://github.com/ActiveInferenceInstitute/fep_formal
• D. A. Friedman, Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, Active Inference Journal (2026). https://doi.org/10.5281/zenodo.19699233

Motivation

The bilinear program

$$\min_{(x,y)} \; c^T x + x^T A y + d^T y \quad \text{subject to} \quad x \in X,\ y \in Y,$$

with $X \subseteq \mathbb{R}^p$ and $Y \subseteq \mathbb{R}^q$ polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on $x$ and on $y$ are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of $X \times Y$ (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set $S$ of pairs $(x, y)$, so that constraints may couple $x$ and $y$. They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.

Setting

Write points of $\mathbb{R}^p \times \mathbb{R}^q$ as $(x, y)$, and let $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ be a nonempty compact set. No convexity of $S$ is assumed. Let $\varphi : \mathbb{R}^p \times \mathbb{R}^q \to \mathbb{R}$ be continuous on $S$.

The function $\varphi$ is biconcave over $S$ (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside $S$: for every fixed $y$, the map $x \mapsto \varphi(x, y)$ is concave on every convex set $C$ with $C \times \{y\} \subseteq S$; and for every fixed $x$, the map $y \mapsto \varphi(x, y)$ is concave on every convex set $D$ with $\{x\} \times D \subseteq S$. Equivalently, $\varphi$ is concave along every segment of $S$ that is parallel to the $x$-block or to the $y$-block. A bilinear objective $f(x) + x^T y + g(y)$ with $f$ and $g$ concave is biconcave; joint concavity of $\varphi$ is not required.

The boundary $\partial S$ is the topological frontier of $S$ in $\mathbb{R}^p \times \mathbb{R}^q$: the closure of $S$ minus its interior. A solution of $\min\{\varphi(x,y) : (x,y) \in S\}$ is a point $z \in S$ with $\varphi(z) \le \varphi(w)$ for all $w \in S$ (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is $d\big((x,y),(x',y')\big) = \sqrt{\|x-x'\|^2 + \|y-y'\|^2}$.

Formalization targets

Goal: Theorem 1 (p. 274)

If $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ ($p + q \ge 1$) is nonempty and compact, and $\varphi$ is continuous on $S$ and biconcave over $S$, then

$$\exists\, z^* \in \partial S \quad \text{with} \quad \varphi(z^*) = \min\{\varphi(x, y) : (x, y) \in S\}.$$

The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on $\partial S$ (a constant $\varphi$ is a counterexample to that).

Milestones

1. Proof of Theorem 1, p. 274. If $(\bar x, \bar y) \in \operatorname{int} S$ and $(x^*, y^*) \in \partial S$ is a nearest boundary point in Euclidean distance $d^*$, then the closed Euclidean ball of radius $d^*$ about $(\bar x, \bar y)$ lies in $S$, and with $(s,t) = 2(\bar x, \bar y) - (x^*, y^*)$ the points $(s,t)$, $(x^*, t)$ and $(s, y^*)$ are feasible.
2. Proof of Theorem 1, p. 275, first display. For $\varphi$ biconcave over $S$ and segments $[x^*, s] \times \{\tfrac12 y^* + \tfrac12 t\}$, $\{x^*\} \times [y^*, t]$, $\{s\} \times [y^*, t]$ inside $S$,

$$\varphi\big(\tfrac12(x^*,y^*) + \tfrac12(s,t)\big) \ge \tfrac12\varphi(x^*, \tfrac12y^*+\tfrac12t) + \tfrac12\varphi(s, \tfrac12y^*+\tfrac12t) \ge \tfrac14\big[\varphi(x^*,y^*)+\varphi(x^*,t)+\varphi(s,y^*)+\varphi(s,t)\big].$$

3. Example, p. 274. The program $\min\{-x + xy - y : -6x + 8y \le 3,\ 3x - y \le 3,\ 0 \le x, y \le 5\}$ has the solution $(7/6, 1/2)$, which is not an extreme point of the feasible region, and no extreme point is a solution.
4. Example, p. 274. $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$, the first of which is not global.

Significance

Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to $\partial S$, and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.

The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.

Difficulty

The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. $S$ need not be convex, so it has no useful extreme-point structure, and $\varphi$ is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.

What remains is local geometry around an interior minimizer: one must find points of $S$ around it at which biconcavity can be applied in both blocks, and control their membership in $S$ without convexity. The feasibility of the mixed points $(x^*, t)$ and $(s, y^*)$, which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.

Formalization scope

• Points are pairs in EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.
• The theorem is the "more general context" of p. 274, independent of the paper's Problem 𝒫: the standing assumptions (a)–(c) of p. 274 (convex $f$, $g$; closed convex $S$; a box $\Omega$) do not enter.
• Hypotheses of the goal: IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on $S$), and BiconcaveOn S φ. One hypothesis is added: $0 < p + q$. For $p = q = 0$ the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.
• Biconcavity is read over $S$: concavity on every convex subset of each section of $S$. Assuming instead concavity of each partial function on the whole space would be a stronger hypothesis and a weaker theorem.
• Trivializing formalizations ruled out: the statement assumes neither joint concavity of $\varphi$ nor convexity of $S$ (either would reduce it to the Bauer principle), and it covers sets with nonempty interior; the case of empty interior, where $\partial S = S$, is included but is not the only case.
• Corrected misprint (milestone 3): the paper prints the solution of example 3 as $(7/16, 1/2)$. That point has objective value $-23/32$, while the feasible vertex $(1,0)$ has value $-1$. On the edge $3x - y = 3$ the objective equals $3x^2 - 7x + 3$, minimized at $x = 7/6$, value $-13/12$, the global minimum. The Lean states the corrected point $(7/6, 1/2)$; the milestone text is kept verbatim.
• In milestone 4, "local solution" is IsLocalMinOn relative to the box, and non-globality of $(-1, 3)$ records the paper's word "proper".
• Infrastructure needed: nearest boundary points of compact sets (Mathlib has IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.

Selected references

• Faiz A. Al-Khayyal and James E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
• James E. Falk, A Linear Max-Min Problem, Mathematical Programming 5:169–188, 1973. https://doi.org/10.1007/BF01580119
• Hiroshi Konno, A Cutting Plane Algorithm for Solving Bilinear Programs, Mathematical Programming 11:14–27, 1976. https://doi.org/10.1007/BF01580367
• Olvi L. Mangasarian, Equilibrium Points of Bimatrix Games, Journal of the Society for Industrial and Applied Mathematics 12(4):778–780, 1964. https://doi.org/10.1137/0112064
• Heinz Bauer, Minimalstellen von Funktionen und Extremalpunkte, Archiv der Mathematik 9:389–393, 1958. https://doi.org/10.1007/BF01900582

Motivation

Bilinear programs, which minimize an objective containing a term $x^\top y$ over constraints on $x$ and $y$, model pooling and blending in petroleum refining, location–allocation, certain dynamic production problems and many other applications (Konno 1971, surveyed in Al-Khayyal and Falk 1983, p. 274). The term $x^\top y$ is not convex, so such problems can have local minima that are not global. For example, $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$. When $x$ and $y$ are constrained separately, a solution lies at an extreme point of the feasible region, and vertex-enumeration and cutting-plane methods apply. When the constraints couple $x$ and $y$, this property is lost.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) gave a branch-and-bound algorithm for this jointly constrained case. It lower-bounds the objective on each box by the convex envelope of the bilinear term, and they proved that it converges to a global solution. The closed form of that envelope, found independently by McCormick (1976) and now called the McCormick envelope, underlies the bilinear relaxations of modern global solvers.

Timeline:

• 1969, Falk and Soland: a branch-and-bound scheme for separable nonconvex programs using convex envelopes, the pattern this algorithm follows.
• 1976, McCormick: convex underestimators of factorable functions, including the envelope of $xy$ on a rectangle.
• 1983, Al-Khayyal and Falk: the envelope of $xy$ over a rectangle (Theorem 2), the branch-and-bound algorithm for jointly constrained biconvex programs, and a proof of its convergence.

Setting

Fix $n \ge 1$ and a box $\Omega = \{(x,y) \in \mathbb{R}^n \times \mathbb{R}^n : l \le x \le L,\ m \le y \le M\}$ with coordinate rectangles $\Omega_i = [l_i, L_i] \times [m_i, M_i]$. Problem $\mathcal P$ is

$$\min\ \varphi(x,y) = f(x) + x^\top y + g(y) \quad \text{subject to } (x,y) \in S \cap \Omega,$$

with $f$, $g$ convex (and continuous) on their boxes, $S$ closed and convex, and $S \cap \Omega \neq \emptyset$. Its optimal value is $v^*$.

The convex envelope $\mathrm{Vex}_B\, h$ of a function $h$ over a set $B$ is the pointwise supremum of all convex functions that underestimate $h$ on $B$. For a box $B$, the node function $\psi^B(x,y) = f(x) + \mathrm{Vex}_B\, x^\top y + g(y)$ is convex and lies below $\varphi$ on $B$. The subproblem at node $B$, minimizing $\psi^B$ over $S \cap B$, is a convex program.

A run of the algorithm is a sequence of stages. Stage $0$ has the single open node $\Omega$. At stage $k$ the Best Bound Rule selects an open node $B_k$ whose subproblem value is least, and the stage point $(x^k, y^k)$ is its subproblem solution. The best lower bound is $v_b^k = \psi^{B_k}(x^k, y^k)$ and the best upper bound is $V_b^k = \min_{l \le k} \varphi(x^l, y^l)$. The selected node is then split. The algorithm picks the coordinate $I$ with the largest gap $x^k_i y^k_i - \mathrm{Vex}_{(B_k)_i}\, x_i y_i$ and replaces the rectangle $(B_k)_I$ by the four subrectangles cut out by the point $(x^k_I, y^k_I)$ (Figure 1 of the paper). All other rectangles are kept. The stage function $\psi^k$ assigns to each point of $\Omega$ the least node value $\psi^B$ among the open boxes containing it.

Formalization targets

Goal: convergence to a global solution

For every run,

$$\text{every accumulation point } (\bar x, \bar y) \text{ of } (x^k, y^k) \text{ solves } \mathcal P, \qquad \lim_k v_b^k = v^* = \lim_k V_b^k .$$

Milestones

In attack order:

• Theorem 2: $\mathrm{Vex}_\Omega\, xy = \max\{mx + ly - lm,\ Mx + Ly - LM\}$ on a rectangle.
• Theorem 3: the envelope is exact on the rectangle's boundary.
• The Corollary, in two parts:
  • separability, $\mathrm{Vex}_\Omega\, x^\top y = \sum_i \mathrm{Vex}_{\Omega_i}\, x_i y_i$;
  • exactness at points whose every coordinate pair lies on $\partial\Omega_i$.
• Along runs: $\psi^k \le \psi^{k+1} \le \varphi$ on $\Omega$.
• The bound chain $v_b^1 \le v_b^2 \le \cdots \le v^* \le \cdots \le V_b^2 \le V_b^1$.
• Termination when $v_b^k = V_b^k$.
• The gradient bound $\gamma_i$.
• The equicontinuity estimate $\|z - w\| < \varepsilon/(n\gamma) \Rightarrow |\mathrm{Vex}_B\, x^\top y(z) - \mathrm{Vex}_B\, x^\top y(w)| < \varepsilon$ within every sub-box $B$.
• The limit identity: along a convergent subsequence of stage points, $v_b^{k_t} \to \varphi(\bar x, \bar y)$.

Theorem 4 of the paper, on the envelope of $\sum f_i(x_i) + x^\top y + \sum g_i(y_i)$ with concave $f_i, g_i$, is included as a further target.

Significance

The convergence theorem certifies that the algorithm computes the global optimum of a nonconvex problem. It is not a local search. Its ingredients carry over to spatial branch-and-bound in general: envelopes that are exact on the boundary of their box, a subdivision at the relaxation's solution, and best-bound selection. Theorem 2 and its separable extension are the building block of McCormick relaxations, used for bilinear terms throughout global optimization.

As far as is known, none of these results is formalized. The mission produces a formal model of a spatial branch-and-bound procedure with rectangular subdivision at the relaxation solution, together with the convex-envelope facts it rests on. The paper's convergence proof is informal and, as printed, passes through two claims that do not hold (see Formalization scope). A machine-checked proof of the convergence theorem would settle the result on firm ground.

Difficulty

The algorithm splits at the relaxation's solution, not at the midpoint, so the boxes of a run need not shrink to points. The usual "exhaustive subdivision" argument, in which the diameters of nested boxes tend to zero, does not apply. What makes the gap close is Theorem 3: after a split, the split point sits on the boundary of the new rectangles in the split coordinate, where the envelope is exact. That exactness has to be carried from the selected points to their accumulation points, across coordinates that may be split finitely or infinitely often. The obvious route through a continuous limit of the stage functions is not available, because the stage functions are not continuous in general.

Formalization scope

Vectors are Fin n → ℝ, points are pairs in (Fin n → ℝ) × (Fin n → ℝ), and boxes are four bound vectors, degenerate boxes allowed. The convex envelope is the paper's definition, the real supremum of values of convex minorants, and is used only at points of convex boxes. The McCormick closed form is Theorem 2, a target, and is not built into any definition. A run is a predicate on four sequences: open nodes as a multiset of boxes, selected node, branching index, stage point. Stages are numbered from $0$ and runs are infinite: the stopping test is ignored, so a run stopped by the paper is a prefix of one. The optional pruning of p. 278 is omitted, and ties are arbitrary. The optimal value enters through IsMinOn, not through an infimum. The Euclidean distance on $\mathbb{R}^{2n}$ is written out explicitly.

Hypotheses and corrections relative to the page:

• Continuity of $f$ and $g$ on their boxes is added; the paper uses it without stating it. $n > 0$ is assumed. The box form of convexity (p. 276) is used.
• Corollary, second clause (p. 276): "for all $(x,y) \in \partial\Omega$" is false for $n \ge 2$ (take $\Omega_1 = \Omega_2 = [0,2]^2$, $x = y = (0,1)$). It is stated for points with every $(x_i, y_i) \in \partial\Omega_i$.
• Well-definedness of the stage function (p. 277) is false from stage 3 on. Two open boxes can share a point at which their node functions differ, and the stage function then jumps. It is not a target. The stage function takes the minimum over the open boxes containing a point, and the continuity asserted on p. 279 is not formalized. The piecewise convexity asserted there is formalized as convexity of each open node function on its box.
• Equicontinuity (p. 282): the display $|H_i^{kj}(x_i,y_i) - H_i^{kj}(u_i,v_i)| \le |x_i y_i - u_i v_i|$ is false, and so is equicontinuity of the stage functions on all of $\Omega$. The estimate is stated within each sub-box, with the paper's $\delta = \varepsilon/(n\gamma)$.

Two trivializations are excluded. The goal is not a statement about an arbitrary sequence of boxes and points whose gap tends to zero: it quantifies over runs of the algorithm as defined, and a separate well-posedness item, run_exists, asserts that runs exist for every instance. Theorem 2 is about the supremum of convex minorants, not about a function defined by the closed form.

Reusable beyond this mission: the convex envelope and its bilinear closed form, and the box-splitting model. Contributions welcome: proofs of the envelope theorems, a proof of run_exists, and a convergence proof that avoids the false intermediate claims.

Selected references

• F. A. Al-Khayyal and J. E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
• J. E. Falk and R. M. Soland, An Algorithm for Separable Nonconvex Programming Problems, Management Science 15(9):550–569, 1969. https://doi.org/10.1287/mnsc.15.9.550
• G. P. McCormick, Computability of Global Solutions to Factorable Nonconvex Programs: Part I — Convex Underestimating Problems, Mathematical Programming 10:147–175, 1976. https://doi.org/10.1007/BF01580665
• H. Konno, Bilinear Programming: Part II. Applications of Bilinear Programming, Technical Report 71-10, Operations Research House, Stanford University, 1971 (reference [10] of Al-Khayyal and Falk; no online copy known). https://doi.org/10.1287/moor.8.2.273