Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Nash's equilibrium existence theorem assumes that each player's set of available strategies is fixed. Many social and economic systems do not work that way: a consumer's budget set depends on prices, which are the choices of another agent, and a firm's feasible production may depend on what other firms do. Gerard Debreu's A Social Equilibrium Existence Theorem (PNAS 38(10), 1952) proves that an equilibrium exists in such a system, called a social system or abstract economy (today also a generalized game). Here each agent's feasible actions depend on the actions of all the others.
Arrow and Debreu used this theorem to prove the existence of a competitive equilibrium (Econometrica 22(3), 1954). It is the standard existence result for generalized Nash equilibrium problems in operations research, where the feasible sets are coupled by shared constraints.
Timeline.
There are finitely many agents . Agent chooses an action in a set , a subset of a finite-dimensional real space. A profile lies in . For each agent, denotes the actions of the others, ranging over .
Given , agent may only choose from a nonempty set , a multi-valued function of the others' actions. Its graph is . The payoff takes values in the completed real line . The best value available to agent and the set of constrained best responses are
An equilibrium point is a profile such that, for every , and .
The topological vocabulary is Debreu's §1:
A multi-valued function is semicontinuous if its graph is closed.
Assume that for every , is a contractible polyhedron, is closed, is continuous on , is continuous on , and is contractible for every . Then
The result. The theorem gives an equilibrium for games in which one agent's choices constrain another's. This is the step that makes competitive equilibrium an equilibrium of a game: the market participant's price choice constrains the consumers' budget sets. The same result gives existence for generalized Nash equilibrium problems, including games with shared constraints. Replacing convexity by contractibility also admits non-convex best-response sets: a contractible set such as a star-shaped region or an arc qualifies. Nash's theorem for finite games and von Neumann's minimax theorem are special cases. With values in , payoffs may take infinite values.
The formalization. The theorem was proved in 1952. None of it is formalized on the platform: neither the theorem itself, nor the LEMMA, nor the topological vocabulary of polyhedra and contractible sets used here. Brouwer's theorem is available on the platform as AGT.brouwer_fixed_point. Nash's existence theorem for finite games (AGT.nash_existence) and Sion's minimax theorem are also formalized. All of these assume convexity. The mission produces a machine-checked existence theorem for generalized games, together with a fixed-point theorem for set-valued maps with contractible values on polyhedra.
Most of the argument reduces to the LEMMA, which is a particular case of the Eilenberg–Montgomery fixed-point theorem. The usual route to Kakutani's theorem does not carry over: it approximates a convex-valued map by continuous selections and applies Brouwer's theorem on a convex set. Contractible values do not admit convex combinations of nearby values, and a contractible polyhedron need not be convex, so neither the selection step nor Brouwer on a simplex applies directly. Debreu cites the LEMMA without proof, and Mathlib has no fixed-point theorem for set-valued maps and none of the algebraic topology of polyhedra that the classical results rest on.
The remaining steps are point-set topology. The product milestones require building homeomorphisms and deformations on products of subspaces, and the closed-graph steps require care with continuity on as opposed to continuity everywhere.
Fintype. Profiles live in . The others' actions range over the product over the subtype , so cannot depend on agent 's own action. With a single agent this product is a point, and the theorem becomes the one-agent statement.EReal with its order topology. is a supremum (sSup) in EReal; under the hypotheses it is attained, so it is Debreu's Max. No arithmetic in EReal is used anywhere.Three formalizations would be easier but are not this theorem: one that replaces contractible by convex (that is the Kakutani–Nash setting), one that maximizes over all of instead of , and one that assumes a fixed point of or states only the closed-graph step. None of these is acceptable, and the LEMMA may not be weakened to convex domains or convex values.
The work needed includes a small library of polyhedra and contractible subsets, and closed-graph correspondences on products. The largest piece is a proof of the LEMMA, a fixed-point theorem that is reusable well beyond this mission. Proofs of any milestone, alternative routes to the LEMMA, and supporting lemmas on polyhedra, such as compactness, triangulation or being absolute neighbourhood retracts, are all welcome.
The stable set problem asks for a largest set of pairwise non-adjacent vertices in a graph; its size is the stability number . It is NP-hard in general, and a standard way to attack it in integer programming is to write down linear inequalities valid for all stable sets and solve the resulting linear program. The weakest such relaxation uses only the edge inequalities ; its optimum can be as large as on graphs with small . Adding, for every odd circuit , the inequality gives the odd-cycle relaxation, the first strengthening that cuts off the fractional point on odd cycles.
Section 7 of V. Chvátal, On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154, doi:10.1016/0095-8956(75)90041-6) identifies a graph class on which this relaxation is exact for the all-ones objective, with an integral certificate on the dual side: the series-parallel networks. The paper conjectures (Conjecture 7.3) that for these graphs the odd-cycle inequalities describe the whole stable set polytope; graphs with that property were later called t-perfect.
Timeline:
All graphs are finite, undirected and loopless, with no parallel edges. A stable set is a set of vertices no two of which are adjacent. We write for the degree of .
A set induces an odd circuit if the induced subgraph is a cycle of length with ; triangles count, and such a cycle has no chords. is the set of all such . The odd-cycle system of is
Its linear programming dual for the objective , with read as sign constraints, has variables , , and reads
A homeomorph of is a graph obtained from by subdividing its edges into paths through new vertices of degree two. is a series-parallel network if no subgraph of is a homeomorph of .
For every series-parallel network ,
and there is a zero–one dual feasible whose dual objective equals the minimum over all real dual feasible points. Both optimality claims are against real points. Chvátal's statement has no constants to improve; the formal goal is his theorem as printed.
The result. Theorem 7.1 says that on series-parallel networks the odd-cycle relaxation computes exactly, and that the optimum is certified by a covering of the vertex set by single vertices, edges and chordless odd circuits whose total weight equals . This is a min–max theorem of König type for a non-bipartite, non-perfect class: odd cycles of length at least five are series-parallel and not perfect, so the clique inequalities of the perfect-graph theory (mission I of this series) do not suffice here. The statement is the unweighted case of the later polyhedral results of Boulala–Uhry and Gerards–Schrijver, and the combinatorial core (milestone 3) is the basis of a polynomial algorithm for on this class, as the paper remarks.
Formalizing it. The theorem has been proved since 1975; neither Mathlib nor the Prove2Me library contains a formal proof of it. A formal proof needs a working notion of graph subdivision (topological minor), which Mathlib does not have, Dirac's degree theorem, the induction of the paper with its four cases, and the passage from the combinatorial core to a pair of LP optima through weak duality. Each of these is reusable: topological minors and the -subdivision-free class appear throughout structural graph theory.
The combinatorial core is proved by induction on removing a vertex of degree at most two, and three of the four cases are routine. The obstacle is Case 4 (, neighbours non-adjacent): deleting alone loses the information needed to recover and , so the proof identifies the two neighbours. That requires the class to be closed under this identification, a statement about subdivisions that is not a local edge count, and a lifting of from the reduced graph with a case split on the component of containing the merged vertex. A second gap is between and the dual: an odd-circuit component of may have chords in and so need not lie in , and the zero–one dual solution must be extracted from it. Finally, Dirac's theorem itself is the one place where the absence of subdivisions is used positively, and it is not a consequence of a degree-counting argument.
Graphs are SimpleGraph V on a Fintype V with decidable equality and decidable adjacency. is a Finset (Finset V) whose members induce a subgraph isomorphic to Mathlib's cycleGraph (2k+1), . The dual variables are indexed by V, by the edge set G.edgeSet, and by the subtype of ; is a sign constraint with no dual variable. "Contains a homeomorph of " is encoded by four distinct branch vertices and six paths (Walk.IsPath) that avoid other branch vertices and meet only at common endpoints; it is not the -minor notion and not the series–parallel composition notion, whose equivalence with it is not part of the paper.
Conventions and implicit hypotheses made explicit:
Corollary 7.2 (stated without proof) and Conjecture 7.3 are not part of this mission. Contributions welcome: a general topological-minor library, Dirac's theorem, and a proof of the combinatorial core.
Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.
Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor over a -approximate one-machine schedule, which is when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio . In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.
Timeline of the relevant results:
There are jobs and identical machines. Job has a processing time and a weight ; every job is available at time (there are no release dates).
The precedence constraints form an in-tree (more generally, an in-forest): every job has at most one immediate successor , and following successors never returns to the start. Write if is reached from by following successors one or more times.
A feasible schedule on machines gives each job a start time and a machine; a job runs without interruption for time units; two jobs on the same machine do not overlap; and implies that starts no earlier than completes. The completion time is and the value of the schedule is .
The critical-path length (Definition 4.1 with no release dates) is if has no predecessors and otherwise.
A list is an ordering of the jobs that obeys the precedence constraints. It defines the one-machine schedule that runs the jobs in list order without idle time; its completion times are , the total processing time of the jobs up to and including in the list. An optimal one-machine schedule is a list minimizing .
List scheduling (Graham's rule, footnote 3 of the paper) on machines with list : whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.
Let be an optimal one-machine schedule and the list schedule on machines with list . Then for every feasible -machine schedule ,
Lemma 4.16 (any precedence-respecting list , with its idle-free one-machine schedule ): for every job ,
Lemma 4.10: , i.e. for an optimal list and every feasible .
Lemma 4.11: , i.e. for every feasible on any number of machines, and the value is attained by a feasible schedule on machines.
The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor for a strongly NP-hard problem, halving the factor that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a share of its one-machine completion time, so the same bound applies to other objectives built from completion times.
Formalizing it. The paper's proof is complete and short, but it argues about events at a time (jobs that finish exactly at , jobs that become ready at , machines freed at ) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.
List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form holds only if such idle time can be accounted for by 's own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.
Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits only in lower-bound instances elsewhere; the bounds here assume .succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.
Minimizing the sum of weighted completion times is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.
Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an -machine schedule, and proves that a -approximate one-machine schedule yields a -approximate -machine schedule for every . The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.
An instance has jobs . Job has processing time , release date and weight . Precedence constraints form a strict partial order : means that may start only after completes.
A feasible nonpreemptive schedule on machines assigns each job a start time and a machine; each job runs uninterrupted for time units on its machine, two jobs on one machine do not overlap, , and whenever . The completion time is and the value of the schedule is . A one-machine schedule is the case .
The critical-path length (Definition 4.1) is for a job without predecessors and otherwise; it is the earliest time could complete with unlimited machines.
A list is an ordering of the jobs. Delay List with parameter processes time continuously. A job is ready once it is released and all its predecessors have completed; is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:
For a job , is the set of jobs up to and including in the list, the set after it, the set of jobs of started before , and . Definition 4.4 builds from the schedule a backward path ending at , whose length is .
Let be a feasible one-machine schedule of the instance with for every feasible one-machine schedule . Let and . Every Delay List schedule built on the completion order of satisfies, for every feasible -machine schedule ,
A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.
The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an -machine algorithm at a bounded loss. With an optimal one-machine schedule and the factor is (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's -approximation for parallel machines with release dates (§4.5).
Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.
The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.
Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; , readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor of an optimal one-machine schedule" and "within a factor of an optimal -machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.
Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's is modelled by machines.
It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.
Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.
Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written ), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.
A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the machines are one machine that is times as fast, and allow preemption.
Timeline:
An instance has jobs and identical machines. Job has a processing time and a release date .
A feasible schedule gives each job a start time and a machine. Job runs without interruption on its machine during , and two jobs on the same machine never overlap. The completion times are and the objective is . denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.
The one-machine relaxation has the same jobs and a single machine. Job has processing time and release date in , and may be preempted. A preemptive schedule of gives each job a processing rate . The rates sum to at most at each time, and no job is processed before its release date. Each job receives units in total. Its completion time is the first time by which all of it has been processed. is optimal if is minimal among all such schedules.
A list is an ordering of the jobs, and the completion order of lists the jobs by nondecreasing . Two ways of turning a list into an -machine schedule are compared.
With optimal, its completion order, the strict-order list schedule of and a Delay List schedule of with , every feasible schedule satisfies
The printed lemma says . Its proof gives , which is stated here.
In the order the proof uses them:
Two existence statements accompany them. One says an optimal exists. The other says a Delay List schedule exists for every list and every .
The result gives a -approximation for that is simple to state and runs in time. It improves the bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.
The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.
All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.
The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.
The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the -machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first jobs of the list and the start of the -th job. Proving this needs the strict order.
The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.
Jobs are Fin n and machines Fin m with . Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and 's optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of .
Committed conventions:
Fin n ≃ Fin n. A list of may break ties in completion time in any way, and every such list is covered.The statement cannot be made easy by the hypotheses. Two existence items show that an optimal and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.
Not stated: the running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.
A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.
In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.
Demand for the season has law on , distribution function and density . As in §3 of the paper, , is strictly increasing on , on , and the generalized failure rate is strictly increasing (IGFR). The expected sales from available units are
The retail price is , the unit production cost , the salvage value , with .
A contract is a pair of wholesale prices . Before production the retailer submits a prebook order of units at . The supplier then produces . During the season, after running out of prebooked stock, the retailer places at-once orders at , filled from the supplier's remaining stock. Pull is ; an advance-purchase discount is . In §5.1 the supplier pays an extra shipping and handling cost per at-once unit. The profits are
A supplier best response to maximizes over . An outcome of is a pair with a best response to and maximizing when every alternative prebook is followed by a best response to it.
Fix and , and suppose the retailer does not prebook under the pull contract : is his unique best reply, followed by the supplier's best response . Then there is with
such that has an outcome, and every outcome of it satisfies
Without shipping costs, advance-purchase discounts with coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.
The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.
The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as . That limit involves , which the model does not provide: is differentiable only on , and for gamma demand with shape above the density vanishes at , so the paper's limit is . A proof of the goal must therefore not rest on the limit display alone.
The second obstacle is the retailer's global choice. The calculus concerns prebooks below the supplier's production . Once , the retailer might instead prefer a prebook at least , turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for close to requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at .
Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on only, so the exponential law is admitted. Quantities range over . Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for , and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue . The prebook function in milestones 5 and 6 is a function pinned on by Eq. (22), which determines it uniquely.
Readings of the paper's words:
A version of the goal that assumed , assumed , compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with , would be weaker than Theorem 8 and is not the target.
A complete development needs the concavity and first-order conditions for , the inverse-function derivative for , and the regime comparison between prebooks below and above . The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.
A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.
The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.
Demand is a random variable with distribution function and density . The paper assumes , strictly increasing, and an increasing generalized failure rate (IGFR): has . Production costs per unit, the retail price is , and leftover units are salvaged for , with . Expected sales with units available are
and the integrated supply chain's expected profit is . It is maximized at with ; write . The efficiency of a contract is , where is the quantity produced.
A contract is a pair of wholesale prices with . The retailer first prebooks units at each. The supplier, seeing , produces . During the season the retailer sells the prebook and, once it runs out, places at-once orders at per unit from the supplier's remaining stock, provided . The supplier's and retailer's expected profits are
with the at-once terms absent when . An outcome of a contract is a pair where maximizes the supplier's profit given , and maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push (), pull () and advance-purchase discount (). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).
For every with , the contract has an outcome and is Pareto; every outcome of every Pareto contract satisfies
and for every some contract with has an outcome with payoffs
A further draft theorem states the step of the proof in which the retailer's outcome profit along falls strictly from to as rises from to .
The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces ; the prebook price then acts as a pure transfer. Every division of is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.
The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.
The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when . Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook always being available and on . Third, the division claim is surjectivity of the retailer's equilibrium payoff over , which needs the solution of to vary continuously with , including at both ends ( at , at ).
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The standing assumptions are a structure: , strictly increasing on , on , and on . Differentiability is required only on , so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over . is a parameter with the hypothesis ; its existence is part of milestone 1.
Readings of informal words: "includes all" means every contract with has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the family; "any division is achievable" is surjectivity onto ; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is " is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when (p. 226, "with push , so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires (p. 228 sets aside as Pareto inferior); pull includes (the paper's remark in the proof) and advance-purchase discounts include (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.
Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of as would turn the goal into algebra, and is ruled out.
Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of , and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.
A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.
Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.
Demand has distribution function and density . The paper's standing assumptions (§3, p. 225) are: , strictly increasing, and the generalized failure rate strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost to produce, sell at the retail price , and are salvaged at .
Expected sales with units available are , and the integrated chain earns . It is maximized at the newsvendor quantity , , with ; the efficiency of a contract is .
A contract is described by the quantity it induces.
Write and (the hazard rate). The retailer's preferred pull contract is and the supplier's preferred push contract is .
A contract Pareto dominates if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.
A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks and the supplier then chooses her production to maximize . A pull contract survives the push challenge if the retailer's profit is strictly highest at .
There is a quantity , , the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that
and every pull contract with survives the push challenge.
The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ( for the supplier, for the retailer) is Pareto, and the least efficient Pareto contract, , is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself.
The results are proved in the paper, with the calculus informal, the unimodality of cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).
The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of (Lemma 1), and that fails to be routine at , where need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records , strictly increasing on , on , and for . Differentiability is not required at : the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy ; no sign is imposed on . Quantities range over . The paper's is a parameter characterized by , and the first milestone proves it exists and is unique.
Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.
Readings of informal words, each named in the item concerned:
The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. , , and are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.
Welcome contributions: basic facts about , and under the demand assumptions, reusable across the series' other two missions.
In the predict-then-optimize framework, a machine-learning model predicts the cost vector of a linear optimization problem , and a decision is made by solving that problem with the prediction. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed judging predictions by the SPO loss, the excess cost of the decision induced by when the true cost is . El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) develop generalization bounds for learning with the SPO loss.
The SPO loss is discontinuous in : its value jumps where the optimization problem has several optimal solutions. The paper's sharper bounds (its Theorems 4 and 5) therefore replace the SPO loss by a margin SPO loss that is Lipschitz, and they hold whenever the feasible region satisfies a geometric condition called the strength property. This mission formalizes the paper's first class of feasible regions for which that condition holds: strongly convex sets, such as Euclidean balls and balls with .
Let be a finite-dimensional real vector space with a norm (the paper's with a generic norm). A cost vector is a linear functional on ; its value at is written , and its dual norm is . The closed ball of radius around is .
The feasible region is nonempty, compact and convex. An optimization oracle is any map with and for all ; no tie-breaking rule is fixed.
If is compact, not a singleton, and -strongly convex for some , then for every oracle ,
The strength parameter equals the strong convexity constant.
Theorem 7 is what makes the paper's margin-based bounds usable for a concrete family of feasible regions. It says two things: the strength property holds with , so the Lipschitz constants in the margin analysis are explicit; and , so the margin of a prediction, and with it the empirical margin SPO loss, is as easy to compute as a dual norm. Combined with bounds on the multivariate Rademacher complexity, this gives generalization bounds for strongly convex regions whose dependence on the dimension improves on the paper's Natarajan-dimension bound. In dimension one it recovers the classical margin bounds for binary classification (Example 7, p. 24).
The results are proved in the paper; Proposition 1 is due to Vial (1983). None of them has a machine-checked proof known to this mission, and Mathlib has no notion of a strongly convex set (its StrongConvexOn concerns functions). The mission produces a formal definition of strongly convex sets for a general norm, the normal-cone characterization, and the connection to the predict-then-optimize strength property. It is one of four missions on this paper; the margin-based generalization bound itself is the subject of mission II, and polyhedral regions of mission IV.
Definition 5 speaks about balls around convex combinations, while Proposition 1 is a pointwise inequality with the exact constant . Evaluating the ball inclusion at any single convex combination loses that constant, since the admissible radius and the displacement of the centre both shrink with the mixing weight. Relating a ball to a linear functional also requires the maximum of over a ball to be attained and equal to , a fact about dual norms whose attainment depends on finite dimensionality.
For , comparing with gives only the inequality ; equality needs every nonzero cost vector to have a unique minimizer over . The oracle minimizes, whereas the normal cone is written for maximizers, so the signs in (5) and (8) do not match directly and are a common source of error.
StrongDual ℝ E), so is c w and the operator norm is the dual norm; balls are Metric.closedBall.S.Nontrivial. Proposition 1 and the ball identity carry no compactness hypothesis, as in the paper.Metric.infDist to the degenerate set; the parameter conditions and are hypotheses of the theorems, not parts of the predicates.Facility location asks where to open service points (warehouses, plants, servers) and how to connect customers to them so that the total opening cost plus the total connection cost is minimum. In the capacitated version each facility can serve only a limited number of customers, which is the situation in most applications: a warehouse has a floor area, a server a bandwidth. The problem is NP-hard, and the algorithms used in practice for it are often simple local search heuristics: start from a solution and repeatedly apply a small change that lowers the cost, until no such change exists.
The quality of such a heuristic is measured by its locality gap: the largest possible ratio between the cost of a solution that no allowed change can improve and the cost of an optimum solution. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave locality-gap analyses for k-median, uncapacitated facility location, and the capacitated problem in which several copies of a facility may be opened. This mission formalizes their §5, the capacitated case.
Timeline (as surveyed on pp. 545–546 of the paper). For the variant 1-CFL, where at most one facility may be opened at each location, Korupolu, Plaxton and Rajaraman (1998) showed that local search with add, drop and swap moves has locality gap at most 8 when capacities are uniform; Chudak and Williamson (IPCO 1999) refined this to 6, and Pál, Tardos and Wexler gave a local search with gap 9 for nonuniform capacities. For ∞-CFL, the variant with copies studied here, the known algorithms were LP-based: a 3-approximation of Chudak and Shmoys (1999) for uniform capacities, a 4-approximation of Jain and Vazirani for nonuniform capacities, and a 2-approximation of Mahdian, Ye and Zhang. Arya et al. (2004) analysed local search for ∞-CFL with nonuniform capacities: with a new move that drops any set of open copies and opens several copies of one facility, the locality gap is at most 4 (Theorem 5.5), and scaling the facility costs gives (p. 561). The tight example for uncapacitated facility location (§4.3) also shows a locally optimum solution of cost 3 times the optimum, so the locality gap of the procedure lies between 3 and 4; its exact value was left open (§6).
An instance consists of a finite set of clients, a set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality; is the cost of serving client from facility . Every facility has an opening cost and an integer capacity . Any number of copies of a facility may be opened; each copy of costs and serves at most clients.
A solution opens a finite list of copies, copy being a copy of facility , and assigns every client to a copy so that each copy serves at most clients. Write for the set of clients served by copy and for the clients served by a set of copies. Its costs are
The neighbourhood (9) of a solution whose multiset of open facilities is consists of
is locally optimum if no neighbour, with any feasible assignment of the clients, has smaller cost.
For every instance with at least one client, every locally optimum solution and every solution ,
In the order the paper's proof uses them:
A companion item states the scaled bound of p. 561: a local optimum for facility costs has cost at most in the original instance.
The result. Theorem 5.5 gives a constant locality gap for a local search procedure for capacitated facility location with copies and nonuniform capacities, a variant previously approached through LP-based algorithms; the drop-add move it analyses is the paper's new operation for this problem. The scaled bound gives an approximation algorithm once local search is run to approximate local optimality. The paper also shows (Figure 13, the procedure T-hunt) that the exponentially large neighbourhood can be searched with a knapsack oracle, so the analysis applies to an implementable algorithm.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a checked model of capacitated facility location with copies (solutions, costs, the multiset neighbourhood) and of the locality-gap argument. The per-copy model and the flow comparison of Lemma 5.4 are reusable for other capacitated location problems and for local search analyses that compare a local optimum with an optimum through a flow or a matching.
The obvious attempt imitates the uncapacitated analysis: close one copy of and send its clients to a nearby copy of . With capacities this fails, since that copy of may be too small to absorb them, and single-copy moves do not certify a constant bound. With the drop-add move a single copy of must be charged for a whole group of copies of , and the groups must be chosen so that the charges add up to a constant times ; the rounding of the number of new copies costs an additional that has to be absorbed as well.
CFLSol Cl Fa u: a number n of open copies, a map loc : Fin n → Fa giving the facility of each copy, and an assignment σ : Cl → Fin n with the capacity constraint for every copy. Copies are separate indices because is per copy. Its multiset of facilities is the image multiset of loc.Contributions are welcome at every level: proofs of the milestones, alternative proofs of Lemma 5.4 or (10) (for instance through a matching argument instead of flows), and general infrastructure for multiset neighbourhoods and assignment problems.
The k-median problem asks where to open facilities so that the total distance from a set of clients to their nearest open facility is as small as possible. It is a basic model of facility location in operations research (placing depots, warehouses or servers) and of clustering with representative centres, and it is NP-hard, so the question of interest is how close a polynomial-time method can come to the optimum.
Local search is among the most widely used heuristics for it: start from any facilities and repeatedly exchange one open facility for a closed one while the cost decreases. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first constant-factor guarantee for this heuristic on metric instances: every local optimum of the single-swap local search costs at most five times any solution with facilities. This mission formalizes that result.
Timeline of the relevant bounds:
A metric instance consists of a finite set of clients, a finite set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality. Write for the cost of serving client by facility .
For a nonempty set of open facilities every client is served by its nearest open facility, and the cost of is
The k-median problem asks for a set of at most facilities of minimum cost.
A swap closes a facility and opens a facility , giving . The neighbourhood of is
and is locally optimum if for every . The local search starts from an arbitrary set of facilities and applies improving swaps until none exists; swaps preserve the number of facilities, so it stops at a locally optimum set of exactly facilities. The locality gap is the supremum, over instances, of the ratio between the cost of a worst local optimum and the optimal cost.
The analysis uses the following notation. For a solution , let assign each client to a nearest facility of , let be the service cost of client , and let be the set of clients served by . For two solutions and put . A facility captures if ; is bad if it captures some and good otherwise.
For every metric instance, every , every locally optimum set of exactly facilities and every nonempty set of at most facilities,
The comparison solution is arbitrary, not an optimum; the statement is the locality gap bound in the form the proof gives.
Theorem 3.2 shows that the simplest exchange heuristic for k-median is a constant-factor approximation on every metric instance, and the paper states that the analysis is tight: its example of §3.5, given for swaps of two facilities, is said to generalize to swaps of facilities, where the bound is 5 for . Combined with the standard device of accepting only swaps that improve the cost by a factor , it yields a polynomial-time -approximation (p. 548). The same capture-and-reassignment argument is reused for multi-swap k-median, for uncapacitated and capacitated facility location in the same paper, and in later work on k-means and on local search for clustering; its milestones (the capture graph and the mapping ) are the reusable part.
The result has been proved since 2001 and is textbook material (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, Chapter 9). No machine-checked proof of it is known; Mathlib has no k-median problem and no locality-gap result for any clustering objective. The work remaining is to formalize the known proof.
The obvious argument adds up the inequalities over a pairing of with , rerouting the clients of the closed facility to the nearest remaining facility. This fails when a single facility of serves most clients of several facilities of : closing it leaves those clients with no nearby open facility, and no bound in terms of follows. The analysis must choose which swaps to consider so that such facilities are never closed, and must reroute the displaced clients of the facilities it does close to a facility other than the closed one while paying only a constant multiple of their own service costs. Both choices must work for arbitrary ties in the nearest-facility assignments and when and share facilities.
Namespace LocalSearchFL.KMedian. Clients and facilities are types Cl, Fa with Fintype and DecidableEq; the distance is a real-valued function on Cl ⊕ Fa with fields for nonnegativity, symmetry and the triangle inequality, and is not assumed. Solutions are Finset Fa. The cost is defined only for nonempty sets, from a nonemptiness proof, so no value is assigned to the empty solution; the goal takes nonempty with S.card = k, which is the paper's . Local optimality quantifies over every swap with and , exactly the neighbourhood of Theorem 3.2, and not only over the swaps with that the proof uses. The inequality is stated multiplied out, , so it is meaningful when .
The milestones quantify over nearest-facility assignments , with arbitrary ties. Capture is stated in integers as . The bijection of is a permutation of all clients fixing every client outside ; in inequality (2) it is a single permutation preserving every . Milestones 1–3 are purely combinatorial and are stated for arbitrary assignments, which contains the paper's case.
A formalization in which local optimality ranges over the swaps , , only, or in which or optimal is assumed, or in which the cost of the empty set is , is a different statement and is ruled out.
A complete development needs the finite-sum and Finset.inf' API of Mathlib, permutations (Equiv.Perm) and finite counting. The capture machinery and the mapping are reusable for the multi-swap and facility location missions of this series. Proofs of individual milestones are welcome independently of the goal.
A coherent risk measure assigns to a future financial position the smallest amount of capital that makes it acceptable to a supervisor. Artzner, Delbaen, Eber and Heath characterised the one-period version: every coherent risk measure has the form for a set of test probabilities (ADEH 1999). Regulators, insurers and banks, however, assess positions that evolve over several periods and whose risk is re-evaluated as information arrives. A multiperiod measurement should then be time consistent: the value assigned today should agree with the values the same method assigns tomorrow, so that it can be computed by backward induction, as in dynamic programming.
Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) identify exactly which sets of test probabilities give time-consistent multiperiod risk-adjusted values. The condition, stability under pasting, also appears as "rectangularity" in the recursive multiple-priors model of decision theory (Epstein and Schneider 2003), and as m-stability in the theory of risk-neutral measures (Delbaen, The structure of m-stable sets, Séminaire de Probabilités XXXIX, 2006). Riedel treated dynamic coherent risk measures on finite state spaces (Riedel 2004); the continuous-time case is in Delbaen's m-stable paper and Cheridito, Delbaen and Kupper 2004.
Let be a probability space with a filtration and a horizon . A value process is an adapted process with every essentially bounded; the class of value processes is . All stopping times take values in , and is the σ-algebra of the stopping time .
A set of test probabilities is a closed convex set of probabilities on , each absolutely continuous with respect to . Its elements are identified with their densities , and "closed" refers to . denotes the elements equivalent to . Each has the density martingale .
Pasting. For with density martingales and a stopping time , the pasted martingale is for and for : the pasted probability follows up to and afterwards. is stable (Definition 3.1) if every such pasting is again in .
Two risk-adjusted values. For a value process and a stopping time ,
the worst conditional expected value over all test probabilities and all later stopping times. The generalized Snell envelope is the backward recursion
For a stopping time let for and for , and for and for .
Assume is -trivial and . Then the following are equivalent:
In attack order, all stated for any set with unless stability is named:
A supporting item states that the essential infimum defining exists.
The result. Theorem 4.2 characterises the sets of test probabilities for which the natural worst-case risk-adjusted value is computable by dynamic programming. Stability is thereby the structural condition behind time-consistent coherent risk measurement, recursive multiple-priors utility and backward-induction pricing under ambiguity. Without it, the worst-case value computed today may disagree with the value obtained by first computing tomorrow's worst case and then today's. The equivalence with the submartingale property says that stability is also exactly what makes the largest submartingale minorant of Theorem 4.1. Theorem 4.3 and the recursivity results for final values in Section 5 are corollaries.
Formalizing it. The paper's proof is complete apart from Lemma 4.1 and its Corollary, whose proofs are left to the reader. No machine-checked version of this result, of the generalized Snell envelope or of essential infima of families of random variables is known to exist. A formal proof would provide a reusable development of discrete-time optimal stopping under a set of probabilities, the essential-infimum calculus of Neveu, and density-martingale pasting — infrastructure that many results on robust optimal stopping, dynamic risk measures and robust Markov decision processes need.
The direction from stability to Bellman's principle needs an essential infimum to be exchanged with a conditional expectation under another probability (step (3) of the proof). This is false for a general family: an essential infimum of conditional expectations is not the conditional expectation of an essential infimum. The exchange works only because stability makes the family closed under minima (Lemma 4.1), so that it is directed downward and its essential infimum is the limit of a decreasing sequence, and because Lemma 3.1 lets the test probabilities used before and after be chosen independently. The converse, from the submartingale property to stability, is not a computation: it uses the separation theorem in against a pasted density assumed outside , which is where convexity and -closedness of are used. Dropping either hypothesis breaks that direction.
Lean represents by its set of densities in : -measurable, a.s. nonnegative, integrable, of mass one, convex, sequentially closed in the seminorm and saturated under a.s. equality. Test probabilities are , and is Mathlib's conditional expectation under . Time is , and every stopping time is bounded by . A -submartingale on is Mathlib's Submartingale of the process frozen after . The essential infimum of a family is defined in the mission (Mathlib has only that of a single function); a supporting item shows that it exists, so its fallback value is never used. All identities between risk-adjusted values hold -almost surely.
Conventions made explicit:
Bellman's principle must be stated with on both sides and for all stopping times . Replacing by , or restricting to deterministic times, turns the goal into a property of the recursion and is not the theorem.
Needed infrastructure, reusable beyond this mission: existence and directedness of essential infima of families; conditional expectations under equivalent measures and the Bayes formula; optional sampling for bounded stopping times under each ; the – separation theorem. Contributions of any of these, and proofs of the milestones in any order, are welcome.
The bilinear program
with and polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on and on are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.
Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set of pairs , so that constraints may couple and . They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.
Write points of as , and let be a nonempty compact set. No convexity of is assumed. Let be continuous on .
The function is biconcave over (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside : for every fixed , the map is concave on every convex set with ; and for every fixed , the map is concave on every convex set with . Equivalently, is concave along every segment of that is parallel to the -block or to the -block. A bilinear objective with and concave is biconcave; joint concavity of is not required.
The boundary is the topological frontier of in : the closure of minus its interior. A solution of is a point with for all (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is .
If () is nonempty and compact, and is continuous on and biconcave over , then
The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on (a constant is a counterexample to that).
Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to , and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.
The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.
The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. need not be convex, so it has no useful extreme-point structure, and is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.
What remains is local geometry around an interior minimizer: one must find points of around it at which biconcavity can be applied in both blocks, and control their membership in without convexity. The feasibility of the mixed points and , which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.
EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on ), and BiconcaveOn S φ. One hypothesis is added: . For the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.IsLocalMinOn relative to the box, and non-globality of records the paper's word "proper".IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.A recent conjecture proposes a holographic duality between a static patch of Jackiw–Teitelboim (JT) gravity with positive cosmological constant, a two-dimensional reduction of three-dimensional de Sitter gravity, and the double-scaled SYK model at infinite temperature (DSSYK). The conjecture comes from Susskind (arXiv:2109.14104, arXiv:2205.00315), Lin–Susskind (arXiv:2206.01083) and Rahman. In the paper arXiv:2209.09999, Susskind looks at the semiclassical limit of de Sitter space, where the horizon entropy diverges. There physics splits into a cosmic sector, sensitive to the de Sitter radius , and a microscopic (string) sector, which does not see it. The paper argues that the limit of DSSYK shows the same split, with the two sectors separated by a factor of . This parallel is offered as evidence for the duality.
Most of the paper's arguments are heuristic scaling estimates. Several of them rest on explicit closed-form expressions: the epidemic scrambling function, the large- correlators, and the second moments of the Hamiltonians. These can be stated and proved as precise limit theorems. This mission collects them.
The SYK model has Majorana fermions with , coupled by -body interactions with Gaussian random couplings. The cosmic Hamiltonian is , where the couplings have variance (eq. (3.4)), and is a fixed energy. The string Hamiltonian is (eq. (3.7)). Cosmic time and string time are related by .
The double-scaled limit is a sequence of models with
In particular . Infinite temperature means expectations are taken in the maximally mixed state.
In DSSYK scrambling is described by the epidemic scrambling probability (eq. (8.1))
The infinite-temperature second moments of the two Hamiltonians are
For a double-scaled sequence and :
Early scrambling is ordinary fast scrambling in string units (8.3). Late scrambling is a quasinormal-mode decay in cosmic units (8.6).
The goal theorem is the paper's clearest quantitative instance of the separation of scales. The same function (8.1) shows a finite-rate exponential onset only in string time, and a finite-rate exponential saturation only in cosmic time. Neither regime survives in the other's units. Milestones 6–7 are the quantitative input to the paper's claim, attributed to H. Lin, that the cosmic Hamiltonian is not in the cosmic algebra while the string Hamiltonian passes the corresponding fluctuation test. Milestones 4–5 make precise the emergence of the string scale and the confinement of fermions near the horizon.
On formalization: the paper derives these limits by informal asymptotics, and some are stated only up to "". The formal statements fix the exact constants. Two of them differ from the paper's displayed formulas: the factor in (11.1)–(11.2), which comes from when , and the factor in the exponent of (9.4). The paper's qualitative conclusions are unchanged. At the time of drafting, a search of the platform found no existing formal statements of these results.
Every statement is a limit in which two large parameters, and , compete inside an exponent. The naive move of expanding to first order is valid only when . In the goal's late-time regime diverges, and at the end of the fast window stays finite. Each regime needs its own uniform control of . The Hamiltonian milestones need the product asymptotics under , which is a second-order effect that first-order Stirling-type estimates miss.
Filter.Tendsto, Real.rpow, Real.log, Real.cosh) and an improper integral of . Reusable lemmas about in the regime are welcome.A set of positive integers is pairwise coprime if for all distinct . The primes are the model example, and a recurring theme in Erdős's combinatorial number theory is that pairwise coprime sets cannot do much better than the primes on natural additive or harmonic statistics. Erdős Problem 1210 asks for a sharp version of this principle for the harmonic weight , which measures how densely a coprime set can crowd the point from below.
Timeline.
Fix a natural number . Consider finite sets of integers with for every , and with for all distinct . For such a set define the reciprocal gap sum
Every term is at most , and the element contributes . Write for the sum of reciprocals of the primes below ; by Mertens' theorem it equals . Throughout, denotes the number of primes .
The goal of the mission is the affirmative answer to Problem 1210: there is an absolute constant such that
for every and every pairwise coprime . A negative answer is equally welcome and is recorded by disproving the goal statement.
The milestones are:
The result itself. An affirmative answer would say that, for the weight , no pairwise coprime set beats the primes by more than a constant, and would give a quantitative form of the heuristic that coprime sets behave like sets of primes near a point. A negative answer would exhibit coprime sets that concentrate near more efficiently than the primes do in the harmonic sense. The [Er77c] variant concerns only primes, and relates the distribution of primes just above to the primes below the interval length .
Formalizing it. Neither the goal nor the [Er77c] variant is known. The mission produces Lean statements checked against the source, a reduction (milestone 2), to be verified in Lean, that isolates exactly which counting estimate would suffice, and the elementary coprimality lemma (milestone 1). These pin down what a proof or disproof must supply.
The natural first attempt splits into elements with a prime factor , of which there are at most , and -rough elements, and then hopes that sieve bounds make the rough part . The obstruction is that may contain many primes in . Bounding the number of primes in a short interval by is a form of the second Hardy–Littlewood conjecture , which is open and known to be incompatible, in its exact form, with the prime -tuples conjecture. So the counting route in milestone 2 needs input on primes in short intervals beyond current knowledge, and any proof of the goal must either supply such input or avoid pointwise counting.
All objects are elementary: is a Finset ℕ, coprimality is Nat.Coprime, primes are Nat.Prime, is Nat.primeCounting, and the sums are real-valued. The source's is encoded as an existentially quantified real constant chosen before and . The source asks a yes/no question; each statement is posed in its affirmative form, and a disproof (a proof of the negation) settles the negative answer. The standing hypothesis means every denominator is at least , so no division-by-zero default can make the statement trivial. The window is written as with truncated natural subtraction together with .
No new definitions are required. Useful reusable contributions include Mertens-type estimates for , partial summation lemmas for finite sums over , and upper bounds for primes in short intervals.
ErdosProblems/1210.lean, https://github.com/google-deepmind/formal-conjecturesAddition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.
Timeline.
The conjecture itself remains open.
For a finite set define the sumset and product set
For nonempty both contain at least elements and at most . The quantity of interest is as a function of .
For every there is such that for every finite set ,
The cannot be removed: there is no with for all (take ; the multiplication table is by Erdős).
A proof of the goal would settle the sharp form of the sum–product phenomenon over . Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over have come together with new incidence-geometric tools.
Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.
Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near , and passing beyond has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to ; even over , where arithmetic structure is available, the best general bounds are the real-number ones.
Sets are Finset ℤ; and are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to . Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis keeps every exponent positive, so the empty set contributes the trivial inequality rather than a junk value . The constant may depend on but not on . The Solymosi milestone is stated for so that .
The statements are for integer sets only; results proved over specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over , multiplicative energy, bounds for the multiplication table) are welcome.
A -dimensional complex abelian variety is of Weil type for an imaginary quadratic field if acts on by rational endomorphisms in such a way that each of the two eigenspaces of on meets in an -dimensional subspace. A. Weil observed that such carry a two-dimensional space of rational -classes, the Hodge–Weil classes, that are in general not generated by divisor classes. Whether they are algebraic is one of the main test cases of the Hodge conjecture; by work of Schoen, Moonen–Zarhin and others, algebraicity for abelian fourfolds of Weil type implies the Hodge conjecture for all abelian fourfolds.
E. Markman (arXiv:2502.03415) proves this algebraicity by a new construction. Its starting point, developed in §§1.2 and 2 of the paper, is linear algebra: the even cohomology of an abelian -fold is a half-spin representation of , where , and a rational plane meeting the variety of pure spinors in two conjugate -points (a -secant) equips with the structure of an abelian variety of Weil type. This mission formalizes that construction and its explicit example in §2.4.
Timeline (as summarized in §1.1 of the source).
Let be a complex torus of dimension . Fix a basis of , so that , and write in dual coordinates. The complex structure of is a real matrix with acting on ; its -eigenspace is . A number acts on by and on multiplicatively; a class of type is multiplied by . The Hodge ring is .
For a complex torus of dimension with ample , and a positive integer : are even pure spinors with , and there is a rational acting by on with
That is, is a polarized abelian variety of Weil type.
Equation (2.4.6) (the annihilator of ), Equation (2.4.5) (the plane lies in the Hodge ring), Lemma 2.2.6 (Weil's condition), the rational similarity of (2.2.4)/(2.4.1), the commutation (§2.4, p. 20), and Lemma 2.4.2 (the formula for ).
The result. The construction supplies, for every imaginary quadratic field and every polarized abelian -fold, a polarized abelian variety of Weil type , together with a description of its Weil structure in spin-representation terms. The rest of the paper deforms this structure ( plays the role of the special Mumford–Tate group) and uses Orlov's derived equivalence to obtain the Hodge–Weil classes from sheaves; the final application is the Hodge conjecture for abelian fourfolds.
Formalizing it. The results of this mission are proved in the paper; none of them has a machine-checked proof. The mission produces a reusable Lean model of the spin representation of , of pure spinors and their annihilators, and of Hodge types on , all built on Mathlib's exterior and Clifford algebras.
The algebra in the explicit example is short, but the general milestones rest on facts about pure spinors (their annihilators are maximal isotropic; a conjugate pair with splits ; rationality of by Galois descent) and on Lemma 2.2.6, whose proof in the source uses Chevalley's isomorphism as a morphism of Hodge structures. A coordinate computation settles the example but not the general statements. Sign conventions (the choice of , the complex structure on , and the sign of ampleness) all enter the final negativity claim.
ExteriorAlgebra ℂ (Fin (2n) → ℂ); contraction is Mathlib's CliffordAlgebra.contractLeft; is the truncated exponential .General relativity describes gravitation through the curvature of the Levi-Civita (Christoffel) connection of a spacetime metric. An alternative description, going back to Einstein's 1928-1930 papers on distant parallelism and developed in modern form as the teleparallel equivalent of general relativity, uses instead a tetrad field and the Weitzenböck connection it defines, a connection with vanishing curvature but non-zero torsion. The paper of Aldrovandi, Pereira and Vu (Braz. J. Phys. 34 (2004) 1374) reviews this formulation as a gauge theory of the translation group, and uses it to discuss the weak equivalence principle and a global (phase-factor) formulation of gravitation.
The claim that both descriptions are physically equivalent rests on a small number of exact tensor identities: the Weitzenböck connection splits as the Christoffel connection plus the contortion tensor, its curvature vanishes identically, and the teleparallel Lagrangian differs from the Einstein-Hilbert Lagrangian only by a total divergence. This mission asks for machine-checked proofs of these identities, in coordinates, exactly as used in Sections 2-3 of the paper.
Timeline (for orientation): Einstein introduced distant parallelism in 1928 (translations in the Delphenich collection Selected Papers on Teleparallelism); Weitzenböck studied the differential invariants of the theory the same year; the modern teleparallel equivalent of general relativity was developed from the 1960s-1970s onward, and the gauge-theoretic reading used here is the one reviewed by Aldrovandi-Pereira-Vu (2004).
Work in a single global chart and write for coordinate partial derivatives. Tangent-space (Latin) indices are raised and lowered with the Minkowski metric .
Curvature of a connection is , Ricci , scalar (Landau-Lifshitz conventions, consistent with the paper's Eq. (15)). The Einstein-Hilbert density is .
For a smooth, positively oriented tetrad (, so ):
The paper states only "up to a divergence"; the divergence term is written explicitly because an unspecified divergence would make the statement empty (every function on is a divergence).
The goal identity is the precise sense in which teleparallel gravity is "equivalent" to general relativity: the two actions differ by a boundary term, so they give the same field equations (the paper's Eqs. (12) and (15)). Milestone 4 is what turns the teleparallel force equation into the geodesic equation (Eq. (20)), and milestone 2 is the dictionary between the gauge field strength and torsion used throughout Sections 3-4. The results are classical and proved on paper; to our knowledge they are not formalized in Mathlib, which has no coordinate tensor calculus of this kind. A formal development would provide reusable coordinate lemmas (derivative of an inverse matrix field, symmetry of second derivatives in index form, Christoffel symbols of ).
Each identity is elementary on paper, but the index computations are long, and in Lean every derivative carries differentiability side conditions: derivatives of inverse matrices and of determinants, and symmetry of mixed partial derivatives, must be justified from smoothness and invertibility of the tetrad. The goal identity involves second derivatives of the inverse metric and a careful bookkeeping of about a hundred index contractions.
Spacetime is as Fin 4 → ℝ with one global chart; partial derivatives are Fréchet derivatives applied to coordinate basis vectors. A tetrad is a family of real functions h a μ, assumed with invertible matrix at every point (IsTetrad). Inverses are matrix inverses (which would be for singular matrices; the invertibility hypothesis excludes this). The physical constants are arbitrary reals. All definitions live in the single definition file of the mission, namespace TeleparallelGravity.
At one loop, the worldsheet of a closed string is a torus, and the one-loop vacuum amplitude of the bosonic string is an integral over all conformally inequivalent tori. Two tori with modular parameters and are equivalent exactly when for an integer matrix of determinant one, so a consistent string amplitude must be built from -invariant data. In David Tong's Cambridge Part III lecture notes (Section 6.4), the partition function of the bosonic string is computed in lightcone gauge and written in terms of the Dedekind eta function; the notes then observe that the measure and the integrand are individually modular invariant. This invariance is the mechanism by which string theory avoids the ultraviolet divergences of point-particle loops: the integration region is a fundamental domain that never reaches (Polchinski 1986).
Write . A modular transformation is the map
generated by and . With the Dedekind eta function is
convergent and non-vanishing on . The partition function of a single free scalar field on the torus is, up to constant factors, (6.20)
and the bosonic string partition function is
where is the standard fundamental domain.
For every and all with ,
The result. Modular invariance of the integrand is what makes the one-loop string amplitude well defined as an integral over the moduli space of tori, rather than over the whole upper half-plane: restricting to is only consistent because nothing depends on the representative. It is the first instance of a consistency condition that, in the superstring, constrains the allowed gauge groups and spectra.
Formalizing it. The eta transformation laws are classical (Apostol 1990, Ch. 3); Mathlib contains the definition of the eta function and results on and its fundamental domain, but, to the mission author's knowledge, not the -transformation law of . The mission produces a self-contained formal statement of the physics claim "both the measure and the integrand are individually modular invariant" and asks for its proof; milestones 1–2 are expected to follow from existing Mathlib results, milestone 6 is the analytic core.
The -law is immediate from the product. The -law is not visible from the product formula at all: it requires either Poisson summation / the Jacobi triple product for theta functions, or a Mellin-transform / Eisenstein-series argument ( is an Eichler integral of ), together with care about the branch of the square root. Passing from generators to all of requires an induction on words in and in which the multiplier must be tracked.
Points of are represented as complex numbers with the hypothesis ; a modular transformation is given by four integers with and acts by TongString.modularAction a b c d τ = (aτ+b)/(cτ+d). The eta function is defined directly by Tong's product formula as TongString.dedekindEta, using Mathlib's unconditional infinite product tprod. The square root in the -law is the principal branch, , which is the one intended since . The invariant measure is formalized as the measure on with density with respect to Lebesgue measure restricted to , and invariance as equality of push-forward measures. Constant prefactors that Tong explicitly drops (powers of , ) are omitted. Because every statement is restricted to , where has no zeros, the reciprocal is never a division by zero, so no statement is vacuous.
Mission Free Energy Principle I published the core variational step of the free energy principle (FEP): whatever recognition density a system carries, the posterior-form variational free energy never undercuts the data's surprisal, the bound is exact at the Bayesian posterior, and equality characterizes the posterior. That mission's shared finite substrate — normalized finite laws, finite kernels, entropy/cross-entropy/KL, and the finite generative model — now exists as platform definitions in the namespace FreeEnergyPrinciple.
The Free Energy Principle II mission formalizes the four structures the FEP literature builds on top of that core, all already machine-checked in the source repository fep_lean / fep_formal (Active Inference Institute):
Timeline of the mathematical content this mission formalizes:
fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 FEP topics compiled with zero proof holes against a pinned Mathlib. This mission transcribes the proved modules behind expected free energy, native Markov blankets, the scalar Gaussian filter/VFE, and Bayesian model reduction onto the platform.Two carriers, both fully machine-checked in the source repository:
Definitions.Def_fep_finite_laws, Def_fep_finite_information, and Def_fep_generative_model — no substrate is re-published. Zero-mass atoms are handled by the same totalized conventions as FEP-I: entropy uses Real.negMulLog (so exactly), KL is the nonnegative klFun integrand, and division premises are explicit.gaussianReal/gaussianPDF at a fixed strictly positive variance; the scalar OU prediction and the closed filter update give the posterior mean/variance the recognition family varies over. The native KL between two family members is exactly — proved against Mathlib's log-likelihood-ratio definition.The four definition items of this mission package exactly these carriers:
Def_fep2_expected_free_energy — the predicted state-outcome joint, preference risk, likelihood ambiguity, epistemic value, pragmatic cost, expected free energy (epistemic sign fixed by definition), the full-support contract, and the marginal/product/conditional-entropy/mutual-information lemmas the decomposition needs. Imports FEP-I.Def_fep2_gaussian_vfe — fixed-variance Gaussian family with its exact KL, scalar OU parameters, the exact scalar Gaussian filter (prediction, observation kernel, gain, closed posterior, evidence law), evidence surprisal, and the posterior-form Gaussian variational free energy. Self-contained.Def_fep2_bayesian_model_reduction — posterior odds, Bayes factor, and the model-odds update , with totalized division boundaries kept explicit. Imports FEP-I.Def_fep2_native_blanket — the static blanket factorization, the Dirac-mass embedding of finite laws into native measures, blanket/internal/external coordinates, the conditional-pair kernel, and the marginal/composition identifications the independence proof needs. Imports FEP-I.For every finite generative model, every policy , and every model with full support:
The epistemic-value sign is fixed by definition ( pragmatic cost epistemic value); the decomposition follows from two entropy identities: epistemic value is predicted outcome entropy minus ambiguity, and risk is cross-entropy minus the same entropy (Gibbs' inequality under full reference support). Nonnegativity of follows as a corollary — but the decomposition, not the bound, is the target.
For the exact scalar Gaussian filter, the posterior-form variational free energy at recognition mean is
the exact fixed-variance Gaussian KL (the recognition-to-posterior gap) plus the density-relative evidence surprisal. Equality with the surprisal holds exactly at the posterior mean — the Gaussian analogue of FEP-I's exactness theorem.
Bayes' rule in odds form: at positive evidence,
with the reference prior mass and reference likelihood as exact division premises. The multiplicative Bayes-factor structure (topic fep-120: factorized evidence ratios multiply; sequential model-odds updates agree with one update by product evidence) is available from the same definition layer as a further target.
The embedded static blanket factorization satisfies Mathlib's native CondIndepFun predicate: internal coordinates are conditionally independent of external coordinates given the blanket coordinate. The result is obtained by identifying the authored finite conditional kernels with Mathlib conditional distributions (the embedding preserves marginals and joints exactly on discrete carriers) — not by a finite mutual-information argument.
These four results are the load-bearing extensions of FEP-I's bound: expected free energy converts the variational principle into a theory of action selection; Markov blankets make "internal states" and "external states" well-defined relative to a blanket, which is what lets the FEP talk about self-organizing systems at all; the Gaussian filter is the tractable regime in which the variational machinery becomes the Kalman update; and Bayesian model reduction is the learning/comparison step that updates structure, not just parameters.
Formalizing them. All four families are proved with zero proof holes in the source repository, against a pinned Mathlib; the definition layer here is faithful (same carriers, same totalized conventions, same support contracts made explicit) and every item below compiles locally against the platform environment. The mission's value is reusable community infrastructure: the definition items publish the EFE layer, the Gaussian filter, the odds layer, and the native-blanket embedding in the shared namespace FreeEnergyPrinciple, so later missions (policy trees, collective inference, predictive coding) can import them instead of re-deriving. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.
Committed conventions of this mission's Lean development:
Free Energy Principle I finite substrate (namespace FreeEnergyPrinciple, definitions Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model); this mission adds definition items Def_fep2_expected_free_energy, Def_fep2_gaussian_vfe, Def_fep2_bayesian_model_reduction, and Def_fep2_native_blanket, all in the same namespace.gaussianReal/gaussianPDF, no finite substrate, no manifold geometry, no singular (zero-variance) branch.nextStaticModel construction.How much fluid does a pipe carry for a given pressure drop? For slow, viscous flow the answer is Poiseuille's law, . It is the standard first quantitative model of blood flow in vessels and appears in Lecture 15 ("The Mathematics of Water") of the Drexel biophysics course PHYS 461/561 (Fall 2011), where it is derived from the Navier–Stokes equation and then used to estimate flow speeds in capillaries. The fourth-power dependence on the diameter is what makes small changes in vessel radius matter so much physiologically.
A Newtonian fluid of viscosity flows steadily through a straight cylindrical pipe of diameter and length under a pressure drop . By cylindrical symmetry the velocity is axial, , where is the distance to the axis. The force balance on a thin cylindrical shell (slide 14), integrated along the pipe (slide 15), gives the radial equation
with boundary conditions: finite at the axis, and no slip, , at the wall. The flow rate is and the average velocity is .
Milestones, in order:
Goal (Poiseuille's law): for every pipe flow as above,
The result is classical and completely known; the value of the mission is a clean, machine-checked version of the full chain from the radial ODE and its boundary conditions to the flow-rate formula, rather than just the final integral. The ODE-uniqueness step (milestones 1–2), which uses boundedness at the axis to exclude the logarithmic solution, is the part lecture notes usually wave through.
Milestones 3 and 4 are calculus exercises. The real work is milestones 1–2: turning "integrate twice" into a rigorous statement on an open interval (a function with zero derivative on an interval is constant), and then showing that boundedness near forces (because ) and that continuity plus no-slip at the wall fixes .
All quantities are real. The ODE is imposed pointwise on the open interval with explicit differentiability; "" is encoded as boundedness of on , and the wall condition as plus continuity from inside. are assumed positive in every theorem; is an arbitrary real. The pressure field itself is not modelled: the statements start from the integrated radial equation of slide 15. Two typos on the slides are corrected: slide 15 writes the homogeneous term as (correct: ), and slide 16 prints (correct, as used on slide 17: ). All definitions are in the single definition file MathematicsOfWater_PipeFlow; all declarations use the namespace MathematicsOfWater.
Neutrinos are produced and detected in charged-current weak interactions as flavour eigenstates , but they propagate as superpositions of mass eigenstates . When the masses differ, the mass components acquire different quantum-mechanical phases and the flavour content of the beam changes periodically along its path: neutrino flavour oscillations, first proposed by Pontecorvo. Oscillations of atmospheric and solar neutrinos are the experimental evidence that neutrinos are massive and that leptons mix, and the vacuum oscillation formula is what experiments fit to extract mass-squared differences, mixing angles and the CP-violating phase.
The formulas are elementary quantum mechanics, but the standard three-flavour form requires careful bookkeeping of phases, of unitarity relations, and of the sign conventions for the CP-odd term. The source for this mission, Section 4 of P. Lipari's lecture notes Introduction to Neutrino Physics, derives the whole chain in a few pages (Eqs. (44)–(73)). The mission turns that chain into machine-checkable statements.
Fix flavours and mass eigenstates. The mixing matrix is a complex matrix, rows indexed by flavour and columns by mass eigenstate , with ; physically is unitary. Let be the squared masses, the distance travelled and the neutrino energy. In the relativistic approximation (, ) the transition amplitude and transition probability are
The antineutrino probability is the same expression with replaced by its entrywise complex conjugate . Write and define the CP-even amplitudes and the CP/T-odd coefficients
For two flavours the mixing matrix is the rotation ; for three flavours the standard parametrization is with mixing angles and CP phase (Eq. (57)).
For unitary and flavours ,
The source writes the last term as ; the formal goal fixes the sign by writing it in terms of .
The goal is the formula used to interpret long-baseline accelerator and reactor oscillation data: the three amplitudes govern the CP-conserving oscillation pattern, and the single product term isolates all CP- and T-violating effects in vacuum. Together with milestones 3–6 it shows that one real number, the Jarlskog parameter, controls CP violation, and that such violation requires a nontrivial phase, three nonzero mixing angles and three active oscillation frequencies.
These results are textbook material and their proofs are known; what this mission adds is a machine-checked derivation with every convention explicit. Two points in the printed source are resolved by the formal statements: the constant term of Eq. (61) is printed with exponent where squaring the amplitude gives exponent , and with the source's own Eqs. (57) and (69), the value of has the opposite overall sign from the one printed in Eq. (70). Milestone 6 is stated with the sign that follows from (57) and (69).
No step is conceptually deep. The work is in the algebra: expanding a squared modulus of a sum of three complex exponentials, and then using unitarity to remove the constant term and to identify the sine coefficients with one another. The unitarity relations among the products (footnote 8 of the source) have to be combined in the right order, and it is easy to lose a sign or a conjugate. Eq. (70) needs an explicit expansion of a product of three complex matrices.
Matrix (Fin n) (Fin n) ℂ; flavours and mass labels are the indices 0, 1, 2. Unitarity is membership in Matrix.unitaryGroup (Fin 3) ℂ, assumed only where the source uses it (Eqs. (67), (68), (71)).m2 : Fin n → ℝ; and are arbitrary reals. No positivity of is imposed: all statements remain true at , where Lean's convention makes every phase vanish.Complex.normSq of the amplitude. Antineutrino probabilities use the entrywise conjugate U.map star, not the conjugate transpose.Chapter 26 bounded the rate of uniform convergence by the Rademacher complexity; Chapter 27 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), introduces a second, metric measure of the size of a set of vectors, its covering numbers , the smallest number of Euclidean balls of radius needed to cover , and connects the two through Dudley's chaining. Covering numbers behave well under scaling and under coordinatewise Lipschitz maps (Lemmas 27.2–27.3), they are easily bounded for sets lying in a low-dimensional subspace (Example 27.1), and the chaining lemma turns a bound on at all scales into a bound on (Lemma 27.4), with the clean corollary when (Lemma 27.5). The chapter's example recovers for sets in a -dimensional subspace, the technique that the book says would sharpen the fundamental theorem's sample complexity from to .
For with the Euclidean metric, is an -cover of if every is within distance of some , and is the cardinality of the smallest -cover (Definition 27.1). The Rademacher complexity is Mission XX's. Chaining is run at the scales , , where is a radius of a ball containing , the book's being the smallest such radius.
For a nonempty , , contained in the ball of radius about some , and every integer ,
Example 27.1 (the grid -cover of a set of norm at most in a -dimensional subspace, of size ); Lemma 27.2 (scaling and translation); Lemma 27.3 (the contraction principle); Lemma 27.5 (the corollary of chaining). Further item: Example 27.2 ( for sets in a -dimensional subspace).
Chaining is the standard way to get sharp uniform convergence rates: a single-scale union bound (Massart's lemma at one resolution) loses a logarithmic factor, and summing Massart bounds over a geometric sequence of scales, applied to the increments between successive nearest cover points, recovers it. Lemma 27.4 is the discrete Dudley integral, and Lemma 27.5 is the form in which it is used: any polynomial-in- covering number gives -type bounds without the extra logarithm. On the platform these items complete the complexity toolbox begun in Mission XX and provide covering numbers as a reusable notion; the contraction and scaling lemmas mirror their Rademacher counterparts.
Lemmas 27.2 and 27.3 are immediate: the image of an -cover under the affine map is an -cover, and under a coordinatewise -Lipschitz map a -cover, since ; formally they are manipulations of the infimum in . Example 27.1 needs an orthonormal basis of the subspace (Gram–Schmidt, or Mathlib's orthonormal bases of finite-dimensional inner product subspaces of with the Euclidean structure) and the rounding of coordinates to a grid. Lemma 27.4 is the real work: after centering, take minimal -covers , the near-maximizer of (which depends on ), its nearest points , the telescoping , the bound , and Massart's lemma (Mission XX) on the sets of increments, of cardinality at most ; a formal proof must handle the supremum not being attained (approximate maximizers) and the dependence of all choices on inside the finite average. Lemma 27.5 lets using and . Example 27.2 combines Example 27.1 at the scales with Lemma 27.5, with the book's constant . The book's derivation uses the count without , so a proof needs the volumetric covering bound for and a direct count for .
Vectors are Fin m → ℝ with an explicit Euclidean norm, because Mathlib's norm on that type is the sup norm; covers are arbitrary finsets of and is an infimum in , so no junk value arises when no finite cover exists, and the chaining statements read through ENat.toNat for the bounded sets they concern, where it is finite. Subspaces are Mathlib Submodules with finrank = d. Two statements are given with the constants their proofs support, and the item texts say so. Example 27.1's grid has points per coordinate, so the cover has size , not , which is less than for and cannot bound a covering number of a nonempty set; Example 27.2 correspondingly has in place of . Lemma 27.4 is stated for any enclosing radius about any center, since the proof only uses that is a -cover of ; the book's minimal radius is the special case, and this is the form Example 27.2 needs (with and ). Lemma 27.5 keeps the book's .
Not stated: nothing else is in the chapter beyond the bibliographic remarks.
The book is discriminative almost throughout: it learns predictors, not distributions, following Vapnik's advice not to solve a more general problem as an intermediate step. Chapter 24 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), presents the generative alternative: assume a parametric form for the data distribution and estimate its parameters. The maximum likelihood principle is introduced on Bernoulli and Gaussian samples, shown to be empirical risk minimization for the log-loss, and analyzed through the decomposition of the true log-loss risk into a relative entropy plus an entropy (24.5), which explains both its consistency under a correct model and its overfitting on small samples. Naive Bayes and linear discriminant analysis show how generative assumptions reduce the number of parameters and make the Bayes classifier linear (24.8). The chapter's main theorem concerns the Expectation-Maximization algorithm of Dempster, Laird and Rubin for latent-variable models such as Gaussian mixtures: EM never decreases the log-likelihood (Theorem 24.3), because it is an alternate maximization of a lower bound that touches the likelihood at the posterior (Lemma 24.2). The chapter ends with Bayesian reasoning and the rule of succession.
A Bernoulli sample has log-likelihood and estimator (24.1); a Gaussian sample has . The log-loss is (24.4); on a finite domain, and . A latent-variable model is a parametric joint , , with ; , over the set of row-stochastic matrices, and EM alternates the E-step (24.10) with the M-step (24.11).
For a positive parametric joint , a sample , and any run of EM (each M-step returning some maximizer of ), the log-likelihood never decreases:
Equation (24.2) (Hoeffding for the Bernoulli estimator); the Gaussian maximum likelihood estimates of §24.1.1; Equation (24.5) (the risk decomposition ); Equation (24.8) (the LDA log-likelihood ratio is affine); Lemma 24.2 (EM as alternate maximization of , with and equality at the posterior). Further items: Gibbs' inequality, the Bernoulli maximum likelihood estimator (24.1)/(24.3), Exercise 1 (the biased variance estimate), Equation (24.6), the overfitting example of §24.1.3, Exercise 3 / (24.14), the weighted-centroid M-step (24.13), and the rule of succession of §24.5.
Theorem 24.3 is the guarantee that makes EM a sensible algorithm: it does not find the maximum likelihood estimate, but it climbs monotonically, and Lemma 24.2 identifies why, the E-step chooses the tightest lower bound at the current parameter and the M-step maximizes it. This variational view underlies a large part of modern latent-variable inference. Equation (24.5) is the information-theoretic content of maximum likelihood: the true risk is the entropy of the data plus the relative entropy to the model, so the best parameter is a projection of the data distribution onto the model class, and Gibbs' inequality is what makes that projection meaningful. The Bernoulli and Gaussian computations are the standard first examples, and Equation (24.8) is the reason linear classifiers appear in generative modeling. On the platform, the mission adds the relative entropy on finite domains, the EM objects, and Gaussian-integral identities that later probabilistic work can reuse.
The Bernoulli and Gaussian maximum likelihood facts are calculus, but as global maximization statements they need the concavity of and an explicit completion of squares rather than the book's stationary-point argument; the Gaussian case reduces to minimizing . Equation (24.5) is a finite-sum identity; Gibbs' inequality is Jensen for with the equality case, or the elementary . Lemma 24.2 is Jensen's inequality applied row by row to , with care at entries , where the convention is exactly Lean's junk value; Theorem 24.3 chains the lemma's three parts as the book does. The Gaussian expectation identities (Exercise 1 and (24.6)) require the moments of gaussianReal and Fubini over the product law. Hoeffding's inequality (24.2) is Mission II's Theorem for Bernoulli variables; the overfitting example is the inequality on . The rule of succession is a Beta-function identity provable by integration by parts.
Parametric families are functions from a parameter type to real-valued probabilities or densities, following the book's convention (p. 344) that denotes either; no measure-theoretic densities are needed except in the two Gaussian-integral items, which use gaussianReal and the i.i.d. law of Mission I, and in the two Bernoulli probability items, which use the Bernoulli law of Mission XIV. Lean's log 0 = 0 is handled explicitly: the EM items assume a positive joint, since with junk logarithms Theorem 24.3 is false (the M-step could pick a parameter with a zero component and inflated ), while the entropy terms use the convention that the book intends; the Bernoulli maximum likelihood statement ranges over ; the log-loss decomposition and Gibbs' inequality take the second distribution positive. The M-step is a predicate ("some maximizer"), so Assumption 24.1 is not modeled, and an EM run is any sequence of such steps. The Gaussian maximum likelihood statement requires a nonconstant sample, without which the likelihood is unbounded; the overfitting example is stated for , the range on which the book's inequality holds. Equation (24.8) is stated as a matrix identity for any symmetric in place of ; the soft k-means M-step is stated as the weighted-centroid minimization it amounts to.
Not stated: Naive Bayes (24.7), which is a rewriting of Bayes' rule; the mixture density itself and the E-step formula (24.12); the Bayesian derivations (24.16) and maximum a posteriori estimation; Exercise 2.
Dimensionality reduction maps data in to , , by a linear map , for computational reasons, for generalization (Chapter 19's curse of dimensionality) and for interpretability. Chapter 23 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies three ways to choose . Principal Component Analysis chooses the pair of compression and recovery matrices that minimizes the total squared reconstruction error, and the answer is the eigenvectors of for the largest eigenvalues (Theorem 23.2). Random projections choose with independent Gaussian entries, and the Johnson–Lindenstrauss lemma says that the norms of any finite set of vectors are then preserved up to with (Lemma 23.4). Compressed sensing exploits sparsity: a matrix with the restricted isometry property compresses every -sparse vector losslessly (Theorem 23.6), the reconstruction can be done by minimization, a linear program, with an error bound that degrades gracefully for approximately sparse inputs (Theorem 23.8, due to Candès), and Gaussian random matrices with rows are RIP with high probability (Theorem 23.9).
Vectors are functions with , and . The PCA problem (23.1) is , and . A random matrix has independent entries, in Lemma 23.3 and afterwards. is -RIP if for every with (Definition 23.5); is restricted to an index set .
Let , , and let be eigenvectors of for its largest eigenvalues, formalized as the first columns of a spectral decomposition with and nonincreasing. Then with minimizes (23.1): for every ,
Lemma 23.1 (the reduction of (23.1) to orthonormal and ); Lemma 23.4 (Johnson–Lindenstrauss); Theorem 23.6 (exact recovery under RIP); Theorem 23.8 (Candès' recovery bound); Theorem 23.9 (Gaussian matrices are RIP). Further items: Equation (23.3), Exercise 2, Remark 23.1 (the optimal value ), the eigenvector transfer of §23.1.1, Lemma 23.3, Theorem 23.7, Lemma 23.10, Lemma 23.11 and Lemma 23.12.
Theorem 23.2 is the Eckart–Young–Mirsky theorem in the form the book states it: PCA is the optimal linear compression-and-recovery scheme in the least-squares sense, and its solution is spectral. The Johnson–Lindenstrauss lemma is the basic tool of randomized dimensionality reduction, with a bound independent of , and the book's variant with explicit constants is what later chapters and the compressed-sensing proofs use. Theorems 23.6–23.9 together are the three "surprising results" of compressed sensing: information-theoretic recoverability from RIP, efficient recovery by convex relaxation, and the existence of RIP matrices by randomness; their proofs, Candès' cone argument and Baraniuk–Davenport–DeVore–Wakin's net-plus-union-bound, are among the cleanest in applied mathematics and are natural formalization targets. On the platform, the mission introduces Gaussian random matrices as product measures and the RIP predicate, usable by later work on sparse recovery.
Lemma 23.1 requires building an orthonormal basis of the range of , padded to vectors when the range has smaller dimension, and the identity ; Equation (23.3) is a trace computation. Theorem 23.2 combines (23.3), the change of basis with , the bound from extending to an orthogonal matrix, and Exercise 2, a rearrangement inequality; Remark 23.1 adds . Lemma 23.3 is the concentration of a variable (Lemma B.12), which must itself be established from the Gaussian moment generating function; the Johnson–Lindenstrauss lemma is then a union bound. Theorem 23.6 is a two-line contradiction with RIP applied to . Theorem 23.8 is the substantial one: the partition of into blocks of largest remaining entries, the bound , the -minimality inequality (23.8), Lemma 23.10, and the two claims combined through (23.5); a formal proof must handle the last, possibly shorter block, which the book's "assume is an integer" sidesteps. Lemma 23.11 is a volumetric net bound; Lemma 23.12 applies the Johnson–Lindenstrauss lemma to the image of an -net of the unit sphere of and closes the gap by the "smallest " argument, and Theorem 23.9 is a union bound over index sets.
Vectors are plain functions Fin d → ℝ with explicit norms, and matrices are Mathlib matrices, so the objectives are finite sums with no coercions between normed spaces. Random matrices are functions Fin n → Fin d → ℝ with the product of Gaussian laws gaussianReal 0 v, applied through Matrix.of; probability statements bound the outer measure of the failure event, and the failure events of Lemmas 23.4 and 23.12 are written with so that the book's strict conclusions follow. "Eigenvectors corresponding to the largest eigenvalues" is formalized as the first columns of a spectral decomposition with nonincreasing diagonal, which is exactly the set of such systems and avoids Mathlib's eigenvalue ordering conventions. Minimizers (, , ) are arbitrary elements of the argmin.
Five statements are given as their proofs support them, and the item texts say so. Lemma 23.3 and the Johnson–Lindenstrauss lemma are stated for : the printed range (and ) is false, since the upper tail decays like , slower than for (at it fails for ); the audit found this. Lemma 23.1 as printed, "every solution has orthonormal columns and ", is false, since has the same objective as ; the item states what the proof shows, that every is dominated by some with , which is all that (23.2) needs. Theorem 23.9 is stated with : Lemma 23.12 with (so that lies within ) and , followed by a union bound over the at most index sets, gives these constants, and the printed and are not reached by the argument. Theorem 23.8's proof assumes is an integer for simplicity; the statement is given without that assumption, since only the last block of the partition can be short and the block inequality still holds. Lemma 23.3 has , and the Johnson–Lindenstrauss lemma , since for its is and the conclusion fails.
Not stated: §23.1.2 (implementation), Remarks 23.2–23.3, §23.4 (the comparison of PCA and compressed sensing), Exercises 1 and 3–6.