Operations Research

Motivation

Richard Bellman's survey The theory of dynamic programming (Bull. Amer. Math. Soc. 60 (1954), 503–515, DOI 10.1090/s0002-9904-1954-09848-8) introduced dynamic programming to a general mathematical audience. It states the principle of optimality (§2, p. 504): "An optimal policy has the property that whatever the initial state and initial decisions are, the remaining decisions must constitute an optimal policy with regard to the state resulting from the first decisions", and derives from it the functional equations of finite and infinite stochastic decision processes, (4.2) and (5.1) (p. 506).

The survey illustrates the method on a small number of worked examples. The second of them, §8 "Stochastic gold mining" (pp. 508–509), is the one with a sharp answer: a two-armed sequential allocation problem with an absorbing failure state, whose optimal policy is a simple index rule. It is an early instance of the allocation-index phenomenon later made general by Gittins and Jones (1974) and Gittins (1979), and the paper itself notes (p. 509) that the rule "is not valid generally in more complicated decision processes", citing a counterexample of Karlin and Shapiro. The full treatment is in Bellman's RAND report R-245 and his 1957 book Dynamic Programming.

Setting

Two gold mines, Anaconda ($A$) and Bonanza ($B$), hold amounts $x \ge 0$ and $y \ge 0$ of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability $p$: it then mines a fraction $r$ of the gold currently in Anaconda and the machine stays undamaged. With probability $1-p$ it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability $q$ and fraction $s$. While the machine works, the operator chooses the next mine; the aim is to maximize the expected amount mined before the machine is destroyed.

The only information the operator ever receives is that the machine still works. A policy is therefore a choice sequence $\sigma = (\sigma_0, \sigma_1, \dots) \in \{A, B\}^{\mathbb N}$: the mine for use number $n$, applied if uses $0, \dots, n-1$ succeeded. With $a_n$, $b_n$ the numbers of $A$- and $B$-uses among the first $n$, use $n$ collects $g_n = r x (1-r)^{a_n}$ if $\sigma_n = A$ and $g_n = s y (1-s)^{b_n}$ if $\sigma_n = B$, and does so with probability $\prod_{k=0}^{n} \pi_{\sigma_k}$ ($\pi_A = p$, $\pi_B = q$). The expected return is

$$J(\sigma; x, y) = \sum_{n \ge 0} \Big(\prod_{k=0}^{n} \pi_{\sigma_k}\Big) g_n ,$$

and Bellman's (8.1) defines the optimal return

$$f(x, y) = \sup_\sigma J(\sigma; x, y).$$

In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.

Formalization targets

Milestone: the functional equation (8.2), p. 508

$$f(x, y) = \max\Big\{ p\,[r x + f((1-r)x, y)],\ q\,[s y + f(x, (1-s)y)] \Big\}.$$

Goal: the decision rule (8.3), p. 509, corrected

Write $V_A = p[rx + f((1-r)x, y)]$ and $V_B = q[sy + f(x, (1-s)y)]$ for the two branches of (8.2). For $0 < p, q, r, s < 1$ and $x, y \ge 0$:

$$\frac{prx}{1-p} > \frac{qsy}{1-q} \Rightarrow V_A > V_B, \qquad \frac{prx}{1-p} < \frac{qsy}{1-q} \Rightarrow V_A < V_B, \qquad \frac{prx}{1-p} = \frac{qsy}{1-q} \Rightarrow V_A = V_B .$$

The paper prints the rule with $(1-r)$ and $(1-s)$ in the denominators:

a. For $prx/(1 - r) > qsy/(1 - s)$, choose A, b. For $prx/(1 - r) < qsy/(1 - s)$, choose B, c. For $prx/(1 - r) = qsy/(1 - s)$, choose either.

and glosses it as "the locus of points where immediate expected gain over immediate expected loss is the same for both choices". The immediate expected loss is the probability of destroying the machine, $1-p$ (resp. $1-q$), not $1 - r$. As printed the rule is false: with $p = 1/2$, $r = 0.9$, $q = 0.9$, $s = 0.1$, $x = 1$, $y = 2$ the printed indices are $4.5 > 0.2$, but $V_A \approx 0.924 < V_B \approx 1.055$. The mission's goal is the corrected rule, the one the paper describes in words.

Companion: the index policy is optimal, p. 509

"Using this prescription, $f(x, y)$ may be computed recurrently": the choice sequence $\sigma^*$ generated by applying the corrected rule to the current amounts at every use satisfies $J(\sigma^*; x, y) = f(x, y)$.

Significance

The decision rule reduces an optimization over infinite sequences to comparing two explicit numbers, one per mine, each depending only on that mine's own data. This is the defining property of an index policy, and gold mining is one of the earliest problems where it was observed. The functional equation (8.2) is the concrete form, for this process, of the infinite-horizon equation (5.1) that the paper states formally.

Formalizing the example yields a complete machine-checked instance of the principle of optimality for an infinite-horizon stochastic process whose state space (the amounts left in the two mines) is infinite, where the supremum over policies is not attained trivially and the finite-horizon recursion does not apply directly. It also records, with a checked statement, the correction of the misprint in (8.3). No machine-checked proof of (8.2) or (8.3) is known to exist.

Difficulty

The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats $f$ as the value of an optimal policy, but $f$ is a supremum over infinite sequences that need not be attained a priori, and the return of a sequence is an infinite series. The finite-horizon recursion (4.2) does not apply as it stands, because the process has no last stage and its state space, the amounts left in the two mines, is infinite.

The rule (8.3) compares the two optimal continuations $f((1-r)x, y)$ and $f(x, (1-s)y)$, which are themselves unknown. A comparison of the one-step gains alone does not decide it, as the misprinted rule shows. Parts a and b are strict preferences, so it is not enough to show that one choice is at least as good as the other.

Formalization scope

• Representation. The mines are a two-element inductive type Mine; a policy is a function ℕ → Mine (ChoiceSeq). All quantities are real numbers. Randomized policies are mixtures of choice sequences and give no larger return, so they are not modelled. No restriction to stationary or Markov policies is made: $f$ is the supremum over all sequences.
• Parameter ranges. The paper does not state them. The theorems assume $0 < p, q, r, s < 1$ and $x, y \ge 0$ (zero amounts allowed). $p, q < 1$ keeps the indices $prx/(1-p)$, $qsy/(1-q)$ well defined.
• Series and supremum. $J$ is a real tsum and $f$ a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by $x + y$, and the family is bounded above, so neither Lean default value (0 for a divergent series or an unbounded supremum) arises; this is stated as the auxiliary theorem expectedReturn_le_add.
• Survival indexing. The gold of use $n$ is counted only if use $n$ itself succeeds, so the survival product runs over $k \le n$.
• The misprint. The goal and the index policy use $(1-p)$, $(1-q)$ in place of the printed $(1-r)$, $(1-s)$. The printed rule appears only as the quotation above.
• No trivializing encoding. $f$ is defined as the supremum of expected returns over all choice sequences, per (8.1); it is not defined as a solution of (8.2), as the value of the index policy, or as a limit of value iteration, any of which would make the milestone or the goal true by definition.
• Auxiliary theorems (not from the paper). The bound $0 \le J \le x + y$ with summability, the one-step unrolling $J(\sigma) = p[rx + J(\sigma'; (1-r)x, y)]$ when $\sigma_0 = A$ (and symmetrically), and the single-mine values $f(x, 0) = prx/(1 - p(1-r))$, $f(0, y) = qsy/(1-q(1-s))$ are included as footholds. They are not milestones.
• Related platform content. AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by $a^t$ at global time $t$; gold mining multiplies by the success probability of each use of the mine used, so it is a different model and is not reused. BertsekasDP.dp_algorithm_optimality is finite-horizon and does not give (8.2).

Contributions welcome: proofs of the auxiliary theorems, of (8.2), of the decision rule, and of the optimality of the index policy.

Selected references

• R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), no. 6, 503–515. https://doi.org/10.1090/s0002-9904-1954-09848-8
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
• J. C. Gittins, K. D. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

Motivation

Many US school districts assign children to public schools centrally. Each family ranks the schools. Each school ranks the children by priority, which is set by state or local law (siblings, walking distance, a lottery). A procedure then turns these rankings into an assignment. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) cast this as a mechanism design problem. They showed that the mechanisms then in use in Boston, Columbus and Minneapolis gave families reasons to misreport their preferences. They proposed two alternatives: the student-optimal stable mechanism of Gale and Shapley, and a school-choice version of Shapley and Scarf's top trading cycles (TTC) mechanism.

Many districts also operate under controlled choice: court-ordered or voluntary rules that keep the racial or ethnic composition of each school within bounds. In Minneapolis, for instance, a 100-seat school could admit at most 75 majority and at most 55 minority students (paper, Section III). Such rules are implemented as type-specific quotas. Section III.B of the paper modifies TTC to respect these quotas. It proves that the modified mechanism keeps both properties that recommend TTC: it wastes nothing beyond what the quotas force (constrained efficiency, Proposition 6), and truth-telling is a dominant strategy (strategy-proofness, Proposition 7). This mission formalizes those two results.

Setting

There is a finite set $I$ of students and a finite set $S$ of schools. School $s$ has a capacity $q_s$, and the total number of seats suffices: $|I|\le\sum_s q_s$. Each student $i$ has a strict preference over all schools, encoded as a ranking $P_i : S\to\{0,\dots,|S|-1\}$ with rank $0$ the favourite. Each school $s$ has a strict priority ranking over all students, with rank $0$ the highest priority. Each student belongs to exactly one type $\tau(i)$, and school $s$ has a type quota $q_s^t$ for each type $t$.

An assignment $\nu$ gives each student a school or nothing ($\varnothing$, worse than every school). It satisfies the controlled choice constraints if every school $s$ receives at most $q_s$ students, and at most $q_s^t$ students of each type $t$. An assignment $\mu$ is constrained efficient if no assignment satisfying the constraints makes every student weakly better off and some student strictly better off.

The top trading cycles mechanism with type-specific quotas, $\mathrm{TTC}^q$, runs in steps. Each school keeps a counter $c_s$ (initially $q_s$) and one type counter $c_s^t$ for each type (initially $q_s^t$). A school is removed when $c_s$ reaches zero. At each step:

• every remaining student points to her favourite remaining school with room for her type, that is, with $c_s>0$ and $c_s^{\tau(i)}>0$;
• every remaining school points to its highest-priority remaining student, whatever her type;
• every student on a cycle of this graph is assigned the school she points to and leaves;
• that school's counter and its counter for her type each drop by one.

A direct mechanism is strategy-proof if no student can ever gain by misreporting her preference, whatever the others report.

Formalization targets

Goal: Proposition 7 (p. 23)

For every student $i$, every profile $P$ of announced preferences and every alternative report $Q_i$,

$$\mathrm{TTC}^q(Q_i,P_{-i})(i)=s' \implies \mathrm{TTC}^q(P)(i)=s \text{ with } P_i(s)\le P_i(s').$$

This holds for all capacities without shortage, all quotas, all types and all priorities. The priorities are fixed data, not reported.

Milestones

1. Section III.B, Step 1 (p. 22). At every step there is at least one cycle, after the convention below has removed the students who cannot point.
2. The Lemma (Appendix, pp. 28–29; declared valid for the modified mechanism on p. 30). Fix the other students' reports, and suppose student $i$ is still present at the beginning of a step under two different reports of hers. Then the two runs have the same remaining students and the same counters at that point.
3. Proposition 6 (p. 23). $\mathrm{TTC}^q(P)$ satisfies the controlled choice constraints and is constrained efficient with respect to $P$.

Significance

Strategy-proofness is what lets a district publish a simple instruction: rank the schools in your true order. A strategy-proof mechanism does not reward families who can afford to gather information and game the system. Proposition 7 shows that this guarantee survives the addition of flexible diversity quotas, which many districts are legally bound to impose. Proposition 6 shows that the quotas cost nothing beyond the losses they themselves cause. Both results were proved in 2003 by pen and paper. The published proof of Proposition 7 is a short adaptation of the proof of Proposition 4 (strategy-proofness of plain TTC). It rests on a lemma about how the algorithm's intermediate states depend on one student's report.

To our knowledge neither result has a machine-checked proof. The related platform theorem AGT.ttc_strategyproof concerns the Shapley–Scarf housing market, where every agent owns one house and the mechanism selects the core. It does not cover capacities, priorities or quotas. A formal proof here would check the adaptation that the paper leaves to the reader, and would give a reusable formal model of cycle-clearing allocation algorithms with multiple counters.

Difficulty

The algorithm clears all cycles of a step at once, and a student's report changes the graph at every step she is present. The paper's argument compares two whole runs of the algorithm, under the true report and under a misreport, step by step. That comparison needs precise control of which parts of the state a single student's report can influence, and when. A local argument about one step does not suffice. The student's outcome can depend on cycles that form several steps after the two runs could first have diverged.

With quotas, the pointing graph also depends on the type counters. A school can be present but closed to one type, and a school points to its best remaining student even when it has no room for her type. The comparison must therefore track the type counters as well as the set of remaining schools. Efficiency cannot be read off step by step against unrestricted matchings either: every competing assignment must satisfy both the capacity and the quota constraints.

Formalization scope

Students, schools and types are finite types; no nonemptiness is assumed. Preferences and priorities are bijective rankings onto Fin, so strictness is built in. Rank $0$ is the favourite or the highest priority. The no-shortage condition $|I|\le\sum_s q_s$ appears in every theorem, as the standing assumption of Section I. No relation between $q_s$ and $q_s^t$ is imposed, which generalises the paper.

The algorithm is a concrete, total definition: a state with remaining students, counters, type counters and partial assignments, a step map that clears all cycles simultaneously, and $|I|$ iterations. run … t is the state at the beginning of the paper's Step $t+1$.

The paper's step is undefined when a remaining student has no remaining school with room for her type. She cannot point, and the promised cycle may not exist. The formalization adopts one convention: at the beginning of each step, such a stuck student is removed unassigned, and her outcome is $\varnothing$, ranked below every school. Counters only decrease, so a stuck student stays stuck. Whenever nobody gets stuck, the algorithm is exactly the paper's, and when every quota is at least the capacity it is plain TTC. The goal and Proposition 6 are stated for assignments that may leave students unassigned. When everyone is assigned, they coincide with the paper's statements over matchings.

The formalization does not add a hypothesis that the run never gets stuck. Such a hypothesis would restrict the algorithm's own behaviour and could make the theorems vacuous. Nor may strategy-proofness be weakened to comparisons at the truthful profile only: the others' reports and the misreport are arbitrary.

Contributions welcome: invariants of the step map (counters bounded by the initial values, assigned students leave for good), the cycle-existence lemma for functional graphs on finite sets, and the comparison lemma. These pieces are shared with the plain-TTC mission of this series.

Selected references

• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
• Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0

Motivation

Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.

The paper drew on earlier results for simpler allocation problems:

• 1974: Shapley and Scarf introduce housing markets and Gale's top trading cycles algorithm, in which each agent owns one house.
• 1977: Roth and Postlewaite show the algorithm finds the unique core allocation of a housing market.
• 1982: Roth proves the core mechanism for housing markets is strategy-proof.
• 1999: Abdulkadiroğlu and Sönmez adapt the algorithm to house allocation with existing tenants and prove strategy-proofness.
• 2000: Pápai introduces hierarchical exchange rules, a wider class that includes these mechanisms.
• 2003: the paper formalized here extends the algorithm to schools with capacities and school-specific priorities (Propositions 3 and 4).

Setting

A school choice problem consists of a finite set $I$ of students, a finite set $S$ of schools, a capacity $q_s \in \mathbb N$ for each school, a strict preference $P_i$ of each student over all schools, and a strict priority ordering $\succ_s$ of each school over all students. The standing assumption is that there is no shortage of seats:

$$|I| \le \sum_{s\in S} q_s .$$

Preferences are rankings: $P_i(s)\in\{0,\dots,|S|-1\}$ is the rank of $s$ for student $i$, with rank $0$ the favourite. Priorities are rankings of students in the same way, with rank $0$ the highest priority. A matching is a map $\mu : I\to S$ with $\#\{i:\mu(i)=s\}\le q_s$ for every school $s$. A matching $\mu$ is Pareto efficient if no other matching $\nu$ gives every student a weakly better school ($P_i(\nu(i))\le P_i(\mu(i))$) and some student a strictly better one.

A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.

The top trading cycles algorithm keeps a counter $c_s$ of free seats at each school, starting at $q_s$. A school is remaining while $c_s>0$. At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list $(s_1,i_1,\dots,s_k,i_k)$ of distinct schools and students in which $s_1$ points to $i_1$, $i_1$ points to $s_2$, and so on, and $i_k$ points to $s_1$. Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism $\mathrm{TTC}(q,\succ,P)$ returns the resulting assignment.

Formalization targets

Goal: Proposition 4 (strategy-proofness)

For all capacities with no shortage, all priorities, every profile $P$, every student $i$ and every alternative report $Q_i$, student $i$ is assigned schools $s = \mathrm{TTC}(q,\succ,P)(i)$ and $s' = \mathrm{TTC}(q,\succ,(Q_i,P_{-i}))(i)$, and

$$P_i(s) \le P_i(s') .$$

Milestones

1. At every step at which some student remains, there is a cycle (Section II.B, p. 15).
2. After $|I|$ steps no student remains, and the outcome is a matching (Section II.B, p. 16).
3. Lemma (Appendix, pp. 28–29): if student $i$ is still remaining at the beginning of a step under two different reports of her own, the remaining students and the remaining schools at that point are the same under both reports.
4. Proposition 3 (p. 17): the outcome is a Pareto efficient matching with respect to the reported profile.
5. When all schools share one priority ordering $\pi$, the mechanism equals the serial dictatorship induced by $\pi$ (Section II.B, p. 16).

Significance

Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.

The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.

Difficulty

The paper's argument moves from the step at which student $i$ leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by $i$'s report. Informally, $i$ is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though $i$ points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.

Formalization scope

Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.

The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.

A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.

Selected references

• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
• Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
• Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0
• Alvin E. Roth and Andrew Postlewaite, Weak versus Strong Domination in a Market with Indivisible Goods, Journal of Mathematical Economics 4(2), 131–137, 1977. https://doi.org/10.1016/0304-4068(77)90004-0
• Alvin E. Roth, Incentive Compatibility in a Market with Indivisible Goods, Economics Letters 9(2), 127–132, 1982. https://doi.org/10.1016/0165-1765(82)90003-9
• Atila Abdulkadiroğlu and Tayfun Sönmez, House Allocation with Existing Tenants, Journal of Economic Theory 88(2), 233–260, 1999. https://doi.org/10.1006/jeth.1999.2553
• Szilvia Pápai, Strategyproof Assignment by Hierarchical Exchange, Econometrica 68(6), 1403–1433, 2000. https://doi.org/10.1111/1468-0262.00166

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$. This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

• 1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
• 1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
• 1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$-tuples $x = (x_1, \ldots, x_n)$, and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$. A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$. It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$, i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$.

A half-space $\langle\alpha,x\rangle\ge 0$ ($\alpha\ne 0$) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$.

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$:

$$x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .$$

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$,

$$\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .$$

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$. Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

1. A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
2. The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
3. The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$, every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
4. Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$.

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$. The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$.

Formalization scope

Conventions committed to in Lean:

• $\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$, as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
• A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
• A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$.
• "All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$, as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
• "Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
• Finiteness of extreme supports is stated up to positive scaling.
• The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$, and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$.

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

• H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
• C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
• G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$, so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$, $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

$$d(x,k)+d(k,y)-d(x,y)$$

and replacing it by the edges $(x,k)$ and $(k,y)$; if $T$ is a single node $i$, TOUR$(T,k)$ is the two-node tour $(i,k),(k,i)$. COST$(T,k)$ is the length of TOUR$(T,k)$ minus the length of $T$.

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$, $1\le i<n$. The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$.

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

$$\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.$$

Milestones

1. (2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
2. (2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$, then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$.
3. Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$, then

$$\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.$$

4. Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$.
5. (3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$.
6. (3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$.
7. (3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$.

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$. The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$. TOUR$(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$, so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ($T_1=[a_0]$, $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

• The distance satisfies $d(i,i)=0$, a normalization not in the paper; a loop never enters any length.
• Ratios are multiplied out ($\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$), so the paper's exclusion of the identically zero distance (1.1) is not needed.
• Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
• (2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
• (2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$.

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

Motivation

In robust stochastic optimization a decision maker chooses a decision $x$ whose outcome depends on a random vector $\mathbf R$, but knows only the first two moments of $\mathbf R$: its mean vector $\mu$ and its covariance matrix $\Sigma$. The decision is evaluated by its worst-case expected utility over every distribution consistent with those moments. This model is standard in portfolio selection, where estimated means and covariances are the usual inputs, and in pricing and inventory problems with mean-variance information. It goes back to Scarf's min-max newsvendor (1958) and the Chebyshev-type moment bounds of Bertsimas and Popescu (2005).

For a linear outcome $x'\mathbf R$, such as the return of a portfolio with weights $x$, the robust objective is

$$U(x) = \min_{\mathbf R \sim (\mu,\Sigma)} E[u(x'\mathbf R)],$$

an optimization over an infinite-dimensional set of $n$-variate distributions. Popescu (2007) showed that this problem depends on $\mu$ and $\Sigma$ only through the scalar mean $\mu_x = x'\mu$ and variance $\sigma_x^2 = x'\Sigma x$. The multivariate robust problem then reduces to a univariate moment problem, and for many utilities to a parametric quadratic program. The reduction rests on one structural fact, the general projection property, which this mission formalizes.

Setting

Fix a dimension $n$. A law on $\mathbb R^n$ is a Borel probability measure on $\mathbb R^n$. For a vector $\mu \in \mathbb R^n$ and a real $n\times n$ matrix $\Sigma$, the mean-covariance class $\mathbb M^n_{(\mu,\Sigma)}$ is the set of laws $P$ under which every coordinate $R_i$ has a finite second moment and

$$\int R_i\,dP(R) = \mu_i, \qquad \int (R_i-\mu_i)(R_j-\mu_j)\,dP(R) = \Sigma_{ij} \qquad (1\le i,j\le n).$$

Writing $\mathbf R \sim (\mu,\Sigma)$ means that the law of $\mathbf R$ lies in $\mathbb M^n_{(\mu,\Sigma)}$. For $n=1$ the superscript is dropped: for real $m$ and $v$, $\mathbb M_{(m,v)}$ is the set of laws on $\mathbb R$ with finite second moment, mean $m$ and variance $v$.

For a vector $x \in \mathbb R^n$, the $x$-projection sends the law $P$ of $\mathbf R$ to the law of the scalar $\mathbf r = x'\mathbf R$, that is, to the pushforward of $P$ under $R \mapsto x'R$. Write $\mu_x = x'\mu$ and $\sigma_x^2 = x'\Sigma x$. The matrix $\Sigma$ is positive semidefinite, $\Sigma \succeq 0$, when $x'\Sigma x \ge 0$ for all $x$ (and $\Sigma$ is symmetric); $\Sigma^{1/2}$ denotes its positive semidefinite square root.

Formalization targets

Goal: Theorem 1 (General Projection Property)

For every $\mu \in \mathbb R^n$, every $\Sigma \succeq 0$ and every nonzero $x \in \mathbb R^n$, the $x$-projection maps $\mathbb M^n_{(\mu,\Sigma)}$ into and onto $\mathbb M_{(\mu_x,\sigma_x^2)}$:

$$\bigl\{\, \text{law of } x'\mathbf R \;:\; \mathbf R \sim (\mu,\Sigma) \bigr\} \;=\; \mathbb M_{(x'\mu,\; x'\Sigma x)}.$$

The "into" half says every projected law has the right mean and variance. The "onto" half says that every univariate law with mean $\mu_x$ and variance $\sigma_x^2$, however heavy-tailed or irregular, is the law of $x'\mathbf R$ for some $\mathbf R \sim (\mu,\Sigma)$. The degenerate case $x'\Sigma x = 0$ is included.

Milestones

1. The into half (§2.1, justification of (4)): $x'\mathbf R$ has mean $x'\mu$ and variance $x'\Sigma x$.
2. The degenerate case: if $x'\Sigma x = 0$ then $x'\mathbf R = x'\mu$ almost surely.
3. Standardization: if $\mathbf r \sim (m, v)$ with $v > 0$, then $v^{-1/2}(\mathbf r - m) \sim (0,1)$.
4. Normalization: for $x'\Sigma x > 0$, the vector $y = (x'\Sigma x)^{-1/2}\Sigma^{1/2}x$ satisfies $y'y = 1$.
5. Isotropic lift: if $y'y = 1$ and $\mathbf z \sim (0,1)$, there is $\mathbf Z \sim (0, I_n)$ with $y'\mathbf Z$ distributed as $\mathbf z$.
6. Affine image: if $\mathbf Z \sim (0,I_n)$ then $\mu + \Sigma^{1/2}\mathbf Z \sim (\mu,\Sigma)$, and $x'(\mu + \Sigma^{1/2}Z) = x'\mu + (x'\Sigma x)^{1/2}\,y'Z$ for every $Z$.

Significance

The result. Theorem 1 immediately yields Proposition 1 of the paper: for every objective $u$,

$$\min_{\mathbf R\sim(\mu,\Sigma)} E[u(x'\mathbf R)] = \min_{\mathbf r\sim(\mu_x,\sigma_x^2)} E[u(\mathbf r)],$$

with minima in the wide sense of infima. The robust objective is therefore a function of $(\mu_x, \sigma_x)$ alone, which makes every robust mean-covariance problem with a linear outcome a bicriteria mean-variance problem. The paper's later results use this: the two-point and one-point support properties, the parametric quadratic programming solution, and the portfolio applications (bonus schemes, value at risk). The projection property holds with no assumption on $u$, so it serves non-concave, discontinuous and quantile-based objectives alike.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. The mission produces a formal definition of mean-covariance classes that treats integrability honestly, a proof of the projection property, and through it a formally verified reduction of multivariate moment-robust problems to univariate ones. The paper's own construction of the lifted vector has a gap (see Difficulty), so a formal proof also records a corrected argument.

Difficulty

The into half is a computation with linearity of expectation. The difficulty is entirely in the onto half. Given an arbitrary univariate law with prescribed mean and variance, one must build an $n$-variate law with a prescribed full covariance matrix whose one-dimensional marginal in direction $x$ is exactly the given law. This is a coupling problem: the obvious approach, taking independent coordinates, fixes the marginal in direction $x$ as a convolution and cannot reproduce an arbitrary target. Taking $\mathbf R$ supported on the line through $\mu$ in a single direction reproduces the target law but has a rank-one covariance and fails whenever $\Sigma$ has rank above one.

The paper's appendix constructs the lift through conditional distributions of the remaining coordinates given the projected one. As printed, the conditional second-moment requirement it imposes cannot hold for unbounded targets, so that argument does not go through verbatim. The milestone for the lift states only the claim, not the printed construction.

The integrability bookkeeping is real work: every intermediate law must be shown to have finite second moments before its moments can be computed.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Borel σ-algebra; $x'R$ is the inner product $\langle x, R\rangle$; $x'\Sigma x$ is x.ofLp ⬝ᵥ S *ᵥ x.ofLp, where the matrix $\Sigma$ is named S (the symbol Σ is reserved in Lean).
• Laws are probability measures. Both classes require finite second moments (MemLp … 2), so that means and covariances are genuine integrals, not the default value $0$ that Lean assigns to non-integrable functions. The univariate class is parametrized by the variance $v = \sigma^2$, not by $\sigma$.
• The projection is the pushforward P.map (fun R => ⟪x, R⟫) under a continuous map. "Pathwise" identities in the paper become equalities of pushforward laws, or pointwise algebraic identities.
• $\Sigma^{1/2}$ is CFC.sqrt S, acting through Matrix.toEuclideanCLM, as in Mathlib's multivariateGaussian.
• The goal is stated as Set.MapsTo ∧ Set.SurjOn with both classes explicit. Its only hypotheses are $\Sigma \succeq 0$ and $x \ne 0$, as in the paper. No bound on $n$, no invertibility of $\Sigma$ and no positivity of $x'\Sigma x$ is assumed. Restricting the target to Gaussian, bounded or finitely supported laws, or dropping the finite-second-moment clause (which would admit Cauchy laws as "mean 0, variance 0"), would trivialize or change the theorem and is ruled out.
• Milestones 3, 4 and 6 assume $x'\Sigma x > 0$ (or $v > 0$), the case the proof treats after its first sentence; milestone 2 covers the complementary case.

Needed infrastructure: moments of pushforwards under linear and affine maps, a covariance calculus for coordinates of random vectors, and a coupling that realizes the isotropic lift. Mathlib's multivariateGaussian, stdGaussian and CFC.sqrt are available. A reusable lemma "the covariance of $A\mathbf Z + b$ is $A\,\mathrm{Cov}(\mathbf Z)A'$" would serve beyond this mission. Related platform work on moment-based ambiguity sets: Wasserstein Distributionally Robust Optimization II. Contributions of any milestone, and alternative proofs of the lift, are welcome.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
• H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• W. W. Rogosinski, Moments of Non-Negative Mass, Proceedings of the Royal Society A 245:1–27, 1958. https://doi.org/10.1098/rspa.1958.0062

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and consider the linear program

$$\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .$$

The slack of a point $x$ is $s(x)=Ax-b$, and the interior is $S^0=\{x : Ax>b\}$, the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$, the weighted penalized objective is

$$f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .$$

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$.

Write $S_x=\mathrm{diag}(s(x))$, $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and the centrality are

$$\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.$$

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$, and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$.

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .$$

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$), and uniformity $\|\vec g(s)\|_\infty\le2$.

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$, let $x^{(old)}\in S^0$, $s^{(old)}=s(x^{(old)})$, and

$$x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$, then $x^{(new)}\in S^0$ and

$$\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$, the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$, $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$,

$$\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,$$

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$, and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$:

$$\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.$$

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$, $c_r$ and $\sqrt{c_1}$. The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$, $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$, which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$, $\frac1{4}$, $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$, so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$: without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$, while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$, and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

1. Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$, $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
2. Size as an upper bound. Definition 4's "$c_1(\vec g)=\|\vec g(s)\|_1$" is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
3. Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$.
4. Lemma 3's $r$ ranges over $r\ge0$, and $\gamma(x,w)$ means $\gamma(s(x),w)$.
5. Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
6. Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$, equal to $0$ for $m=0$).
7. The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$, spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
• Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791