Motivation

In 1935 Hassler Whitney asked which properties of linear dependence among the columns of a matrix can be stated without reference to the matrix at all. His answer, On the Abstract Properties of Linear Dependence (American Journal of Mathematics 57, 1935), introduced the matroid: a finite set together with a rank function obeying three short postulates. The notion now underlies combinatorial optimization (the greedy algorithm is optimal exactly on matroids, and matroid intersection and partition generalize bipartite matching and arborescence packing), graph theory (graphic and cographic matroids), coding theory and the study of linear representations over finite fields.

A defining feature of the subject is that the same structure can be axiomatized in several apparently unrelated ways: by rank, by independent sets, by bases, by circuits. Each axiom system is convenient for different arguments, and passing between them, a so-called cryptomorphism, is routine in practice. Whitney's paper is where these equivalences first appear. Part I, §§2–4 and §6 (pp. 510–514), derives the basic properties of rank from the rank postulates, deduces from them the postulates for independent sets, and shows that the two systems are equivalent. This mission formalizes that first equivalence.

Setting

Let $M$ be a finite set of elements $e_1, \dots, e_n$. Following Whitney, write $N + e$ for $N \cup \{e\}$, $M_1 + M_2$ for the union and $M_1 M_2$ for the intersection of subsets; $\rho(N)$ is the number of elements of $N$.

A rank system is a function $r$ on the subsets of $M$ satisfying

• (R₁) $r(\emptyset) = 0$;
• (R₂) for every subset $N$ and element $e \notin N$, $r(N + e) = r(N)$ or $r(N + e) = r(N) + 1$;
• (R₃) for every subset $N$ and elements $e_1, e_2 \notin N$, if $r(N + e_1) = r(N + e_2) = r(N)$ then $r(N + e_1 + e_2) = r(N)$.

The nullity of $N$ is $n(N) = \rho(N) - r(N)$, and $N$ is independent when $n(N) = 0$. The increment of (3.1) is $\Delta(M', N) = r(M' + N) - r(M')$, written $\Delta(M', e)$ when $N = \{e\}$.

An independence system is a predicate "independent" on the subsets of $M$ satisfying

• (I₁) any subset of an independent set is independent;
• (I₂) if $N$ and $N'$ are independent and $N'$ has exactly one element more than $N$, then $N + e'$ is independent for some $e' \in N'$ with $e' \notin N$.

From an independence system one recovers a rank by letting $r(N)$ be the number of elements in a largest independent subset of $N$. In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.

Formalization targets

Goal: (R) and (I) are equivalent (§6, p. 514)

1. If $r$ satisfies (R₁)–(R₃), then $\{N : \rho(N) = r(N)\}$ satisfies (I₁), (I₂), contains $\emptyset$, and

$$r(N) = \max\{\rho(I) : I \subseteq N,\ \rho(I) = r(I)\} \quad \text{for every } N.$$

2. If "independent" satisfies (I₁), (I₂) and $\emptyset$ is independent, then $r(N) = \max\{\rho(I) : I \subseteq N \text{ independent}\}$ satisfies (R₁)–(R₃), and $N$ is independent if and only if $\rho(N) = r(N)$.

Both translations and both round trips are part of the goal: Whitney's conclusion is not only that each system implies the other but that "the definitions of the rank and the independence or dependence of any subset of $M$ agree under the two systems".

Milestones

• Lemma 1 (p. 510): $r(N) \ge 0$, $n(N) \ge 0$, and $N \subseteq M'$ implies $r(N) \le r(M')$, $n(N) \le n(M')$.
• Lemma 2 (p. 510): any subset of an independent set is independent, which is (I₁).
• Lemma 3 (p. 511): $\Delta(M + e_2, e_1) \le \Delta(M, e_1)$.
• Lemma 4 (p. 511): $\Delta(M + N, e) \le \Delta(M, e)$.
• Theorem 3 (p. 511): $\Delta(M + N_2, N_1) \le \Delta(M, N_1)$; equivalently

$$r(M + N_1 + N_2) \le r(M + N_1) + r(M + N_2) - r(M), \qquad r(M_1 + M_2) \le r(M_1) + r(M_2) - r(M_1 M_2).$$

• §4 (pp. 511–512): the independent sets of a rank system satisfy (I₂).

Significance

The equivalence makes the rank function and the family of independent sets two descriptions of one object. Every later result of Whitney's paper, and of matroid theory generally, moves between them without comment: the circuit postulates of §5 and §8, the base postulates of §7 and the duality of §§11–13 are all phrased through rank or independence as convenient. Theorem 3 is the submodularity of rank, the property that connects matroids to submodular function minimization and polymatroids; here it is derived from the purely local postulates (R₁)–(R₃), which constrain the rank only under the addition of one or two elements.

On the formal side, Mathlib defines Matroid through independent sets (with constructors from other axiom systems) and proves submodularity of its rank; the platform has submodularity for Mathlib matroids (FamousTheorems.matroid_rank_submodular_7a). Neither starts from Whitney's local rank postulates. What this mission adds is a machine-checked derivation of the global properties of rank from (R₁)–(R₃) and of Whitney's original equivalence, stated for his own postulates, so that the later missions of this series, which work from the same postulates, rest on a verified foundation. The result itself has been settled since 1935; the open work is the formal proof.

Difficulty

The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound $r(N) \le \rho(N)$ follow by adding elements one at a time, but the submodular inequality relates arbitrary sets, and nothing in (R₃) mentions more than two new elements. The gap between the local and the global statement is the substance of Lemmas 3, 4 and Theorem 3, and the deduction of (I₂) depends on it.

In the converse direction the rank is defined as a maximum over independent subsets, while (I₂) only augments a set from an independent set with exactly one element more; (R₃) for the derived rank is a statement about three sets that are not given in that form. The round trips are where the two halves meet, and each depends on the global properties of the first half rather than on the postulates alone.

Formalization scope

Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid $M$ is the whole type. Ranks, nullities and increments take values in ℤ, so differences never truncate; Whitney allows any number, but (R₁) and (R₂) force nonnegative integers. Postulate (I₂) is stated in Whitney's form with N'.card = N.card + 1, not the general augmentation for $\rho(N) < \rho(N')$. Postulates (R₂), (R₃) keep their hypotheses $e, e_1, e_2 \notin N$. Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets $M, N, N_1, N_2$; Lemma 1's monotonicity for arbitrary $N \subseteq M'$, the form in which the paper uses it. rankOfIndep is the supremum of cardinalities over the independent members of the powerset.

The paper takes for granted that the empty set is independent in system (I). Without that hypothesis, the predicate declaring nothing independent satisfies (I₁) and (I₂) vacuously, the supremum defining the rank returns $0$, and the round trip fails; the goal therefore assumes $\emptyset$ independent in part 2 and proves it in part 1. A formalization in terms of Mathlib's Matroid would make the goal a restatement of library facts, since Mathlib's matroids are independence systems by construction; the goal is deliberately about the postulates as predicates on functions and on families of sets.

A complete development needs only finite set combinatorics (Finset.card, induction on finite sets, Finset.sup). The derived lemmas (monotonicity, submodularity, (I₂)) are reusable for any later work from Whitney's rank postulates, including the circuit-postulate equivalence of the companion mission. A bridge from rank systems to Mathlib's Matroid (via IndepMatroid.ofFinset) would be a welcome addition but is not part of the goal. Proofs of the milestones in any order are welcome; Theorem 3 and the §4 deduction are the natural first targets.

Selected references

• H. Whitney, On the Abstract Properties of Linear Dependence, American Journal of Mathematics 57 (1935), no. 3, 509–533. https://doi.org/10.2307/2371182
• J. Oxley, Matroid Theory, 2nd ed., Oxford Graduate Texts in Mathematics 21, Oxford University Press, 2011. https://doi.org/10.1093/acprof:oso/9780198566946.001.0001
• J. Kung (ed.), A Source Book in Matroid Theory, Birkhäuser, 1986. https://doi.org/10.1007/978-1-4684-9199-9
• Mathlib, Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.html

Why restricted policy classes

Abstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping $H(x,u,J)$: the cost of using control $u$ at state $x$ when the future is valued by the function $J$. Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors $\mu:S\to C$ and $H$ is defined on all extended-real functions on $S$.

That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which $H$ acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class $\tilde M$ and $H$ is only defined on a prescribed class $\tilde F$ of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.

Setting

The data are a state space $S$, a control space $C$, nonempty constraint sets $U(x)\subseteq C$, and three restricted classes: sets of functions $F^*\subset\tilde F\subset F$, where $F$ is the set of all functions $S\to[-\infty,\infty]$, and a set $\tilde M$ of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$. The mapping $H:S\times C\times\tilde F\to[-\infty,\infty]$ is monotone: $J\le J'$ in $\tilde F$ implies $H(x,u,J)\le H(x,u,J')$. For $\mu\in\tilde M$ and $J\in\tilde F$,

$$T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).$$

A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ with every $\mu_k\in\tilde M$; their set is $\tilde\Pi$. Given $J_0\in F^*$ with $J_0>-\infty$, the $N$-stage and infinite-horizon costs are

$$J_{N,\pi}=(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0),\qquad J_\pi(x)=\lim_{N\to\infty}J_{N,\pi}(x),$$

and the optimal costs are $J^*_N=\inf_{\pi\in\tilde\Pi}J_{N,\pi}$ and $J^*=\inf_{\pi\in\tilde\Pi}J_\pi$. For a stationary policy $(\mu,\mu,\dots)$ write $J_\mu$.

Five standing conditions tie the classes together: A.1 (every control $u\in U(x)$ is the value $\mu(x)$ of some $\mu\in\tilde M$), A.2 ($F^*$ is closed under $T$ and under adding constants), A.3 ($\tilde F$ is closed under every $T_\mu$, $\mu\in\tilde M$, and under adding constants), A.4 ($\varepsilon$-minimizing selectors for $T(J)$, $J\in F^*$, exist in $\tilde M$), and A.5 ($\tilde F$ and $F^*$ are closed under pointwise limits). Assumption $\tilde C$ asks for a closed subset $\bar B$ of the space $B$ of bounded real functions with the sup norm $\|\cdot\|$, containing $J_0$ and invariant under $T$ on $\bar B\cap F^*$ and under $T_\mu$ on $\bar B\cap\tilde F$, such that every $J_\pi$ exists and is real, each $T_\mu$ is $\alpha$-Lipschitz on $B\cap\tilde F$, and every $m$-fold composition $T_{\mu_0}\cdots T_{\mu_{m-1}}$ is a $\rho$-contraction on $\bar B\cap\tilde F$ for some $\rho<1$.

Formalization targets

Goal: Proposition 6.4 (p. 97)

Under A.1–A.5 and $\tilde C$: $J^*\in\bar B\cap F^*$ is the unique fixed point of $T$ in $\bar B\cap F^*$, with $T(J')\le J'\Rightarrow J^*\le J'$ and $J'\le T(J')\Rightarrow J'\le J^*$; each $J_\mu$, $\mu\in\tilde M$, is the unique fixed point of $T_\mu$ in $\bar B\cap\tilde F$;

$$\lim_{N\to\infty}\|T^N(J)-J^*\|=0\ \ (J\in\bar B\cap F^*),\qquad\lim_{N\to\infty}\|T_\mu^N(J)-J_\mu\|=0\ \ (J\in\bar B\cap\tilde F);$$

a stationary $(\mu^*,\mu^*,\dots)\in\tilde\Pi$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$; and for every $\varepsilon>0$ some stationary policy in $\tilde\Pi$ satisfies $\|J^*-J_{\mu_\varepsilon}\|\le\varepsilon$.

Milestones

In attack order:

1. Proposition 6.3(a) (p. 96) — under A.1–A.4 and the exact selection assumption, a uniformly $N$-stage optimal policy exists iff the infimum in $T^{k+1}(J_0)(x)=\inf_{u\in U(x)}H[x,u,T^k(J_0)]$ is attained for each $x\in S$ and $k<N$.
2. Proposition 6.5(a) (p. 97) — under A.1–A.5, $\tilde C$ and exact selection: if for each $x$ some policy in $\tilde\Pi$ is optimal at $x$, then an optimal stationary policy exists in $\tilde\Pi$.

Further results of the chapter

The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:

• Proposition 6.2 — $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu_k^*}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$; such a policy forces $J^*_N=T^N(J_0)$.
• Proposition 6.1(a) — under Assumption $\tilde F.2$ and $J^*_k>-\infty$: $J^*_N=T^N(J_0)$ and $N$-stage $\varepsilon$-optimal policies exist in $\tilde\Pi$.
• Proposition 6.1(b) — under Assumption $\tilde F.3$ and $J_{k,\pi}<\infty$: $J^*_N=T^N(J_0)$ and $\{\varepsilon_n\}$-dominated convergence to optimality.
• Proposition 6.3(b) — compact level sets $U_k(x,\lambda)$ give both $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy.
• Proposition 6.5(b) — compact level sets of the iterates $T^k(J)$, $k\ge\bar k$, give an optimal stationary policy.

Significance

Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary $\varepsilon$-optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm $J^*_N=T^N(J_0)$, and their hypotheses ($\tilde F.3$, exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.

The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case ($F^*=\tilde F=F$, $\tilde M=M$) of Chapters 3 and 4.

Difficulty

The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to $T$ on $\bar B$. Here the obvious transcription fails at two points. First, $T$ maps $\bar B\cap F^*$ into itself but $T_\mu$ only maps $\bar B\cap\tilde F$ into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in $\tilde M$: pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.

Formalization scope

Functions on $S$ are S → EReal. $H$ is a total Lean function, but monotonicity is assumed only on $\tilde F$ and every statement evaluates $H$ only at functions of $\tilde F$. $J_\pi$ is limUnder; Assumption $\tilde C$ makes the limit exist. $B$ is Mathlib's $\ell^\infty(S,\mathbb R)$; a bound $\|G-G'\|\le c$ between extended-real functions means both are real everywhere and $|G(x)-G'(x)|\le c$, which is how the book's convention $\infty-\infty=\infty$ reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. $J^*_N$ and $J^*$ are infima over $\tilde\Pi$ only, the $\varepsilon$-optimality notions keep the book's two-case form at $-\infty$, and $N$ is a positive integer.

The chapter collapses to Chapters 3–4 if $F^*=\tilde F=F$ or $\tilde M=M$ is built in; here $F^*$, $\tilde F$ and $\tilde M$ are arbitrary and constrained only by A.1–A.5, and $J^*$ is never defined as a fixed point.

A complete development needs the $m$-step contraction mapping theorem on a closed subset of $\ell^\infty$, monotonicity lemmas for $T$ and $T_\mu$, and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption $\tilde C$ contraction, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 6. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control and Optimization 15(3), 1977, 438–464. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 1967, 165–177. https://doi.org/10.1137/1009030

Motivation

Linear programming, $\min\{c^\top x : Ax=b,\ x\ge0\}$ with $A\in\mathbb R^{d\times n}$, is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs $(x,s)$ with $x,s>0$ and $x_is_i=t$ for every $i$, as the path parameter $t$ decreases to $0$. A classical short-step method needs $O(\sqrt n\log(n/\delta))$ iterations, each solving a linear system with the matrix $A\frac XSA^\top$, for a total of roughly $n^{2.5}$ operations or more.

Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time $n^{\omega+o(1)}\log(n/\delta)$ (for the current values of the matrix multiplication exponent $\omega$ and its dual $\alpha$), matching the cost of multiplying two $n\times n$ matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.

Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the $O(\sqrt n\log(1/\delta))$ path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to $\widetilde O(\sqrt d)$; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached $n^\omega$; van den Brand (2020) derandomized the result.

Setting

Vectors are in $\mathbb R^n$ and products, quotients and roots of vectors are coordinatewise. For $\epsilon$ and vectors $a,b$, $a\approx_\epsilon b$ means $(1-\epsilon)b_i\le a_i\le(1+\epsilon)b_i$ for all $i$; $a\approx_\epsilon t$ for a scalar $t$ is defined likewise. The number of variables is $n\ge10$ and $A$ has full row rank $d\le n$.

The potential is $\Phi_\lambda(r)=\sum_{i=1}^n\cosh(\lambda r_i)$, evaluated at $r=\mu/t-1$ with $\mu=xs$; it is small exactly when every $x_is_i$ is close to $t$.

StochasticStep (Algorithm 1) takes positive $x,s$, a direction $\delta_\mu$, a sampling parameter $k$ and the output $\widetilde v$ of a data structure with $x/s\approx_{\epsilon_{\mathrm{mp}}}\widetilde v$. It rescales to $\overline x=x\sqrt{\widetilde v/w}$, $\overline s=s\sqrt{w/\widetilde v}$ ($w=x/s$), draws a sparse vector $\widetilde\delta_\mu$ with independent coordinates, $\widetilde\delta_{\mu,i}=\delta_{\mu,i}/p_i$ with probability $p_i=\min(1,k(\delta_{\mu,i}^2/\|\delta_\mu\|_2^2+1/n))$ and $0$ otherwise, and computes the step $(\widetilde\delta_x,\widetilde\delta_s)$ through the projection $\overline P=\sqrt{\overline X/\overline S}A^\top(A\frac{\overline X}{\overline S}A^\top)^{-1}A\sqrt{\overline X/\overline S}$. The draw is repeated until $\|\overline s^{-1}\widetilde\delta_s\|_\infty$ and $\|\overline x^{-1}\widetilde\delta_x\|_\infty$ are at most $1/(100\log n)$; the output is $(x+\widetilde\delta_x,s+\widetilde\delta_s)$.

Main (Algorithm 2) sets $\epsilon=\frac1{40000\log n}$, $\epsilon_{\mathrm{mp}}=\frac1{40000}$, $k=1000\epsilon\sqrt n\log^2n/\epsilon_{\mathrm{mp}}$, $\lambda=40\log n$, starts at $t=1$, and in each iteration sets $t^{\mathrm{new}}=(1-\frac{\epsilon}{3\sqrt n})t$, takes the direction

$$\delta_\mu=\Big(\frac{t^{\mathrm{new}}}{t}-1\Big)xs-\frac\epsilon2t^{\mathrm{new}}\frac{\nabla\Phi_\lambda(\mu/t-1)}{\|\nabla\Phi_\lambda(\mu/t-1)\|_2},$$

runs StochasticStep, and falls back to a deterministic ClassicalStep whenever $\Phi_\lambda(\mu^{\mathrm{new}}/t^{\mathrm{new}}-1)>n^3$.

Formalization targets

Goal: Lemma 4.14

For every iteration $j$, almost surely Assumption 4.1 holds for the input of iteration $j$ (in particular $x^js^j\approx_{0.1}t_j$ and $\|\delta_\mu\|_2\le\epsilon t_j$), almost surely the resampling loop of iteration $j$ succeeds with positive probability, and

$$\mathbb P(\text{ClassicalStep is used in iteration }j)\le\frac{10}{n^2}.$$

The paper writes $O(1/n^2)$; its proof gives the constant $10$.

Milestones

Lemma A.1 (variance of a product), Lemma 4.12 (properties of $\Phi_\lambda$), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of $\mu^{\mathrm{new}}$), and Lemma 4.13:

$$\mathbf E\Big[\Phi_\lambda\Big(\frac{\mu^{\mathrm{new}}}{t^{\mathrm{new}}}-1\Big)\Big]\le\Phi_\lambda\Big(\frac\mu t-1\Big)-\frac{\lambda\epsilon}{15\sqrt n}\Big(\Phi_\lambda\Big(\frac\mu t-1\Big)-10n\Big).$$

Significance

Lemma 4.14 is what makes the randomized method usable: the iterates stay in the $0.1$-neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, $\widetilde O(n^{2.5})\cdot 10/n^2$, is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).

The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).

The running-time claims of the paper (Theorem 2.1's expected time $n^{\omega+o(1)}$, Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.

Difficulty

The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that $\Phi_\lambda$ is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps $\Phi_\lambda$ at $n^3$, and by an induction over iterations of $\mathbf E[\Phi]\le10n$ under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.

Formalization scope

Coordinates are Fin n, vectors Fin n → ℝ, $A$ a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and $\log$ the natural logarithm. $\|\cdot\|_2$ is written out as $\sqrt{\sum_iv_i^2}$; $\|\cdot\|_\infty\le c$ is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every $\mathbf E$, $\mathbf{Var}$ of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value $\overline P(\overline X\overline S)^{-1/2}\widetilde\delta_\mu$; the data structure and ClassicalStep are arbitrary measurable functions $U_j$, $C_j$ of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. $n$ is the number of variables of the program the loop runs on.

Deviations from the page, all recorded in the items: Assumption 4.1 is used with $\epsilon\le1/(40000\log n)$ instead of the printed $<$, because Main sets $\epsilon$ to exactly that value; $O(1/n^2)$ is instantiated as $10/n^2$, the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while $t>\delta^2/(32n^3)$; at $\nabla\Phi_\lambda=0$ the second term of $\delta_\mu$ is $0$. No hypothesis $k\le n$ is imposed.

A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles $U_j$, $C_j$ cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.

Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.

Selected references

• M. B. Cohen, Y. T. Lee, Z. Song, Solving Linear Programs in the Current Matrix Multiplication Time, J. ACM 68(1), Article 3, 2021. https://doi.org/10.1145/3424305 (arXiv:1810.07896, https://arxiv.org/abs/1810.07896)
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984. https://doi.org/10.1007/BF02579150
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40, 1988. https://doi.org/10.1007/BF01580724
• P. M. Vaidya, Speeding-up linear programming using fast matrix multiplication, Proc. 30th FOCS, 1989.
• Y. T. Lee, A. Sidford, Path finding methods for linear programming, FOCS 2014. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, Z. Song, Q. Zhang, Solving Empirical Risk Minimization in the Current Matrix Multiplication Time, COLT 2019. https://arxiv.org/abs/1905.04447
• J. van den Brand, A deterministic linear program solver in current matrix multiplication time, SODA 2020. https://doi.org/10.1137/1.9781611975994.16

Motivation

The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.

Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.

Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.

Setting

A population consists of $M\ge2$ individuals, each carrying an allelic type. Its description is $\mathbf M=(M_1,\dots,M_M)$, where $M_i$ is the number of allelic types carried by exactly $i$ individuals, so that

$$\sum_{i=1}^{M} iM_i=M. \qquad (7.3)$$

For a real parameter $\nu>0$, the Ewens distribution on descriptions is

$$\pi_M(\mathbf M)=\binom{\nu+M-1}{M}^{-1}\prod_{i=1}^{M}\Big(\frac{\nu}{i}\Big)^{M_i}\frac{1}{M_i!}, \qquad (7.6)$$

where $\binom{x}{k}=x(x-1)\cdots(x-k+1)/k!$ is the binomial coefficient for real $x$. In the infinite alleles model, individuals die at rate $\mu$, each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability $u$; then (7.6) is the equilibrium distribution with $\nu=(M-1)u/(1-u)$ (7.5).

A random sample of size $1\le m\le M$ without replacement is a uniformly random $m$-element subset of the $M$ labelled individuals, each of the $\binom Mm$ subsets being equally likely; the sample has a description in the same sense.

The number $j$ of individuals carrying one given allele performs a random walk on $\{0,\dots,M\}$ with intensities

$$q(j,j-1)=\mu\frac jM\Big(\frac{M-j}{M-1}+\frac{j-1}{M-1}u\Big),\qquad q(j,j+1)=\mu\frac{M-j}{M}\frac{j}{M-1}(1-u). \qquad (7.8)$$

An allele is quasi-fixed when it is the only allele present ($j=M$).

Formalization targets

Goal: consistency under sampling (Theorem 7.1)

If $M\ge2$ and the population description is distributed as $\pi_M$, then a random sample of size $1\le m\le M$ drawn without replacement has description $\mathbf m$ with probability $\pi_m(\mathbf m)$, the same $\nu$ being used for both sizes:

$$\sum_{\mathbf M}\pi_M(\mathbf M)\,P\big(\text{sample has description }\mathbf m\mid\text{population has description }\mathbf M\big)=\pi_m(\mathbf m).$$

Milestones

1. (7.6) is a distribution: $\pi_M(\mathbf M)>0$ and $\sum_{\mathbf M}\pi_M(\mathbf M)=1$ (Exercise 7.1.3).
2. Theorem 7.1 for $m=M-1$, the case the book's proof establishes first.
3. Corollary 7.5, the identity of its proof: the probability that a uniformly chosen individual's allele is carried by exactly $i$ individuals is

$$\sum_{\mathbf M}\frac{iM_i}{M}\pi_M(\mathbf M)=\frac{\nu}{M}\binom{\nu+M-1}{i}^{-1}\binom Mi. \qquad (7.9)$$

4. Theorem 7.9: the probability $Q$ that the walk (7.8) started at $1$ reaches $M$ before $0$ satisfies

$$Q^{-1}=\sum_{i=0}^{M-1}\binom{M-1}{i}^{-1}\binom{\nu+M-1}{i}.$$

Significance

The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on $\nu$. Kelly deduces from it the sufficiency of the number of alleles in a sample for $\nu$ and the heterozygosity $\nu/(\nu+1)$ (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).

Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.

Difficulty

The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between $M-1$ and $M$, a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives $\pi_{M-1}$ and $\pi_M$. Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of $m$-subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.

Formalization scope

• Descriptions of $n$ individuals are integer partitions Nat.Partition n, with $M_i$ the multiplicity of the part $i$; the product in (7.6) runs over $i=1,\dots,n$. The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.
• The population is Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is $\binom Mm^{-1}$ times the number of $m$-subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.
• The goal and Corollary 7.5 quantify over an arbitrary choice of labelling for each population description. They assume $M\ge2$, as required by the chapter's rule that a parent is chosen among the other $M-1$ individuals; the goal also assumes $1\le m\le M$. Because $\pi_M>0$, this forces the conditional sampling law to depend on the population only through its description. Types are natural numbers, so every description is realized and the hypothesis is never vacuous.
• The quasi-fixation probability is defined through the jump chain of (7.8): the limit of the probabilities of reaching $M$ within $n$ jumps without reaching $0$. The theorem assumes $M\ge2$, $\mu>0$, $0<u<1$ and $\nu=(M-1)u/(1-u)$.
• Corollary 7.5 is formalized as the identity of its proof. The identification of the oldest allele's frequency with that of a randomly chosen individual uses allele ages and the reversibility of the labelled process (Theorem 7.2) and is not formalized. Theorem 7.2 itself, whose state space orders the allele labels within each class, and the allele-age results (Corollaries 7.3, 7.4, 7.7, 7.8, Theorem 7.6, Corollary 7.10, Theorem 7.11) are not part of the mission.

Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity $(1-x)^{-\nu}=\prod_j e^{\nu x^j/j}$) are reusable beyond this mission.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979, Chapter 7. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• W. J. Ewens, The sampling theory of selectively neutral alleles, Theoretical Population Biology 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
• J. F. C. Kingman, The representation of partition structures, Journal of the London Mathematical Society (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
• M. Kimura and J. F. Crow, The number of alleles that can be maintained in a finite population, Genetics 49 (1964), 725–738. https://doi.org/10.1093/genetics/49.4.725

Motivation

The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.

Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.

Setting

Time is indexed by the integers $t \in \mathbb Z$. The retailer faces i.i.d. demand

$$D_t = \mu + \epsilon_t,$$

where the error terms $\epsilon_t$ are independent and identically distributed from a symmetric distribution with mean $0$ and variance $\sigma^2 > 0$.

Single-stage policy (§2). With $p \ge 1$ observations, a lead time $L$, a safety factor $z$ and a constant $C_{L,\rho}$, the retailer forms the moving-average estimates

$$\hat D^L_t = L\,\frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat\sigma^L_{et} = C_{L,\rho}\sqrt{\frac{\sum_{i=1}^p e_{t-i}^2}{p}}, \qquad e_t = D_t - \hat D^1_t,$$

raises its inventory position to the order-up-to point $y_t = \hat D^L_t + z\hat\sigma^L_{et}$, and so orders $q_t = y_t - y_{t-1} + D_{t-1}$. Orders may be negative: excess inventory is returned without cost.

Decentralized chain (§3). Stages $k = 1, 2, \dots$ form a serial chain; stage 1 is the retailer, and $L_k$ is the lead time between stages $k$ and $k+1$. No stage sees customer demand except the retailer. Stage $k$ forecasts from the orders it receives,

$$\hat D^{(1)}_t = \frac{\sum_{i=1}^p D_{t-i}}{p}, \qquad \hat D^{(k)}_t = \frac{\sum_{j=0}^{p-1} q^{k-1}_{t-j}}{p} \quad (k \ge 2),$$

uses the order-up-to point $y^k_t = L_k\hat D^{(k)}_t$, and orders

$$q^1_t = y^1_t - y^1_{t-1} + D_{t-1}, \qquad q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t \quad (k \ge 2).$$

Formalization targets

Goal: Theorem 3.2 (Eq. (7))

For every stage $k \ge 1$ and every period $t$,

$$\frac{\operatorname{Var}(q^k_t)}{\operatorname{Var}(D_t)} \;\ge\; \prod_{i=1}^{k}\left(1 + \frac{2L_i}{p} + \frac{2L_i^2}{p^2}\right).$$

The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.

Milestone: Eq. (6)

For the single-stage policy with any safety factor $z$ and any constant $C_{L,\rho}$,

$$\frac{\operatorname{Var}(q_t)}{\operatorname{Var}(D_t)} \;\ge\; 1 + \frac{2L}{p} + \frac{2L^2}{p^2}.$$

This is the i.i.d. case $\rho = 0$ of the paper's Theorem 2.2. With $z = 0$ and $L = L_1$ the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case $k = 1$ of the goal.

Significance

The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage $k$ in the i.i.d. case equals $1 + 2(\sum_{i\le k}L_i)/p + 2(\sum_{i\le k}L_i)^2/p^2$ (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio $L/p$.

Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at $\rho = 0$); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean $0$ and variance $\sigma^2$. Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.

Difficulty

The natural first idea is induction on the stage: treat the orders of stage $k-1$ as the demand of stage $k$ and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage $k \ge 2$ are not i.i.d.: they are autocorrelated, and stage $k$'s moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term $z\hat\sigma^L_{et}$ is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.

Formalization scope

All objects live in the namespace ChenBullwhip.Decentralized.

• IIDDemand P is the demand model on a probability space $(\Omega, P)$: a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in $L^2$, with mean $0$ and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.
• SingleStage defines $\hat D^L_t$, $e_t$, $\hat\sigma^L_{et}$, $y_t$ and $q_t$ of §2; $C_{L,\rho}$ is a free real parameter, as the paper does not fix it.
• Chain defines the forecasts $\hat D^{(k)}_t$ and the orders $q^k_t$ by recursion on the stage, with the convention $q^0_t = D_{t-1}$, so that stage 1 orders $y^1_t - y^1_{t-1} + D_{t-1}$. The recursion $q^k_t = y^k_t - y^k_{t-1} + q^{k-1}_t$ is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is $q^{k-1}_t$, as the sequence of events on p. 440 describes.

Disclosed hypotheses not on the page: $p \ge 1$ (a moving average needs an observation), $\sigma > 0$ (the paper divides by $\operatorname{Var}(D) = \sigma^2$), and square-integrable errors (Mathlib's variance is $0$ off $L^2$). The paper's model (1) asks $\mu \ge 0$; since $\mu$ affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period $t$, with no stationarity hypothesis.

Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is $\sigma^2 > 0$.

A complete development needs variance and covariance calculus for finite linear combinations of independent $L^2$ variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.

Selected references

• F. Chen, Z. Drezner, J. K. Ryan, D. Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain: The Impact of Forecasting, Lead Times, and Information, Management Science 46(3):436–443, 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• H. L. Lee, V. Padmanabhan, S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546
• J. K. Ryan, Analysis of Inventory Models with Limited Demand Information, Ph.D. dissertation, Department of Industrial Engineering and Management Science, Northwestern University, 1997.
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13 (formalized on Prove2Me as SupplyChainTheory.*).

Motivation

A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?

This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless $\mathrm{P}=\mathrm{NP}$, d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.

Historical note

The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.

Setting

Let $X=\{x_0,\ldots,x_{n-1}\}$ be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size $n$; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function $\nu:X\to\{0,1\}$. A positive literal $x_i$ is true when $\nu(x_i)=1$; a negative literal $\neg x_i$ is true when $\nu(x_i)=0$. A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.

The input also contains one positive integer weight $c_i$ for each variable and a positive threshold $t$. The weight of an assignment is

$$w(\nu)=\sum_{i=0}^{n-1} c_i\nu(x_i).$$

The DNF is valid for this problem when every literal index is below $n$ and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least $t$.

Formalization targets

Partial result — weighted satisfiability

For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least $t$ has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.

Partial result — unary-weight falsifiability

For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.

Goal — binary-weight falsifiability

For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.

The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.

Dependency graph

Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)

Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.

Significance

A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly $t$) is a different problem and is outside this mission's scope; the goal here is specifically weight at least $t$.

Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.

Difficulty

The direct search over all $2^n$ assignments is exponential in $n$. Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.

Formalization scope

The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.

The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.

The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.

Selected references

• Albertine Amarilli, “Weighted falsifiability for unambiguous DNFs,” List of open questions in theoretical computer science, https://a3nm.net/work/research/questions/#weighted-falsifiability-for-unambiguous-dnfs.
• Mikaël Monet, “Is this problem on unambiguous DNFs hard?”, Theoretical Computer Science Stack Exchange, https://cstheory.stackexchange.com/questions/53733/is-this-problem-on-unambiguous-dnfs-hard.

Motivation

Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?

F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on $\{0,1,2,\dots\}$, stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.

Timeline:

• 1951–1953, Kendall. Introduces the imbedded chains of M/G/1 and GI/M/1 and obtains most of their classification by direct methods.
• 1953, Foster. Derives the classification from general criteria: Theorem 2 (ergodicity), Theorems 4–6 (transience and recurrence).
• 1950s onward. The criteria become the standard tools (Feller's text; later the drift conditions of Meyn and Tweedie).

Setting

A Markov chain on the states $\{0,1,2,\dots\}$ is given by a transition matrix $P=[p_{ij}]$: $p_{ij}\ge0$ and $\sum_j p_{ij}=1$ for every row $i$. Write $f_{ij}^{(n)}$ for the probability that the chain started in $i$ first reaches $j$ (for $i=j$, first returns to $j$) at step $n\ge1$. The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor $1$. A state $j$ is recurrent if $f_{jj}=\sum_n f_{jj}^{(n)}=1$ and transient if $f_{jj}<1$; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time $\sum_n n f_{jj}^{(n)}$ is finite. The mean first-passage time from $i$ to $j$ is $\mu_{ij}=\sum_{n\ge1} n f_{ij}^{(n)}\in[0,\infty]$.

The M/G/1 matrix is built from a sequence $k_0,k_1,\dots$ of positive numbers summing to one ($k_n$ is the probability of $n$ arrivals during one service):

$$[p_{ij}] = \begin{bmatrix} k_0 & k_1 & k_2 & \cdots \\ k_0 & k_1 & k_2 & \cdots \\ 0 & k_0 & k_1 & \cdots \\ 0 & 0 & k_0 & \cdots \\ \vdots & \vdots & \vdots & \end{bmatrix},$$

that is, $p_{0j}=k_j$ and, for $i\ge1$, $p_{ij}=k_{j-i+1}$ when $j\ge i-1$ and $0$ otherwise. The traffic intensity is

$$\rho=\sum_{n=1}^{\infty}n\,k_n\in[0,\infty],$$

the mean number of arrivals per service.

Formalization targets

Goal: the M/G/1 classification (§3, p. 358)

$$\text{the chain is ergodic}\iff\rho<1,\qquad\text{the chain is recurrent}\iff\rho\le1 .$$

The goal leaves $k$ arbitrary apart from positivity and normalization; in particular $\rho=\infty$ is allowed and falls in the transient case.

Milestones (the paper's general theorems and the step of §3 they feed)

1. Theorem 2 (drift criterion): a nonnegative solution of $\sum_j p_{ij}y_j\le y_i-1$ ($i\ne0$) with $\sum_j p_{0j}y_j<\infty$ makes the system ergodic. Already posed on the platform and referenced here.
2. Theorem 3: in an ergodic system the mean first-passage times $d_j=\mu_{j0}$ are finite and satisfy $\sum_{j\ge1}p_{ij}d_j=d_i-1$ ($i\ne0$), $\sum_{j\ge1}p_{0j}d_j<\infty$.
3. §3 display: for the ergodic M/G/1 chain, $\mu_{i,i-1}=\mu_{10}$ and $\mu_{i0}=i\mu_{10}$ ($i\ne0$).
4. Theorem 5: a solution of $\sum_j p_{ij}y_j\le y_i$ ($i\ne0$) with $y_i\to\infty$ makes the system recurrent.
5. Theorem 7: for a probability distribution $\{p_n\}$ with $p_0>0$, $\sum_n z^np_n=z$ has a root in $(0,1)$ iff $\sum_{n\ge1}np_n>1$.
6. Theorem 4: the system is transient iff $\sum_j p_{ij}y_j=y_i$ ($i\ne0$) has a bounded nonconstant solution.

Significance

The result. The classification is the stability theorem for the M/G/1 queue: for $\rho<1$ the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for $\rho=1$ the queue empties infinitely often but has no steady state; for $\rho>1$ it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.

Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.

Difficulty

The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the $n$-step probabilities $p_{ij}^{(n)}$ and of hitting probabilities of state $0$, none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic $\Rightarrow\rho<1$, recurrent $\Rightarrow\rho\le1$) need exact identities for mean first-passage times, not just bounds, and these must be handled in $[0,\infty]$ because the means may be infinite. And the boundary case $\rho=1$ (null recurrence) separates the two equivalences: an argument that only compares the mean drift $\rho-1$ with $0$, such as a law of large numbers for the increments, cannot tell recurrence from transience there.

Formalization scope

• The chain is the published QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to $1$ as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.
• States are indexed from $0$, as in the paper; "$i\ne0$" is i ≠ 0.
• The M/G/1 matrix is a function mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for $k_i=2^{-(i+1)}$).
• $\sum_n k_n=1$ is added as the meaning of "stochastic matrix"; §3 writes only $k_i>0$.
• $\rho$ and all mean first-passage times are extended nonnegative reals ($[0,\infty]$), so divergent means are $\infty$, never $0$. Theorem 7's mean is also taken in $[0,\infty]$.
• Recurrent means $f_{jj}=1$ for every state $j$; transient means $f_{jj}<1$ for every state. For irreducible chains these are complementary, which is a theorem, not a definition.
• The general Theorems 3, 4 and 5 assume irreducibility and aperiodicity, the paper's standing assumption of §1. The goal does not assume them: they follow from $k_i>0$.
• Every series in a hypothesis carries its convergence (Summable or HasSum); Theorem 3's equation (6) is written as $d_i=1+\sum_{j\ge1}p_{ij}d_j$ in $[0,\infty]$ together with finiteness of the $d_j$, $j\ne0$.
• Theorem 7's distribution is renamed $q$ in Lean to avoid a clash with $p_{ij}$. Theorem 1 of the paper (§2) and Theorem 6 are not targets of this mission.

Ruled out: $\rho$ as a real tsum (which is $0$ for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix $P$ that need not exist.

Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem $p_{ij}^{(n)}\to\pi_j$ for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 355–360, 1953. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Some problems in the theory of queues, Journal of the Royal Statistical Society B 13(2), 151–185, 1951. https://doi.org/10.1111/j.2517-6161.1951.tb00093.x
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, The Annals of Mathematical Statistics 24(3), 338–354, 1953. https://doi.org/10.1214/aoms/1177728975
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, Wiley, 1950.
• S. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511626630