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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The word chaos entered mathematics with a precise meaning, and Robert L. Devaney's An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003) is the text that fixed the meaning now used in most of the literature: a map is chaotic when it is unpredictable (sensitive dependence on initial conditions), indecomposable (topological transitivity), and nevertheless regular (dense periodic points). The book develops this definition on the simplest possible object — the real quadratic family on the unit interval — and shows that for large the map is chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.
This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8: the invariant set of the quadratic family, symbolic dynamics on the sequence space , topological conjugacy, and Devaney's definition of chaos. Everything later in the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets — is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the vocabulary of the whole series.
Write and let for a real parameter . Iterates are written , with the identity.
For the maximum value of exceeds , so some points of leave after one iteration. Let
so that is the set of points escaping from at the -st iteration. The set of points that never escape is
The complement consists of two closed intervals, to the left of the midpoint and to its right.
On the symbolic side, is the set of one-sided infinite sequences with , metrized by
and is the shift map . The itinerary of is the sequence with when and when .
Following Devaney, is topologically transitive if for every pair of open sets meeting there is with ; it has sensitive dependence on initial conditions if there is such that every point of has points of arbitrarily near it whose orbit eventually separates from its own by more than ; and it is chaotic on when it has sensitive dependence, is topologically transitive, and has a dense set of periodic points in .
The goal is Devaney's Example 8.8: for ,
The milestones are the results the book uses to get there, in the book's own order: the escape of orbits outside (Proposition 5.2), the tame regime (Proposition 5.3), the Cantor structure of (Theorem 5.6), the metric and dynamics of the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of on all of (Example 8.9).
The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic by producing a conjugacy with a shift. The conjugacy also gives quantitative information that is otherwise inaccessible — for example, that has exactly points fixed by , which no direct computation with the degree- polynomial delivers.
Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's three chaos conditions, the sequence space with its metric and shift, topological conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the foundation the rest of the book's series will import.
The obvious route to the goal — analyze on directly — fails, because has no explicit description: it is a nested intersection of intervals whose endpoints are not available in closed form. The whole argument therefore goes through the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which needs the nested-interval construction together with the fact that these intervals are nonempty and nested; and (ii) injectivity, which needs the hyperbolicity estimate on , valid exactly because , and the mean value theorem. The hypothesis is not cosmetic: Devaney notes the results hold for , but only with a more delicate argument.
The Lean development fixes the following conventions.
Set.ncard and are restricted to ; for every point is fixed by and the
claim would be false.Contributions of any kind are welcome: full proofs, reductions splitting a milestone into lemmas, and reusable lemmas about or about conjugacy that later missions in the series can import.
The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files
elaborate with no errors, the only warnings being the expected sorry placeholders in the
theorem bodies.
A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript Ideals in Balanced Algebras and the Genesis of Mathematics (A. Winkler, 2020) applies that pattern to a single primitive: a partial binary operation, an operation that need not be defined for every pair. Under one axiom — balance, which asserts that is defined exactly when is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.
No individual argument here is deep. What makes them worth machine-checking is that their content is definedness rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).
An algebra on a type is a partial binary operation: a rule assigning to some pairs a value . Write for " is defined". In the Lean development the operation is a total function , where the value means undefined. Nothing else is assumed: no totality, no unit, no associativity.
The vocabulary used throughout, all relative to this one partial product:
This is the statement that gives the manuscript its notion of society: the gregarious elements of an association form the gregarious ideal, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.
The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.
The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of quivered (the elements admitting a unit on one side form an ideal, §1), of cancellative (the non-cancellable elements form a prime ideal, §4) and of principal (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.
What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose Magma-style structures are total and whose Quiver/Category hierarchy starts from typed hom-families rather than a single partial product.
The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of " — fails at its first step, because from alone one cannot conclude ; that inference is exactly what the hypothesis " is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.
The partial product is A → A → Option A; none is undefined, and a · b = c is rendered as the product evaluating to some c. Subsets are Set A, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.
Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.
The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.
The Langlands program proposes that the arithmetic of number fields is encoded in the representation theory of reductive groups over their adele rings. Its conjectures — reciprocity and functoriality — are stated in the survey this mission formalizes, Gelbart 1984, only after a long preparatory part on the classical results they generalize, and it is that classical part (Part II of the survey) that admits precise formal statements today.
The classical engine is a theorem of Hecke (1936): a holomorphic function on the upper half-plane, given by a Fourier expansion in , transforms in a prescribed way under exactly when the Dirichlet series built from its Fourier coefficients continues analytically and satisfies a functional equation. One side of the equivalence is a symmetry of an analytic object on the upper half-plane; the other is an analytic property of a series assembled from arithmetic data. Gelbart presents this as the prototype of the "reciprocity" that the Langlands conjectures extend to and beyond.
Timeline of the material covered here.
Fix a sequence of complex numbers subject to the growth condition for some , a period , a weight , and a sign . Three objects are attached to this data.
Two conditions on this data are compared.
Condition (B) says that is automorphic of weight for the group of transformations generated by and ; invariance under is built into the Fourier expansion.
for every coefficient sequence of polynomial growth and all , . The goal fixes no particular group, no level and no arithmetic input: it is the general equivalence, from which the classical examples follow by specialization.
The milestone list follows the survey: the local-global principle of §II.A, the Riemann–theta computation that motivates Hecke's proof (§II.B.2, p. 187), the Mellin representation of , the two implications of Theorem 1 separately, and the Euler-product criterion of Theorem 2 (p. 189).
Hecke's theorem is what makes "this -function is automorphic" a checkable assertion: it converts a statement about analytic continuation and a functional equation — often the only handle one has on an arithmetically defined Dirichlet series — into the existence of an automorphic form with prescribed Fourier coefficients. Weil's converse theorem, the modularity of elliptic curves, and the automorphy criteria used throughout the Langlands program are descendants of this statement. Downstream of it sit the classical applications listed in the survey: the functional equations of and of Dirichlet -functions, and the identification of theta series of quadratic forms with modular forms.
Status. Hecke's theorem is a classical, fully proved result (Hecke 1936; a textbook treatment is
Ogg, Modular forms and Dirichlet series, Ch. 1). Hasse–Minkowski is likewise classical. Neither
has a formalization in Mathlib at the pinned revision: Mathlib supplies the completed Riemann
zeta function and its functional equation, the Jacobi theta transformation law, LSeries and its
abscissa theory, the Gamma function and the Mellin transform, and modular forms with
SlashAction, but no converse theorem and no local-global principle for quadratic forms. What
this mission produces is therefore new formal mathematics on top of an old result, not a
re-derivation of something already machine-checked.
The forward implication (B) (A) is Riemann's argument: split at , substitute in the lower piece, and use (B). The obstacle is not the algebra but the analysis that licenses it: exchanging the sum defining with the integral, controlling as , where the naive termwise bound diverges, and showing the result is entire and bounded on vertical strips rather than merely holomorphic on a half-plane.
The reverse implication (A) (B) is harder, and it is where the first idea fails: one cannot simply run the computation backwards, because the Mellin inversion integral converges only once boundedness in vertical strips is combined with Stirling decay of , and the contour shift that produces the terms needs both. Mathlib has the Mellin transform and an inversion theorem, under hypotheses that are not met verbatim here; supplying that bridge is the main work.
Conventions committed to in Lean, all of them invisible in the prose.
tsum over , so it takes the junk value where
the series fails to converge; every statement about is guarded by ,
and a separate item asserts summability there.LSeries, whose term is by definition, so never enters
the Dirichlet series — only the correction terms and .cpow; on the
upper half-plane has positive real part, so no branch ambiguity arises.No trivializing reading is available: condition (A) requires the entire function to agree with on , where is genuinely defined, so it is not satisfied by an arbitrary entire function; and the hypotheses of the goal are satisfiable — the Jacobi theta coefficients with , , are an instance, recorded as its own item.
A complete development needs: summability and holomorphy of -expansions of polynomial growth;
the Mellin transform of an exponentially decaying series; entirety and strip-boundedness of the
continued ; Mellin inversion with Stirling control of ; and, for the Euler-product
item, the passage from multiplicativity to an Euler product for LSeries. All of these are
reusable beyond this mission. Contributions to any single item are welcome; the two implications
of the goal are independently valuable and are listed as separate milestones for that reason.
In Esquisse d'un Programme (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a dessin d'enfant, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above , and , and that curve and map are defined over the field of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function , the action of is obtained simply by applying to the coefficients of and . Grothendieck states in §2 (p. 9) that the resulting outer action of on the profinite fundamental group of is faithful, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, On Galois extensions of a maximal cyclotomic field, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over is defined over a number field if and only if it admits a map to unramified outside ; the "only if" half is an explicit construction with polynomials over . Grothendieck (1984) drew the consequence that acts on dessins and asserted faithfulness of the action on . Lenstra, in an appendix to L. Schneps (ed.), The Grothendieck Theory of Dessins d'Enfants (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of plane trees, equivalently on Shabat polynomials. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
Work over , realized as the algebraic closure of , and write for its group of field automorphisms fixing pointwise.
A nonconstant polynomial over a field is a Belyi polynomial (classically a Shabat polynomial) when every critical value of lies in : for every with one has or . Over an algebraically closed field of characteristic zero this says exactly that , viewed as a degree- map , is unramified outside the fibres over , and . The associated dessin is the preimage , a plane tree with edges whose vertices are the points above and , with vertex orders equal to the multiplicities of the corresponding roots of and of .
Two Belyi polynomials define the same dessin exactly when they are affinely equivalent: for some and some . The target coordinate is already rigidified by the normalisation of the critical values to ; only the source coordinate remains free.
The group acts coefficientwise: is the polynomial obtained from by applying to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of : every nontrivial automorphism of is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that embeds into the outer automorphism group of .
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over and , so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all , and has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number , a tree whose isomorphism class remembers ; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
AlgebraicClosure ℚ, and is its group of -algebra automorphisms.Trivialization is ruled out as follows: the goal asserts the existence of a moved Belyi polynomial for each nontrivial , with the nondegeneracy 0 < deg P built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ( is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
The Riemann hypothesis asserts that every non-trivial zero of the Riemann zeta function lies on the line ; the simplicity hypothesis asserts in addition that every such zero is a simple zero of . Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.
Kawahira (2016) gives a reformulation of a different kind. He attaches to an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is equivalent to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the holomorphic index (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.
For a non-constant meromorphic , define the nu function
If is a zero of of order , then is a fixed point of with multiplier
and if is a pole of order the multiplier is . A fixed point of a holomorphic map is attracting if , indifferent if , and repelling if .
The holomorphic index of at a fixed point is
the integral being over a small positively oriented circle around . When the multiplier is not one has , and the Möbius map carries the unit disk onto the half-plane . So a fixed point is attracting, indifferent or repelling exactly according to whether is , or : the critical line reappears, in the index plane.
The point of the construction is that is engineered so that the index of at a simple zero of is itself (and at a zero of order ). Writing for : a non-trivial zero of order has index , so , and asking that this equal is asking for and .
The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function ), and Proposition 13 of the appendix (the Newton map , for which every zero of becomes an attracting fixed point — the contrast that explains why , and not , sees the critical line).
The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.
Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.
The obvious route to the goal — compute at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets for each non-trivial zero of order , which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair with , whose index is ; only the two inequalities together force and . A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip , that and are zeros of the same order, and that the trivial zeros and the pole at give repelling fixed points.
The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that has exactly one zero inside; the other genuinely analytic milestone is the order- computation of , where vanishes at the fixed point when and the singularity is removable rather than absent.
The development is over with Mathlib's riemannZeta. Conventions the Lean statements commit to:
Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of is known not to model the meromorphic map.
Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order — all stated for an arbitrary function analytic at the point, not for .
https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a gauge-invariant weight over the space of vector potentials (connections) of a principal bundle. The integrand is constant on the orbits of the group of gauge transformations, so the integral over diverges and one is supposed to integrate instead over the orbit space . The Faddeev–Popov procedure realizes this by fixing a gauge: choosing, continuously in the orbit, exactly one vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for potentials on (or ) with suitable conditions at infinity, the Coulomb gauge condition does not do this: the Coulomb slice through the zero potential meets the orbit of the zero potential again, far from the origin. These extra intersections are the Gribov copies; R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, Some Remarks on the Gribov Ambiguity (Commun. Math. Phys. 60 (1978) 7–12), showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity are those of Gribov — gauge transformations extending to the one-point compactification with value at infinity, so that the base manifold is or — then no continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space of irreducible connections is weakly contractible, while the gauge group is not, and a weakly contractible principal bundle admits no global continuous section.
Fix and take the structure group , the group of complex matrices with and , topologized as a subspace of matrices. Let denote the unit sphere of , with base point the north pole.
For the trivial -bundle over a space , a gauge transformation is a map , and the gauge group is
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects matter. The based gauge group is the subgroup of transformations that are the identity at the base point. The constant transformations with value in the centre of form a normal subgroup, and the reduced gauge group is the quotient
with the quotient topology. The centre acts trivially on vector potentials, so is the group that acts effectively.
A group acting continuously on a space has orbit space with the quotient topology, and a gauge fixing is a continuous map with , where is the projection: a continuous choice of exactly one point on each orbit. The action is principal when it is free and the division map, which sends a pair of points on one orbit to a group element carrying the second to the first, can be chosen continuously; this is the topological content of " is a principal -bundle". The space is weakly contractible when it is nonempty and all its homotopy groups vanish.
In the paper, is the affine space of connections, its set of irreducible members, and Theorems 1 and 2 say exactly that is a weakly contractible principal -space.
For , , and every weakly contractible principal -space :
By Theorems 1 and 2 of the paper the space of irreducible connections over or is such an , so the goal contains Singer's Corollary 4 for that space; it leaves the analytic construction of the space of connections unfixed, which is what makes it statable today.
The result rules out the existence of a global gauge in the topological sense: every gauge condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be read as a local statement, patched with a partition of unity over the orbit space (as the last section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks: homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for , and the classical computations , for , . Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned revision contains homotopy groups as a definition together with their group structure, but essentially no computation of them.
The naive approach to the goal — build a section by hand, or average over the group — fails because is neither compact nor contractible and the obstruction is global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no local argument can produce a contradiction. The proof has to convert a section into a homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the group as a retract of the total space, so all homotopy groups of the group would vanish; the work is then to show that some homotopy group of the reduced gauge group does not vanish, which needs the identification of the based gauge group with a mapping space, the exact sequences relating , and , and non-trivial homotopy groups of — including for the case of Theorem 3.
The formalization commits to the following conventions, all of them visible in the definitions of this mission.
HomotopyGroup, based at the identity element.Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is about what continuity gives once the domain is compact or connected. Three of its theorems are used in nearly every later argument of the book: a continuous function on a compact set has compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a connected set has connected image (4.22), hence takes intermediate values (4.23); and a continuous function on a compact metric space is uniformly continuous (Theorem 4.19) — the can be chosen independently of the point.
The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place where compactness upgrades a pointwise hypothesis into a global one with a quantitative conclusion.
This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric topology of Mission II and is a prerequisite for Missions V–VII.
Let be metric spaces, , , and let be a limit point of . Rudin writes when for every there is with for all satisfying ; the exclusion of is deliberate, and it is what makes the notion agree with continuity only when (Theorem 4.6). is continuous at if the same holds with the condition dropped, and continuous if it is continuous at every point.
is uniformly continuous on if for every there is a single such that for all with . A real function on is monotonically increasing if implies ; its one-sided limits are written and , and it has a discontinuity of the first kind at when both exist but do not agree with .
Uniform continuity is the hypothesis that converts local approximation into global approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the two existence theorems of elementary analysis, and both come from this chapter by combining Chapter 2's compactness and connectedness with continuity.
Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book where a countability argument (Chapter 2) pays off analytically.
Mathlib has continuity, compactness and connectedness in general topological spaces, and most
of the milestones can be matched to library results after the statements are put in Rudin's
metric form. The formalization value is again in the dictionary: Rudin's punctured-limit
definition versus ContinuousWithinAt, and his – uniform continuity versus
the library's uniformity-filter definition.
There is no single hard step; the difficulty is in the hypotheses being weaker than they look. In Theorem 4.6 the limit is taken through , so the equivalence with continuity genuinely needs and a limit point; dropping the second hypothesis makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick at each point by continuity and take the infimum — fails because the infimum over infinitely many points can be ; compactness is used to reduce to finitely many, and the factor of two in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the discontinuity set into , built from the gap between and .
Conventions fixed by this mission:
Continuous, ContinuousOn, ContinuousWithinAt; Rudin's
along is Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q).Rudin.UniformlyContinuous, stated with explicit and
as in Definition 4.18, rather than through the uniformity filter.Rudin.IsLimitPoint from the Chapter 2 mission, so the two missions share
one notion.[CompactSpace X], matching
Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is
the form later missions use.MonotoneOn f (Set.Ioo a b); one-sided limits are 𝓝[<] x and
𝓝[>] x filters, and 4.29 also identifies them with the supremum and infimum of the
corresponding one-sided images, as Rudin does.The goal is not vacuous and does not follow by unfolding: uniform continuity fails for continuous functions on non-compact domains (e.g. on , or on ), so compactness is doing the work.
Von Neumann introduced amenability in 1929 in response to the Banach–Tarski paradox: a group is amenable when it carries a finitely additive, translation-invariant probability measure on its subsets, and no amenable group contains a free subgroup of rank — which is exactly what the paradox needs. The converse is the von Neumann conjecture, and it is false: Ol'shanskii in 1980 and Adyan in 1982 produced finitely generated counterexamples. A finitely presented counterexample was harder, and one candidate stood out — Richard Thompson's group , finitely presented, with nobody able to decide whether it was amenable.
Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that , and more generally the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints, contains no free subgroup of rank greater than . Whether is amenable they could not determine, and it is still open today; claimed proofs have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes (Ol'shanskii–Sapir 2002; Lodha–Moore 2016), so is no longer needed as a candidate. This mission formalizes the half that was settled.
Let be the group of orientation-preserving homeomorphisms of the line: the strictly increasing bijections under composition. The support of is the set of points it moves, , an open subset of .
A continuous is piecewise linear when there is a discrete set of breakpoints with differentiable off and constant on each component of ; for finite this is the same as being affine on a neighbourhood of every point outside . Nothing is required at the points of , so the two affine pieces meeting at a breakpoint may disagree — that is what makes such an more than an affine map. Write for the piecewise-linear elements of and
for the subgroup this mission is about. The distinction matters: the goal below holds in and fails in , where Brin and Squier build free subgroups of rank by lifting them from the circle. Write for the commutator subgroup, which Brin and Squier identify as the elements whose slope at each end is — an element has slope at an end when it agrees with a single affine map of slope on a ray out to that end. Thompson's group — the piecewise-linear homeomorphisms of with dyadic breakpoints and power-of-two slopes — is realized inside .
Since a free group of rank greater than contains one of rank , this is Brin and Squier's Theorem (3.1).
Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the full-strength (3.2) are milestones of their own here. The goal itself only ever uses the rank-two form.
Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2) both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3), likewise in both strengths. Five are piecewise-linear infrastructure the source treats as routine: closure of under composition and under inverse, the same two for slope at each end, and finiteness of the number of components of a support. Five more are steps the source asserts without proof — that the line carries no non-fixed periodic points, that a map fixing a set's complement preserves its components, that the iterated images of a pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays inside the union of the two supports (p. 495), and that the derived subgroup of a free group of rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian subgroup of a free group is cyclic, which is what lets the goal finish through Nielsen–Schreier.
The theorem closes the standard route to proving a group non-amenable. To show a group amenable the classical routes are elementary amenability and subexponential growth, and is neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth, having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route is to exhibit a free subgroup of rank — the route this theorem closes. sits in the gap, which is why its status has survived sustained attention.
The result reaches past . Monod's groups of piecewise projective homeomorphisms are counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof that paper says it will "largely follow [Brin–Squier, § 3]".
What formalizing it adds. Mathlib has no piecewise-linear maps and no amenability predicate for groups. This mission builds the piecewise-linear layer: a workable , its closure properties, and the structure of supports.
The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the breakpoint set is what gives an element slopes at at all, and what makes two elements affine on each side of a common fixed point. Compactness is the other — throughout, — and it splits: that the closure of is compact needs only slope at each end, with no piecewise linearity at all, which is why (2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays inside is what reaches back to finiteness. Keeping straight which fact does which job is most of the work.
The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that makes them commute: only their intersections with one chosen component are disjoint, and commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.
What the Lean fixes. Elements are order isomorphisms of — strictly increasing
bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows
Mathlib's convention , the opposite of the source's right action, so the
conjugation identity reads here;
getting this backwards states a different theorem that still compiles. A support is the bare
moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with
local affineness off it — the set need not be minimal and may be empty.
A copy of is an injectivity statement about , not a subgroup
isomorphism, and the goal is about a single pair rather than a subgroup. The dichotomy
hypothesises slope at both ends directly, not membership in a derived subgroup — that these
coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and
the identification asserted on p. 493 gives the other.
Beyond a workable , the development needs Nielsen–Schreier, already
in Mathlib as subgroupIsFreeOfIsFree: it is what lets an abelian subgroup of a free group be
cyclic, and so lets the goal finish without the source's metabelian ending. That ending is
formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a
free group of rank two is non-abelian; the goal simply does not route through it.
One trivializing reading is ruled out. Slope at both ends is not a compact-support condition — every translation satisfies it — so (3.2) is not secretly a statement about compactly supported maps.
Nothing is built for specifically, and amenability is not touched. That is the one piece deliberately omitted, and contributions are welcome on it: modelling and embedding it in . The piecewise-linear layer is reusable beyond this theorem — Thompson's groups and , and piecewise-linear topology generally, need exactly it.
Chapter 3 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) develops the theory of convergence for sequences and series of numbers: subsequential limits and upper limits, the Cauchy criterion, the comparison, root and ratio tests, power series, summation by parts, and products of series. Its final section answers a question that distinguishes analysis from algebra: an infinite sum is not a sum. For a series that converges only conditionally, the value of the sum depends on the order of the terms, and Riemann's rearrangement theorem (Theorem 3.54) makes the dependence total — by reordering the terms one can prescribe any pair of limit inferior and limit superior for the partial sums, including divergence to .
This mission is the third in a series formalizing Rudin Chapters 1–11. It uses the real and complex number systems of Mission I and the compactness results of Mission II, and it supplies the convergence machinery used by Missions VII and VIII.
A series is the sequence of partial sums ; the series converges to when , and converges absolutely when converges. The upper limit of a real sequence is , taken in the extended real number system , and a subsequential limit is a limit of a subsequence there. A rearrangement of is a series with a bijection of the index set onto itself.
The distinction that drives the chapter: for real or complex terms, absolute convergence is equivalent to convergence of for every , to the same sum (Theorem 3.55), whereas mere convergence is not.
Let be a series of real numbers which converges but not absolutely, and let . Then there is a rearrangement with partial sums such that
The rearrangement theorem is the precise statement of why conditional convergence must be handled with care, and it is the reason later chapters insist on uniform or absolute hypotheses before interchanging limit operations: Theorem 3.50 (Mertens) needs absolute convergence of one factor, and the Fourier and Lebesgue theories of Chapters 8 and 11 are built on and convergence rather than pointwise summation. The supporting milestones are the standard convergence tests, which are used constantly in the rest of the book, and the characterization of , which is the tool that makes the root test and the radius of convergence formula precise.
Mathlib's Summable/HasSum express unconditional summability, which over and
is equivalent to absolute convergence. The conditionally convergent series that
this chapter is about are therefore invisible to that API, and the mission works with partial
sums directly. Some of the classical tests exist in Mathlib in Summable form and will need
restating; the rearrangement theorem itself has to be built.
The goal theorem is a construction, not an estimate: one splits into its positive and negative parts , observes that and both diverge while , and then alternately draws blocks of positive and negative terms to overshoot targets and undershoot targets . Formalizing the alternating greedy construction requires defining the permutation recursively together with the invariant that every index is eventually used — the bookkeeping, not the analysis, is the hard part. The endpoint cases or must be carried through the same construction rather than treated separately.
Conventions fixed by this mission:
Rudin.SeriesConvergesTo / Rudin.SeriesConverges, defined through
Rudin.partialSum a n = ∑_{i<n} a i. Absolute convergence is Rudin.SeriesConvergesAbsolutely.
Mathlib's Summable is deliberately not used, since it would collapse the distinction the
chapter is about.EReal via Filter.limsup/Filter.liminf, so
are allowed as values of and in the goal.Equiv.Perm ℕ, and the rearranged series is fun k => a (σ k).α‖z‖ < 1 and α‖z‖ > 1 rather than
‖z‖ < 1/α, to avoid inversion in EReal.The goal is not vacuous: conditionally convergent series exist (the alternating harmonic series), so the hypotheses are satisfiable, and the conclusion fixes both limit points exactly rather than merely bounding them.
Convergence, continuity and integration are all statements about nearness, and Chapter 2 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) isolates the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a single theorem, Heine–Borel (Theorem 2.41), which says that in — and, as the chapter's examples show, only in spaces resembling it — three very different-looking finiteness conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a continuous function on attains its maximum, is uniformly continuous, is Riemann-integrable) is an application of that equivalence.
This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the number systems of Mission I and supplies the topological input for Missions III–VII.
A metric space is a set with a distance that is positive for distinct points, symmetric, and satisfies the triangle inequality. The neighbourhood is the set of with . A point is a limit point of if every neighbourhood of contains a point of different from ; is closed if it contains all its limit points, open if each of its points has a neighbourhood inside , and its closure is together with its limit points. is perfect if it is closed and every point of is a limit point of , and bounded if it is contained in some neighbourhood.
An open cover of is a family of open sets whose union contains ; is compact if every open cover of has a finite subcover. A -cell is a product . Two sets are separated if , and is connected if it is not the union of two nonempty separated sets.
For , the following are equivalent:
Heine–Borel is the bridge between the order completeness of established in Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves -cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass, Theorem 2.42), and compactness is what converts local information into global statements. Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the connected subsets of the line as the order-convex ones, is the topological content of the intermediate value theorem proved in Chapter 4.
Mathlib has an extensive metric-space and compactness library, so much of this chapter exists
there in some form. What this mission adds is the explicit correspondence with Rudin's
formulations: his open-cover definition of compactness against the library's filter-based
IsCompact (a milestone in its own right), his -style limit points against
closure, and his -cells against the library's boxes. The resulting dictionary is what the
remaining missions in the series use when they need a compactness argument.
The mathematics is standard, and the difficulty is almost entirely in the translation layer.
Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the
statement is a -type over families of sets, while Mathlib's IsCompact is a statement
about filters; the equivalence is available in the library but only after the cover is
presented in the right indexed form. Second, "limit point" in Rudin's sense is not
p ∈ closure E: the point must be approached by points of other than , so isolated
points of are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two
notions are conflated.
Conventions fixed by this mission:
[MetricSpace X]; IsOpen, IsClosed, closure, Perfect,
IsCompact, Bornology.IsBounded and IsPreconnected are used for Rudin's corresponding
notions.Rudin.IsLimitPoint p E, defined with the explicit
and the condition , and his open-cover compactness is Rudin.IsCoverCompact.Rudin.kCell k a b inside EuclideanSpace ℝ (Fin k); the case where some
gives the empty set, which is why the nested-cell milestone assumes each cell is
nonempty, exactly as Rudin's construction does.IsPreconnected, which admits the empty set, matching Rudin's convention
that a set is connected unless it splits into two nonempty separated pieces.TFAE list in Rudin's order (a), (b), (c).The equivalence is not vacuous: all three conditions are satisfied by any -cell and all three fail for itself when .
Every course in analysis begins by fixing what a real number is, because the theorems that follow — the intermediate value theorem, the convergence of monotone bounded sequences, the compactness of closed bounded intervals — are false over the rationals and true over the reals for exactly one reason: the least-upper-bound property. Walter Rudin opens Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) with this point. His Example 1.1 exhibits the gap concretely: the set of rationals with has no least upper bound in . Chapter 1 then constructs an ordered field in which no such gap occurs, and derives from that single axiom the archimedean property, the density of , and the existence of -th roots.
This mission is the first in a series formalizing Rudin Chapters 1–11. It covers the chapter's number-system foundations: the ordering axioms, the real field, the complex field, and euclidean space .
An ordered set is a set with a transitive relation such that for exactly one of , , holds. If and there is with for all , then is bounded above and is an upper bound. A least upper bound (supremum) of is an upper bound such that no is an upper bound. The ordered set has the least-upper-bound property if every nonempty that is bounded above has a least upper bound in .
An ordered field is a field carrying an order such that whenever , and whenever and . Rudin's Theorem 1.19 asserts that an ordered field with the least-upper-bound property exists and contains as a subfield; the members of are the real numbers. The complex field is the set of ordered pairs of reals with the usual operations, written , with ; euclidean -space is the set of -tuples with the inner product and norm .
Existence of such a field is witnessed in Lean by itself; what carries the content of Rudin's theorem, and what the goal asks for, is that the least-upper-bound property pins the field down up to a unique isomorphism of ordered fields. Uniqueness of also gives Rudin's second assertion for free: any embedding of is the canonical one, so contains as an ordered subfield.
The least-upper-bound property is the only non-algebraic input to the whole of single-variable analysis, and the chapter shows how much follows from it alone: the archimedean property, which rules out infinitesimals; the density of , which makes approximation arguments possible; and the existence of -th roots, which repairs precisely the defect exhibited by . The uniqueness statement is what licenses the common practice of treating "the" real numbers as a single object regardless of the construction used (Dedekind cuts, as in Rudin's appendix, or Cauchy sequences).
Mathlib already contains , , and a uniqueness theorem for conditionally complete linearly ordered fields, and several of the milestones are available there in some form. The work this mission asks for is therefore bridging work: stating Rudin's hypotheses in his own terms — an order with the least-upper-bound property as a hypothesis on a set, not as a typeclass whose data includes a chosen supremum operator — and deriving the standard library form from them. That bridge is what later missions in the series reuse.
The individual statements are elementary, and the mathematical difficulty is genuinely low;
what makes the chapter non-mechanical in a proof assistant is the mismatch between hypothesis
and structure. Mathlib's completeness is packaged as ConditionallyCompleteLinearOrder, a
structure carrying sSup and sInf as data; Rudin's is a proposition about an arbitrary
ordered field. Turning the proposition into the structure (in order to invoke the library's
uniqueness theorem) is the one step where the obvious "just apply the Mathlib lemma" move does
not typecheck.
Conventions fixed by this mission:
Rudin.HasLeastUpperBoundProperty, using
Mathlib's IsLUB, BddAbove, lowerBounds; no completeness typeclass is assumed of K.[Field K] [LinearOrder K] [IsStrictOrderedRing K], which is exactly
Rudin's Definition 1.17.≃+*o (OrderRingIso), so "unique isomorphism"
is stated as ∃ e, ∀ e', e' = e.ℂ and is the norm ‖z‖; euclidean -space is
EuclideanSpace ℝ (Fin k) with the inner product inner ℝ x y, so Rudin's
facts are norm and inner-product inequalities.Nothing here is vacuous: the goal quantifies over an arbitrary ordered field satisfying the
property, and ℝ itself is such a field, so the hypothesis is satisfiable and the conclusion
is not automatic.
Before a mechanism can pay anyone, it must decide something — and the impossibility theorems of social choice say that deciding honestly is already hard. Arrow's theorem (1951) showed that any method of aggregating individual rankings into a social ranking that respects unanimity and independence of irrelevant alternatives must be a dictatorship; Gibbard (1973) and Satterthwaite (1975) showed the voting analogue: any non-dictatorial voting rule onto three or more candidates can be strategically manipulated. These two results frame all of mechanism design — they are the reason Chapter 9 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), this mission's source, introduces money and quasilinear utilities immediately after proving them: without transfers, incentive compatibility is an impossibility, not a design constraint.
A timeline: Arrow proved the aggregation impossibility in his 1951 monograph Social Choice and Individual Values; Gibbard (1973) established the manipulability of non-dictatorial voting schemes via game forms, Satterthwaite (1975) independently via a direct argument; the derivation of Gibbard–Satterthwaite as a corollary of Arrow's theorem, which the book follows and this mission adopts as its attack path, is standard since the 1970s.
Fix a finite set of alternatives (candidates) and a finite set of voters. A preference is a strict total order on ; we write the relation as , read " is strictly preferred to " (the book writes ). A preference profile assigns a preference to each voter. A social welfare function maps profiles to a social preference; a social choice function maps profiles to a single chosen alternative (Definition 9.1).
The properties at stake (Definitions 9.2, 9.4, 9.5, 9.7):
with no cardinality or finiteness assumptions: the two properties are quantifier-for-quantifier the same data viewed twice.
These are the two foundational impossibility theorems of social choice, and the pivot of the whole mechanism-design part of this series: the VCG mission that follows exists because Gibbard–Satterthwaite closes the door on non-trivial strategyproof choice without money. The chapter derives Gibbard–Satterthwaite from Arrow through the top-set extension (Definition 9.9, Lemmas 9.10–9.11), so a solver of the capstone gets Arrow as a stepping stone, not a detour.
Formalizing them produces the platform's first social-choice library: preference profiles as strict total orders, the aggregation vocabulary, and the impossibility pair. Arrow's theorem has been formalized before in other proof assistants (Nipkow's Isabelle formalization, 2009; a Mizar formalization by Wiedijk), which is evidence the statement shapes here are the standard ones — but no Lean 4/mathlib formalization exists, and none on this platform.
The proofs are short on paper and famously slippery in the details. Arrow's proof (the book gives Geanakoplos's pairwise-neutrality route) is a sequence of profile surgeries: each step swaps one voter's ranking of a pair and tracks the social outcome through IIA; the formal cost is constructing the intermediate profiles and proving they remain strict total orders — pure bookkeeping, but a lot of it. The hybrid-profile argument needs, over three or more alternatives, custom orders placing chosen pairs at chosen positions; building these on an abstract finite type is where most of the work lies. For the capstone, the book's route through the top-set extension (move to the top, Definition 9.9) requires proving the extension is again a strict total order (Lemma 9.10) and inherits unanimity, IIA, and non-dictatorship (Lemma 9.11); a solver may equally take any direct proof of Gibbard–Satterthwaite — the statement fixes no route. Proposition 9.6 is a genuine warm-up: unfolding both definitions and rearranging quantifiers.
Preferences are relations A → A → Prop carrying IsStrictTotalOrder; r a b means " is strictly preferred to ", the reverse of the book's — every definition's docstring states this orientation. Aggregators are total functions on all relation-valued profiles; every property quantifies only over genuine preference profiles, so behavior on invalid inputs is irrelevant, and nothing can be smuggled through junk inputs. Unanimity is the book's identical-profile form (Definition 9.2), which together with IIA yields the pairwise form used in proofs. Both alternatives and voters are finite types; |A| ≥ 3 enters as 2 < Fintype.card A. Arrow's theorem carries Nonempty ι, matching the book's setting of voters; it is not needed for truth — with zero voters the identical-profile unanimity is already unsatisfiable over three or more alternatives, so that case is vacuous either way. Gibbard–Satterthwaite deliberately omits it: with zero voters ontoness onto three alternatives is unsatisfiable, and the statement holds vacuously. Dictatorship for choice functions is Definition 9.7 exactly: whenever some alternative is the dictator's unique maximum, it is elected.
Equilibrium concepts are static; play is dynamic. The bridge between the two is regret minimization: simple adaptive rules that, against arbitrary — even adversarial — opponents, perform nearly as well as the best fixed alternative in hindsight. The subject begins with Hannan (1957) and Blackwell (1956), whose consistency theorems predate most of computational learning theory; the modern multiplicative-weights style bounds are due to Littlestone–Warmuth (1994) and Freund–Schapire (1997); the reduction from external to swap regret, and with it the algorithmic route to correlated equilibria, is Blum–Mansour (2005), following Foster–Vohra (1997) and Hart–Mas-Colell (2000). Chapter 4 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Blum and Mansour, is the source text of this mission.
The punchline of the chapter, and of this mission, is that a computationally trivial form of rationality — each player privately running a no-swap-regret algorithm — drives the empirical play of any finite game into an approximate correlated equilibrium (Aumann, 1974). No coordination, no knowledge of the game, no fixed-point computation: the equilibrium concept that Chapter 1 of the series defines through a correlating device is reached by decentralized learning.
The online model (§4.2): there are actions. At each time an online algorithm selects a distribution over actions, as a function of the loss vectors observed so far; then the adversary reveals a loss vector and the algorithm suffers . Cumulatively, and for a fixed action . The external regret of is . A modification rule rewires the algorithm's play, giving the modified loss ; the swap regret is over all rules.
A finite game (the vocabulary of Mission I of this series, in loss form): players , finite action sets , cost functions . A joint distribution on action vectors is an -correlated equilibrium (Definition 4.11) if for every player and every switching rule ,
An online algorithm with vanishing per-round swap regret, with the constant the chapter's own route produces.
A player with external regret over rounds has average loss at most , where is the game value — no-regret play guarantees the minimax value against any opponent.
Any algorithm with external regret on all -loss sequences yields one with swap regret .
If every player's swap regret over steps of mixed play is at most , the empirical joint distribution is an -correlated equilibrium.
Every deterministic algorithm has a -loss sequence forcing loss while some action loses at most : randomization is necessary, not a convenience.
Correlated equilibrium is the equilibrium concept with a defensible dynamic foundation: Nash equilibria are PPAD-hard to find, but the capstone plus Theorem 4.12 exhibit polynomial-time decentralized dynamics whose empirical play is an -correlated equilibrium after rounds. Later missions in this series lean on this machinery: the price-of-anarchy chapters bound the cost of no-regret play (not just of exact equilibria), and the routing-game chapter uses precisely the convergence result formalized here.
Formalizing it produces the platform's first online-learning library: the adversarial protocol, regret in both external and swap forms, the multiplicative-weights analysis, and correlated equilibria. The regret vocabulary is directly reusable for the bandit-flavored missions already on the platform. All results are classical, with textbook proofs; the work requested is machine-checked proof, not new mathematics.
The Polynomial Weights bound is a potential-function argument: the total weight falls geometrically with the algorithm's loss and is bounded below by the weight of action ; the formal work is inequalities for on and careful bookkeeping of the recursion. The reduction (Theorem 4.15) is the structurally interesting step: the master algorithm runs copies of the external-regret procedure, feeds copy the true losses scaled by the master's own probability , and — the crux — plays the stationary distribution of the column-stochastic matrix assembled from the copies' outputs. Existence of that fixed point is exactly the existence of a stationary distribution of a finite Markov chain, available on this platform as the goal of Markov Chains and Mixing Times I — or provable directly. Theorem 4.12 is an averaging argument, deliberately easy; Theorem 4.3 is an adversary construction; Theorem 4.9 combines the regret bound with the security level the minimax theorem of Mission I supplies, through the opponent's empirical mixture. The capstone is the composition of 4.6 (tuned at ) with 4.15, plus the arithmetic that turns into the stated bound.
An online algorithm is a deterministic function from the observed history (the list of past loss vectors) to the mixed action played next — the standard formal reading of the full-information model; randomization lives in the mixed action, and losses are expected losses. Boundedness of losses () is a hypothesis on theorems, never part of a definition. The Polynomial Weights algorithm is defined concretely by its weight recursion, and its learning rate carries the hypothesis : the book writes only , but at the bound's term degenerates and the claim is false, so positivity is explicit. Action sets are Fin (n+1), keeping them nonempty. The number of steps is a known parameter (the book's convention; guess-and-double is out of scope). Correlated equilibria use the switching-rule form of Definition 4.11, over the game vocabulary (IsLottery, IsMixedProfile, profileProb) published with Mission I of this series. In Theorem 4.12 the empirical distribution is the average of product distributions of the played profiles, is required (at there is no empirical distribution), and costs are not assumed bounded — the averaging is scale-free.
Trivializing readings are ruled out: the existential algorithms in Theorem 4.15 and the capstone are quantified before the loss sequence and the modification rule, so a witness must work uniformly against every adversary — nothing may be chosen with hindsight.
Let be a finite connected graph. In Bernoulli bond percolation each edge is independently retained with probability and deleted otherwise, and one writes for the probability that vertices and lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is -hard.
The bunkbed graph is built from two copies of , joined by vertical edges called posts above a chosen set of transversal vertices. Percolation is performed on the two copies while every post is retained. Writing for a vertex in the lower copy and for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.
The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:
Section 7 of the source is a candid account of a large-scale machine-learning-guided search that failed to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.
Fix a finite graph with vertex set and edge set , and a retention function (the uniform case is ). A configuration is a subset of open edges, occurring with probability
and is the total probability of those for which and are connected in .
Given , the bunkbed graph has vertex set . Its edges are a copy of in each level together with a post for every . In bunkbed percolation the two level-copies are percolated independently while all posts are retained; denotes the resulting connection probabilities.
For the gadget on vertices,
The result itself. A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from down to .
Formalizing it. Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains no percolation of any kind — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.
The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with edges has configurations; for the counterexample here the probability gap is on the order of , so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.
The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single -hyperedge cannot be simulated by bond percolation on any gadget graph. The source's answer is to prove a robust version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.
The development commits to the following conventions.
ℚ and evaluate by #eval, and small instances close by decide.Finset and realised through SimpleGraph.fromEdgeSet; connectivity is Mathlib's SimpleGraph.Reachable.Sym2 V → ℚ), since the gadget genuinely needs two different weights: its spokes are retained with probability and its path edges with probability .0 is the lower copy; posts over T are unconditionally present and are not percolated. The two levels are percolated independently.IsPlanar, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.Infrastructure. Mathlib supplies SimpleGraph, boxProd, Reachable with a DecidableRel instance, fromEdgeSet, edgeFinset and Finset.powerset. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's Reachable decision procedure enumerates walks and is far too slow to evaluate the -configuration check of Lemma 3.1 by decide. A solver will want a linear-time reachability procedure together with a proof that it agrees with Reachable; that is itself a worthwhile reusable contribution.
The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If and are finite based chain complexes over a finite field, their tensor product is graded by total degree,
Each complex carries a basis-dependent homological distance: is the least Hamming weight of a degree- cycle that is not a boundary, with when the degree- homology vanishes. A natural candidate for the distance of the tensor product is therefore
Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has . The substantive question is whether this upper bound is always sharp.
In the preprint Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates, posted in 2018 and subsequently published in Physical Review Letters, Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates. The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.
Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in Minimal distances for certain quantum product codes and tensor products of chain complexes, published in 2020. In the corresponding arXiv preprint, Conjecture 18 asserts the unrestricted equality
The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.
The common foundation is recorded in the Prove2Me entry Based binary chain complexes and homological distance. In particular, the boundary in degree is a map , and
The one-complex result is separately available as Eq. (13) — Exact distance with a one-complex. The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.
Begin with binary CSS check maps
assumed surjective and satisfying . Suppose there are logical vectors such that
The check maps determine two dual three-term complexes
Their degree-two tensor space has three bidegree summands, corresponding to , , and . Under the natural matrix identifications, consider the element whose three blocks are
The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly , whereas the componentwise candidate in degree two reduces to
Consequently, any CSS datum satisfying
produces the strict inequality . For orientation, a binary quantum Golay CSS presentation with parameters has , giving the numerical comparison . The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.
The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element is a nontrivial degree-two cycle of weight , and the componentwise minimum is .
The second milestone constructs and verifies one explicit CSS datum for which . This is the step that turns the general mechanism into an actual counterexample.
The capstone packages the construction as the direct existential statement
Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.
The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.
The broader literature also indicates why additional structure matters. Bravyi and Hastings introduced homological-product codes and analyzed logical representatives in product constructions; Audoux and Couvreur developed tensor products of CSS codes through chain-complex methods. More recently, Akhmechet et al. discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while Berthusen et al. restated it as Conjecture 5.1 in their study of automorphism gadgets. Golowich and Guruswami obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.
Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.
The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with -valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.
A quantum circuit of depth built from gates of fan-in at most two cannot let an output wire depend on more than input wires. The argument is folklore and takes a paragraph on paper: the causal cone of the measured wire grows by at most a factor of two per layer. Formalizing it exposes a subtlety that the paper argument hides, and that is what this mission is about.
Define the backward cone step of a wire set through a layer by adjoining the support of every gate of that meets . There is a choice here: test each gate against the incoming set , or against the partially accumulated cone. Testing against the accumulator over-approximates, and the doubling bound fails. Testing against the incoming set gives the bound — but is only correct when the gates within a layer act on pairwise disjoint wires.
Without that hypothesis (LayerOk) the semantic statement is false, and the counterexample is
small: on three wires, the single layer [cnot 2 1, cnot 1 0] has cone around wire
, yet wire ends up holding . So the cone under-approximates
the true dependence. This mission's development carries LayerOk throughout, and the
counterexample is recorded in the source.
Layered circuits over on wires, with states as amplitude functions on bit-strings and no tensor products anywhere. On top of that:
acceptProb is a genuine probability in ;The semantic half is proved in the Heisenberg picture. The measurement observable is conjugated backwards through the circuit and its support tracked: a gate meeting the support enlarges it by that gate's own wires, and a gate missing it commutes with the observable and cancels against its own adjoint. That cancellation is the reason the non-cascading cone step is correct, and it is why unitarity of the gate set is needed at the -dimensional level rather than gate by gate. Supporting this is a small reusable algebra of local operators: locality is monotone, closed under adjoint and product, and disjointly supported operators commute.
The published depth bound assumes each input wire lies in the syntactic cone of the output. That is weaker than saying the wire matters. Milestone 1 asks for the semantically honest version, stated in terms of genuine functional dependence; the bridge is the semantic cone theorem already in the development.
Beyond that, the natural continuations are the same argument for fan-in- gates (), for geometrically local circuits where cone growth is linear rather than exponential, and ultimately the Bravyi–Gosset–König separation — which needs machinery (non-local games, magic squares) that this development deliberately does not build.
When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.
Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (BertsekasDPModel), its policy cost recursion, and the open-loop cost of a fixed control sequence (BertsekasDPOpenLoopCost). For rollout (§6.4.1): a graph search problem — a finite digraph with destination set and terminal costs on destinations (BertsekasGraphSearch); a base heuristic producing from every node a path to a destination (BertsekasBaseHeuristic), with projection and heuristic cost ; the rollout algorithm repeatedly moves to a neighbor minimizing (BertsekasIsRolloutRun). is sequentially consistent if its paths have the tail property (Def. 6.4.1), sequentially improving if (Def. 6.4.2).
For sequentially improving and any terminating rollout run :
— BertsekasDP.rollout_sequential_improvement (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects ), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).
Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.
The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the IsLeast membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.
Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets per Eq. (6.19); all statements at the level of the Mission I model.
An LLM agent acting in an environment spends most of its wall-clock time waiting. Each step — a model call, a tool or MCP request, a browser action, sometimes a human reply — must complete before the next can be issued, and the round trips dominate end-to-end latency: a chess game between two reasoning agents runs for hours, and an operating-system tuning task for tens of minutes. When a training or prompt-optimization loop repeats such a run thousands of times, the waiting is the cost.
Speculative actions (Ye, Ahuja, Liargkovas, Lu, Kaffes, Peng, ICLR 2026) transplants a classical systems idea — speculative execution in microprocessors, and speculative decoding for LLM inference — to the agent's environment loop. A cheap, fast speculator guesses the action a slow, authoritative actor is about to produce, the guess is used to launch the next environment call early, and the work is committed only when the actor's real action confirms the guess. The interface stays sequential and lossless; the internals run in parallel.
What makes this a formalization target rather than an engineering report is the paper's §5 cost–latency analysis. Speculating more branches buys hit probability but costs tokens, and the paper derives closed-form expressions for both sides of that trade — a self-contained piece of applied probability sitting underneath a systems paper. This mission asks for those expressions, machine-checked.
Fix a horizon and index steps . At each step a policy maps the state to an API call; the actor executes it with latency , while the speculator proposes candidate actions with latency , where (the speculator is faster in expectation). A speculative branch hits when the action it guesses implies the same next call the actor's true action would have implied; branches hit independently across steps with probability .
Two knobs define the two regimes analyzed. Breadth : at each step, launch independent one-step speculations in parallel, each immediately followed by a real call. At least one of the succeeds with probability
Depth: follow a single branch, extending it whenever a speculative or real call returns and pruning subtrees the actor contradicts.
The quantity driving both results is , the expected number of hits by round . A hit consumes the following step's speculation window — after a correct guess the next call is already cached, so no new speculation is launched there — which yields the two-term recursion
Write for the latency and token cost of strictly sequential execution, and for their speculative counterparts. In the depth regime latencies are taken deterministic: for a real call, for a speculative one.
The goal theorem is the finite-horizon latency ratio for breadth-focused speculation (Proposition 1), with abbreviated :
The supporting targets, ordered as the analysis builds them:
The analysis is what turns speculation from a trick into a tunable system. Proposition 1 and Theorem 4 are governed by the same quantity , so a practitioner who can estimate hit probability can choose offline against a latency/cost budget rather than by trial. The 50% ceiling is a genuine negative result — it says breadth alone cannot do better, and motivates the depth regime, where the ceiling becomes 1. Theorem 3 explains why confidence-based branch selection is cheap in practice: the whole dynamic program collapses to one scalar continuation value, so a runtime system sorts confidences and adds branches greedily in per step.
The paper's proofs are pen-and-paper and, as far as we are aware, none of these results has a machine-checked proof. Three parts reward formalization specifically. The recursion's closed form is derived by a characteristic-equation argument with a particular solution that collides with the homogeneous part — routine but error-prone. The per-hit saving is an honest two-dimensional integral over independent exponentials. And Theorem 6's cost expression is stated in the paper with a floor function and then immediately replaced by an approximation, so formalizing it forces a decision about which claim is actually being asserted (see Formalization scope).
The obvious first move on the recursion — guess a constant particular solution — fails, because is a root of the characteristic polynomial and a constant trial collides with the homogeneous family; the particular solution is linear in , and the coefficient comes out of matching both initial conditions, not one.
The interesting hypothesis is the one the recursion's shape encodes and the prose states only in passing: a hit at round removes the speculation window at round . Drop it and the recursion becomes one-term and the answer changes.
For the per-hit saving, the difficulty is analytic rather than algebraic: the inner antiderivative of must be handled, and the outer integral runs over an unbounded interval, so integrability has to be established rather than assumed.
The asymptotic statements need the oscillating term controlled uniformly — it is bounded, not vanishing termwise in an obvious way — before the prefactor can be taken to zero.
Everything is over . The model lives in one definition bundle,
Def_SpecActions_model, in namespace SpecActions; the mission's Lean names match the
prose symbols ( is hits, is phit, is kt).
The model is formalized at the level the paper's own proofs use: and
are defined by the expressions Appendix A derives for them
(specTime, specCost, and their depth analogues), and the theorems assert the
algebraic and asymptotic identities relating those quantities. Deriving those
expressions from a measure-theoretic model of the execution trace is deliberately not
in scope — with one exception: milestone 2 states the per-hit saving as a genuine
iterated integral against the exponential densities, so the one probabilistic step the
paper actually computes is formalized as an integral rather than assumed.
Conventions a solver should know before starting:
hits takes (the per-step hit probability ), not the per-branch ;
phit relates the two, and Thm_SpecActions_phit_bounds supplies the
range facts the other statements assume.Reusable beyond this mission: the two-term linear recursion solved in milestone 1, and
the computation for independent exponentials, which is a standard
fact absent from Mathlib. Contributions extending the model toward an actual measure on
execution traces — deriving specTime rather than defining it — are welcome as
follow-on work.
Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code over a finite field has a dual code consisting of the words orthogonal to all words of under the standard coordinatewise bilinear form.
The MacWilliams identity states that the full Hamming-weight distribution of is determined by that of through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.
This development isolates the arbitrary- Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.
Let be a finite field of cardinality , let be a finite coordinate type, and let a word be a function . A linear code is an -linear subspace of the word space. The standard bilinear form is
and the dual code is
The Hamming weight is the number of coordinates at which is nonzero. Writing , the homogeneous Hamming weight enumerator of is the integer-coefficient polynomial
Thus the coefficient of is the number of codewords of weight . The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.
For a primitive complex additive character of , define
The first milestone states that when and otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.
For every word and all , the second milestone records the full character-weighted transform of the Hamming monomial:
This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.
The capstone is the following equality of integer polynomials:
This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula
The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.
The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.
The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in ; and the final result is most reusable as an equality of symbolic polynomials over . The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.
The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.
The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.
The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in and variables indexed by Fin 2. Variable records zero coordinates and variable records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.
The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to . The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.
Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the same number reappears throughout combinatorics as the number of spanning trees of the complete graph , a special case of Kirchhoff's Matrix–Tree Theorem, and as the base case against which more refined tree-counting results (trees with a prescribed degree sequence, forests, spanning trees of general graphs) are measured.
Several independent proofs of the count are known — a direct recursive argument, a determinant computation via the Matrix–Tree Theorem, a double-counting argument on increasing trees — and each exposes a different piece of structure. This mission formalizes the proof via Prüfer sequences, due to Prüfer (1918): an explicit, computable bijection between labeled trees and certain finite sequences, presented here following Gross and Yellen, Graph Theory and Its Applications, 3rd ed. (CRC Press, 2018), Section 3.7, pp. 157–162.
Fix and take the vertex set to be (formalized as Fin n).
A labeled tree on vertices is a simple graph on this vertex set that is
connected and acyclic (Mathlib's SimpleGraph.IsTree). Two labeled trees are the same
exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the
source are both paths but are different labeled trees, since the labels sit on
different vertices.
A Prüfer sequence of length is any sequence of labels drawn from , repetitions allowed (so there are of them, by the rule of product).
The encoding of a tree (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by repeating, times: find the leaf (degree-one vertex) with the smallest label among those not yet removed, record the label of its neighbor, then delete that leaf. The decoding of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the tree edge by edge, at each step joining the smallest label not yet used and not appearing later in the sequence to the next label in the sequence, finishing by joining the two labels left over.
This is the weakest stable statement: it is exactly the count Cayley identified, phrased without reference to any particular proof method, so it is not tied to properties of Prüfer sequences beyond what is needed to establish the count.
The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree Theorem (which computes the analogous count for spanning trees of an arbitrary graph as a cofactor of its Laplacian) and it appears as an ingredient in random graph theory (counting spanning trees of bounds the number of ways a random graph process can build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding itself is used as a compact serialization of a labeled tree.
The result has been proved by hand for over a century, and its most classical proof (the
one formalized here) has not, to this project's knowledge, appeared as a
machine-checked Lean proof; Mathlib's Combinatorics.SimpleGraph library has the tree
and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or
the count itself. Formalizing it here means constructing the encoding and decoding maps
explicitly as computable, total recursive functions, and proving they are mutually
inverse — the mission's four milestones below are exactly the four supporting results
the source uses for this.
The obvious first attempt is to define the encoding by structural recursion, peeling one
leaf per step, but this immediately runs into a dependent-typing obstacle: after
deleting a vertex, the "remaining graph" naturally lives on a smaller vertex type, so
a naive recursive definition changes type at every step and the final sequence's type
(length ) is not visible to the recursion by construction. The formalization here
sidesteps this by keeping the ambient vertex type fixed at Fin n throughout and
tracking the shrinking set of "active" vertices as an ordinary Finset (Fin n)
parameter, so the recursion is on a natural number step-counter rather than on the type
itself; the price is that every step's "leaf" and "neighbor" must be picked out by an
explicit Finset.filter/Finset.min computation whose well-definedness (there is
always a smallest active leaf, and it always has a unique active neighbor) is exactly
the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system
gives for free. The inverse direction has the dual issue in reverse: decoding recurses
structurally on the sequence while tracking a shrinking label set, and showing the two
recursions undo each other (Proposition 3.7.4) requires the same induction run in both
directions simultaneously.
Trees are SimpleGraph (Fin n) satisfying Mathlib's SimpleGraph.IsTree; no alternate,
weaker notion of "tree" is used. Prüfer sequences are functions Fin (n - 2) → Fin n
(equivalently, by Fintype.card_fun, exactly the count needed) rather than
List or Vector, so that the final counting step is immediate once the bijection is
established. The encoding and decoding functions (pruferEncode, pruferDecode) are
supplied as noncomputable definitions in Definitions.Def_GYGraphTheory — noncomputable
only because Prop-level decidability of a general SimpleGraph.Adj is classical, not
because the algorithm is non-constructive; every step is the literal Prüfer procedure,
junk-valued (defaulting to label 0) outside its intended domain in exactly the way a
hand proof would say "this step is meaningless once fewer than two active vertices
remain." The four milestones give the precise faithful statements of the source's
Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal
theorem is the immediate corollary once all four are in hand, via Fintype.card_congr
and Fintype.card_fun. A trivializing formalization is not available here: IsTree is
Mathlib's standard, non-vacuous notion, and the milestones pin down pruferEncode
and pruferDecode to the source's specific algorithm rather than leaving the bijection's
existence as a free black box. Beyond the four milestones, a full development needs:
basic Finset/List manipulation lemmas relating pruferPeel's step-indexed recursion
to pruferDecodeAux's list-indexed recursion (reusable in any future mission touching
Prüfer-style encodings); and the final cardinality argument tying the bijection to
n ^ (n - 2). Contributions connecting this formula to Mathlib's general Matrix–Tree
machinery (if and when it exists) would be a natural, welcome extension but are out of
scope for this mission.
The Fourier series of a periodic function decomposes it into sinusoidal components, but the partial sums of that series need not converge to the function even when the function is continuous: du Bois-Reymond exhibited in 1873 a continuous -periodic function whose Fourier partial sums diverge at a point. Fejér's 1904 theorem repairs this failure by replacing the partial sums with their Cesàro (arithmetic) averages: for every continuous periodic function, these averages converge to the function, uniformly, with no smoothness hypothesis beyond continuity. This was the first universally valid summation method for Fourier series, and its underlying technique — averaging against a kernel whose mass concentrates at the origin — became the template for what is now called a good kernel or approximate identity, the basic device used throughout harmonic analysis (heat-kernel smoothing, Poisson summation, Fourier-inversion arguments) [Stein & Shakarchi, 2003].
Timeline.
Let be continuous and -periodic, i.e. for every . Its -th Fourier coefficient, for , is
Its -th partial sum is , and its -th Cesàro (Fejér) mean is the arithmetic average of the first partial sums,
This is the full 1904 statement: no restriction to pointwise convergence, and no extra regularity assumed on beyond continuity.
The result itself. Fejér's theorem gives the first universally valid summation method for the Fourier series of a continuous function, closing the gap left open by pointwise convergence tests that need extra regularity. It also yields, essentially for free, a proof of the Weierstrass approximation theorem on the circle — the trigonometric polynomials are dense in the continuous -periodic functions under the uniform norm — and it is the historical prototype of the good-kernel/approximate-identity method underlying Poisson summation, heat-kernel smoothing, and Fourier-inversion arguments.
Formalizing it. Mathlib currently has no infrastructure for this at all. Mathlib.Analysis.Fourier.AddCircle defines Fourier coefficients on the circle and proves convergence (Parseval's identity, via the orthonormal Fourier basis), but it has no notion of a partial sum, no Dirichlet or Fejér kernel, and no pointwise or uniform convergence result for Fourier series of any kind. This mission builds that classical convergence theory — the Fejér kernel, its closed form and positivity, the good-kernel estimates, and the uniform convergence theorem itself — from first principles.
The obvious first attempt is to bound termwise from the individual Fourier coefficients. This fails outright: a continuous function's Fourier coefficients need not be absolutely summable, which is exactly the mechanism behind du Bois-Reymond's divergence example. The real difficulty is representing as a convolution,
against the Fejér kernel , and then proving is a good kernel: nonnegative, integrating to over one period, and — the genuinely quantitative step — with its mass outside any fixed neighborhood of vanishing as . That last estimate needs the closed form
which carries a removable singularity at that must be handled carefully, together with a genuine decay estimate — via a lower bound on — valid uniformly outside any fixed -neighborhood of the origin.
is complex-valued, and only continuity together with exact -periodicity is assumed — no differentiability, no bounded variation, no realness. Uniform convergence is stated with Mathlib's TendstoUniformly. The period is fixed at , matching the classical circle-group convention, rather than a general ; the -periodic statement is a routine rescaling of this one and is not separately targeted here. One route to a trivializing formalization is worth ruling out explicitly: assuming any extra regularity on (differentiability, bounded variation, Lipschitz continuity) would let the uniform-convergence conclusion follow from the much easier Dirichlet-kernel estimates, and would no longer be Fejér's theorem — the entire content of the result is that continuity alone suffices.
The needed infrastructure is the four definitions above (Fourier coefficient, partial sum, Cesàro mean, Fejér kernel) and the milestone lemmas below, culminating in the goal. The Fejér kernel's closed form, positivity, and good-kernel estimates are reusable well beyond this mission: directly for a Lean proof of the Weierstrass approximation theorem on the circle, and for any future development that needs an explicit approximate identity on the circle group. Contributions are welcome at every milestone; the concentration estimate is the analytic heart of the mission and a natural place to start.
In 1956 Kelly answered a question that looks like gambling and is really about information: if a channel gives you a noisy advance signal about a sequence of bets, how much is that signal worth? His answer was that the maximum exponential rate of growth of a gambler's capital equals the rate of transmission over the channel -- so information rate and capital growth rate are the same quantity in different units. The betting fraction that achieves it is now called the Kelly criterion, and it is the basis of a large practical literature on position sizing.
The result is short, entirely explicit, and has no analytic subtleties -- which makes it a good formalization target and a surprising gap: the platform currently has fifteen missions on bandit algorithms and none on optimal growth.
This mission formalizes the simplest case of Kelly's Section 4: an even-money bet with no
track take, won independently with probability p and lost with probability q = 1 - p. A
gambler stakes a fixed fraction l of current wealth on each bet, so wealth is multiplied by
1 + l on a win and 1 - l on a loss. The exponential rate of growth is
Kelly shows this is maximised at l = p - q, with maximum value 1 + p log p + q log q in
bits. We state G in nats (natural logarithm), so the maximum carries an additive log 2;
dividing by log 2 recovers Kelly's bit-valued form, which is exactly 1 - H(p) for the
binary entropy H. The maximiser is unaffected by the choice of base.
The goal theorem is that l = 2p - 1 maximises G over the admissible range (-1, 1) when
the bet is favourable (p > 1/2). Milestones supply the maximum value (Kelly's
information-rate identity), the admissibility of the maximiser, and the concavity that makes
the first-order condition sufficient.
J. L. Kelly Jr., A New Interpretation of Information Rate, Bell System Technical Journal
35 (1956) 917-926, Section 4 ("the simplest case"). The growth-rate expression and the
maximiser l = p - q are stated there; the maximum value in bits is Kelly's eq. for G_max.
The identity and maximiser were checked numerically before drafting: for p = 0.55, 0.6, 0.7,
0.9 the claimed maximum matches log 2 + p log p + q log q to six decimals, and a grid search
over (-1, 1) at 1e-5 resolution returns 2p - 1 in every case.
Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function is positive-definite if, for every finite family of points and complex coefficients , the Hermitian quadratic form is real and nonnegative. This single algebraic condition is exactly what makes realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.
Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a necessary condition for such a representation, but exactly characterizes it. A continuous, normalized () function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure on — i.e. is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where is additionally Lebesgue-integrable, so that has an explicit continuous density given directly by the ordinary Fourier transform of .
Fix IsPositiveDefinite f as above, for (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, (IsPositiveDefinite.conj_neg), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with f continuous and normalized. No further hypothesis (in particular, no integrability of f) is assumed for the general representation theorem: the representing measure need not be absolutely continuous (e.g. for a periodic , is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that f is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is fourierTransform f, the (real part of the) Fourier transform of f — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers f from it.
The central representation theorem: no integrability hypothesis on , so may be any probability measure, not necessarily a density.
L¹ (density) caseThe special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.
Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.
The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from f, a strongly continuous unitary representation of on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since f need not be integrable and need not have a density. The L¹ milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: IsPositiveDefinite.conj_neg) that a positive-definite function is Hermitian-symmetric.
IsPositiveDefinite is formalized exactly as the finite Hermitian-form condition above, over Fin n → ℝ point families and Fin n → ℂ coefficients, matching the standard convention in the literature, with f : ℝ → ℂ — the fully general, complex-valued statement, not restricted to real-valued kernels. fourierTransform f ξ is defined as the real part of ∫ Complex.exp(-i2πξ x) * f(x) dx; this is provably the exact (not merely real-part-of) Fourier transform once f is positive-definite, since Hermitian symmetry forces the integral to be real already.
A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.
This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's Discrete Mathematics—Lecture Notes, §6.1. Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.
A finite simple graph consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A bipartition is a pair of disjoint sets whose union is the vertex set, such that every edge joins a vertex in to a vertex in . The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow Definition 1.1 of the notes.
For a vertex , the neighbor set contains the vertices joined to . For a set of vertices, write . A matching is an edge set in which no vertex is used twice. It is complete on if every left vertex is used, and perfect if every vertex is used. A subgraph may retain selected edges of the original graph. Its degree counts the retained neighbors of .
A demand is a natural number attached to each . Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.
The ordinary matching criterion is Theorem 6.2:
The development also includes Exercise 6.3, asserting that a -regular bipartite graph has a perfect matching when . Proposition 6.4 states the quantitative deficit version:
The capstone is the prescribed-degree equivalence of Exercise 6.5:
This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.
The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets has a system of distinct representatives, meaning an injective choice , exactly when
Only the index family is finite; the sets themselves may be infinite.
The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of Exercises 6.3 and 6.5 and Proposition 6.4.
Mathlib already provides finite-family and graph versions of Hall's theorem in its Hall development and graph interface. The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.
Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.
Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.
The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.
Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.
The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.