The OR Formalization Drive

Motivation

Alternating-offer bargaining asks how an agreement is selected when two people can keep making proposals until one accepts. A prediction based only on behavior at the start may rely on threats that would no longer be sensible after a rejection. Ariel Rubinstein's 1982 paper studies strategies after every possible sequence of offers and gives a characterization of the partitions compatible with perfect equilibrium. Its setting has a unit pie, complete information, no fixed last round, and preferences that may describe more than a particular discount formula.

The question matters for sequential bargaining models in which the order of moves and the cost of delay affect the agreement. The paper distinguishes the set obtained when player 1 offers first from the set obtained when player 2 offers first. It also provides applications to fixed bargaining costs and fixed discount factors. This mission targets the paper's general characterization, from which those examples can be studied without building a new equilibrium concept for each preference family.

Setting

A partition is a number $s\in S=[0,1]$: player 1 receives $s$ of the unit pie and player 2 receives $1-s$. An outcome $(s,t)$ means that the offer $s$ is accepted in period $t$; $(0,\infty)$ denotes perpetual disagreement. Periods of actual play start at 1. The paper also uses $(s,0)$ when comparing acceptance of a current offer with a future outcome. Each player $i\in\{1,2\}$ has a complete, reflexive, transitive preference relation $\succcurlyeq_i$ on outcomes. Strict preference $\succ_i$ and indifference $\sim_i$ are derived from it.

The game alternates proposals and responses. One player offers a partition, the other accepts or rejects, and rejection makes the responder the next proposer. A strategy specifies what a player does after every possible history, including histories inconsistent with the player's earlier plans. A perfect equilibrium requires the relevant player's continuation to withstand every alternative continuation strategy at each rejected history and to make a planned acceptance or rejection consistent with the current offer. The empty history is included, so the opening proposer must also have no profitable deviation.

Write $A$ for the set of player-1 shares reached by perfect equilibria when player 1 opens, and $B$ for the corresponding set when player 2 opens. Perpetual disagreement contributes no share to either set. Define $\Delta\subseteq S\times S$ by a pair of one-period thresholds: for $(x,y)\in\Delta$, $y$ is the smallest share whose immediate acceptance player 1 weakly prefers to $(x,1)$, and $x$ is the largest share whose immediate acceptance player 2 weakly prefers to $(y,1)$. Let $\Delta_1$ and $\Delta_2$ be its coordinate projections. All four sets contain numbers interpreted as player-1 shares, even when player 2 moves first. These are the objects of Sections 2–5.

Formalization targets

Characterization

Under the paper's five preference assumptions (A-1)–(A-5), the goal is its THEOREM on p. 106:

$$A=\Delta_1\ne\varnothing,\qquad B=\Delta_2\ne\varnothing,$$

with $A$ and $B$ nonempty closed intervals and some $e\ge 0$ satisfying

$$B=\{a-e:a\in A\}.$$

The translation parameter is allowed to be zero, and either interval may be a single point. The goal fixes the paper's general shape without choosing a particular utility representation or assuming immediate agreement in every equilibrium.

Milestone statements

The attack path follows Lemmas 1–4 and Propositions 1–4 in their printed order. The lemmas constrain how a partition in one opening order relates to a feasible continuation in the other. Proposition 1 places each pair in $\Delta$ inside $A\times B$; Proposition 2 asserts existence; Proposition 3 describes $\Delta$ as a closed segment parallel to the diagonal; Proposition 4 gives the reverse containment of $A$ and $B$ in the threshold projections. Each numbered result is a separate theorem target.

Significance

The theorem identifies the full set of equilibrium partitions from preference comparisons one period apart. Nonemptiness says the model admits at least one equilibrium partition in either opening order. The interval conclusion describes cases with multiple equilibrium shares, while the translate relation states exactly how reversing the first mover changes the two sets. In the paper's discounting example, a single share is selected under the stated parameter conditions; in a fixed-cost boundary case, multiple shares can occur. These are applications in Section 6, not assumptions of the general target.

Rubinstein proved the result in 1982. Here the definitions and theorem statements are Lean drafts; the numbered targets and the main theorem still require machine-checked proofs. A local verification module establishes that one discounting instance satisfies the first three axioms and that the paper's Section 3 strategy example accepts its first offer in period 1. Completing the mission would give a reusable formal account of an infinite-horizon alternating-offer game and its subgame equilibrium conditions, alongside the paper's characterization.

Difficulty

A first-round equilibrium condition does not control what a strategy promises after an offer is rejected. The paper's equilibrium definition checks the entire continuation at every history, with the player's role changing after each rejection. As a result, showing that a proposed share is an equilibrium partition requires more than checking the opening offer: the answer and the next proposal must remain consistent throughout the game tree. The model also allows arbitrary complete preferences satisfying axioms, so a calculation with one discount function cannot establish the general theorem.

The boundary at a zero share requires care. Assumption (A-2) asserts strict preference for earlier positive shares; it says nothing directly about a player receiving zero. The printed proof of Lemma 1 invokes it for a comparison that can occur at that boundary. The local lemma drafts explicitly carry the paper's (A-4) closedness axiom to support that comparison. This added assumption, and its propagation to Lemmas 2–4, is disclosed in the audit notes rather than silently attributed to the Section 4 statement.

Formalization scope

Lean represents $S$ as the subtype of real numbers in $[0,1]$. Outcomes are an option type: an agreement contains a partition and a natural-number period, while none is perpetual disagreement. This prevents an endless play from acquiring a default last partition. Strategies are unrestricted functions of lists of past offers. The play uses the first accepted offer, with period number one greater than its zero-based sequence index. A subgame after a rejected history restarts the period count and swaps the opening role when the history has odd length. The perfect-equilibrium predicate includes the empty history; acceptance comparisons use period 0 for the offer already on the table.

The threshold correspondence uses actual least and greatest elements among partitions in $S$. No real infimum or supremum supplies a default for an empty candidate set. “Closed interval” in the goal means an explicit $[\ell,u]$ with $\ell\le u$. “$A-e$” is the image of $A$ under $a\mapsto a-e$. Proposition 3's “parallel line segment” is the full image of a nonempty interval under $x\mapsto(x,x-e)$. These readings exclude a vacuous equilibrium set, a disagreement-to-zero coercion, and a hard-coded discounting special case.

The common outcome and preference definitions, the history-based strategy and play, and the equilibrium predicate are reusable for other alternating-offer questions. Contributions toward their structural properties, the numbered milestones, and the full theorem are in scope. The two displayed claims inside proofs and the fixed-cost and discounting conclusions are deferred to keep this proposal on the theorem's numbered path. Existing platform entries on Nash's axiomatic bargaining solution and a sealed-offer double auction concern different objects; neither supplies this game's equilibrium definition.

Selected references

• Ariel Rubinstein, Perfect Equilibrium in a Bargaining Model, Econometrica 50(1), 97–109, 1982. DOI 10.2307/1912531.

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$. Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$. A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$. Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$. There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$. If the price changes at deterministic time $s\in[0,t]$, let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$, and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$. The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$, is a stopping time for the history of $N_1$, and occurs before stock is exhausted almost surely. At $s=0$, $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$, switching immediately earns the optimal value; when $t>x_n$, a correction $F(n,t)$ is added:

$$J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}$$

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$. For $n\ge1$, set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$, where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$. A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$, the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$.

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$. Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$, the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

• Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

Why priority queues with cheap decrease key matter

Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with $n$ vertices and $m$ edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in $O(\log n)$ worst-case time.

Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take $O(\log n)$ amortized time and every other operation, decrease key included, takes $O(1)$ amortized time. This brings Dijkstra's algorithm to $O(n \log n + m)$ and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.

Setting

An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank $r(x)$ of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.

Linking two trees with roots $x$ and $y$ makes $y$ the last child of $x$ if the key of $x$ is smaller, and otherwise makes $x$ the last child of $y$; the root that becomes a child is unmarked. The operations act as follows:

• make heap adds an empty heap; find min acts on a nonempty heap and returns a root of minimum key; insert adds a one-node tree for a new item; meld concatenates two root lists.
• delete min removes a root $x$ of minimum key, adds the children of $x$ to the roots, then repeats the linking step, "find any two trees whose roots have the same rank, and link them", in any order, until all root ranks are distinct.
• decrease key $(\Delta, i, h)$, $\Delta \ge 0$, lowers the key of $i$ and, if the node $x$ of $i$ is not a root, cuts $x$ from its parent, making its subtree a new tree. delete $(i, h)$ cuts $x$ the same way, destroys it and adds its children to the roots; a minimum root is deleted as in delete min.
• After every cut of a child of $p$, if $p$ is not a root it is marked if unmarked and cut from its own parent if marked: a cascading cut, which may repeat upwards.

The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential $\Phi$ of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of $\Phi$.

Formalization targets

Goal: THEOREM 1 (p. 604)

There is an absolute constant $C > 0$ such that for every sequence of $T$ operations started from no heaps, with $n_t$ the number of items in the heap that operation $t$ acts on, just before it acts,

$$\sum_{t<T} \mathrm{cost}_t \;\le\; \sum_{t<T} b_t, \qquad b_t = \begin{cases} C(\log_2 n_t + 1) & \text{delete min or delete},\\ C & \text{otherwise.}\end{cases}$$

The paper's wording is "the total time is at most the total amortized time, where the amortized time is $O(\log n)$ for each delete min or delete operation and $O(1)$ for each of the other operations"; the goal pins the $O(\cdot)$ to one constant and does not name the potential.

Milestones

1. LEMMA 1: the $i$th child of a node, in linking order, has rank at least $i - 2$.
2. $F_{k+2} \ge \varphi^k$, with $F_k$ the Fibonacci numbers and $\varphi = (1+\sqrt5)/2$.
3. COROLLARY 1: a node of rank $k$ has at least $F_{k+2} \ge \varphi^k$ descendants, itself included.
4. A node of rank $k$ in an $n$-item heap has $\varphi^k \le n$, hence $k \le \log n / \log\varphi$.
5. make heap, find min and meld leave $\Phi$ unchanged; insert raises it by one.
6. delete min raises $\Phi$ by at most $\log n / \log \varphi$ minus the number of linking steps.
7. decrease key raises $\Phi$ by at most three minus the number of cascading cuts.
8. From no heaps, the total amortized time bounds the total actual time.

Significance

THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in $O(n\log n + m)$, all-pairs shortest paths and the assignment problem in $O(n^2 \log n + nm)$, and minimum spanning trees in $O(m\,\beta(m,n))$.

The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.

Difficulty

The obvious argument, that every tree is a binomial tree and so every rank is at most $\log_2 n$, fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank $k$ can be left with only $k+1$ descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.

Formalization scope

All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.

Logarithms in the goal are base 2 (footnote 1, p. 600), with a $+1$ so that one-item heaps have positive budget. The paper's constant "$\le 1.4404 \log n$" on p. 604 is a rounding slip ($1/\log_2 \varphi = 1.44042\ldots$); milestones use the exact $\log_\varphi n$.

The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, $C$ is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.

Selected references

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, J. ACM 34(3):596–615, 1987. https://doi.org/10.1145/28869.28874
• J. Vuillemin, A data structure for manipulating priority queues, Comm. ACM 21(4):309–315, 1978. https://doi.org/10.1145/359460.359478
• R. E. Tarjan, Amortized computational complexity, SIAM J. Algebraic Discrete Methods 6(2):306–318, 1985. https://doi.org/10.1137/0606031
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1:269–271, 1959. https://doi.org/10.1007/BF01386390

Motivation

Commuters choose not only a route but also a departure time, trading travel delay against the penalty of arriving early or late. Static traffic assignment, in the tradition of Wardrop's user-equilibrium principle, ignores the time dimension; dynamic traffic assignment adds it, and its central modelling question is what "equilibrium" means when flows, delays and costs all vary over a time horizon. Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41(1), 1993) proposed the simultaneous route-departure (SRD) equilibrium of a path-based dynamic model and showed that it is equivalent to an infinite-dimensional variational inequality. That equivalence is the starting point of a large literature on dynamic user equilibrium: existence theory, solution algorithms and differential-variational formulations all take the variational inequality as their definition of the problem.

Timeline, as far as this mission is concerned:

• 1952: Wardrop states the static user-equilibrium criterion (equal and minimal travel times on used routes).
• 1979–1980: Smith and Dafermos formulate static user equilibrium as a finite-dimensional variational inequality.
• 1989: Friesz, Luque, Tobin and Wie treat dynamic route choice with a fixed departure schedule as an optimal-control problem.
• 1993: Friesz et al. (this paper) formulate simultaneous route and departure-time equilibrium and prove its equivalence with a variational inequality on $(L^2[0,T])^{|P|}$ (Theorem 2, p. 187).

Setting

A traffic network has a finite set $P$ of paths. Each path $p$ connects exactly one origin–destination (OD) pair $kl$; $P_{kl}$ denotes the paths of pair $kl$. Travellers depart during the horizon $[0,T]$, $T>0$, which carries Lebesgue measure $\nu$; "$\forall_\nu(t)$" means "for $\nu$-almost every $t\in[0,T]$".

A vector of departure-time densities $h=(h_p)_{p\in P}$ assigns to each path a square-integrable, almost everywhere nonnegative function $h_p$ on $[0,T]$: $h_p(t)$ is the rate at which travellers depart at time $t$ on path $p$. The set of such vectors is $H_+$. Each OD pair has a fixed travel demand $Q_{kl}$, and the feasible set is

$$\Lambda=\Big\{h\in H_+ : \sum_{p\in P_{kl}}\int_0^T h_p(t)\,d\nu(t)=Q_{kl}\ \text{for every OD pair } kl\Big\}.\qquad(38)$$

A cost operator gives the effective delay $C_p(t,h)\ge 0$ of departing at time $t$ on path $p$ when the densities are $h$: travel time plus a penalty for early or late arrival (13). Because densities are defined only up to null sets, the relevant lowest achievable cost on a path is an essential infimum,

$$\mu_p(h)=\operatorname{ess\,inf}\{C_p(t,h):t\in[0,T]\}=\sup\{x\in\mathbb R:\ \nu\{t: C_p(t,h)<x\}=0\},$$

and the lowest achievable cost for pair $kl$ is $\mu_{kl}(h)=\min_{p\in P_{kl}}\mu_p(h)$.

Definition 3. For $h\in\Lambda$ and a nonnegative vector $\mu=(\mu_{kl})$, the pair $(h,\mu)$ is an SRD equilibrium if for every OD pair $kl$ and every $p\in P_{kl}$:

$$h_p(t)>0\ \Rightarrow\ C_p(t,h)=\mu_{kl}\quad\forall_\nu(t),\qquad C_p(t,h)\ge\mu_{kl}\quad\forall_\nu(t).$$

No positive-measure set of travellers can lower its cost by switching route or departure time.

Formalization targets

Goal: Theorem 2 (PIE VIP)

For $h^*$ with nonnegative, square-integrable costs $C_p(\cdot,h^*)$:

$$\big(\exists\,\mu^*:\ (h^*,\mu^*)\ \text{SRD equilibrium}\big)\ \Longrightarrow\ h^*\in\Lambda\ \text{and}\ \sum_{p\in P}\int_0^T C_p(t,h^*)\,[h_p(t)-h^*_p(t)]\,d\nu(t)\ge 0\ \ \forall h\in\Lambda,\qquad(39)$$

and conversely, if $h^*\in\Lambda$ solves (39), then $(h^*,\mu(h^*))$ with $\mu^*_{kl}=\mu_{kl}(h^*)$ is an SRD equilibrium. The formal goal states the two directions as two conjuncts; the second names the equilibrium cost vector explicitly, which is stronger than an equivalence with an existential $\mu^*$.

Milestones

1. Lemma 2: a measurable function positive on a set of positive measure exceeds some $\varepsilon_0>0$ on a set of positive measure.
2. The pointwise inequality (42) at an equilibrium, and the necessity half of Theorem 2.
3. Condition (17) holds by construction for $\mu^*=\mu(h^*)$.
4. The positive-measure sets (44)–(46) and (47) produced by a failure of (16).
5. Feasibility (50) of the mass-shifted vector (48)–(49), the value bound (54), and the sufficiency half of Theorem 2.

Significance

The result. Theorem 2 converts an equilibrium defined by almost-everywhere complementarity conditions into a single variational inequality over a convex subset of a Hilbert space. This is what makes dynamic user equilibrium accessible to the general theory of variational inequalities: existence via monotonicity or compactness arguments, and projection-type algorithms in function space or after time discretization. The sufficiency half also identifies the equilibrium cost levels: they are the essential infima $\mu_{kl}(h^*)$, so the multiplier $\mu^*$ need not be found separately.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires essential infima, the shifting of mass between paths on sets of prescribed measure (the paper cites Halmos, Proposition 41.2, for the nonatomicity of Lebesgue measure), and careful integrability bookkeeping. The development is a self-contained template for "complementarity conditions a.e. ⇔ variational inequality in $L^2$" arguments, which recur in continuous-time equilibrium models.

Difficulty

Necessity is routine once integrability is in place, though the paper's text asserts the per-path identity $\int_0^T[h_p-h^*_p]\,d\nu=0$, which is false; only the sum over $P_{kl}$ vanishes, and that suffices. Sufficiency is the substantive half. The obvious approach, testing (39) against a perturbation that moves flow from an expensive to a cheap route, has to be carried out with sets rather than points: the costs are only defined almost everywhere, the minimal cost is an essential infimum that need not be attained at any time, and the perturbation must keep the demand constraints exact. This forces the choice of sets of exactly equal positive measure inside the positive-measure sets $S_p(\varepsilon,\delta)$ and $T_q(\varepsilon)$, a nonatomicity argument that a pointwise proof would miss.

Formalization scope

Densities are plain functions $\mathbb R\to\mathbb R$ with a square-integrability condition with respect to $\nu=$ Lebesgue measure restricted to $[0,T]$, not $L^2$ equivalence classes; every pointwise condition is $\nu$-almost everywhere, and values outside $[0,T]$ are unconstrained. Paths and OD pairs are finite types, with a map sending each path to its OD pair. The essential infimum is the literal formula (12), a real supremum; it is not the pointwise infimum, which changes when $C$ is altered on a null set and makes sufficiency false. $\mu_{kl}$ is a real infimum over $P_{kl}$; for a pair with no paths it is an unused default value.

The cost operator C is abstract, with the paper's measurability assumption strengthened to square-integrability so that every integral in (39) is a genuine Lebesgue integral. The network dynamics (3)–(11) that produce C in the paper are not formalized. Nonnegativity (the codomain $\mathbb R_+$ of (13)) and square-integrability are assumed only at $h^*$, which makes the formal statements stronger than the paper's. Without integrability, Lean's integral of a non-integrable function is $0$, so (39) could hold vacuously; the added hypothesis excludes that trivialization. The goal quantifies over every cost operator satisfying these hypotheses and never fixes one. In the milestones, the reduction from $p=q$ to $p\ne q$ (p. 188) is taken as the hypothesis $p\ne q$.

A complete development needs: properties of the real essential infimum (12) on a finite measure space; Lemma 2 (continuity of measure from below); the existence of measurable subsets of prescribed measure in Lebesgue measure (nonatomicity, available in Mathlib in some form); and integral bookkeeping for products of $L^2$ functions on a finite measure. The essential-infimum and mass-shift lemmas are reusable for other continuous-time equilibrium models. Proofs of any milestone, and cleaner restatements of the essential-infimum API, are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3):325–362, 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. J. Smith, The existence, uniqueness and stability of traffic equilibria, Transportation Research B 13(4):295–304, 1979. https://doi.org/10.1016/0191-2615(79)90022-5
• S. Dafermos, Traffic equilibrium and variational inequalities, Transportation Science 14(1):42–54, 1980. https://doi.org/10.1287/trsc.14.1.42
• T. L. Friesz, J. Luque, R. L. Tobin and B. W. Wie, Dynamic network traffic assignment considered as a continuous time optimal control problem, Operations Research 37(6):893–901, 1989. https://doi.org/10.1287/opre.37.6.893
• P. R. Halmos, Measure Theory, Van Nostrand, 1950 (Proposition 41.2, nonatomicity of Lebesgue measure).

Motivation

Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time $t$ leaves it at time $\tau(t)$. The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.

Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.

Timeline:

• 1969. Vickrey's bottleneck model introduces deterministic queueing at a single bottleneck (Vickrey 1969).
• 1986. Ben-Akiva and De Palma show (Trans. Sci. 20 (1986)), for uniform entry rates and deterministic queueing delays, that it is not possible to "arrive earlier by departing later".
• 1993. Friesz et al. prove (Theorem 1, p. 185) that for every linear arc delay $D = \alpha x + \beta$ the exit time is strictly increasing, extending the 1986 result to all continuous entry-rate patterns (remark, p. 186).

Setting

Consider one arc. Vehicles enter it at the entry rate $u(t) \ge 0$, a continuous function of time $t \ge 0$; the first vehicle enters at time $0$. For an exit-time function $\tau$, the arc volume at time $t \ge 0$ is the inflow mass of the vehicles that entered during $[0,t]$ and have not left by time $t$:

$$x(t) = \int_{\{s \in [0,t]\,:\,\tau(s) > t\}} u(s)\,ds .$$

The linear delay function (18) of the paper is

$$D(t) = \alpha\, x(t) + \beta, \qquad \alpha, \beta > 0,$$

a fixed free-flow travel time $\beta$ plus a queueing time determined by the service rate $1/\alpha$. The exit time is entry time plus delay, so $\tau$ is pinned by the exit-time equation

$$\tau(t) = t + \alpha\, x(t) + \beta \qquad (t \ge 0).$$

The equation is implicit: $\tau$ appears on the right through the volume. The proof partitions time at $t_0 = 0$, $t_{n+1} = \tau(t_n)$; in particular $t_1 = \tau(0) = \beta$ is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.

Formalization targets

Goal: Theorem 1 (p. 185)

For $\alpha, \beta > 0$ and a nonnegative continuous entry rate $u$, every $\tau$ satisfying the exit-time equation is strictly increasing on $[0, \infty)$:

$$0 \le s < t \implies \tau(s) < \tau(t),$$

and hence injective there, so $\tau^{-1}$ exists.

Milestones

1. Lemma 1 (19): for a differentiable invertible $f$, $[f^{-1}]'(z) = 1/f'[f^{-1}(z)]$.
2. First interval (21)–(24): $t_1 = \beta$; on $[0, t_1]$, $x(t) = \int_0^t u$, $\tau(t) = t + \alpha\int_0^t u + \beta$, and $\tau' = 1 + \alpha u > 0$.
3. Second interval (25)–(28): on $[t_1, t_2]$, $\tau(t) = t + \alpha\int_{\tau^{-1}(t)}^t u + \beta$ and $\tau'(t) = \alpha u(t) + 1/(1 + \alpha u[\tau^{-1}(t)]) > \alpha u(t)$.
4. Induction (29)–(34): the same representation and $\tau'(t) > \alpha u(t)$ on every $[t_{n+1}, t_{n+2}]$, with $\tau$ strictly increasing there.
5. Covering: $t_{n+1} - t_n \ge \beta$ and $\mathbb R_+ = \bigcup_{n \ge 0}[t_n, t_{n+1}]$.

A supporting, non-milestone item states that the exit-time equation has a solution for every admissible $u$.

Significance

The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.

The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.

Difficulty

The obvious argument differentiates $\tau(t) = t + \alpha x(t) + \beta$ and bounds the outflow rate. But the volume can only be written as $\int_{\tau^{-1}(t)}^t u$ once $\tau$ is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on $[t_n, t_{n+1}]$ the volume depends only on $\tau$ restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions $t_n$, where $\tau$ is generally not differentiable, and show that the junctions do not accumulate.

Formalization scope

Time is real; the entry rate is a function $u : \mathbb R \to \mathbb R$ with $u(t) \ge 0$ and $u$ continuous on $[0, \infty)$. Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on $[0,\infty)$ only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval $[t_n, t_{n+1}]$. The paper's separate pieces $\tau_k$ are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis $f'[f^{-1}(z)] \ne 0$, without which it is false.

The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through $\tau^{-1}$ or assumed $\tau$ monotone would assume the conclusion and is ruled out.

The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• M. Ben-Akiva and A. de Palma, Some circumstances in which vehicles will reach their destinations earlier by starting later: revisited, Transportation Science 20(1):52–55, 1986. https://doi.org/10.1287/trsc.20.1.52
• M. Ben-Akiva, A. de Palma and P. Kanaroglou, Dynamic model of peak period traffic congestion with elastic arrival rates, Transportation Science 20(3):164–181, 1986. https://doi.org/10.1287/trsc.20.3.164
• W. S. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–261, 1969. https://www.jstor.org/stable/1823678

Motivation

A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).

This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.

Setting

There are $n$ tasks, indexed $i=0,\ldots,n-1$. Task $i$ has a nonnegative length $l_i$, a nonnegative preferred starting time $a_i$, and an actual starting time $s_i$. Once started, it occupies the one processor until $s_i+l_i$. Each start must be nonnegative. For the fixed-order problem, task $i$ must finish before task $i+1$ starts, so $s_i+l_i\le s_{i+1}$. This permits idle time when the inequality is strict. The task's discrepancy is $|s_i-a_i|$; because its preferred completion is $a_i+l_i$, this is also its absolute completion-time discrepancy. The total discrepancy is

$$\operatorname{cost}_n(s)=\sum_{i=0}^{n-1}|s_i-a_i|.$$

A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule $S_n$ for the first $n$ tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).

For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.

Formalization targets

Fixed-order optimality

The main target is the paper's Theorem 2. For all nonnegative task data and every $n$, the actual schedule $S_n$ produced by the block-shifting algorithm is feasible and satisfies

$$\operatorname{cost}_n(S_n)\le\operatorname{cost}_n(s) \qquad\text{for every feasible fixed-order schedule }s.$$

This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of $S_n$ has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).

Equal-length schedules

The companion target is Theorem 3. If every task has a common length $L\ge0$ and the preferred starts are indexed so that $a_i\le a_{i+1}$, then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:

$$\exists s\;\bigl[ \operatorname{cost}_n(s)\le\operatorname{cost}_n(t) \text{ for every feasible }t \bigr] \quad\text{with }s_i\le s_{i+1}\text{ whenever }i+1<n.$$

The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).

Significance

Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).

The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.

Difficulty

Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).

Formalization scope

The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below $n$ count. Task $i$ in Lean is the paper's $T_{i+1}$. Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's $l_i\ge0$ model.

The algorithm is defined by its stated insertion and single-block-shift operations. Defining $S_n$ as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.

Selected references

• Michael R. Garey, Robert E. Tarjan, and Gordon T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2), 330–348, 1988. DOI: 10.1287/moor.13.2.330.

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$, origin $0$ and terminal $n$. Its arcs are ordered pairs $(i,j)$ with $i<j$, at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$, and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$, let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$.

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$, where $v_i$ is the length of arc $(i,j)$, with probabilities $p_j(v)\ge 0$ summing to $1$. Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$. Three numbers are attached to each event $i$:

1. the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$;
2. the mean-length estimate $g_i=\ell_i(\bar t)$, where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$;
3. Fulkerson's numbers $f_0=0$ and, for $j\neq0$,

$$f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).$$

Formalization targets

Goal: (4.4)

$$g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .$$

Milestones

In the order of Fulkerson's induction (pp. 10–12):

1. the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
2. $\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
3. (4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$;
4. (4.5)/(4.9): if $g_k\le f_k$ for all $k<j$, then $g_j\le f_j$;
5. (4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$;
6. (4.10)/(4.14): if $f_k\le e_k$ for all $k<j$, then $f_j\le e_j$.

Companion statements

• $g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
• Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$, so (4.4) fails without bundle independence.
• (4.17): an independent example with $g_3=f_3=1<e_3=5/4$.
• Fig. 4.1: explicit values $g_4=3/2$, $f_2=1/2$, $f_3=9/8$, $f_4=55/32$, and $f_i=e_i$.

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$, while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$, which gives the weaker bound $g\le e$. Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

• Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$. Fulkerson's numbering condition "$i\le j$" on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
• Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$.
• Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$, for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
• Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
• No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$.

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

• D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
• J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
• D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

Motivation

The maximal multi-commodity flow problem asks how much total flow several commodities, each travelling from its own sources to its own sinks, can send through a network whose arcs have shared capacities. It arises in communication and transportation planning: Kalaba and Juncosa's 1956 study of communication networks (Management Science 3(1)) leads to linear programs of this form. For a single commodity the problem has a clean combinatorial theory: the max-flow min-cut theorem of Ford and Fulkerson (1956, doi:10.4153/CJM-1956-045-5) and the labeling algorithm. With several commodities both fail: the min-cut equality is false, and simplex bases are no longer triangular.

In a short note received in October 1957 and published in Management Science in 1958, L. R. Ford Jr. and D. R. Fulkerson proposed a way to solve the multi-commodity problem with the simplex method anyway (doi:10.1287/mnsc.1040.0269, reprinted 2004). They use the arc-chain formulation, which has one variable per chain from a source to a sink of a commodity. That formulation has far too many variables to write down. The note's point is that the simplex method never needs them explicitly. The "pricing" step (finding a variable to enter the basis, or recognizing that none exists) can be carried out by one shortest-chain computation per commodity, with the simplex multipliers as arc lengths.

Timeline. Ford (1956, RAND P-923) gave the label-correcting shortest-chain procedure the note uses. Ford and Fulkerson (1958) applied it to price the columns of the arc-chain program. Dantzig and Wolfe (1960) generalized the idea into the decomposition principle. Gilmore and Gomory (1961) applied the same pattern to the cutting-stock problem, and it is now called column generation.

Setting

A network has finitely many nodes $P_1,\dots,P_N$ and arcs $A_1,\dots,A_m$. Each arc $A_r$ joins two nodes, has a capacity $b_r$, and is either directed (traversable one way only) or undirected (traversable both ways). There are finitely many commodities; commodity $k$ has a set of sources $S_k$ and a set of sinks $T_k$.

A chain from $u$ to $w$ is the arc set of a path $u = v_0, v_1, \dots, v_p = w$ with distinct nodes, each arc traversable from $v_{i-1}$ to $v_i$. A commodity chain of $k$ is a chain from a node of $S_k$ to a node of $T_k$. List the commodity chains, for all commodities, as $C_1,\dots,C_n$, and let $A = (a_{rs})$ be the incidence matrix: $a_{rs} = 1$ if $C_s$ contains $A_r$ and $0$ otherwise. With $x_s$ the flow along $C_s$ and $x_{n+r}$ the slack of arc $A_r$, the problem is the linear program

$$\text{maximize } \sum_{s=1}^{n} x_s \quad\text{subject to}\quad \sum_{s=1}^{n} a_{rs}x_s + x_{n+r} = b_r,\qquad x_1,\dots,x_{n+m} \ge 0. \tag{2–3}$$

A basis is a set of $m$ columns of $[A \mid I]$ forming an invertible matrix $B = (b_{rj})$. Its simplex multipliers $\alpha_1,\dots,\alpha_m$ satisfy, for every basic column $j$,

$$\sum_{r=1}^{m} \alpha_r b_{rj} = \begin{cases} 1 & j \le n,\\ 0 & j > n.\end{cases} \tag{4}$$

Read as arc lengths, the $\alpha_r$ give each chain $C_s$ the length $\sum_r \alpha_r a_{rs}$. The labeling process for a source set $S$ starts with labels $\pi_i = 0$ on $S$ and $\pi_i = \infty$ elsewhere. It repeatedly finds an arc traversable from $P_i$ to $P_j$ with $\pi_i + l_{ij} < \pi_j$ and replaces $\pi_j$ by $\pi_i + l_{ij}$. In Lean the labels are lab : V → WithTop ℝ, the multipliers are α : E → ℝ, and all objects live in the namespace FordFulkerson58.ArcChain.

Formalization targets

Goal: the shortest-chain pricing test (§3, pp. 1779–1780)

Let $B$ be a basis with basic feasible solution $z$ and multipliers $\alpha \ge 0$. Then:

$$\begin{aligned} &\text{(a) for every commodity, every run of the labeling process with lengths } \alpha \text{ is finite;}\\ &\text{(b) if all final sink labels are } \ge 1, \text{ then } \textstyle\sum_s x_s \le \sum_s z_s \text{ for every feasible } x;\\ &\text{(c) if a final sink label } \pi_t < 1, \text{ some non-basic chain column to } t \text{ has length } \pi_t \text{ and } 1 - \textstyle\sum_r \alpha_r a_{rs} > 0. \end{aligned}$$

Milestones (§3, the labeling process and the test)

1. Termination of the labeling process for non-negative lengths (p. 1780).
2. Final labels are shortest-chain lengths from $S$; the smallest label on $T$ is the $S$-to-$T$ distance (p. 1780).
3. The trace-back: a chain of tight arcs from $S$ to every labeled node, of length its label (p. 1780).
4. If $\alpha \ge 0$ and every commodity chain has length $\ge 1$, the basis is optimal (p. 1779).

Further items state the remarks of §3–§4: a negative multiplier lets a slack enter; the slack basis is a feasible start; dominated chains can be ignored; limited supplies reduce to the same problem by adding new directed source arcs; Figure 2 is the incidence matrix of Figure 1; with negative lengths the labeling process may not terminate.

Significance

The result. The test turns a linear program with exponentially many columns into one whose pricing step costs one shortest-path computation per commodity. Only the $m \times m$ basis is ever stored. This is the first instance of column generation, which now underlies solvers for multi-commodity flow, cutting stock, vehicle routing, crew scheduling and many other set-partitioning models, typically inside branch-and-price. Part (a) together with milestones 2–3 also gives the correctness of Ford's label-correcting algorithm with non-negative lengths, started from a source set and with any order of arc scans.

Formalizing it. The results are classical and proved in the paper's informal style. None of them is formalized: the platform has no arc-chain LP, no column pricing, and no formal statement of Ford's label-correcting process. The general LP facts are on the platform (the simplex optimality criterion and weak duality, both proved) and are included as references. This mission adds the network-specific layer: chains as arc sets of simple paths, the labeling process as a relation on labelings, and the link from final labels to reduced costs. One sentence of the paper is corrected. The trace-back "eventually" reaches $S$ only along some backward path, because zero-length cycles can trap a naive backward search, and milestone 3 states the true version.

Difficulty

The obvious argument for termination says each step lowers a label and there are finitely many chains. It fails: labels are lengths of walks, not chains, and with zero-length arcs (multipliers are often $0$) there are infinitely many walks. Termination needs the finiteness of the set of walk lengths below a bound, not positivity. The correctness of the final labels needs both properties of the labeling: it is produced by the process (so every label is the length of a walk from $S$), and it is terminal. A terminal labeling alone, such as all labels $0$, is not a distance labeling. Finally, the optimality claim is an LP statement about the full, never-enumerated column set. It must be derived from (4), $\alpha \ge 0$ and the shortest-chain lengths, with the chain columns indexed abstractly.

Formalization scope

Nodes, arcs and commodities are finite types V, E, ι. Each arc has tail, head, a per-arc directed flag and a capacity b : E → ℝ; commodities have src snk : ι → Finset V. Parallel arcs and mixed directed/undirected networks are allowed. No sign of the capacities and no disjointness of sources and sinks is assumed, except 0 ≤ b in the zero-flow item, where it is disclosed. Chains are arc sets of simple paths. The null chain at a source is a chain, so sources have distance $0$. Columns are pairs (commodity, chain), so one arc set used by two commodities gives two columns. The columns of $[A \mid I]$ are indexed by Col N ⊕ E. A basis is β : E → Col N ⊕ E with IsUnit (basisMatrix N β).det; its basic feasible solution and multipliers (4) are hypotheses about this β. Labels are in WithTop ℝ with ⊤ for $\infty$. Shortest-chain lengths are finite infima (Finset.inf), equal to ⊤ when there is no chain. The process scans arcs, not node pairs, which handles parallel arcs and the undirected case $l_{ij} = l_{ji}$.

The standing assumption of §3 ("a stage has been reached in the computation where all $\alpha_r$ are non-negative", p. 1779) is a hypothesis of the goal and of milestones 1–4. Milestones 1–3 are stated for any non-negative length function. The paper has no numbered theorems; every milestone is an unnumbered sentence of §3, cited by page and position.

A trivializing formalization is ruled out: the goal does not assume shortest-chain lengths, the trace-back, or any reduced-cost fact beyond (4). Statements about final labels require labelings that are both reachable from the initial labels and terminal, and part (a) shows such labelings exist.

Reusable beyond this mission: the chain and labeling layer (a label-correcting shortest-path algorithm from a source set over mixed networks) and the arc-chain LP. Contributions to the LP layer, which can import the referenced Matoušek–Gärtner results after reindexing, are particularly welcome.

Selected references

• L. R. Ford Jr., D. R. Fulkerson, A suggested computation for maximal multi-commodity network flows, Management Science 5(1):97–101, 1958; reprinted Management Science 50(12S):1778–1780, 2004. https://doi.org/10.1287/mnsc.1040.0269
• L. R. Ford Jr., D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
• L. R. Ford Jr., Network Flow Theory, RAND Corporation Paper P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• G. B. Dantzig, P. Wolfe, Decomposition principle for linear programs, Operations Research 8(1):101–111, 1960. https://doi.org/10.1287/opre.8.1.101
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. https://doi.org/10.1287/opre.9.6.849
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007. https://doi.org/10.1007/978-3-540-30717-4

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

• Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
• Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
• Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$. Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$. A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$, either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$. Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$, and the total discrepancy of $S$ is

$$\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .$$

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$.

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$, is there a schedule with $\mathrm{cost}(S)\le k$?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$, can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$, write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$. A schedule is ordered if, on each side of $M$, shorter tasks lie nearer to $M$. The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

$$\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}$$

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

1. Even-odd partition is in NP; the instance $x_1=1$, $x_{2i}=x_{2i-1}+y_i$, $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
2. The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$), LEMMA 3 ($|A(S)|=|B(S)|$), LEMMA 4 ($m_0(S)=M$), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ($\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

$$k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .$$

3. At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$; equality forces the ordered, gap-free form in item 2.
4. The reduction: the instance D with $l_0=x_1-1$, $l_i=x_i$, $l_{2n+1}=2$, $M_j=M=\sum_{i\le 2n}l_i/2$, $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$, the $i$-th pair of lengths in the $i$-th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$, so they must be restated for every $M$. Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$, exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$, and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$. Together these force the two sides to have equal total length. A proof that only cites the large-$M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$.

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$, double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

• Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$, and integer data are cast to $\mathbb R$. Restricting to integer starting times would be a different problem and is not what is stated.
• Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
• Tasks are indexed by Fin N from $0$. In the special case $T_i$ is index $i$, and the paper's $T_{2i-1},T_{2i}$ ($1\le i\le n$) are the indices $2k+1,2k+2$ for $k=i-1$.
• Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
• The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
• Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
• N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

A game without side payments (an NTU game) describes cooperation in which utility cannot be transferred between players: each coalition $A$ of players is assigned the set $V(A)$ of payoff vectors it can secure on its own. The core is the set of payoffs to the grand coalition that no coalition can improve upon. Whether the core is nonempty is the basic stability question of cooperative game theory. For games with side payments the answer is the Bondareva–Shapley theorem. For NTU games it is Scarf's theorem (Scarf 1967): a balanced game has a nonempty core. Billera (1970) gave a convex version, in which the payoff sets are convex and balancedness is stated with weighted Minkowski sums.

Aubin's paper (Aubin 1981) obtains Billera's version of the theorem by a different route. Players may join coalitions at fractional rates of participation, and the paper first proves a core existence theorem for these fuzzy games. The game on ordinary coalitions is then embedded into a fuzzy game whose core lies inside the core of the original game.

Setting

The players are $N = \{1,\dots,n\}$. A coalition $A \subseteq N$ is identified with its characteristic vector $\tau^A \in \{0,1\}^n$, and $\tau^N = (1,\dots,1)$. A fuzzy coalition is a vector $\tau \in [0,1]^n$ of participation rates with support $A_\tau = \{i : \tau_i > 0\}$. Write $(\tau\cdot c)_i = \tau_i c_i$, $\mathbb{R}^\tau = \tau\cdot\mathbb{R}^n$ for the vectors vanishing off $A_\tau$, $\mathbb{R}^\tau_+$ for its nonnegative part, and $\mathring{\mathbb{R}}^\tau_+$ for the vectors strictly positive on $A_\tau$.

A fuzzy game without side payments assigns to each $\tau \ge 0$ a nonempty, closed, convex set $V(\tau)\subseteq\mathbb{R}^\tau$. Each $V(\tau)$ is comprehensive, meaning $V(\tau) = V(\tau)-\mathbb{R}^\tau_+$, and bounded above, meaning $V(\tau)\subseteq C-\mathbb{R}^\tau_+$ for some $C$. The map is positively homogeneous: $V(t\tau) = tV(\tau)$ for every $t>0$. Its core is the set of $c\in V(\tau^N)$ such that $\tau\cdot c\notin V(\tau)-\mathring{\mathbb{R}}^\tau_+$ for every fuzzy coalition $\tau\neq 0$. With the support function $v(\tau,\lambda)=\sup_{c\in V(\tau)}\sum_i\lambda_i c_i$ and the simplex $M^n$, a weak (resp. strong) canonical cooperative equilibrium is a $c\in V(\tau^N)$ together with a $\bar\lambda\in M^n$ (resp. $\bar\lambda$ with all coordinates positive) satisfying $\sum_i\bar\lambda^i\tau_ic_i\ge v(\tau,\bar\lambda)$ for every $\tau\in[0,1]^n$.

A usual NTU game lives on a family $\mathcal{C}$ of coalitions that contains $N$ and every singleton. For each $A\in\mathcal{C}$, the set $V(A)\subseteq\mathbb{R}^A$ is nonempty, closed, convex, comprehensive and bounded above. A balance of $\tau$ is a vector of weights $m\ge 0$ on $\mathcal{C}$ with $\sum_{A\ni i}m(A)=\tau_i$ for every $i$, and $\mathcal{C}(\tau)$ is the set of balances of $\tau$. The fuzzy extension of the game is

$$\pi V(\tau)=\bigcup_{m\in\mathcal{C}(\tau)}\ \sum_{A\in\mathcal{C}} m(A)\,V(A),$$

and the game is balanced if $V(N)=\pi V(\tau^N)$.

Formalization targets

Goal: Theorem 7.1

For a balanced game without side payments,

$$\emptyset\neq\operatorname{core}(\pi V)\subseteq\operatorname{core}(V),\qquad \mathrm{CCE}_{\rm strong}(V)\subseteq\operatorname{core}(\pi V)\subseteq\mathrm{CCE}_{\rm weak}(V),$$

and in particular $\operatorname{core}(V)\neq\emptyset$.

Milestones

• Proposition 3.1: $c\in V(\tau^N)$ is in the core iff the maximum complaint $\alpha(c)=\sup_{\tau\neq0}\inf_{\lambda\in M^\tau}[v(\tau,\lambda)-\sum_i\lambda^i\tau_ic_i]$ is $\le 0$.
• Proof of Theorem 3.1(b): if $V$ is superadditive, $V(\tau)+V(\sigma)\subseteq V(\tau+\sigma)$, then $\tau\mapsto v(\tau,\lambda)$ is concave on $\mathbb{R}^n_+$.
• Theorem 3.1: strong equilibria lie in the core, and for a superadditive game the core lies in the set of weak equilibria.
• Theorem 5.1: a superadditive fuzzy game has a nonempty core.
• §7, (6), (7), (11): $\pi V$ is a superadditive fuzzy game that extends $V$, and its support function is $\pi v(\tau,\lambda)=\sup_{m\in\mathcal{C}(\tau)}\sum_A m(A)v(A,\lambda)$.
• §7 and the proof of Theorem 7.1: under balancedness, $\operatorname{core}(\pi V)\subseteq\operatorname{core}(V)$, and the equilibria of $V$ coincide with those of $\pi V$.

Significance

Theorem 7.1 gives the core existence result for convex NTU games under Billera's balancedness condition. Its proof goes through a statement about fuzzy coalitions, Theorem 5.1, which uses no combinatorial pivoting. That theorem also has independent uses. Its fuzzy core is the solution concept that §4 of the paper identifies with Walras equilibria of exchange economies. The canonical cooperative equilibria give a price-like certificate, a common rate of transfer $\bar\lambda$, that sandwiches the core.

The results are classical and proved. Prove2Me holds no statement of Scarf's or Billera's theorem, of NTU cores, or of balancedness for games without side payments, and Mathlib has none of these notions. The mission produces faithful statements of the paper's chain of results, and their proofs once solvers close them. It also builds reusable infrastructure: support functions of comprehensive sets, Minkowski combinations indexed by balances, and positively homogeneous set-valued maps.

Difficulty

Most of §7 is bookkeeping with Minkowski sums. The hard part is Theorem 5.1, the existence of a point in the fuzzy core. The core is defined by infinitely many exclusion conditions, one for each $\tau\in[0,1]^n$, so a finite intersection argument does not apply directly. The paper's route works with prices: it uses the superdifferential of the concave map $\tau\mapsto v(\tau,\lambda)$ at $\tau^N$, Ky Fan's inequality on a truncated simplex where all $\lambda_i\ge\varepsilon$, and a limit as $\varepsilon\to0$. That limit requires compactness of the approximating payoffs, and at the boundary of the simplex the superdifferential map is not upper semicontinuous. Theorem 3.1(b) needs a minisup theorem for a function that is concave in $\tau$ and convex and lower semicontinuous in $\lambda$. Mathlib has neither Ky Fan's inequality nor this minimax theorem in that form.

Formalization scope

All statements import one definitions file, FuzzyGames.NTUCore.Basic. The formalization commits to the following conventions.

• Players are Fin n, and payoffs, fuzzy coalitions and rates of transfer are Fin n → ℝ, ordered coordinatewise. $\mathbb{R}^\tau$ is encoded as "vanishes where $\tau_i=0$", which equals $\tau\cdot\mathbb{R}^n$ for $\tau\ge0$.
• Fuzzy games are defined directly on the orthant $\tau\ge0$, the paper's extension of $V$ from $[0,1]^n$ by homogeneity. Homogeneity holds for every $t>0$, and superadditivity holds on $\mathbb{R}^n_+$.
• Support functions, $\alpha$ and $\pi v$ take values in EReal, so an unbounded supremum is $+\infty$ and never a junk $0$.
• The supremum defining $\alpha(c)$ ranges over $\tau\neq0$. Since $M^0=\emptyset$, including $\tau=0$ would make $\alpha\equiv+\infty$ and Proposition 3.1 false. Blocking coalitions are likewise $\tau\neq0$, as in §3 (4).
• $\mathcal{C}$ is a finite family of nonempty coalitions that contains $N$ and every singleton. "$\forall A\neq\emptyset$" in §7 ranges over $\mathcal{C}$.
• The paper leaves $n\ge1$ implicit. Theorem 3.1(b) and Theorem 5.1 carry $0<n$: for $n=0$ the simplex is empty while the core is not.
• In §7 (11), $\pi v(\tau,\lambda)$, which the paper uses without defining it, is taken to be the extension §6 (2) applied to $A\mapsto v(A,\lambda)$, for $\lambda\ge0$.
• The §7 sentence after (5) is stated with two extra conclusions: $\pi V(\tau)$ is nonempty and contained in $\mathbb{R}^\tau$. These are the remaining requirements of §3 (3) that are needed to apply Theorem 5.1.
• Sums and scalings of sets are Mathlib's pointwise operations.

The fuzzy-game axioms are a Prop-valued structure and are hypotheses of every theorem. The core and the equilibria are defined for an arbitrary set-valued map, so the theorems about $\pi V$ do not presuppose that it is a fuzzy game. That fact is the content of the §7 milestones and is not assumed. Non-vacuity has been checked locally on a concrete instance: $V(\tau)=\{c\in\mathbb{R}^\tau: c\le\tau\}$ is a superadditive fuzzy game, and $V(A)=\{c\in\mathbb{R}^A:c\le\tau^A\}$ is a balanced game on every admissible $\mathcal{C}$, with $(1,\dots,1)$ in both cores.

Contributions are welcome at every level: the §7 Minkowski-sum lemmas, the support-function identities, and a minisup or Ky Fan theorem in the form the proofs need. Reusable pieces include support functions of comprehensive sets and Sion-type minimax.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• H. E. Scarf, The Core of an N Person Game, Econometrica 35(1) (1967) 50–69. https://doi.org/10.2307/1909888
• L. J. Billera, Some Theorems on the Core of an n-Person Game without Side-Payments, SIAM Journal on Applied Mathematics 18(3) (1970) 567–579. https://doi.org/10.1137/0118053
• K. Fan, A Minimax Inequality and Applications, in O. Shisha (ed.), Inequalities III, Academic Press (1972) 103–113.