All missions

Motivation

This mission develops Chapter 5 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

The period-finding problem: we are given $f:\mathbb N\to\{0,\dots,N-1\}$ for which there is an unknown $r\in\{1,\dots,N\}$ with $f(a)=f(b)$ if and only if $a\equiv b\pmod r$.

Let $q=2^\ell$ be the power of two with $N^2<q\le2N^2$ and $n=\lceil\log_2N\rceil$. Let $O_f$ be the unitary $|a\rangle|z\rangle\mapsto|a\rangle|z\oplus f(a)\rangle$ on $\ell+n$ qubits, with $a$ read as an $\ell$-bit number and $f(a)$ written in $n$ bits, and let $F_q$ be the quantum Fourier transform on the first register. One run of Shor's algorithm prepares

(one evaluation of $f$ and two Fourier transforms) and measures the first register in the computational basis, obtaining $b\in\{0,\dots,q-1\}$. Call $b$ good if

Then:

1. There are constants $C>0$ and $N_0$ such that for every $N\ge N_0$, every $r\in\{1,\dots,N\}$ and every $f$ as above with period $r$, the outcome is good with probability at least $C/\log\log N$. Hence an expected number of $O(\log\log N)$ independent runs (each with one evaluation of $f$ and two QFTs) produces a good outcome.
2. If $|b/q-c/r|\le1/(2q)$ with $1\le r\le N$, $0\le c<r$ and $\gcd(c,r)=1$, then $c/r$ is the only fraction $p/s$ with $1\le s\le N$ within distance $1/(2q)$ of $b/q$, and the denominator of $c/r$ in lowest terms is $r$.

So a good outcome determines $r$: continued-fraction expansion of $b/q$ finds the unique fraction with denominator at most $N$ near $b/q$, and its denominator is the period. This is the quantum core of Shor's factoring algorithm.

Formalization Note The state $|\Phi\rangle$ is the shared shorRunState, with $\ell=\lceil\log_2(N^2+1)\rceil$ (which gives $N^2<2^\ell\le2N^2$) and second register $\lceil\log_2N\rceil$ qubits. The intermediate measurement of the second register is omitted: it does not change the distribution of the first register. The probability of a good outcome is the total weight of the basis states whose first register is good. The constants $C$ and $N_0$ are quantified before $N$, $r$ and $f$. The source's per-run constant $4/\pi^2$ is not stated (see notes).

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §5.2: Factoring reduces to period finding: the number-theoretic core of Shor's reduction.
• §5.3: One run of Shor's period-finding circuit reveals the period with probability Omega(1/log log N).

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Ronald de Wolf, Quantum Computing: Lecture Notes, 27 August 2026. https://homepages.cwi.nl/~rdewolf/qcnotes.pdf.

Motivation

The value of the Riemann zeta function at five is the convergent sum

The target is that this number cannot be expressed as a ratio of integers. This mission concerns the complete proof development in mo271/Zeta5, pinned to commit 7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. The repository follows Aabir Fauzan's preprint ζ(5) is irrational, while explicitly changing parts of its arithmetic normalization. Its formal target is the individual value at five. Results asserting that at least one member of a list of odd zeta values is irrational do not establish this target.

The repository reports a complete Lean proof with only the standard axioms propext, Classical.choice, and Quot.sound. That is a statement about the source project. The existing Prove2.me goal remains Open, and importing and checking the source proof against the platform environment is the work tracked here. The exact existing goal is reused as a reference; there is no second copy of the irrationality assertion.

Setting

The construction uses Hankel matrices, whose entries depend on the sum of their row and column indices. For a natural index $n$, put $K=40n$, $N=3n$, and $h=37n$. The rational polynomial $D_m(t)=\prod_{j=1}^m(t+j^2)$ controls a family of rational functions. A rational linear functional takes prescribed Bernoulli-number values on powers of $t$ and prescribed affine-polynomial values on the simple poles $(t+j^2)^{-1}$. Polynomial division and residues extend it to $P(t)/D_K(t)$.

Applying this functional to $D_N(t)^6t^{i+j}/D_K(t)$ gives an $h\times h$ matrix $G_n(X)$ over $\mathbb Q[X]$. Write $\Delta_n(X)=\det G_n(X)$ and $F_n(X)=S_n\Delta_n(X)$, where $S_n$ is the explicit positive factorial ratio in the construction module. These are specified polynomials; their existence and properties are not abstract supply assumptions. The real number zeta5 is the convergent series, and a short bridge identifies it with Mathlib's complex zeta value.

Formalization targets

The goal is

It is the existing theorem FCP.Zeta.irrational_zeta_five. The supporting target from the source main estimate is

The formal statement also requires $Q_n$ to be a positive rational multiple of the explicit $F_n$.

The milestone list records the general polynomial irrationality criterion, the exact degree calculation, the moment representation with integrability, strict determinant positivity, the real-value upper bound, integral normalization with its growth estimate, and the final small-value statement. A further supporting theorem states that $b^{37n}e^{-cn^2}$ tends to zero for every fixed positive integer $b$ and every $c>0$. These targets cover the analytic, arithmetic, and final assembly parts of the source project.

Significance

The goal distinguishes a single zeta value from the disjunctive irrationality results for finite lists. The intermediate results also provide reusable infrastructure: an irrationality criterion for polynomials of varying degree, integral moment representations of rational functionals, determinant positivity, and estimates controlling rational normalizers.

For formalization, the concrete task is to transplant the source development while preserving its definitions, hypotheses, and actual constants. The source's existing proofs provide the intended implementations; the mission does not replace the difficult analytic or arithmetic statements with assumed approximation families. Proof imports and accepted submissions must eventually connect those implementations to the existing goal. The source's Apache-2.0 license and commit-pinned attribution accompany the code.

Difficulty

Small real values alone do not suffice: the integer coefficients and the degree growth must be controlled at the same time. The normalization needed to obtain integer coefficients can enlarge the values enough to destroy the analytic estimate. The decisive quantitative requirement is that its growth constant stay below the magnitude of the negative analytic constant.

Here the analytic estimate uses $U=-2733991/2000000$, and the implemented normalization uses $A_{\rm eff}=136/100$. Their exact rational sum is negative. The milestone assertions retain the source's lower-order terms $27K\log K+200K$ and the eventual quantifiers in the normalization estimate. They do not strengthen an eventual estimate to a uniform one, or infer positivity from a vanishing upper bound.

Formalization scope

The scope is the complete importable proof path to Apery.irrational_five in the pinned repository, including the arithmetic modules, logarithmic-energy estimates, finite certificates, and the external prime-number-theorem dependency where the proof uses it. The headline milestones organize that full development; they are not a claim that every internal lemma is already published on the platform. The repository's optional stronger numerical rate and the preprint's irrationality-measure claim are outside this goal.

The source uses cutoff $400$, a full rank loss in its outer-prime estimate, and direct class-wise partial fractions, as documented in its implementation notes. Its final estimate asserts some positive decay constant, not the paper's $139/5$. The draft retains those choices. Polynomial evaluations take place over the reals, coefficients begin in the rationals and are normalized into the integers, and the moment integrals are Lebesgue integrals over $(0,\infty)$. Definitions are total at zero, while the positivity and real-bound milestones explicitly require $n>0$.

The source pins Lean 4.34.0-rc1 and Mathlib f385f9fd18abed332ebcd3df239cb357e264aceb. This proposal targets the available Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 environment. The draft definitions and milestone statements are checked locally in that target environment; acceptance of the complete imported proof graph is a separate verification step. The external dependency is mo271/PrimeNumberTheoremAnd at 04d81b2a68ea3548b9990813fdc463c78511f412. Any imported proof must retain a standard-axiom-only dependency check.

Selected references

• Aabir Fauzan, ζ(5) is irrational, preprint, 17 September 2026. Zenodo record and manuscript.
• mo271 and contributors, Zeta5, Lean source project, commit 7fe736760f4b96bfdb4334b68e3b3124ecbe10b0. Pinned repository.
• mo271 and contributors, PrimeNumberTheoremAnd, pinned dependency. Source.
• The Formal Conjectures Authors, Formal Conjectures, RiemannZetaValues.irrational_five. Pinned challenge source.

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$. They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$, and every job has unit execution requirement $p_j=1$, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) are the case $q_i=1$; uniform machines ($Q$) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$. Resource $R_h$ has a positive integer size $s_h$, the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$. Its completion time is $C_j=S_j+1/q_{\mu(j)}$, and it is being executed at every time $t$ with $S_j\le t<C_j$. A schedule is feasible when:

• jobs on the same machine do not overlap in time;
• at every time $t$, the set $S_t$ of jobs being executed satisfies

The makespan is $C_{\max}=\max_j C_j$.

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$, and every requirement satisfies $r_{hj}\le1$. A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$, whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$:

• PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
• PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$, required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

1. The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
2. The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$.
3. Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
4. The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$, $q_2=1$ has a feasible schedule with $C_{\max}\le t$.

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$, so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

• Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$, and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
• Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
• Decision versions. "NP-hard" refers to the decision version with a threshold $y$. Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
• Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$, so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
• Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
• Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$-factor.
• Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$. A diagonal resource would make every job infeasible.
• Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

• J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.

Timeline:

• 1970: Edmonds proves the polymatroid intersection theorem.
• 1982: Frank proves the discrete separation theorem for submodular/supermodular set functions, with integrality.
• 1984: Fujishige proves a Fenchel-type min-max theorem for submodular functions.
• 1976–1981: Iri and Tomizawa characterize optimality for independent assignment by potentials; Frank proves the weight splitting theorem for weighted matroid intersection (1981).
• Early 1990s: Dress and Wenzel introduce valuated matroids.
• 1995–1996: Murota proves the valuated matroid intersection theorem (SIAM J. Discrete Math. 9, 1996) and the M-concave intersection theorem (Bonn report, 1995), and in the present paper the Fenchel-type duality (Theorem 6.4).
• Later: the result becomes the central duality theorem of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM, 2003).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is its characteristic vector; for $x\in\mathbb R^V$, $\operatorname{supp}^{\pm}(x)$ are the sets of coordinates where $x$ is positive or negative, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v\in B$. These are exactly the integer points of integral base polytopes of submodular systems. $\overline B$ is the convex hull of $B$.

A function $\omega:B\to\mathbb R$ has the exchange property (EXC), and is called M-concave, if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and

A function $\zeta$ is M-convex when $-\zeta$ is M-concave.

For $\omega:B_1\to\mathbb R$ and $\zeta:B_2\to\mathbb R$ the concave conjugate and convex conjugate are

and the concave closure and convex closure are $\hat\omega(b)=\inf_p(\langle p,b\rangle-\omega^\circ(p))$ and $\check\zeta(b)=\sup_p(\langle p,b\rangle-\zeta^\bullet(p))$; they are finite exactly on $\overline{B_1}$ and $\overline{B_2}$.

The primal problem maximizes $\omega(x)-\zeta(x)$ over $x\in B_1\cap B_2$; the relaxed primal problem maximizes $\hat\omega(b)-\check\zeta(b)$ over $b\in\overline{B_1}\cap\overline{B_2}$; the dual problem minimizes $\zeta^\bullet(p)-\omega^\circ(p)$ over $p\in\mathbb R^V$. A maximum over an empty family is $-\infty$.

Formalization targets

Goal: Theorem 6.4

If $\omega$ and $-\zeta$ satisfy (EXC), then

with (P1) a finite dual infimum forces $B_1\cap B_2\neq\emptyset$, and (P2) if $B_1\cap B_2\neq\emptyset$ all values are finite and equal and the infimum is attained. If $\omega,\zeta$ are integer-valued, the infimum may be taken over $p\in\mathbb Z^V$ and is attained there when finite.

Milestones

1. Lemma 6.3 (weak duality): for arbitrary $\omega,\zeta$ on finite nonempty sets, primal $\le$ relaxed $=$ dual (the Fenchel identity (6.5)).
2. Lemma 6.1: $(-f)^\circ(p)=-f^\bullet(-p)$ and $(-f)^\wedge=-\check f$ on $\overline B$.
3. Lemma 4.5: an M-concave $\omega$ satisfies $\hat\omega=\omega$ on $B$.
4. Theorem 2.1: (B1) is equivalent to being the integer points of an integral submodular (or supermodular) base polytope, with the describing functions $\max_{x\in B}x(X)$ and $\min_{x\in B}x(X)$.
5. Theorem 6.5 (Frank's discrete separation theorem, cited in the paper).
6. Lemma 6.7: four equivalent forms of boundedness of the dual problem.
7. Theorem 6.6 (the M-concave intersection theorem, cited in the paper): optimality of $x^*$ for $\omega_1+\omega_2$ is equivalent to a potential $p^*$ with $x^*$ maximizing both $\omega_1[-p^*]$ and $\omega_2[p^*]$, integral when the data are.

Significance

The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.

All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.

Difficulty

Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope $\overline{B_1}\cap\overline{B_2}$ must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of $\overline{B_1}\cap\overline{B_2}$ (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that $p$ can be taken integral, is again specific to (EXC) and fails for general concave extensions.

Formalization scope

Lean conventions, all in namespace SteinitzExchange.Duality:

• $V$ is a type with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).
• A function on $B$ is a total (V → ℤ) → ℝ used only at points of $B$. M-convexity of $\zeta$ is (EXC) for fun x => -ζ x; $\omega$ lives on $B_1$ and $\zeta$ on $B_2$, which are distinct sets in general.
• Conjugates are real-valued min/max over the finite set. The closures are real ⨅/⨆ over $p\in\mathbb R^V$ and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of $\mp\infty$, which no statement uses.
• The three optimal values are in EReal, as suprema and infima of coerced reals, so no $\infty-\infty$ occurs. EReal's supremum of the empty family is $-\infty$, the paper's convention. The dual infimum is never a real ⨅ (which would return $0$ when unbounded and make (P1) meaningless).
• Every "max" of the page includes attainment: (P2) asserts points $x$, $b$, $p$ at which the three values are achieved; the integral dual infimum is attained when it is not $-\infty$.
• "Integer-valued" means $\omega(x)\in\mathbb Z$ on $B_1$ and $\zeta(x)\in\mathbb Z$ on $B_2$; integral potentials and separating vectors are V → ℤ.
• Theorem 2.1's "$\forall X\subset V$" is read as all $X\subseteq V$.

Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from $\zeta^\circ$ instead of $\zeta^\bullet$, a single base set for both functions, and a relaxed maximum taken over all of $\mathbb R^V$ instead of $\overline{B_1}\cap\overline{B_2}$.

Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
• K. Murota, Valuated matroid intersection I: optimality criteria, SIAM J. Discrete Math. 9 (1996) 545–561.
• K. Murota, Submodular flow problem with a nonseparable cost function, Report 95843-OR, Forschungsinstitut für Diskrete Mathematik, Universität Bonn, 1995 (source of Theorem 6.6).
• A. Frank, An algorithm for submodular functions on graphs, Annals of Discrete Mathematics 16 (1982) 97–120 (source of Theorem 6.5).
• A. Frank, A weighted matroid intersection algorithm, J. Algorithms 2 (1981) 328–336.
• J. Edmonds, Submodular functions, matroids and certain polyhedra, in: Combinatorial Structures and Their Applications, Gordon and Breach, New York, 1970, 69–87.
• S. Fujishige, Theory of submodular programs: a Fenchel-type min-max theorem and subgradients of submodular functions, Mathematical Programming 29 (1984) 142–155.
• M. Iri and N. Tomizawa, An algorithm for finding an optimal "independent assignment", J. Oper. Res. Soc. Japan 19 (1976) 32–57.
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Motivation

Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to $0/1$ vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).

The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.

Setting

Let $V$ be a finite nonempty set, $n=|V|$. For $u\in V$ let $\chi_u\in\mathbb Z^V$ be the unit vector, for $X\subseteq V$ let $\chi_X$ be its characteristic vector, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$. For a finite $B\subseteq\mathbb Z^V$, $\overline B$ is its convex hull.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC) (is M-concave) if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and $\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v)$. Write $\omega[p](x)=\omega(x)+\langle p,x\rangle$ and $\operatorname{argmax}(g)$ for the maximizers of $g$ on $B$.

The support function of $B$ is $\psi^\circ(p)=\min\{\langle p,x\rangle\mid x\in B\}$. A positively homogeneous $h:\mathbb R^V\to\mathbb R$ is "matroidal" if

• (C1) $X\mapsto h(\chi_X)$ is supermodular, and
• (C2) $h(p)=\sum_{j=1}^n(p_j-p_{j+1})\,h(\chi_{V_j})$ whenever $V=\{v_1,\dots,v_n\}$ with $p(v_1)\ge\dots\ge p(v_n)$, $p_j=p(v_j)$, $V_j=\{v_1,\dots,v_j\}$, $p_{n+1}=0$.

The concave conjugate is $\omega^\circ(p)=\min\{\langle p,x\rangle-\omega(x)\mid x\in B\}$, the concave closure is $\hat\omega(b)=\inf_p\{\langle p,b\rangle-\omega^\circ(p)\}$, the subdifferential is $\partial\omega^\circ(p_0)=\{b\mid\omega^\circ(p)-\omega^\circ(p_0)\le\langle p-p_0,b\rangle\ \forall p\}$, and the localization of $\omega^\circ$ at $p_0$ is $\hat L(\omega^\circ,p_0)(p)=\inf\{\langle p,b\rangle\mid b\in\partial\omega^\circ(p_0)\}$.

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

For $\omega$ on a finite integral base set $B$,

The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: $B=\{(2,0),(1,1),(0,2)\}$, $\omega=(0,-10,0)$.

Milestones

1. Theorem 2.1: (B1) is equivalent to $B$ being the integer points of an integral submodular (equivalently, supermodular) system, whose defining function is determined by $B$.
2. Theorem 5.1: if $B=\mathbb Z^V\cap\overline B$, then $B$ satisfies (B1) iff $\psi^\circ$ is "matroidal".
3. Lemma 5.2: sums of "matroidal" functions are "matroidal".
4. Theorem 4.4: (EXC) holds iff every $\operatorname{argmax}(\omega[p])$ satisfies (B1).
5. Eq. (5.12): $\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\}$.

Significance

The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of $\omega^\circ$, in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.

The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of $\operatorname{conv}(\operatorname{argmax}\,\omega[-p_0])$ to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.

Difficulty

$\omega^\circ$ depends only on the concave closure $\hat\omega$, so any characterization of (EXC) through $\omega^\circ$ alone cannot see values of $\omega$ below $\hat\omega$. That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near $p_0$.

Formalization scope

Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of $\mathbb Z^V$ is a Finset (V → ℤ). A function on $B$ is a total function (V → ℤ) → ℝ whose values off $B$ are never used. The mission commits to the following readings:

• Minima. $\psi^\circ$, $\omega^\circ$ are real infima over the finite set $B$, hence minima for nonempty $B$ (every statement has $B$ nonempty). $\hat\omega$ is a real infimum used only at points of $B$, where it is bounded below.
• Localization. $\hat L$ is a real sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.
• (C2). It is required for every bijection Fin n ≃ V along which $p$ is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.
• Theorem 2.1. The page's "$\forall X\subset V$" is read as all $X\subseteq V$. The set functions are integer-valued, and "Moreover" is read strongly: every $f$ (resp. $g$) as in (b) (resp. (c)) equals the displayed max (resp. min).
• Theorem 4.4. "$\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope" is read as "$\operatorname{argmax}(\omega[p])$ satisfies (B1)", following Lemma 4.3 and the proof of Theorem 5.3. The literal convex-hull reading makes the "if" direction false (same counterexample).
• Theorem 5.1 keeps the page's hypothesis $B=\mathbb Z^V\cap\overline B$.

Trivializing formalizations are ruled out. Defining $\hat L$ by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An $\omega^\circ$ taken as a supremum would reverse the sign conventions.

The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996), 272–311. https://doi.org/10.1006/aima.1996.0084
• A. W. M. Dress, W. Wenzel, Valuated matroids: a new look at the greedy algorithm, Applied Mathematics Letters 3 (1990), 33–35.
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005.
• L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983, 235–257. https://doi.org/10.1007/978-3-642-68874-4_10
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Motivation

Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.

This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is the characteristic vector of $u$. For $x\in\mathbb R^V$, $\operatorname{supp}^+(x)=\{v\mid x(v)>0\}$, $\operatorname{supp}^-(x)=\{v\mid x(v)<0\}$, $\|x\|=\sum_v|x(v)|$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.