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.
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?
Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.
The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.
The links are , link carrying circuits. A route belongs to a set of routes, and the link-route incidence matrix records how much of each link a route needs: a call on route requires circuits from link and is lost if any link has fewer than free. (The classical case is a – matrix and exactly when ; from section 3.3 the book allows any non-negative integers.)
Calls requesting route arrive as a Poisson process of rate , independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing for the number of calls in progress on route , the process is Markov on
and is called a loss network with fixed routing.
Write for Erlang's formula, , published in mission I of this series. The Erlang fixed point equations are
The factor removes link 's own thinning from the product, so in the – case the argument is , the reduced load offered to link .
The goal fixes no formula for and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube ; uniqueness is the substance.
The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution on ; and the acceptance probability . Then the optimization side: that and the utilization are strictly increasing in , which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on , equation (3.6).
The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by . That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector coming from the maximum-probability problem.
Formalizing it. Nothing here is open. What the mission produces is the loss network model in
Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked
statement of the object the reduced-load approximation computes. It is also where this series'
earlier missions pay off: the uncapacitated network is literally the open migration process of
mission II with , , , and the exact distribution
(3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of
mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I
published.
Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization is strictly increasing in , which is itself a milestone here.
A second, formal difficulty: the equations involve , so a solution with would be meaningless. It is worth checking before starting that no such solution exists for , rather than assuming it.
Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only –), capacities are natural numbers, and arrival rates are positive reals. The feasible set is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.
Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route is and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; is the reciprocal of the sum in the book's notation. Capacities are assumed at least in the goal: a link with no circuits blocks everything, identically, and the factor would then be undefined rather than merely large.
The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.
Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the – equations (3.1) of section 3.2; the utilization function and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.
Consider a decision maker who must choose, at each of rounds, between two actions on the advice of "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.
At each round , a decision maker chooses one of two actions, or . After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. experts also each commit to a prediction every round, and the decision maker may consult their record.
The Weighted Majority (WM) algorithm maintains a weight for each expert , initialized to . It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by for a fixed parameter , leaving correct experts' weights unchanged. denotes the algorithm's own mistake count through round , and expert 's.
The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, , and follows that expert's prediction; is its expected mistake count.
Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses suffered by expert at round . It samples expert with probability from weights updated multiplicatively in the loss, . Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round is .
where . This is the chapter's most general result and the one the book reuses later on; it leaves free (no asymptotic tuning), so it survives whatever later chapters do with .
Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two
maximally simple experts, any deterministic strategy is beaten by a factor of by an
adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable —
first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic
penalty from to ), then Theorem 1.5 removes the
binary-mistake restriction altogether, replacing it with an explicit second-moment correction
term that vanishes as losses shrink. Together they trace
the chapter's own narrative arc from "no algorithm beats " to "an explicit, parameter-free
family of algorithms gets within of the best expert for any ."
All four results are proved by the book via the same device — a potential function
— one of the first instances of the potential-function method that
recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and
throughout online learning generally. None of these four statements, in this exact form, has a
formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest
existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope
below), proves an asymptotically similar bound by an entirely different route and under a
different loss model.
The natural first attempt at any of these bounds is to track (or , or ) directly and induct on ; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round says nothing about round 's outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using , or, for Hedge, for ) and a lower bound via the single best expert's weight, — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing .
Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight
sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own
output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun
fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and
x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote
prediction rule explicitly (per the triage rubric, the algorithm is part of the audited
statement here, not a black box the proof is free to instantiate). Randomization in RWM and
Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the
inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as
a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification
explicit ("denote in vector notation the expected loss of the algorithm by
"), so no probability space is introduced. Theorem
1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction
(prediction at round depends only on outcomes before ), instantiated at the book's own
two-expert construction (one expert always predicts , the other always ) rather than a
fully general -expert adversary argument — a strictly weaker instance of the general claim,
but the exact one the book's proof establishes, so no scope is lost relative to what is proved.
is kept as an explicit free parameter throughout, per the book's own presentation
(no substitution of the corollary's optimized
into the milestone statements).
A trivializing formalization to rule out: fixing (a single expert) would make Lemmas 1.3–1.5 hold vacuously with regardless of the potential-function argument; every formal statement here quantifies over an unconstrained with , not a hard-coded small case.
The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the
book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's
proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves
for exponential weights on the simplex against -valued losses,
via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a
different proof technique, a different (bounded, not merely non-negative) loss assumption, and
stated for simplex-comparator regret rather than the per-expert loss comparator here; it is
listed as a reference/comparison point, not reused.
Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables ) followed by a corrective decision made after (the second-stage, or recourse, variables ). Solving such a program means minimizing , where is the expected cost of the best recourse action given -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.
Fix natural numbers and a finite scenario count . A two-stage recourse instance consists of first-stage data , , , a fixed recourse matrix , and, for each scenario , a cost vector , a right-hand side , a technology matrix , and a probability with (Eq. (1.1)). The first-stage feasible region is .
For a fixed and scenario , the second-stage value is
(Eq. (1.6)), taken as an extended real: if no feasible exists, if the inner program is unbounded below. The expected recourse value is (Eq. (1.3)), combined so that -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is , and the deterministic-equivalent objective is (Eq. (1.2)). For with finite, the subdifferential is the set of satisfying for every (p. 115).
A simple-recourse instance is the special case : the recourse cost splits as , and decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions of each .
given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes " is optimal" a statement about a point that exists rather than an infimum that may not be reached.
Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of ; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), ) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of , and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.
The obvious shortcut is to treat as an opaque convex function and apply a textbook convex-KKT
theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the
specific function , built from finitely many parametric linear programs, each of which can be infeasible
() or unbounded () depending on . Convexity of
must come from convexity of the value function of a parametric LP in its right-hand side
(the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand
sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed
hypothesis. Handling correctly is a second, easy-to-miss source of error: the book
fixes an explicit, non-default convention ( dominates ) for combining
per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses,
so any formalization that reaches for EReal's built-in addition to aggregate silently
states a different theorem. Theorem 8's attainment condition is a genuine existence result, not
an automatic consequence of convexity: continuity alone does not give attainment on an unbounded
feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with
infimum attained by no finite ) shows the boundedness/recession hypotheses are load-bearing.
The scenario set is modeled as Fin K, a finite discrete random variable, matching Section
3.1b's development; under this model " has finite second moments" (the standing hypothesis
of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not
appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal
via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is
⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner
minimization rather than assumed convex; this rules out the chapter's trivializing
formalization, which the paper-level triage explicitly warns against: taking Q(x) as an
opaque convex-function hypothesis instead of deriving its properties from the inner LP's
structure. Aggregating the per-scenario values into uses a bespoke bookAdd operation
implementing the book's stated convention , since Mathlib's EReal
addition is defined with the opposite convention (). is
the ordinary subgradient-inequality set for this extended-real-valued function.
Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold
and the recession value depend on the point and direction exactly as
written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book
itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that
milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the
closed form of from Eq. (1.10) as a hypothesis on an abstract , matching how
the book itself uses (1.10) as an already-established fact rather than re-deriving it from the
second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result
() is deliberately left out of
this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would
require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art
match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived
VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a
differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces,
not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over
the specific polyhedral set , so none is a faithful match and all items here are original
drafts.
Let be an odd squarefree positive integer and let be a set of units modulo with . Then : every residue class, unit or not, is a sum of three elements of .
This is Corollary 1.5 of Xuancheng Shao, A density version of the Vinogradov three primes theorem, Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2. It is the local input to Shao's density version of the three primes theorem, and it is a clean finite statement in its own right.
At the set has five elements, so exactly, and is not a sum of three of its elements. The hypothesis therefore fails by nothing at all and the conclusion already fails. If is weakened to , the statement is false.
The corollary cannot be proved by induction on sets. Passing from to a prime factor splits into fibers of different densities, and a set is the wrong object to carry through that split. The induction has to run on functions , and the corollary is the case of a weighted statement, Proposition 1.4. That is the one step from which the rest follows.
The weighted statement then splits at the primes 3 and 5. For coprime to 30 the induction runs on the prime factors, using Cauchy-Davenport-Chowla for three sets modulo a prime, and it produces the stronger bilinear conclusion . The modulus 15 is handled separately by a linear program over the eight units. Two averaging inequalities, one symmetric and one asymmetric, are what turn a density above into a single good triple in both halves.
The nine milestones follow Shao's own numbering: the two averaging inequalities of Section 2 (Lemmas 2.1 and 2.2), the finite check at (Lemma 2.3), the three-set Cauchy-Davenport-Chowla bound, the divisor reduction that lets the proof assume , the induction away from 3 and 5 (Proposition 3.1), the modulus-15 case (Proposition 3.2), the weighted local result (Proposition 1.4), and the counting bridge that the units modulo number .
Every item is stated in Mathlib primitives alone, so the mission needs no definition items: IsUnit, Nat.totient, Odd, Squarefree, Finset, and Antitone. The set of units modulo is written Finset.univ.filter (fun x => IsUnit x) at each use rather than through a defined abbreviation, so a reader auditing a statement has to trust only Mathlib. That is also why open scoped Classical appears in the preamble.
The density hypothesis is written 5 * Nat.totient m < 8 * A.card, which is cleared of division so the whole statement stays in with no rounding.
Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors and , the primal is within of optimal.
The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.
Fix finite index types (primal variables) and (primal constraints), a matrix , a cost vector and a right-hand side . The covering primal and packing dual are
Note the index convention: carries the primal-variable index first, so the primal constraint indexed by sums over and the dual constraint indexed by sums over .
Given , the pair satisfies approximate complementary slackness when
For a primal-feasible , a dual-feasible , and satisfying the two conditions above,
Taking recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.
with no nonnegativity assumption on , or beyond feasibility itself.
Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of , produce a dual optimum of of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.
The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.
This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.
It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.
The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on versus and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.
Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.
Mirror symmetry began as an empirical observation in string theory: certain pairs of Calabi–Yau threefolds, with no evident geometric relation, give rise to the same physical theory, and invariants that are hard to compute on (counts of holomorphic curves) turn into easy computations on (variations of complex structure). The paper Mirror symmetry is T-duality by A. Strominger, S.-T. Yau and E. Zaslow, Nucl. Phys. B 479 (1996) 243–259, proposed the first structural explanation: should carry a fibration by special Lagrangian 3-tori, the mirror should be obtained by replacing each fibre with its dual torus, and the mirror map should be fibrewise T-duality. This proposal is now called the SYZ conjecture, and it organises most later geometric work on mirror symmetry.
The string-theoretic argument of Sections 1–2 of the paper is heuristic and is not formalizable as stated. Section 3 is different: it is a self-contained piece of differential geometry about the moduli space of a special Lagrangian submanifold together with a flat connection on it. This mission formalizes Section 3.
A short timeline of the mathematics the section rests on:
Fix . The ambient Calabi–Yau manifold is modelled by , carrying
Here is the standard Hermitian product of , conjugate-linear in its first argument.
The brane is an -torus. It is presented by its universal cover: a map that is periodic up to translation,
for a fixed family of periods . Such an is exactly a map of the torus into the complex torus , and integration over is integration over the unit cube .
Write for the partial derivatives of . The map is Lagrangian at if for all , i.e. ; it is special Lagrangian if in addition , i.e. . This is the supersymmetry condition of the paper (Section 2, conditions (ii) and (iii)). The induced metric is , the volume density is , and the second fundamental form of a Lagrangian immersion is the totally symmetric tensor
Given a family of such maps, its deformation -form is
the -form obtained by contracting the velocity into the Kähler form. For an -parameter family , , one gets such forms , , one per moduli direction.
The moduli data of Section 3 is a smooth -parameter family of special Lagrangian tori, all with the same periods, subject to two normalizations taken from the paper: each is harmonic for the induced metric (closed and co-closed), and the cohomology class of each is constant along the family. The (McLean) metric on the moduli parameters is
The full moduli space of the paper also records the flat connection; its moduli form a torus of the same dimension, with coordinates . On , modelled by with coordinates , the paper puts the block-diagonal metric and the constant almost complex structure , , with fundamental -form .
The goal theorem is the conclusion of Section 3: for every such family, the fundamental -form of the moduli space is closed,
and since is constant in these coordinates it is integrable, so is Kähler.
The milestones are the numbered intermediate results of the paper, in the paper's own order:
$$\textbf{ closed:}\quad \partial_c \int_L \theta^{a_1}\wedge\cdots\wedge\theta^{a_n} = 0 .
\textbf{Hessian} \Rightarrow \textbf{Kähler:}\quad \partial_a g_{bc} = \partial_b g_{ac} ;\Longrightarrow; d,\omega_{\mathcal M} = 0 .$$
Together, Propositions 1 and 2 are the statement that the tangent space to the moduli space consists of harmonic -forms — McLean's theorem in the form the paper uses it. Eq. (3.4) is the technical heart, and the last milestone is the step from it to the goal.
The result. Section 3 supplies the only rigorous mathematics in the paper. It says that the object the physics predicts to be a Calabi–Yau manifold — the moduli space of a supersymmetric brane — does carry the first piece of that structure, a Kähler metric, and that it carries a natural -form which, for toroidal branes, is a holomorphic -form and hence a candidate for the Calabi–Yau form of the mirror. Eq. (3.4) says the McLean metric is locally the Hessian of a potential; this affine-Hessian structure of the SYZ base is the starting point of the later large-complex-structure-limit programme.
Formalizing it. The Section 3 results have rigorous published proofs (McLean for the tangent space, Hitchin for the Hessian property), but no machine-checked proof exists for any of them, and Mathlib currently has no special Lagrangian geometry, no Hodge theory, and no differential forms on manifolds. The mission therefore also produces reusable infrastructure: a workable coordinate model of calibrated submanifold geometry, the variation formulas for the induced metric and for the pullbacks of and , and the Hessian-metric criterion for a Kähler structure, which is independent of the rest and reusable wherever affine-Kähler geometry appears.
The obvious approach to the goal — "the metric is Hessian, so take the potential and write down the Kähler form" — is not available: the potential is not part of the data, and producing it requires the symmetry first. That symmetry is the hard step, and it is hard for a specific reason: differentiating in the direction produces four terms — from , from , from the inverse metric , and from the volume density — and only their sum is symmetric in . Two of them are killed by an integration by parts that needs both harmonicity of and compactness of (this is where the torus, and not a coordinate patch, is essential); one is killed because a special Lagrangian submanifold is minimal, so the mean curvature term in vanishes; what survives is , which is symmetric because is a symmetric -tensor. Every one of those four cancellations has to be carried out.
Proposition 2 carries a separate difficulty: it is an identity between the variation of a determinant and a divergence, and it is false without the hypothesis that is special Lagrangian at the point in question — for a merely Lagrangian there is a further term proportional to the Lagrangian angle.
The formalization commits to the following, all of which are visible in the definition item and none of which are silent:
fderiv returns at a point of non-differentiability, so a statement about derivatives of a non-smooth map is a statement about zeros; every item therefore carries an explicit smoothness hypothesis, and the moduli-level items carry it inside the family structure.A complete development needs, beyond the definition item: the chain and product rules for fderiv on , symmetry of second derivatives, differentiation under the integral sign on a compact box, integration by parts for periodic functions on , and the derivative of and of matrix inversion. The last two, and the Hessian-implies-Kähler milestone, are reusable outside this mission. Contributions that replace the flat ambient by a general Kähler ambient chart, or that lift the model to Mathlib manifolds once differential forms exist there, are welcome and would supersede parts of this development.
Waldspurger's non-standard fundamental lemma is an identity between stable orbital integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even isogenous as algebraic groups, but whose root data become identified after tensoring with . The basic example is the pair , whose root systems and are exchanged by Langlands duality; the identity is what allows the twisted fundamental lemma to be deduced from the ordinary one. Waldspurger formulated the conjecture in L'endoscopie tordue n'est pas si tordue (2008); it is Theorem 1.12.7 of Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), proved there in equal characteristic by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.
Before any of that geometry can start, the two sides have to be compared: one needs a single Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving both groups at once. Producing that comparison is a self-contained piece of linear algebra over the root data, carried out in Ngo's §1.12, and it is what this mission asks for.
Let and be split reductive groups over a field, pinned, with maximal tori and . Each is determined by its root datum , where is the set of roots, the set of coroots and the set of simple roots singled out by the pinning.
An isogeny of root data between and (Ngo, Definition 1.12.1) is a pair of isomorphisms of -vector spaces
which are transposes of one another, such that carries the set of lines () bijectively onto the set of lines (), matching lines of simple roots with lines of simple roots, and such that has the same property for the lines spanned by coroots. Two semisimple groups with the same adjoint group are isogenous in this sense; so are a group and its Langlands dual, the interesting cases being , and , where a short root is sent to and a long root to with . Groups obtained by twisting a pair of isogenous pinned groups by a common torsor are called paired.
A prime is good with respect to when it divides neither of the indices
the two lattices being compared inside the single -vector space identified by .
i.e. conjugation by carries the Weyl group acting on onto the Weyl group acting on . Ngo's reason is that the reflection attached to a root depends only on the line through that root, so the bijection of root lines transports reflections to reflections. This equivariance is what makes the induced isomorphism descend to an isomorphism of the spaces of characteristic polynomials, which is Lemme 1.12.6 and which is what allows two points and with to be compared at all.
Two steps lead there: the reflection computation that makes a matched pair of root lines give a matched pair of reflections, and the integral statement behind Ngo's good-characteristic hypothesis — that when the two indices above are invertible in the base ring, the two lattices become identified after base change.
Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over with residue characteristic exceeding twice the Coxeter numbers, and for points and corresponding under , the stable orbital integrals of the characteristic functions of and agree. Waldspurger showed that this identity, together with the ordinary fundamental lemma, implies the twisted fundamental lemma. None of the objects in that statement — reductive group schemes over a discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the isomorphism the two sides of Theorem 1.12.7 cannot even be matched up.
Beyond this paper, the notion of an isogeny of root data and the good-characteristic base change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands duality for split groups, and neither is currently available.
The reflection step looks like a one-line computation and is one — but only once the two proportionality constants are known to agree. If and , the conjugate of is exactly when , and that is forced by transposition together with . The genuine difficulty in the goal is different: the definition only says that and permute lines, so one has to show that the bijection induced on root lines and the bijection induced on coroot lines are the same bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.
The lattice milestone has its own trap: the quotient must be shown to have vanishing after base change, not merely to vanish, or the inclusion becomes only surjective.
Root data are modelled by Mathlib's RootPairing ι ℚ M N, with the character space,
the cocharacter space, and rational coefficients throughout, so that "tensoring with
" is built into the ambient objects rather than performed explicitly. A choice of
simple roots is recorded as a subset of the index type rather than as a RootPairing.Base;
nothing in the statements depends on that subset beyond its role in the definition of an
isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space
generated by the coreflections, which is the form in which it acts on the Cartan.
The goal is stated as a two-sided intertwining property rather than as an equality of subgroups: every element of is intertwined by with some element of and conversely. This avoids introducing a conjugation homomorphism, and it is the form in which the statement is used. Both root pairings in the goal are required to be finite, reduced root systems, matching Ngo's hypothesis that and are reductive groups.
The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility in the base ring of the two indices, each expressed as the cardinality of an explicit quotient group; the conclusion is the bijectivity of the map induced on the tensor product by the inclusion of the intersection. If a quotient were infinite its cardinality is reported as , and invertibility of then forces the base ring to be trivial, so no false statement hides in that corner.
No statement here is vacuous: any pair consisting of a root system and itself, with and the identity, satisfies every hypothesis, and the pair gives the intended non-trivial instances.
A stochastic partial differential equation is driven by noise that lives on an infinite-dimensional function space, and the first object one has to control is the law of that noise: a Gaussian measure on a separable Banach space. Martin Hairer's lecture notes An Introduction to Stochastic PDEs (arXiv:0907.4178) devote their first technical chapter (Section 4) to exactly this, because every later construction — stochastic convolutions, invariant measures for semilinear equations, the ergodic theory of the stochastic Navier–Stokes equations — is phrased against it.
The single structural fact that chapter produces is the Cameron–Martin theorem (Theorem 4.44, p. 31). It answers the question: in which directions may one translate an infinite-dimensional Gaussian measure without destroying its null sets? In finite dimensions the answer is "all of them", because Lebesgue measure is translation invariant. In infinite dimensions the admissible directions form a proper, and typically much smaller, Hilbert subspace — the Cameron–Martin space — and the translated measure is either equivalent to or mutually singular with it, with nothing in between. This dichotomy is the reason Girsanov-type changes of measure, Schilder-type large deviation rate functions, support theorems and Malliavin calculus all take the form they do.
Throughout, is a separable Banach space, its topological dual, and a Borel probability measure on .
is Gaussian (Definition 4.4, p. 19) if for every continuous linear functional the push-forward is a Gaussian measure on in the sense of Definition 4.1, i.e. has characteristic function ; the degenerate case , a Dirac mass, is included. It is centred if all these one-dimensional laws have mean zero, which is expressed here as .
For a centred Gaussian the covariance form (4.2, p. 20) is
It is well defined because is -integrable, and it is a bounded bilinear form (Corollary 4.14, p. 22).
The Cameron–Martin space (Definition 4.26, p. 27) is classically built as the completion of
under . This mission uses the equivalent intrinsic description of Exercise 4.38 (p. 29), which avoids the completion:
The supremum is taken in ; since is admissible whenever is, it equals over the same set. For write , .
For a centred Gaussian measure on a separable Banach space and ,
Both implications are asserted: translation along a Cameron–Martin direction produces an absolutely continuous measure, and translation along any other direction does not (in fact it produces a mutually singular measure).
The milestone list follows the route of Section 4.2:
The Cameron–Martin theorem is what makes the Cameron–Martin space a canonical object rather than a formal construction: is simultaneously the set of admissible shifts, the intersection of all full-measure linear subspaces (Proposition 4.45), and the space whose unit ball governs Gaussian isoperimetry (Theorem 4.53, Borell–Sudakov–Cirel'son). Downstream in the notes it is used to identify invariant measures of linear SPDEs and to compare them; outside the notes it is the starting point of Malliavin calculus and of large deviation theory for Gaussian measures.
Status, precisely. The Mathlib library pinned by this mission already contains a substantial part of Section 4: the predicate IsGaussian (Definition 4.4), uniqueness of measures with equal characteristic functionals on a separable Banach space (Propositions 4.8 and 4.11), invariance of under rotations (Proposition 4.12), Fernique's theorem (Theorem 4.13), and the covariance form of (4.2) together with its boundedness (Corollary 4.14) as a continuous bilinear form on the dual. Those results are therefore not milestones here; they are the assumed foundation. What is absent, and what this mission asks for, is everything from the Cameron–Martin space onwards: its definition, its elementary properties, and Theorem 4.44 itself. No machine-checked proof of the infinite-dimensional Cameron–Martin theorem is known to the captain in any Lean library.
The naive route — write down the two densities and take their ratio — is unavailable: there is no translation-invariant reference measure on an infinite-dimensional Banach space, so "the density of " does not exist and the Radon–Nikodym derivative of with respect to must be produced directly, as the exponential of a random variable.
That random variable is the obstruction. For the functional is continuous and the computation is a characteristic-function identity. But is in general strictly smaller than : a general has an associated that exists only as an -limit of continuous functionals, defined -almost everywhere and linear only on a measurable subspace of full measure (Propositions 4.34 and 4.39). Establishing that these limits are Gaussian with the expected variance (Proposition 4.40) is the technical bridge, and it is why milestone 3 is stated as a statement about -limits rather than about elements of .
The converse half has a different shape. One must produce, for , a single one-dimensional projection that separates from arbitrarily well; unboundedness of over the covariance unit ball supplies with and as large as desired, and the quantitative Gaussian total-variation bound of milestone 5 converts this into total variation distance , i.e. mutual singularity.
The development is in Lean 4 with Mathlib, in the namespace HairerSPDE, shared by the whole series drawn from these notes. The conventions it commits to:
NormedAddCommGroup, NormedSpace ℝ, its Borel σ-algebra, CompleteSpace and SecondCountableTopology — the last two encode "separable Banach space".IsGaussian, which is Definition 4.4 verbatim; centredness is the extra hypothesis , needed because IsGaussian permits a non-zero mean.covarianceBilinDual, which equals (4.2) for centred measures with finite second moment and is set to zero otherwise; Fernique's theorem rules the degenerate branch out for Gaussian measures.fun x ↦ x + h, absolute continuity is Mathlib's ≪, and "measurable linear subspace" is a Submodule ℝ B whose carrier is a measurable set.The goal is an equivalence, so neither half can be discharged vacuously: the direction is non-trivial already for in finite dimensions, and the converse has content precisely when . Note that always, and that for a Dirac mass the covariance form vanishes and ; both degenerate cases are inside the statement rather than excluded by hypothesis.
Contributions welcome beyond the milestones: the reproducing kernel space and the isomorphism of Proposition 4.34, measurable linear extensions (Proposition 4.39), the dilation singularity of Proposition 4.43, and in the infinite-dimensional case (second half of Proposition 4.45). All of these are reusable outside this mission.
Chapter 11 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) replaces the Riemann integral of Chapter 6 with the Lebesgue integral, and the reward is a theory of integration whose limit theorems have no superfluous hypotheses and whose space of square-integrable functions is complete. The chapter runs from set functions and outer measures, through the Carathéodory construction of Lebesgue measure, measurable functions and the integral, to the convergence theorems (monotone convergence, Fatou, dominated convergence) and finally to the space and the Riesz–Fischer theorem (Theorem 11.42):
That completeness is what makes a Hilbert space, and it is the reason the Fourier series of Chapter 8 converge in the mean to the functions they represent.
This mission is the eleventh and last in a series formalizing Rudin Chapters 1–11. It uses the Riemann–Stieltjes integral of Mission VI (for Theorem 11.33, comparing the two integrals) and the trigonometric Fourier series of Mission VIII (for the reading of Parseval's theorem).
A set function on a ring of sets is countably additive if it takes the value on a countable disjoint union. Rudin constructs an outer measure from such a by covering with elementary sets and taking an infimum, calls a set measurable when it is approximable by elementary sets in the metric , and proves that the measurable sets form a -algebra on which is countably additive (Theorem 11.10). A real function is measurable when is measurable for every , and the integral is defined first for simple functions, then for nonnegative measurable functions as a supremum, and then for general by .
The space consists of the measurable with , normed by ; a sequence converges in the mean to if .
Mathlib's measure theory is used wherever it is mathematically the same object:
MeasureTheory.OuterMeasure and its Carathéodory -algebra, MeasurableSet,
Measurable, the lower Lebesgue integral ∫⁻ for nonnegative extended-real functions, the
Bochner integral ∫ and Integrable for the general case. What is set up freshly is Rudin's
of functions — Rudin.MemL2, Rudin.L2Norm, Rudin.CauchyL2,
Rudin.TendstoL2 — rather than Mathlib's quotient space Lp, because the Riesz–Fischer theorem
as Rudin states it produces an honest limit function, and the ε-N phrasing of Cauchyness and
of mean convergence is part of the statement.
If is a Cauchy sequence in , then there exists with : the space is complete.
Rudin's proof extracts a subsequence with , sums the telescoping series, uses the monotone convergence theorem and the Schwarz inequality to show that the sum converges almost everywhere, and identifies the pointwise limit as the mean limit of the whole sequence. Every ingredient is a milestone of this mission.
The Lebesgue theory is the point at which analysis acquires limit theorems that do not require uniform convergence. Monotone convergence, Fatou's lemma and dominated convergence are the three statements that make the integral usable in probability, in Fourier analysis and in the theory of partial differential equations, and the Riesz–Fischer theorem is what makes a Hilbert space and therefore the natural home of Fourier expansions: Parseval's identity (11.45) is the assertion that the Fourier coefficient map is an isometry onto .
Theorem 11.33 is the bridge back to the earlier chapters — every Riemann-integrable function is Lebesgue-integrable with the same integral, and a bounded function on is Riemann-integrable exactly when it is continuous almost everywhere — so the two halves of the book agree wherever both apply.
Mathlib has an extensive measure theory and proves many of these results in considerable generality. This mission's contribution is to state them in Rudin's formulation, for Rudin's of functions and with his explicit ε-N definitions, so that the chapter is available as a coherent, self-contained unit that matches the textbook line by line and links back to the Riemann–Stieltjes integral of Mission VI.
Individually, most milestones will reduce to Mathlib results after the correct dictionary is in
place, and the interesting work is exactly in that translation: Rudin's measurability
({x : f(x) > a} measurable) versus Mathlib's Measurable, Rudin's integral of a nonnegative
function versus ∫⁻ with values in ℝ≥0∞, Rudin's of genuine functions versus
Lp as a quotient by almost-everywhere equality. The last of these is what makes the goal
theorem nontrivial to derive: Mathlib's completeness of Lp gives a limit class, and one must
choose a measurable representative and verify Rudin's mean convergence with the concrete norm
Rudin.L2Norm, which is Real.sqrt (∫ f²) and not an ENNReal quantity.
Theorem 11.33 (Riemann implies Lebesgue) and Theorem 11.38 (density of continuous functions)
are the two other places where real work is required: the first has to connect the Chapter 6
definition of the Riemann integral with intervalIntegral, and the second is an approximation
argument.
Conventions fixed by this mission:
MeasureTheory.Measure, MeasurableSet,
Measurable, Integrable, ∫⁻ x, f x ∂μ for nonnegative ℝ≥0∞-valued integrands and
∫ x, f x ∂μ for the general real case. Rudin's Carathéodory construction is
MeasureTheory.OuterMeasure.caratheodory.ℝ≥0∞-valued
functions, matching Rudin's use of extended real values there.Rudin.MemL2 μ f is "f is measurable and f² is integrable"; Rudin.L2Norm μ f is
Real.sqrt (∫ x, (f x)^2 ∂μ); Rudin.CauchyL2 and Rudin.TendstoL2 are Rudin's ε-N Cauchy
condition and mean convergence. No quotient is taken, so the goal theorem produces a function.Rudin.RiemannIntegrable and Rudin.RiemannIntegral from
Mission VI, so the two integrals are literally compared.Contributions of the convergence theorems (11.28, 11.31, 11.32) and of the Schwarz inequality (11.35) are especially useful, since the goal theorem consumes them directly.
Chapter 8 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) puts the general theory of the preceding chapters to work on concrete functions. Power series are differentiated term by term; the exponential function is defined by its series and the trigonometric functions and the number are extracted from it; the fundamental theorem of algebra is proved; Fourier series are introduced through general orthonormal systems; and the Gamma function is characterized by log-convexity.
The chapter's capstone is Parseval's theorem (Theorem 8.16): for Riemann-integrable -periodic functions, the Fourier series converges in the mean square sense and the inner product is computed by the (absolutely convergent) sum of products of Fourier coefficients. It is the statement that the trigonometric system is not merely orthonormal but complete, and it is the finite-dimensional Pythagorean theorem carried to infinite dimensions.
This mission is the eighth in a series formalizing Rudin Chapters 1–11; it uses the convergence tests of Mission III and the uniform-convergence and approximation theorems of Mission VII, and it is the analytic counterpart of the abstract theory of Mission XI.
A power series is ; by Chapter 3 it converges on an interval . A sequence of complex functions on is an orthonormal system if for and ; the Fourier coefficients of relative to it are , and the Fourier series is . For the trigonometric system on one writes
A trigonometric polynomial is a finite sum . The Gamma function is for .
For Riemann-integrable -periodic and with Fourier coefficients and :
Parseval's theorem is the completeness statement for the trigonometric system: Bessel's inequality (8.12) holds for every orthonormal system, and equality for all is exactly what distinguishes a complete system. The proof shows how the pieces of the book fit together: it uses the approximation theorem 8.15 (itself a corollary of Stone–Weierstrass from Chapter 7), the minimizing property 8.11, and the Schwarz inequality of Chapter 1. Chapter 11 generalizes the conclusion to arbitrary complete orthonormal systems in , where the Riemann-integrable hypothesis can be dropped.
The other milestones are where the elementary functions acquire their properties: the -periodicity of the complex exponential, the definition of as twice the first positive zero of the cosine, and the log-convexity characterization of the Gamma function are all established here rather than assumed.
Mathlib has the exponential and trigonometric functions, , the fundamental theorem of algebra, the Gamma function with the Bohr–Mollerup theorem, and a Fourier theory on the additive circle. The work in this mission is to state Rudin's versions — -periodic functions on , generic orthonormal systems on an interval, Riemann-integrable rather than square-integrable hypotheses — and connect them to that library.
Parseval's theorem is where an approximation argument in the uniform norm has to be converted into one in the mean square norm. The chain is: approximate in by a continuous periodic (a nontrivial step for a merely Riemann-integrable , and the place where the hypothesis is really used), approximate uniformly by a trigonometric polynomial , and then use the minimizing property of the partial sums to conclude is small. The first step has no analogue in the uniform theory and is the main obstacle; the third depends on being an orthogonal projection, which is Theorem 8.11.
Conventions fixed by this mission:
∫ x in a..b, f x, not the real-valued Riemann–Stieltjes integral built in Mission VI; for
the Riemann-integrable integrands of this chapter the two agree. Integrability hypotheses are
stated as IntervalIntegrable.Rudin.fourierCoeff, Rudin.fourierPartialSum, Rudin.L2Norm,
Rudin.IsTrigPolynomial, Rudin.HasPeriodTwoPi, and, for general systems,
Rudin.IsOrthonormalSystem and Rudin.genFourierCoeff, all following Rudin's normalizations
(in particular the in and in ).Rudin.SeriesConvergesTo from Mission III, so that conditional
convergence is expressible; the two-sided sums of Parseval are
stated as limits of the symmetric partial sums , as in Rudin.Chapter 10 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) builds the calculus of differential forms in and proves the theorem that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the Green, divergence and classical Stokes theorems all say the same thing — that integrating a derivative over a region is the same as integrating the original object over the boundary of that region — and Stokes' theorem (Theorem 10.33),
is that statement, once "region" is made precise as a chain of parametrized surfaces and "derivative" as the exterior derivative.
This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse function theorem and the several-variable calculus of Mission IX.
For an open , a -surface in is a -mapping from a parameter domain — a -cell or the standard simplex — into ; surfaces are maps, not point sets. A -form in is a formal sum
with continuous coefficients, whose meaning is the rule assigning to each -surface the number
The exterior derivative of is the -form with coefficients ; the pullback along a differentiable substitutes into the coefficients and the differentials. A -chain is a formal integer combination of -surfaces with parameter domain , its integral is the corresponding combination of integrals, and its boundary is obtained from the alternating sum of the faces of .
If is a -chain of class in an open and is a -form of class in , then
For this is the fundamental theorem of calculus, for Green's theorem, for the divergence theorem, and for , the theorem of Stokes.
Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that and are adjoint, which is also the starting point of de Rham cohomology. Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form being exact disappears, so the failure of exactness measures the shape of the domain. The change of variables theorem (10.9) is what makes integrals independent of the parametrization and is used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for passing from local to global statements.
Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their boundaries, nor a version of Stokes' theorem for such chains. This mission builds that apparatus and states the chapter's theorems for it; the definitions are reusable for any development that wants a hands-on, coordinate-based treatment of forms.
This is the most demanding mission of the series, for two reasons. First, the objects have to be set up before anything can be said: forms as coefficient families, their integrals as Jacobian integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved by reducing to a single oriented simplex, transporting along the parametrization by Theorem 10.25, and then computing the integral over by an iterated integral in which all but two terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the face maps right, and it is where a formalization will spend its time.
A further subtlety: with forms presented by coefficients indexed by all index tuples, the identity is false coefficient-wise and true as an identity of forms. Since Rudin defines a form to be its integration functional, statements of the shape "this form vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20, 10.22(c) and 10.39 are stated here.
Conventions fixed by this mission:
Fin n → ℝ. A -form is Rudin.KForm k n, a coefficient
function indexed by all tuples Fin k → Fin n, following Rudin's equation (34).Rudin.integralOverCell and Rudin.integralOverSimplex are Rudin's equation (35) for the two
admissible parameter domains, with Rudin.jacobian the determinant of the matrix of partial
derivatives. The integral over the parameter domain is the Lebesgue integral for the volume
measure, which agrees with Rudin's Riemann integral for continuous integrands.Rudin.extDeriv and Rudin.pullback are the exterior derivative and the pullback;
Rudin.Chain, Rudin.Chain.integral and Rudin.Chain.boundary are chains with integer
multiplicities, their integrals, and the boundary built from the faces of the standard simplex
with Rudin's signs .ContDiff ℝ 1 and ContDiff ℝ 2 for Rudin's and .Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are especially welcome, since they are exactly the lemmas the goal theorem consumes.
Chapter 5 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is the differential calculus of one real variable, developed from the definition of the derivative as a limit of difference quotients. Its organizing result is the mean value theorem and the family of consequences that follow from it: monotonicity criteria, L'Hospital's rule, and — the chapter's capstone — Taylor's theorem (Theorem 5.15), which approximates a function by a polynomial of degree and expresses the error exactly as a single -th derivative evaluated at an unspecified intermediate point.
Taylor's theorem is what makes differentiability quantitatively useful. It is the tool that turns local smoothness into explicit error bounds, and the estimates of Chapter 8 for the exponential, trigonometric and Gamma functions all rest on it.
This mission is the fifth in a series formalizing Rudin Chapters 1–11; it uses the continuity and compactness results of Mission IV.
Let be real-valued on . For the derivative is
whenever the limit exists. Higher derivatives are defined by iteration; exists on a set only if exists in a neighbourhood of each of its points. has a local maximum at if for all near .
Given a positive integer and a point , the Taylor polynomial of at of degree is
Let be continuous on , let exist for , and let be points of . Then there is a point strictly between and such that
For this is exactly the mean value theorem.
The mean value theorem converts a hypothesis about derivatives into a statement about increments, and everything in the chapter is an application of that conversion. Monotonicity criteria (5.11) are the basis of every "the function is increasing, hence injective" argument, including the change of variable in Chapter 6. Darboux's theorem (5.12) shows that derivatives, though not necessarily continuous, cannot have simple discontinuities — a fact that is easy to state and impossible to guess from the definition. Theorem 5.19 is the form of the mean value theorem that survives for vector-valued functions: the equality is lost (there need be no single point where the vector increment is proportional to the derivative), and only the inequality remains; the same phenomenon dictates the statements of Chapter 9.
Mathlib contains the mean value theorem, L'Hospital's rule, and a Taylor theorem with various remainder forms. The value of this mission is a statement of Taylor's theorem in Rudin's exact formulation — arbitrary distinct endpoints in , hypotheses only on and , an intermediate point strictly between them — and the derivation of the chapter's other results in a form the later missions can quote.
Taylor's theorem is proved by choosing the constant so that and applying Rolle's theorem times to ; the bookkeeping is in tracking that for and that each application produces a new intermediate point strictly inside the previous interval. In a proof assistant the iteration is the awkward part: the induction is on with the interval shrinking, and the statement must be general enough in and (either order) for the inductive step to apply. The hypothesis that exists only on the open interval, while is merely continuous on the closed one, must be preserved — strengthening it to on would make the statement weaker than Rudin's.
Conventions fixed by this mission:
deriv and iteratedDeriv, which are total functions returning
0 where the function is not differentiable; every statement therefore carries explicit
differentiability hypotheses exactly where Rudin states them.Set.Icc a b and Set.Ioo a b, and "for some between and
" is stated as an explicit disjunction, since the goal does not assume
.EuclideanSpace ℝ (Fin k), and the conclusion
is the inequality, not an equality — the equality version is false, as Rudin notes.A reservoir computer learns a dynamical input/output relation with a recurrent network whose internal weights are fixed once and never trained; only a linear readout on the state is fitted. The method works in practice — it is a standard tool for learning chaotic dynamics — but its justification requires an approximation theorem: the family of reservoirs used must be rich enough to reach any reasonable target system.
The target class is fixed by fading memory, the continuity notion Boyd and Chua introduced in 1985 for the approximation of nonlinear operators: a filter has fading memory when inputs that agree on the recent past produce nearby present outputs, however much they differ long ago. The question is then which reservoir families are dense in that class.
Non-homogeneous state-affine systems are the family that answers it. They are affine in the state, with coefficients depending polynomially on the input, and the density result proved for them is what every later universality theorem for reservoir computing rests on — including the one for echo state networks, whose proof approximates a target filter by a state-affine system first and only then by a network.
Timeline.
Time is indexed by the nonpositive integers, so an input has an infinite past and a present. Inputs are real-valued and bounded by one: the set of sequences with .
A non-homogeneous state-affine system is the reservoir
where is a polynomial with matrix coefficients, a polynomial with -vector coefficients, and the linear readout. Writing , the system is affine in the state and polynomial in the input.
Two constants govern it: and . When the state map contracts, the system has the echo state property — exactly one bounded state sequence per input — and the states obey . The induced map from input history to present output is the SAS functional .
Any fading memory filter on uniformly bounded scalar inputs is approximated, uniformly over all such inputs, by a state-affine system read out linearly.
The result itself. It is the density theorem of reservoir computing. Without it, nothing guarantees that a reservoir family can represent the system one is trying to learn, and the practice of fitting only a linear readout has no theoretical backing. It is also the input to the universality theorem for echo state networks: that proof replaces the target filter by a state-affine system before replacing it by a network, so the present result is a prerequisite rather than a parallel statement.
Formalizing it. The supporting target is a specialization of a result already published on this platform: a state-affine system is a contracting reservoir map, so its echo state property follows from the abstract contraction theorem rather than from a new argument. What this mission adds beyond that is the density statement itself, which is of a different nature — an approximation theorem in a function space, not a fixed point argument.
The obvious approach to the goal is to exhibit an approximating system directly, and it fails: the target is an arbitrary fading memory filter, given by no formula, so no construction can be read off it. The proof is not constructive in that sense. It proceeds instead by showing that the family of SAS functionals is a polynomial algebra which separates points and contains the constants, and by applying a Stone-Weierstrass argument on a space of input sequences made compact by the weighted topology.
Two points resist. The compactness is not that of the supremum norm — the space of uniformly bounded sequences is not compact for it — but of the weighted norm, and it is that topology in which the approximation is obtained. And the algebra property is delicate: the product of two SAS functionals must again be one, which is what forces the non-homogeneous form. The corresponding statement fails for linear reservoirs, whose products leave the family.
Time is indexed by , index denoting the instant steps into the past and the present; the system equation reads . This is a relabelling of the source's indexing, not a weakening.
Inputs are scalar, as in the source's Section 3, where the restriction is made explicit and the multidimensional extension deferred to a remark. Polynomials are given by their coefficient families, and evaluated as ; the bounds and are stated as explicit operator and norm bounds valid on rather than through a maximum, so that any valid bound may be supplied.
The fading memory property of the target is the one already published on this platform, stated for a functional rather than a filter: the two are in linear bijection, so nothing is lost and causality and time-invariance need not be formalized separately.
One trivialization is ruled out. The goal quantifies over state sequences satisfying the system equation, and the supporting target is what guarantees such a sequence exists and is unique under the stated bounds; without it, the approximation claim could be read as vacuous.
A complete development needs the Stone-Weierstrass theorem, available in Mathlib, together with compactness of the weighted sequence space, which is not and has to be built. Contributions are welcome on both targets.
How short can a code for a data source be, if the code must still be uniquely decodable — if every string of concatenated codewords can be unambiguously split back into the original symbols? Shannon's 1948 source coding theorem answers this exactly: the entropy of the source is a hard lower bound on the average codeword length of any uniquely decodable code, and it is also achievable up to a one-symbol slack. Entropy is not just a measure of "average surprise" — it is the literal, tight answer to a combinatorial question about how densely symbols can be packed into strings without losing decodability. This is the theorem that gives Shannon's entropy its operational meaning, and it underlies every practical lossless compression scheme (Huffman coding, arithmetic coding, Lempel–Ziv) as the benchmark they approach.
Timeline.
A source has a finite alphabet of symbols , with at least two symbols, and probability distribution (, ). A code assigns to each symbol a codeword , a finite string over a -ary code alphabet (); the code is uniquely decodable if every finite sequence of codewords is determined by its concatenation. The entropy of in base is
The expected codeword length of under is .
(For a source with symbols — see Formalization scope for why the single-symbol case must be excluded.)
The result itself. This theorem is the reason entropy is called entropy in an information-theoretic sense at all: it converts a quantity defined by an abstract formula () into the exact answer to an operational question (minimum achievable expected code length), with a slack no worse than one symbol. It is the founding theorem of lossless source coding and the benchmark every practical compressor is measured against.
Formalizing it. Mathlib recently gained genuine information-theoretic coding content: InformationTheory.UniquelyDecodable and the necessity direction of the Kraft–McMillan inequality (McMillan's 1956 result: a uniquely decodable code's lengths satisfy ) are already proved, via a counting argument on concatenations of codewords. This mission builds directly on that foundation rather than duplicating it. What Mathlib does not have — and what this mission's milestones supply — is Kraft's original 1949 sufficiency direction (existence of a uniquely decodable code realizing any length assignment satisfying the Kraft sum bound), any notion of Shannon entropy for a general finite distribution, and the source coding theorem itself.
The lower bound () is the easier half: it follows from the Kraft–McMillan inequality (already in Mathlib) via Gibbs'/Jensen's inequality applied to the two probability-like sequences and (where is the Kraft sum) — a short, self-contained convexity argument.
The achievability half is the genuine construction. Given the ideal (generally non-integer) lengths , one rounds up to (Shannon–Fano–Elias lengths); a one-line estimate shows , so the Kraft sum of the rounded lengths is still , and the bound gives immediately once a code with exactly these lengths is shown to exist. Producing that code is Kraft's sufficiency direction, and it needs an explicit construction: order the lengths, and assign to symbol the first digits of the -ary expansion of the cumulative sum . Verifying this assignment is injective, has the prescribed lengths, and is uniquely decodable (indeed prefix-free) is a careful but standard combinatorial argument — the main open piece of this mission.
The source alphabet must have at least two symbols (), not merely be nonempty. A single-symbol source forces and entropy , so the achievability conjunct would demand a codeword of length — but a uniquely decodable code can never contain the empty codeword (InformationTheory.UniquelyDecodable.epsilon_not_mem, provable from the definition: the empty string decodes ambiguously as zero or two copies of itself), so no admissible code exists and the theorem would be false, not merely hard, at . The same defect breaks Kraft's sufficiency direction (Milestone 2) whenever any prescribed length is , independent of ; that milestone accordingly requires every length strictly positive. With and full support, every strictly, so the Shannon–Fano lengths are automatically all , and the achievability construction only ever needs Milestone 2 at positive lengths. The code alphabet is likewise an arbitrary finite type (matching Mathlib's own Fintype/Nonempty conventions for the Kraft–McMillan file), with required to keep Real.logb non-degenerate. The source distribution is required strictly positive () — the standard simplifying assumption (zero-probability symbols can always be dropped without loss). Unique decodability is stated exactly as Mathlib's InformationTheory.UniquelyDecodable, not re-derived from a "prefix code" definition, so the mission's results transport directly onto Mathlib's existing Kraft–McMillan file. A trivializing route to rule out: proving only the lower bound (citing Mathlib's inequality) while leaving the existential achievability half unaddressed would not be Shannon's theorem — the sandwich is the theorem's actual content, and the lower bound alone (already essentially free from Mathlib) is not a novel contribution on its own.
Reusable output: the Kraft sufficiency construction (Milestone 2) is directly reusable for any future formalization of Huffman coding optimality, arithmetic coding, or the general "Kraft-inequality-achieving code exists" fact used throughout coding theory. Contributions are welcome starting from Milestone 2 (the open construction) or Milestone 3 (the Gibbs'-inequality lower bound, which only needs Milestone 1, already available via Mathlib).
Mathlib.InformationTheory.Coding.UniquelyDecodable and Mathlib.InformationTheory.Coding.KraftMcMillan (2026).The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.
Linear dynamics and measurements
with quadratic cost , , . The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history to ; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).
— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).
This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.
The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.
Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).
Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.
A finite directed graph with arc set , real arc lengths , origin and destination (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).
The algorithm state (BertsekasLCState) carries labels , the scalar UPPER, and the candidate list OPEN. Initially , all other labels , UPPER , OPEN . One iteration (BertsekasLCStep, nondeterministic): remove any from OPEN; for each child of in any order, if set , and put in OPEN if , or update UPPER if . The algorithm terminates when OPEN is empty.
for every execution, under the nonnegative arc length assumption of §2.3 ( for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from , which needs neither (label_correcting_invariant).
The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test , and with a negative arc a longer prefix can still reach more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample , , , , (a graph with no cycles at all), where the algorithm terminates with while the shortest distance is . Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.
Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.
Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.
Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.
The fundamental group is the first algebraic invariant a student of topology meets, and is the first computation of it that carries real content. Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; freely available at pi.math.cornell.edu/~hatcher/AT/AT.pdf) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).
This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace Hatcher.
A path in a topological space is a continuous map , where . A homotopy of paths is a family , , such that the endpoints and are independent of and the associated map , , is continuous. A loop at a basepoint is a path with . The set of homotopy classes of loops at is the fundamental group ; its product is , where traverses and then , each at double speed (Hatcher, Proposition 1.3).
The circle is realised as the unit circle of , so the point is and the basepoint is . Hatcher's map
is Hatcher.circleCover. The loops
based at are Hatcher.omegaLoopN n, and is Hatcher.omegaLoop; its class is Hatcher.omegaClass.
A covering space of is a space together with a map such that every has an open neighbourhood for which is a disjoint union of open sets each mapped homeomorphically onto by (Hatcher's condition , p. 29; such a is evenly covered). A lift of a map is a map with .
is an infinite cyclic group generated by . In the form stated in Lean:
Surjectivity of says generates; uniqueness of says the group is infinite cyclic rather than finite.
The result itself. The computation assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.
Formalizing it. Mathlib (revision 0df444a) already contains the covering-space infrastructure: IsCoveringMap, path lifting (IsCoveringMap.liftPath, eq_liftPath_iff'), homotopy lifting (IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff'), monodromy, and the fact that Circle.exp is a covering map (Circle.isCoveringMap_exp). It also has FundamentalGroup X x as the endomorphism group of the fundamental groupoid. It does not contain the computation , nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as Complex.exists_root (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.
The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because is discontinuous on ; the integer has to be produced by lifting the loop through and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of : this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.
Connecting the concrete loops to Mathlib's abstract is its own obstacle. FundamentalGroup Circle 1 multiplies by composing morphisms of the fundamental groupoid, so identifying with the class of the explicit loop (milestone 6) requires reparametrization arguments for concatenated paths, for negative as well as positive.
For Theorem 1.9 the difficulty is the construction and continuity of the retraction from a fixed-point-free map, and then the non-existence of a retraction, which uses that . For Theorem 1.10 Hatcher's proof lifts a loop through and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.
Circle (the unit circle in ) with basepoint 1; is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1; is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, with the antipodal point.IsCoveringMap p. This agrees with Hatcher's condition ; neither requires to be surjective.C(I, X) or Mathlib Paths; for homotopies of paths, the square is written I × I with Hatcher's coordinate order : the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is Y × I with an arbitrary topological space, as in Hatcher.FundamentalGroup Circle 1, and is FundamentalGroup.fromPath ⟦omegaLoop⟧. Because the goal quantifies over integer powers of a single element, the order of multiplication in FundamentalGroup is immaterial to its truth.FundamentalGroup Circle 1 ≃* Multiplicative ℤ sending to is an immediate corollary and a welcome contribution.0 < f.degree, which excludes both the zero polynomial and nonzero constants.Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism packaged for reuse, and any lemma about concatenation and reparametrization of loops in Circle that later chapters of the series can import.
Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting for covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.leanMathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (the fundamental group). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.leanThe strategic-form game is the basic object of noncooperative game theory, and the Nash equilibrium — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium (Nash, Non-cooperative games, Ann. Math. 54 (1951)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).
A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.
A finite strategic-form game consists of a finite set of players, for each player a finite nonempty set of pure strategies, and for each player a payoff function ; all players are utility maximizers. A mixed strategy for player is a probability distribution on , represented as a weight function with and (a lottery). Players randomize independently, so a mixed profile induces the product distribution on pure strategy vectors, and player 's expected payoff is
A mixed profile is a (mixed) Nash equilibrium if for every player and every lottery on , replacing by does not increase .
A two-person zero-sum game is given by a matrix : the row player picks a row distribution , the column player a column distribution , and the column player pays the row player in expectation.
The market of §1.8.1 of the source has finitely many divisible goods, good in units, and finitely many buyers, buyer bringing budget and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. Market-clearing prices are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.
Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.
Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.
of the explicit two-player game with payoffs to the row player and to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.
The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.
The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (IsLottery, IsMixedProfile, expectedPayoff, IsMixedNash) from this mission.
Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.
The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.
Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (Mathlib.Topology.Sion) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.
Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into ; mixed strategies are weight functions with a IsLottery predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (Fin (m+1), Fin (n+1)), payoffs flow from the column player to the row player, stdSimplex plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by matrixGameStrat/zeroSumPayoff/matrixGameProfile from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is with no division anywhere.
Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).
The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound means that, over the field under consideration, matrices can be multiplied using arithmetic operations for every . Improvements to are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.
The existing Prove2Me mission formalizes Schönhage's bound from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; Romani recorded its tensor form and the parameter choice , , which gives . Schönhage's 1981 paper reports the equivalent bound in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality .
For a field , the matrix-multiplication tensor encodes multiplication of an matrix by a matrix:
A direct sum places several such tensors in disjoint coordinate blocks. A tensor has border rank at most when it is a polynomial degeneration of the diagonal tensor . In the Lean development this relation is Degenerates T (TensorObj.diagObj K 3 r). The argument order matters: the first tensor is the target and the diagonal tensor is the source.
The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent matMulExp K, the equivalent Strassen-preorder exponent matMulExp_strassen K, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of is introduced.
The goal has exactly the same quantified proposition as the existing mission, with only the rational endpoint changed:
The source construction to be formalized is
Each summand has volume :
The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication
and the resulting Strassen-form exponent bound. The public goal then transfers the bound to matMulExp K through the already established equality of the two exponent definitions.
Mathematically, this construction improves the concrete exponent certified by the existing mission from to without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.
For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.
The theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.
The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.
Romani's published summary states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's TensorObj.bigAdd coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.
All theorems quantify over an arbitrary type with [Field K], matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by MMObj; the three products are combined with TensorObj.bigAdd. Border rank is represented by the existing finitely supported polynomial-family predicate Degenerates. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.
The mission includes no placeholder laser-value definition and makes no claim about the later analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond . A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of matMulExp is outside scope.
Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the , witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.
The coupling method of Mission III asks for a coupling of two copies of a chain from every pair of starting states — often painful to construct globally. Chapter 14 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) replaces that global demand by a local one. The path coupling technique of Bubley and Dyer says: put a connected graph structure on the state space, and couple one step of the chain only across edges; if each edge contracts in expectation, contraction propagates automatically along paths to arbitrary pairs of distributions. The bookkeeping runs through the transportation metric (Kantorovich distance) between distributions, whose theory — attainment by an optimal coupling, the triangle inequality — is developed on the way. The chapter's payoff is the sharpest elementary bound for sampling proper colorings (Theorem 14.8: the Glauber dynamics mixes in steps once ), and, through the sampling-to-counting reduction of Jerrum–Valiant–Vazirani, a polynomial-time approximation algorithm for counting colorings — the paradigm of the Markov chain Monte Carlo method as an algorithmic tool.
All chains live on a finite state space with a transition matrix ; is the time- distribution from , the total variation distance, the worst-case distance to the stationary distribution , and the mixing time. A coupling of distributions is a distribution on with marginals and .
Given a metric-like cost on pairs of states, the transportation metric between two distributions is the cheapest expected cost of moving one onto the other:
Given a connected graph structure on the state space with edge lengths , the path metric is the least total length of a -path from to .
For the colorings application: a -coloring of the vertices of a graph is proper when adjacent vertices receive distinct colors, and the Glauber dynamics on proper colorings picks a uniform vertex and re-samples its color uniformly among the colors legal there; its stationary distribution is uniform on the proper colorings. Throughout, is the number of vertices and the maximum degree of the graph being colored.
Theorem 14.8, the capstone of Chapter 14: for the Glauber dynamics on proper -colorings, if then
The results. Path coupling converted the coupling method from an art into a calculus: one bounds a single-edge contraction constant, and the machinery does the rest. It is the standard tool for Glauber dynamics on colorings, independent sets, and other constraint-satisfaction models, and the colorings bound is its flagship application. Theorem 14.12 is the discrete embodiment of the Jerrum–Valiant–Vazirani equivalence between approximate counting and sampling — the conceptual foundation of the entire MCMC approach to -hard counting problems.
Formalizing them. Mathlib has no transportation/Kantorovich metric in the finite setting, no path coupling, and nothing on approximate counting. The transportation-metric layer (optimal couplings, triangle inequality) is reusable far beyond this mission — it is the finite Wasserstein distance. The path-coupling theorem feeds directly into Mission IX (Ising) and is quoted throughout modern mixing literature.
The transportation metric asks for minimization over the (compact) polytope of couplings: attainment is a finite-dimensional compactness argument, and the triangle inequality requires gluing two optimal couplings along their common marginal — the classic construction that must be carried out with explicit finite sums here. Path coupling itself is an induction along geodesics of the path metric, with the subtlety that the composite coupling produced along a path need not be optimal, only admissible; the bookkeeping of the contraction constant through the induction is exactly the kind of argument Lean keeps honest. Theorem 14.8 instantiates the machinery: the single-edge coupling for colorings needs a careful case analysis of the proposed recolorings at the two endpoints (matching legal colors bijectively), and the contraction constant emerges from counting disagreeing proposals. Theorem 14.12 layers a probabilistic-amplification argument (medians of means over independent runs) on top of the mixing bound; its combinatorial core — expressing as a telescoping product of marginal probabilities — is elementary but notation-heavy, and the formal statement quantifies over explicit seed spaces, so the whole estimator is a finite object.
The transportation metric is an sInf over coupling costs (the coupling polytope is nonempty for genuine distributions, and attainment is part of the milestone, so the junk value never propagates); the path metric is an sInf over walk lengths in a connected graph. The Glauber dynamics on colorings is the restriction to proper colorings of the single-site heat-bath chain of Mission II, matching §3.3 of the book; its state space is the subtype of proper colorings, nonempty whenever (a fact the hypotheses of the goal supply). Mixing-time upper bounds are stated with the book's explicit ceilings, so no rounding slack is hidden. In Theorem 14.12 the estimator is presented concretely as a function of finitely many uniform seeds, and "with probability " is a counting inequality over the seed space — no measure theory enters. Contributions of intermediate lemmas (optimal-coupling gluing, geodesic decompositions, colorings edge-coupling) are welcome and will be reused by Mission IX.
A reversible Markov chain is an electrical network: states are nodes, and the conductance turns hitting probabilities into voltages and hitting times into resistances. This dictionary, going back to Kakutani and popularized by Doyle and Snell, converts probabilistic estimates into the physical laws of circuits — series/parallel reduction, energy minimization, monotonicity under edge removal. Chapters 9–11 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the dictionary and its two crown results: the commute time identity of Chandra–Raghavan–Ruzzo–Smolensky–Tiwari, , and the Matthews method bounding cover times by hitting times with harmonic-number precision.
A network is a symmetric nonnegative conductance function on pairs of vertices; the associated walk moves with probabilities
where , and . A function is harmonic at if . The voltage with boundary values at and at is , the harmonic extension of its boundary data; the current flowing out of has strength , and the effective resistance is . A flow from to is an antisymmetric edge function obeying the node law off ; its energy is . Hitting times , their expectations, the Green's function , the maximal hitting time , and the cover time (expected time to visit every state, maximized over starts) all use the trajectory calculus of Mission I.
This is Proposition 10.6, the commute time identity — the exact bridge between the probabilistic and electrical sides, and the engine of the transience/recurrence theory of Mission XII.
Reversibility and stationarity of the network walk with (§9.1); Proposition 9.1 (existence and uniqueness of harmonic extensions with given boundary values, ); Lemma 9.6 (the Green's function identity ); Theorem 9.10 (Thomson's principle: is the minimal energy of a unit flow, attained); Theorem 9.12 (Rayleigh monotonicity: lowering conductances raises effective resistance); Lemma 10.1 (the random target lemma: does not depend on ); Corollary 10.8 (the resistance triangle inequality); Theorem 11.2 (Matthews: ); Proposition 11.4 (the matching Matthews lower bound over subsets).
The results. The commute time identity computes hitting times from circuit reductions — this is how hitting times on trees, tori and glued graphs are actually evaluated — and, through Thomson and Rayleigh, makes them monotone under graph operations, something invisible probabilistically. The Matthews bounds pin cover times up to a factor in complete generality; they are the tool behind cover-time results for lamplighter groups in Mission XI's sequel. Green's function identities feed Mission XII's recurrence theory, where decides transience.
Formalizing them. Mathlib has graph Laplacians but no electrical network theory: no effective resistance, no flows, no energy, no Thomson/Rayleigh, no hitting or cover times. This mission publishes that layer over the trajectory calculus of Mission I. It is the most reusable single block of the series outside Missions I–II: effective resistance on finite networks is of independent interest to combinatorics (spanning trees, spectral sparsification) well beyond mixing times.
The identity chain behind the goal runs: Green's function of the stopped walk escape probability (via harmonic uniqueness) the Aldous–Fill occupation identity for stopping times with — each step is a manipulation of infinite series of trajectory sums whose exchange steps (splitting a path at its first visit, last-exit decompositions) need summability from Mission I's Lemma 1.13. Thomson's principle is a finite-dimensional convex minimization: existence of the minimizer needs a compactness or completing-the-square argument, and the identification of the minimizer with the current flow needs the cycle law; the naive "differentiate the energy" route must be made exact. Matthews' method is a clean but genuinely clever argument — a uniformly random ordering of targets and the harmonic-number telescoping; the formal cost is the exchangeability of the randomized order against the chain, handled combinatorially.
Networks are functions with a symmetry-and-nonnegativity predicate; loops are permitted; connectivity enters as irreducibility of the induced walk. The voltage is defined probabilistically as (the book's harmonic characterization is Proposition 9.1); is the reciprocal of the explicit current strength, with total division junk when are disconnected — statements carry irreducibility so this does not arise. Energy counts each undirected edge once, formalized as half the ordered double sum, and handles absent edges. Cover times are tail sums of the explicit event "some state unvisited". The Matthews lower bound is stated with an arbitrary lower bound for the pairwise hitting times of the subset — equivalent to the book's min over pairs and easier to instantiate.
Welcome contributions: series/parallel reduction laws, the cycle and node law API for flows, escape-probability lemmas — all reused in Mission XII's infinite-network arguments.
Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.
Finite Markov chains are the basic model for memoryless random dynamics: card shuffles, random walks on graphs and groups, Monte Carlo samplers, and queueing systems are all chains on a finite state space. The single most used fact about them is that an irreducible chain has exactly one stationary distribution — a probability vector with — and that this is strictly positive and encodes the long-run behaviour of the chain through the return-time identity . Every later result in the theory of mixing times (convergence theorems, coupling bounds, spectral methods, cutoff) is a statement about the distance of the chain from this , so nothing in the subject can be formalized before this mission is.
This mission is the first in a series formalizing D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times (AMS, 2009), covering Chapters 1–2: the basic vocabulary of finite chains (stochastic matrices, irreducibility, period, reversibility, time reversal, random walks on graphs and groups) and the classical examples of Chapter 2 (gambler's ruin, coupon collecting, the reflection principle for simple random walk on ). Later missions in the series build on the definitions published here.
A chain on a finite state space is presented by its transition matrix, a matrix with nonnegative entries whose rows sum to . A distribution is a row vector with nonnegative entries summing to ; one step of the chain carries to , and the -step transition probabilities are the entries of the matrix power .
The chain is irreducible if for all states there is a with . The period of a state is where , and the chain is aperiodic if every state has period . A distribution is stationary if , and and are in detailed balance (the chain is reversible) if for all .
Trajectory events over a finite horizon are finite sums of path weights: a length- trajectory is a function , with weight conditional on its starting state. The tail probability of the first hitting time is the sum of the weights of the trajectories from that avoid at times , and expectations of hitting times are recovered by the tail-sum formula , formalized as a tsum over .
This is Corollary 1.17 of the book. It asserts only existence and uniqueness, leaving the finer structure of to the milestones; it is the weakest statement on which the rest of the series can stand, which is why it is the goal.
The milestone list follows the book's own route: well-definedness of the period (Lemma 1.6), positivity of some matrix power for irreducible aperiodic chains (Proposition 1.7), finiteness of expected hitting times (Lemma 1.13), existence of a positive stationary distribution together with
(Proposition 1.14), constancy of harmonic functions (Lemma 1.16), stationarity from detailed balance (Proposition 1.19), the stationary and reversible measure of simple random walk on a graph (Examples 1.12 and 1.20), the time reversal and its path-reversal identity (Proposition 1.22), and the random walks on finite groups of Section 2.6 (Propositions 2.12–2.14). From Chapter 2 the list adds the gambler's ruin formulas and (Proposition 2.1), the coupon collector expectation and tail bound (Propositions 2.3 and 2.4), and the reflection principle and the bound for simple random walk on (Lemma 2.18 and Theorem 2.17).
The result itself. Existence and uniqueness of is the pivot on which the entire quantitative theory turns: it defines the target of convergence, and the identity ties the stationary measure to return times, which later missions use for hitting-time and cover-time results. Detailed balance is the practical tool by which stationary measures of graph and group walks are computed, and the Chapter 2 examples (gambler's ruin, coupon collecting, reflection) are the standard building blocks reused throughout the book — the coupon collector bound, for instance, is exactly the estimate behind the analysis of the top-to-random shuffle in a later mission of this series.
Formalizing it. Mathlib currently has no theory of finite Markov chains: no stochastic-matrix predicate, no stationary distribution, no periodicity, no hitting times. Everything proved in this mission is new formal mathematics, and the definition layer published here (mm_basic, mm_path, mm_classical) is the shared foundation that all twelve subsequent missions of the series import. All results are classical and have textbook proofs; none has a machine-checked proof.
The delicate point is the existence proof. The natural first idea — extract from an eigenvector of for eigenvalue , or invoke a fixed-point theorem — either does not give positivity and nonnegativity without further work, or uses compactness machinery (Brouwer) that is unavailable. The book's proof instead builds and verifies by reindexing trajectory sums; formalizing it requires managing infinite series of path sums (summability from the geometric tail bound of Lemma 1.13, exchanging tsum with finite sums, splitting a trajectory at its last step). The uniqueness half is linear algebra via constancy of harmonic functions (Lemma 1.16), which is elementary but requires a maximum-principle argument over a finite state space. The reflection principle and Theorem 2.17 are finite combinatorics on paths — the bijection is easy to describe and fiddly to implement.
States form a Fintype with decidable equality; chains are Matrix V V ℝ with the row-stochasticity predicate IsStochastic; distributions are functions V → ℝ with the predicate IsDist. Everything is distribution-side: no probability space or measure theory is used. The period is formalized as , which equals when and takes the junk value otherwise. Expectations of hitting times are tsums of tail probabilities, with the usual junk value for non-summable families — the statements are arranged (e.g. multiplicatively, ) so that junk values cannot make them vacuously true. Existence statements carry a Nonempty V hypothesis; irreducibility on the empty space is vacuous, and without nonemptiness the goal would be false, not trivial. The coupon collector and the walk on are presented directly by their driving randomness (uniform draws Fin t → Fin n, uniform sign strings Fin r → Bool), so those probabilities are elementary counting; in particular the reflection principle is stated as an equality of cardinalities of sets of sign strings — this is equivalent to the probabilistic statement because all strings are equally likely.
Contributions welcome beyond the milestone list: simp lemmas for the definition layer, the taboo-matrix representation of avoidance probabilities (useful for Lemma 1.13), and any interface lemmas connecting pathWeight sums to matrix powers — these will be reused by every later mission in the series.
The classical convergence theory of smooth convex minimization. For a function that is -strongly convex and -smooth (), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a damped phase in which every backtracking step decreases the objective by a fixed amount , and a quadratically convergent phase in which the scaled gradient norm squares at each step, . Together they give the iteration count of B&V (9.36),
with the Lipschitz constant of the Hessian and the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.
The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.