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.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A set of integers is sum-free when no two of its members add up to a third. Schur's theorem (1916) says that for every there is a largest interval that can be split into sum-free classes, and the resulting Schur numbers are notoriously hard to compute: was settled only in 2018, by a SAT computation with a machine-checked proof certificate.
Replacing "adds up to" by "adds up to, modulo " gives a family that behaves very differently. Modular Schur numbers were introduced by Chappelon, Revuelta Marchena and Sanz Domínguez, who settled the moduli and proved the universal bound (Electron. J. Combin. 20(2) (2013) #P61). D'orville, Sim, Wong and Ho then closed by residue case analysis and posed the general modulus as an open problem (Integers 25 (2025) #A62, their Problem 1). Each additional modulus had cost a separate case analysis, and the case analysis grew with .
The timeline matters for reading what follows. The 2013 paper supplies the universal cap. The 2025 paper supplies a singleton criterion (its Theorem 4) and a divisibility obstruction (its Corollary 3), and applies the latter only in the coprime case (its Corollary 5). What remained was to optimise that obstruction over every residue rather than only in the coprime case, which is what collapses the whole family to one formula.
Fix integers , and . A set of integers is -sum-free modulo when there are no and , repetitions among the allowed, with
The repetition clause is not a technicality: a single element can make its whole class unsafe. The modular Schur number is the greatest such that the interval can be partitioned into at most classes, each -sum-free modulo . A partition into such classes is called valid.
Two derived quantities carry the whole story. Write
Then exactly, and by construction. All Lean statements in this mission use these same names.
Closed form here means something precise: the value is produced from and by one gcd, one division and one subtraction, with no search over colourings, no recursion, and no case split on . The statement fixes no constants and no modulus, so it is not invalidated by any later refinement of the threshold in .
together with the complementary regime , where the value is if and otherwise. The two together give a value for every admissible pair at , and the tree carries that combined formula at the residue level and at the integer level.
What the results give. One expression replaces an open-ended sequence of per-modulus case analyses. The moduli of the 2013 paper and of the 2025 paper are specialisations, and every remaining modulus is covered at once in the stated range of .
The mechanism is a single self-defeating value. Take copies of : they sum back to modulo , so the lone class already breaks the rule, while every smaller value is safe. That one observation supplies a matching upper and lower bound.
Status of the tree, stated precisely. Everything listed under Formalization targets is both proved and machine-checked.
{propext, Classical.choice, Quot.sound}.Relation to the accompanying paper. The paper states the single-colour value only under
. Three results in the tree go beyond it: the complementary regime
, and the combined formula covering every and , stated once at
the residue level and again at the integer level. Two further results, the coset-cardinality
bounds, are supporting work of the Lean development and are not numbered results of the paper.
Each theorem's source field records which of these it is.
The obvious attack on the general modulus is to guess that only singletons can be safe classes. The threshold in would then be exactly , and the problem would close for all at once. That guess is false.
Take and , so and . The two-element set is -sum-free modulo , and three colours then suffice where the singleton count would demand five.
So the least at which the closed form takes hold, written , is not in general. What is known about it:
Theorem 8 of D'orville, Sim, Wong and Ho gives a three-branch formula at prime-power moduli. Its middle branch is false. The correction is stated here in full because it bears directly on the threshold.
It is proved from a valuation-layer colouring that consumes classes, together with the universal cap. The hypothesis forces and , so the replacement reaches the goal theorem's value at in place of , and it contradicts the printed middle branch for infinitely many triples .
Status of that correction, stated precisely.
For the classes must be simultaneously large and -sum-free, and no formula is known. The value is empirically eventually periodic in for fixed , verified through .
None of these open directions is weakened by the goal theorem, which deliberately assumes enough colours to avoid the question.
Two levels appear in the tree, and the distinction between them is the first thing to fix.
ZMod m: Mathlib's type of residues modulo , a commutative ring with exactly elements
for , carrying the reduction map from and the arithmetic that map
preserves.Working in ZMod m turns "adds up to, modulo " into a plain equation instead of a
divisibility side condition, and it makes every colour class a subset of a finite type.
The development works residue-by-residue in ZMod m and commits to the following conventions,
all of which are silent in the prose and load-bearing in Lean.
Fin ℓ → ZMod m valued in the class. This builds in
"repetitions allowed" rather than leaving it to a side condition.Finsets, so finiteness is structural.Both a residue-level and an integer-level number are defined, and a reduction theorem proves them equal for every . Bounds are proved on the residue side and quoted on the integer side.
Both are defined with Nat.findGreatest against the bound . That cap is neither an
approximation nor a trivialising choice: a separate theorem shows any admitting a valid
partition satisfies with no hypothesis on , because admits no
valid partition at all. A reader checking for a vacuous formalization should also note that the
goal is an equality, not a bound, so it cannot be satisfied by weakening a hypothesis.
Contributions welcome on the open directions named under Difficulty, in particular any lowering of the threshold in toward , and a closed form for at composite moduli.
This mission formalizes John Milnor's Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968) 447–449 (doi:10.4310/jdg/1214428659), a three-page addendum to J. A. Wolf's Growth of finitely generated solvable groups and curvature of Riemannian manifolds, which precedes it in the same issue (421–446, doi:10.4310/jdg/1214428658). Milnor's note has one theorem and three lemmas, and "for definitions and explanations the reader is referred to" Wolf.
Wolf proved that a polycyclic group "either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial growth, or has no such subgroup and is of exponential growth" (p. 421). Milnor's Theorem closes the gap between polycyclic and solvable: "Let be a solvable group which is not polycyclic, and a finite set of generators for . Then there exists an exponential lower bound for the growth function of ." Together the two papers give the Milnor–Wolf theorem, "that a finitely generated solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth" (Wolf, p. 421). Milnor notes that Wolf's results "provide a partial answer to a problem which was posed by the author in Amer. Math. Monthly 75 (1968) 685–686", and Wolf raises "the question of whether every finitely generated group , which is not of exponential growth, necessarily has a nilpotent subgroup of finite index" (p. 422); Grigorchuk's groups of intermediate growth (1984) later answered that in the negative, while Gromov (1981) proved that polynomial growth does force a nilpotent subgroup of finite index. Chou's 1980 extension of the Milnor–Wolf theorem to elementary amenable groups, the mission Chou: elementary amenable groups on this platform, cites exactly this theorem. Wolf's paper is the subject of a companion mission.
Growth. For a finite subset of a group , Wolf's growth function (p. 426)
is the number of elements expressible as words of length based on , a word
having length . MilnorWolf.growthFunction S m
takes as the size of the ball Chou.wordBall S m of the published growth bundle, the set of
products of at most factors from . has
exponential growth, the published Chou.HasExponentialGrowth, if for some finite generating
set there is with for all ; Wolf shows (p. 434) that this does not
depend on .
Polycyclic groups. Wolf's Proposition 4.1 (p. 433) gives eleven equivalent conditions; the
definition used here is condition (1): "There is a normal series
with every quotient finite or
infinite cyclic." This is MilnorWolf.IsPolycyclic. A solvable group is
Mathlib's Group.IsSolvable: the derived series reaches the trivial subgroup.
Milnor's standing assumptions. The three lemmas concern a group extension where "we will always assume that is abelian and that is finitely generated." In the statements, is a finitely generated group, an abelian normal subgroup, and the quotient .
"Let be a solvable group which is not polycyclic, and a finite set of generators for . Then there exists an exponential lower bound for the growth function of ." Stated for an arbitrary finite generating set :
This is the goal. The constant is existentially quantified, so a sharper bound does not change the statement. The milestones are Milnor's three lemmas, in order, followed by one published Open theorem of the Chou mission that they prove: Chou's form of Lemmas 1 and 2, where the normal subgroup need not be abelian.
Milnor's Theorem is the half of the Milnor–Wolf theorem that reaches beyond polycyclic groups: with Wolf's polycyclic dichotomy it says that a finitely generated solvable group is either almost nilpotent, of polynomial growth, or of exponential growth, with nothing in between. That statement is what Chou's Theorem 3.2 extends to elementary amenable groups, and it is the reason a group of intermediate growth cannot be solvable or elementary amenable, the fact that placed Grigorchuk's groups outside those classes.
Formalizing it produces, besides the Theorem, the three lemmas as reusable library results: the subgroup spanned by the conjugates is finitely generated when is not of exponential growth; a normal subgroup with finitely presented quotient is normally generated by finitely many elements; and polycyclic-by-abelian without exponential growth is polycyclic. The proof is complete in the paper; nothing here is open mathematics. On this platform the Theorem and the lemmas are stated and unproved; Chou's mission holds the Open non-abelian form of Lemmas 1 and 2 and two Open reductions that resolve once this mission and the Wolf mission close their externals.
The obvious attempt, to bound the growth of below by the growth of a free subsemigroup found inside it, is not what Milnor does and does not obviously work for an arbitrary abelian-by-solvable extension. Milnor's argument turns the growth hypothesis into finite generation: among the expressions two must coincide, and the resulting relation expresses in terms of . The delicate step is running this over a whole set of normal generators of and over each of finitely many 's in turn, so that itself comes out finitely generated (Lemma 3), and then up the derived series of . In Lean the work is in Lemma 2, which needs the finite presentation of transported to a presentation on the images of chosen generators of , and in Lemma 3, which needs that a polycyclic group is finitely presented and that an extension of polycyclic groups is polycyclic.
Growth is measured on the closed balls of the published bundle Chou_Growth: Chou.wordBall S m
is the set of products of at most letters from , and is its cardinality
(a Nat.card, finite because is a Finset). "Not of exponential growth" is the negation of
the existential definition, so it is a statement about every finite generating set. Polycyclic is
Wolf's condition (1); the definition fixes the reading of "normal series". The abelian hypothesis on is Mathlib's
IsMulCommutative on the subgroup; finite generation and finite presentation are Mathlib's
Group.FG and Group.IsFinitelyPresented.
The Theorem's hypotheses are satisfiable: the trivial group is polycyclic, so "not polycyclic" excludes it, and a solvable non-polycyclic finitely generated group exists (the lamplighter group ). No hypothesis is vacuous and no definition makes a target trivially true.
The definitions of polycyclic group, polynomial growth and Wolf's growth exponents are
stated in the bundle MilnorWolf_Growth here because Milnor defers all definitions to Wolf; the
results of Wolf's paper, in particular the polycyclic dichotomy that combines with this Theorem
into the Milnor–Wolf theorem, belong to the companion mission. Nothing of Milnor's note is
omitted. Contributions welcome: proofs of the three lemmas and the Theorem, and general
library results they need, such as finite presentability of polycyclic groups.
Every consistency guarantee for an empirical-risk-minimization procedure — the Lasso, kernel ridge regression, maximum likelihood — ultimately rests on relating an empirical average to its population expectation, uniformly over the class of candidate functions or parameters being searched. Chapter 4 established the classical form of this connection: a uniform law of large numbers, bounding by an absolute quantity governed by the (unlocalized) complexity of . Such a bound is often wasteful: it treats a function with small population norm the same as one with large population norm, when intuitively the empirical and population norms of a small function should already agree closely. This mission formalizes the sharper, localized form of this uniform law — the same localization principle Chapter 13 used for nonparametric least squares, now applied directly to the empirical-versus-population norm comparison itself, giving relative rather than absolute control and recovering optimal convergence rates that the unlocalized theory misses.
Fix a probability distribution over a covariate space and i.i.d. samples . For , the population norm is and the empirical norm is ; by linearity of expectation, , so the question is how tightly concentrates around , uniformly over a function class . A class is star-shaped around the origin if , and -uniformly bounded if for every . The relevant complexity measure is the population localized Rademacher complexity
where are i.i.d. Rademacher signs independent of the samples — note that, unlike Chapter 13's Gaussian complexity for fixed design points, this expectation integrates out the randomness of the samples themselves, since this chapter treats as genuinely random throughout. A critical radius is any positive solution of .
Theorem 14.1 (goal). Given star-shaped and -uniformly bounded, and solving the critical inequality, for any ,
with probability at least ; and if additionally ,
with probability at least .
Theorem 14.1 is the technical engine behind two of the book's other sharp results: Example 14.2's derivation of the optimal rate for bounded quadratic function classes (where the unlocalized analogue of this theorem only achieves the slower rate), and, more broadly, every later argument in the book that needs to translate an empirical-norm guarantee (as produced directly by an M-estimator's optimality, e.g. Chapter 13's nonparametric least-squares bounds) into a population-norm guarantee, or vice versa. The gap between the "absolute" uniform law of Chapter 4 and the "relative" one here is exactly the difference between a bound that is only informative for functions of order-one population norm, and one that remains sharp arbitrarily close to the origin — which is precisely where a consistent estimator's error eventually lives. Formalizing the statement produces, for the first time on the platform, the localized-Rademacher-complexity vocabulary at the population level (as opposed to Chapter 13's fixed-design Gaussian-complexity version), reusable by any future mission needing to pass between empirical and population norms.
The naive approach — apply Hoeffding's inequality to for a fixed , then union-bound (or apply the unlocalized Rademacher-complexity uniform law of Chapter 4) over — gives a bound whose complexity term does not shrink as , since it uses the complexity of all of regardless of a given function's own size. This is exactly the sub-optimality Example 14.2 exhibits concretely: the naive bound gives rate where the truth is . The fix is not merely technical bookkeeping — it requires a genuine peeling argument over dyadic norm-scales (exactly as in Chapter 13's proof of Theorem 13.13), applying the localized complexity at the scale appropriate to each individual , and controlling the resulting geometric sum of tail probabilities across scales. A reader's first instinct — bound in terms of and substitute — is circular, since is itself the random quantity being controlled.
The covariate space X carries an arbitrary MeasurableSpace structure (no topology
needed for the statement); the sample sequence and the Rademacher signs are both represented
as families of measurable functions on a shared probability space Ω, with their joint
independence stated as a single IndepFun between the two vector-valued sequences (rather
than building a combined-index iIndepFun), since it is the two sequences — not each pair
of individual variables — whose independence the book invokes. The two conclusions of Theorem
14.1 are stated as a conjunction with the second gated behind its own extra hypothesis, never
collapsed into a single implication, since the book's own statement keeps them syntactically
and logically distinct (the second requires a strictly stronger and additional condition on
top of the first's). The universal constants (c1,c2,c0,c1',c2') are quantified before every
instance object, so they cannot secretly depend on the function class, sample size, or radius.
Every f ∈ F is required measurable (hF_meas, added in revision): the book's own framing
implicitly restricts to measurable, square-integrable f throughout (p. 454), and without this
hypothesis the population norm popNormSq, which appears directly in the goal's conclusion,
could silently take Mathlib's Bochner-integral junk value 0 for a non-measurable,
pointwise-bounded member of a star-shaped, uniformly-bounded F.
The trivializing formalization ruled out here is stating the localization constraint at the
empirical rather than population norm in popRademacherComplexity — this chapter's whole
point (contrast Chapter 13's Gn, correctly localized at the empirical norm since there the
design is fixed) is that 's localization is a population-level object,
precisely because the samples are random here. Welcome future contributions: Corollary 14.3's
covering-number sufficient condition for the empirical version of the critical inequality,
and Theorem 14.20's Lipschitz/strongly-convex cost-function uniform law, both deferred from
this mission (see STATUS.md) as they need substantial additional apparatus (metric entropy
integrals; cost functions and strong convexity) beyond what Theorem 14.1 itself requires.
Many high-dimensional data sets — gene-expression profiles, sensor networks, social interactions — come with no natural ordering of variables, only pairwise dependencies whose structure is itself the object of interest. A graphical model encodes these dependencies as an undirected graph: vertices are variables, and edges mark direct (conditional) dependence. Recovering the graph from samples — graphical model selection — is a combinatorial problem masquerading as a statistical one: there are candidate graphs on vertices, far too many to search directly. For Gaussian data, however, graph structure is exactly the sparsity pattern of the inverse covariance (precision) matrix, which turns graph selection into coupled sparse-regression problems — one per vertex — each of which the Lasso theory of Chapter 7 already knows how to solve. This mission formalizes the theorem, due to Meinshausen and Bühlmann (2006), that shows this reduction actually works: solving independent Lasso problems and combining the results recovers the exact graph with high probability, at a sample complexity governed by the same kind of incoherence condition that governs Lasso support recovery itself.
An undirected graphical model on a finite vertex set pairs a graph with a random vector . Two equivalent structural properties connect to (Theorem 11.8, Hammersley-Clifford): factorizes according to if its density is a product of nonnegative functions, one per clique of , each depending only on the variables in that clique (Definition 11.1); is Markov with respect to if, for every vertex cutset separating into disjoint pieces and , the sub-vectors and are conditionally independent given (Definition 11.5). For a strictly positive density, these are the same condition.
For a zero-mean -dimensional Gaussian vector with covariance and precision matrix , the graph structure is exactly the support of : . The neighborhood of each vertex is itself a vertex cutset (separating from everything else), so the conditional independence holds, and — by standard Gaussian conditioning — decomposes as a linear function of plus independent Gaussian noise, with regression coefficients supported exactly on . Neighborhood regression exploits this directly: for each vertex , solve the Lasso
read off , and combine the per-vertex estimates into a single edge set via the OR rule ( iff or ) or the more conservative AND rule (iff both hold). The relevant incoherence condition, analogous to Chapter 7's, is stated for a positive definite matrix and subset : is -incoherent with respect to if .
Theorem 11.8 (Hammersley-Clifford). Factorizes G p ↔ IsMarkov G X P for any strictly
positive density .
Theorem 11.12 (goal — graph selection consistency). Suppose for every , is -incoherent with respect to , and . With , the neighborhood-Lasso estimate combined via either rule satisfies, with probability at least :
Theorem 11.12 is the statistical justification for one of the two standard approaches to Gaussian graphical model selection (the other being the penalized-likelihood "graphical Lasso" of §11.2.1). Its significance is computational as much as statistical: rather than solving one -dimensional penalized-likelihood problem, neighborhood regression solves independent, embarrassingly parallel Lasso problems, each of dimension — a substantial practical advantage at scale, with (as this theorem shows) no loss in statistical guarantee. Formalizing it produces, for the first time on the platform, statement-level infrastructure for undirected graphical models (Hammersley-Clifford, the Markov property via vertex cutsets, neighborhood structure) together with the random-design analogue of the Lasso support-recovery machinery — a genuinely different technical regime from Chapter 7's fixed-design Lasso theory, since here the "design matrix" is itself Gaussian and statistically coupled to the response through the very covariance structure being estimated. As with the other missions in this series, only the statements are formalized here; the proofs (an extension of the primal-dual witness technique to random design, per the book's own proof sketch) are left as the draft goal for future proof contributions.
The proof of Theorem 7.21 (Chapter 7's Lasso support-recovery guarantee) is for a deterministic design matrix, with all randomness confined to the additive noise. Here the "design" is itself random and Gaussian, and — critically — it is statistically dependent on the very quantity (, encoded in 's support) the Lasso is trying to recover, since 's own covariance structure is exactly what the incoherence condition constrains. The naive approach of just conditioning on the realized design matrix and invoking Theorem 7.21 fails, because the deterministic-design incoherence condition would then need to hold for the sample covariance , not the population covariance that is actually assumed — and controlling the gap between sample and population incoherence under the joint (not fixed) randomness of predictors and response is exactly the extra step the book's proof needs, handled via an extension of the primal-dual witness technique that tracks both sources of randomness together.
The vertex set V is an arbitrary finite type; the covariate space for X is ℝ
throughout (all variables jointly Gaussian). The Gaussian design is characterized via its
one-dimensional projections (every linear combination is univariate Gaussian with the matching
variance) rather than via Mathlib's multivariate-Gaussian machinery directly, to keep the
definition self-contained. IsAlphaIncoherent's ambient index set is realized as a subset of
the full vertex type rather than as a literal submatrix, since the book's condition never
references an entry outside it. The theorem states the conclusion jointly for both the
OR-rule and AND-rule estimated edge sets on one shared high-probability event, matching "based
on either rule" literally rather than picking one. The trivializing formalization ruled out
here is treating the neighborhood-Lasso estimate as a fixed-design Lasso problem (silently
dropping the joint randomness of predictors and response) — every design realization in this
formalization is the actual random vector Xdes i ω, not a deterministic parameter, and the
Gaussian design hypothesis (IsIIDGaussianDesign) is stated over the same probability space
Ω as the least-squares residual. Theorem 11.8 (Hammersley–Clifford) is formalized only for the
continuous case — a random vector with a density with respect to Lebesgue measure — matching
what the Gaussian goal (Theorem 11.12) actually needs; the book's own Definition 11.1 also
permits a discrete (counting-measure) density, with the Ising model (Example 11.4) as a worked
instance, which this mission does not cover. Contributions welcome: the graphical Lasso's own
guarantees (Propositions 11.9, 11.10, deferred from this mission — see STATUS.md), and the
proof of Theorem 11.12 itself via the primal-dual witness extension the book sketches.
A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.
Fix a subset . For a standard Gaussian vector , the Gaussian width of is (Chapter 7), and the stable dimension of a bounded is up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of , which can jump discontinuously under a small perturbation of , unlike .
An Gaussian random matrix with i.i.d. entries is a random matrix each of whose entries is an independent standard normal random variable.
for every Gaussian random matrix with i.i.d. entries, every bounded containing the origin, and every , where is the Euclidean ball of radius centered at the origin. The probability is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.
Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every -dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube , for instance, is proportional to itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.
The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).
The natural first idea — bound directly using concentration of for each fixed — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one at a time, even with a union bound over a net of , does not obviously extend to the full convex hull without first controlling uniformly over both and on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment via a support- function duality argument (a convex body is pinned down by its support function, so bounding uniformly over on the sphere is exactly what is needed).
A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d.
, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image
of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence
with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth
convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same
ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as
08-matrix-deviation). The stable dimension is formalized directly as rather than via the book's literal (but only asymptotically equivalent, per
Exercise 7.6.1) definition through a squared Gaussian width — the goal theorem's own
proof uses only the inequality direction of that equivalence, and the goal's hypothesis already
carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution
preserves the theorem's exact truth content (see StableDimension's own doc-comment and
MODERATION_NOTES.md for the full argument) rather than approximating it.
Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that contains the origin; its proof opens by translating so that it does ("Translating if necessary, we can assume that contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.
This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that
if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random
projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones
should be cut rather than the goal substituted. All three are left out, not approximated, given
this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup,
GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development
needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions
are welcome on the goal theorem itself and, beyond this mission's current scope, on the three
named milestones.
The exponential function turns addition into multiplication. When its inputs are algebraic numbers, that elementary identity meets a rigid arithmetic boundary: distinct algebraic exponents cannot produce an algebraic linear relation among their exponentials. This principle is the Lindemann–Weierstrass theorem, one of the central results of transcendence theory. Its familiar consequences include the transcendence of Euler's number and of , and therefore the impossibility of squaring the circle with straightedge and compass.
The historical line runs from Hermite's 1873 proof that is transcendental, through Lindemann's 1882 proof that is transcendental, to Weierstrass's general formulation in 1885. Modern algebraic presentations organize the theorem around conjugates, Galois symmetry, algebraic integers, and an auxiliary-polynomial estimate. The Lean development formalized here follows Yuyang Zhao's mathlib contribution PR #28013, whose mathematical reference is Jacobson's Basic Algebra I, §4.12, Theorem 4.22.
A complex number is algebraic if it is a root of a nonzero polynomial with rational, equivalently integer, coefficients. A complex number is transcendental if it is not algebraic. Write for the field of algebraic complex numbers and for the complex exponential.
For a family in , injectivity means that distinct indices carry distinct exponents. A family is linearly independent over when every finite relation with algebraic coefficients has all . It is algebraically independent over when no nonzero multivariate polynomial with algebraic coefficients vanishes on the family.
The strongest target uses natural-number linear independence of : distinct finitely supported tuples of natural coefficients give distinct sums . This is exactly the condition needed to distinguish the exponent attached to every monomial.
For every injective algebraic family ,
This includes the finite Lindemann–Weierstrass relation as its load-bearing finite core.
For every nonzero algebraic ,
The same development records the transcendence of , the transcendence of , and the transcendence of every nonzero principal logarithm of an algebraic complex number.
Let be algebraic and let be injective. The proved Hermite–Lindemann theorem discharges the formerly conditional winding interface and gives
The integer labels are inputs to this arithmetic theorem. A separate topological or dynamical development is responsible for producing them as winding numbers.
If is a natural-number-linearly-independent family in , then
This is the mission's capstone because it turns the linear theorem into a reusable multivariate interface: polynomial monomials become exponentials of distinct natural combinations.
The theorem separates two kinds of structure that otherwise coexist in the exponential map. The character law supplies exact multiplicative relations, but the theorem rules out unintended linear relations over algebraic coefficients. For integer winding consumers, one algebraic nonzero generator produces the two-sided phase family ; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over . Winding supplies the discrete labels, while transcendence supplies arithmetic distinguishability.
The formalization contributes more than the named corollaries. It exposes a finite exponential-relation theorem, the algebraic orbit-sum reduction used by it, and general infinite-family interfaces. These components can be reused in later work on exponential polynomials, logarithms of algebraic numbers, and arithmetic representations of topological charges.
This mission formalizes a known theorem; it is not presented as an open mathematical problem. The private theorem graph is already machine-checked against Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The mission records that proof as an independently inspectable dependency graph before any later upstream integration.
The analytic approximation alone is insufficient. It produces a small complex error, but smallness does not imply vanishing, and taking a field norm does not repair the gap because the other embeddings have no corresponding analytic bound. Likewise, a field automorphism of cannot be moved through the complex exponential as an algebraic operation.
The formal statement therefore requires both an analytic and an arithmetic layer. The arithmetic layer must replace a hypothetical algebraic relation by a Galois-stable relation with integer data and a genuinely nonzero integer contribution. The analytic layer must then make the absolute value of that integer strictly less than one. Managing conjugacy classes, root multisets, denominator clearing, finite supports, and the asymptotic prime choice in one kernel-checked chain is the central formalization difficulty.
The development is pinned to Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Algebraic complex numbers are represented by integralClosure ℚ ℂ; transcendence corollaries are stated with Transcendental ℤ, which is equivalent to the usual absence of a nonzero integer polynomial relation. The finite theorem uses Fintype; the general linear and algebraic independence theorems permit arbitrary universe-zero index types and reduce relations to finite support internally.
The auxiliary algebraic theorem is stated over an arbitrary algebraically closed field over and a multiplicative character on its additive group. The analytic consumer specializes this character to the complex exponential. Two small support modules provide quotient lifting for finitely supported functions and evaluation identities for symmetric multivariate polynomials.
The condition in Hermite–Lindemann is load-bearing: is algebraic. Injectivity of the exponent family is load-bearing for linear independence: duplicate exponents duplicate vectors. The capstone's natural-number linear independence is not algebraic independence of the exponents and must not be silently strengthened or weakened.
The source is an attributed, compatibility-preserving port of the May 2026 Lean 4.30 snapshot of mathlib PR #28013. Platform packaging uses the conservative ASCII rename linearIndependent_exp_finite for the upstream private helper and phi for one Greek binder. The elaborated theorem types were compared against the upstream source; these are naming changes only.
Integer winding is one of the simplest ways that continuous geometry produces discrete arithmetic. A loop in the circle has an integer winding number, while the complex exponential turns an additive parameter into a multiplicative phase. This mission asks what arithmetic information survives when those two constructions are combined. Its answer is a conditional but exact bridge: once Hermite--Lindemann supplies one transcendental phase, distinct integer winding labels produce a linearly independent family over the algebraic numbers.
The transcendence input is classical. Lindemann proved in 1882 that the exponential of a nonzero algebraic number is transcendental, and Weierstrass subsequently established the broader theorem now called Lindemann--Weierstrass. A modern statement appears as Theorem 1.1 of Javier Fresán's notes on the Hermite--Lindemann--Weierstrass theorem: exponentials of rationally linearly independent algebraic numbers are algebraically independent. The present mission deliberately does not formalize that analytic theorem. It isolates and formalizes the algebraic consumer that becomes available immediately after its one-variable consequence is supplied.
Let be a field extension and let . For every integer , the Laurent power is defined when . An element is transcendental over when no nonzero polynomial with coefficients in vanishes at . The first target proves that transcendence rules out every finite -linear relation among the two-sided family
For a complex parameter , define the integer exponential character
It satisfies and the character law . The mission registers the Hermite--Lindemann assertion as an explicit proposition: for every nonzero complex number algebraic over , is transcendental over .
Write for the subfield of complex numbers algebraic over . If is algebraic, then is nonzero and algebraic. Hermite--Lindemann therefore makes transcendental, first over and then over . Integer phases are exactly the Laurent powers .
For every field extension and every transcendental over ,
For every and ,
Assuming Hermite--Lindemann, if is nonzero and algebraic over , then
For any injective integer label under the same hypotheses,
The label may be supplied downstream by a winding-number construction, a self-linking number, or another independently proved integer invariant. This packet consumes the integer; it does not manufacture winding from continuous data.
The result separates topology from arithmetic cleanly. A geometric or dynamical development is responsible for producing an integer label and proving when labels are distinct. The present mission then turns that discrete distinction into a strong arithmetic conclusion about the corresponding complex phases. Because the Laurent-power theorem is stated over an arbitrary field extension, it is reusable outside circle topology and transcendence theory.
The formalization also records the exact limits of the conclusion. The phase with label zero is and is not individually transcendental. Repeated winding labels force repeated vectors and therefore destroy linear independence. At zero coupling every phase collapses to . Finally, the character law supplies multiplicative relations, so the indexed phases are not being claimed algebraically independent as separate variables. The theorem is linear independence over , not algebraic independence of an unconstrained family.
The main algebraic difficulty is the presence of negative exponents. Ordinary polynomial evaluation detects finite relations among nonnegative powers, but an integer-indexed relation is a Laurent polynomial. The formal statement must ensure that evaluation of Laurent polynomials at a nonzero transcendental element is injective. It must also transport transcendence from to the algebraic closure embedded in without replacing the registered field by an informal copy.
The transcendence theorem itself is a much larger analytic and algebraic-number-theoretic development. Treating it as an explicit hypothesis is therefore load-bearing: no unproved axiom or hidden instance may assert Hermite--Lindemann. Full Lindemann--Weierstrass is stronger than needed for this one-parameter family, since all exponents are integer multiples of a single algebraic generator.
The mission targets Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f with Lean 4.30. Laurent polynomials are Mathlib's finitely supported integer-indexed monoid algebra. The algebraic numbers are represented by algebraicClosure ℚ ℂ, the subtype of complex numbers algebraic over the rationals. Linear independence is the ordinary Mathlib module-theoretic predicate.
The reusable core proves Laurent-power independence for arbitrary fields and arbitrary field extensions. The complex consumer uses Mathlib's complex exponential, the algebraicity of , and the algebraic-closure transcendence transfer. The mission includes explicit degenerate controls for zero coupling and duplicate labels. It does not prove Hermite--Lindemann, Lindemann--Weierstrass, transcendence of , a topological winding theorem, or algebraic independence of the phase family.
Mathlib.Algebra.Polynomial.Laurent, Laurent-polynomial definitions and evaluation. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Laurent.htmlThe central limit theorem says that converges to a normal random variable. Donsker's theorem says something much stronger: the whole rescaled path of the random walk converges to the whole path of a Brownian motion, as a random element of .
The payoff is a machine. Once in , every functional of the path that is continuous — or merely continuous at almost every Brownian path — transfers automatically. The maximum of the walk converges to the maximum of Brownian motion; the fraction of time the walk spends above a level converges to the corresponding occupation time; the last zero before time converges to the last Brownian zero before time , which is how the arcsine law escapes the simple random walk it was proved for. This is the invariance principle of Erdős and Kac: the asymptotic behaviour of a functional of should not depend on the step distribution, as long as the central limit theorem applies.
Chapter 8 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) proves this by embedding rather than by the usual tightness argument. Skorokhod's representation theorem puts a mean-zero, finite-variance random variable inside a Brownian motion as the value at a stopping time; iterating puts the whole walk inside one Brownian motion at a sequence of stopping times whose gaps are i.i.d.; and the law of large numbers then forces the embedded walk to be uniformly close to the Brownian path.
Let be i.i.d. with mean and variance , and . Define to be at integer and linear in between, and set
a random element of , the continuous functions on the unit interval with the uniform norm and its Borel -algebra.
On the Brownian side, let be a Brownian motion, and write for its restriction to , again a random element of .
that is, the laws of on converge weakly to the law of Brownian motion. This is a statement about measures on a function space, not about finite-dimensional marginals: it is exactly the extra content over the central limit theorem.
Theorem 8.1.1, Skorokhod's representation theorem: a mean-zero, square-integrable law is the law of for a stopping time with ; Theorem 8.1.2, the embedding of the whole walk, giving stopping times with distributed as the walk and with i.i.d. gaps; Theorem 8.1.5, the continuous mapping theorem for almost surely continuous functionals; and its two workhorse instances, Example 8.1.6 on maxima and Example 8.1.8 on occupation times of half-lines.
The results themselves. Donsker's theorem is the reason the arcsine law, the distribution of the maximum, and the occupation-time law are universal rather than artefacts of the simple random walk for which they were first computed. It is also the prototype for every later functional limit theorem — for martingales in Durrett's section 8.2, for stationary sequences in 8.3, for the empirical process converging to a Brownian bridge in 8.4.
Skorokhod's embedding deserves separate billing. It says any centred law with finite variance sits inside Brownian motion, which is what makes the path-space comparison possible at all, and it is the tool behind the law of the iterated logarithm in Durrett's section 8.5. The construction is a two-point mixture: write the law as a mixture of two-point laws with mean zero, use the exit time of for each, and the exit-time identity integrates to .
Formalizing them. Mathlib has the i.i.d. central limit theorem, convergence in distribution for
random elements of an arbitrary topological space (TendstoInDistribution, with the continuous
mapping theorem and Slutsky), Brownian motion as a process with its invariances, and the machinery
of stopping times for filtered spaces. It has no functional limit theorem of any kind, no Wiener
measure on , no Skorokhod embedding, and no continuous-time optional stopping. Nothing in
the library relates a random walk to a Brownian path.
The goal is the hardest item in this series, and the embedding route is the reason the mission is stated the way it is. Durrett's proof: with and stopping times realizing as , Lemma 8.1.9 says that if in probability for each , then in probability. The hypothesis is the weak law applied to the i.i.d. gaps of Theorem 8.1.2 after Brownian scaling; the conclusion plus the converging-together lemma gives the theorem. The work is uniform control of the Brownian path over shrinking time windows — the modulus of continuity — together with the bookkeeping of the polygonal interpolation.
Skorokhod's theorem needs the two exit-time facts for Brownian motion, Durrett's Theorems 7.5.3 and 7.5.5: takes the values and with probabilities and , and . Both come from optional stopping applied to and , and continuous-time optional stopping is itself not in the library. The mixture identity,
is elementary but needs Fubini and the two expressions for .
Theorem 8.1.5 is the Mann–Wald theorem in the form that allows a discontinuous : Mathlib's
TendstoInDistribution.continuous_comp handles genuinely continuous maps, and the extension to maps
continuous almost everywhere with respect to the limit law is the milestone. Given it, the two
examples are short — the maximum is continuous outright, and the occupation-time functional is
continuous at every path spending no time at the level , which Fubini shows is almost every
Brownian path.
is C(Set.Icc (0:ℝ) 1, ℝ), whose compact-open topology is the uniform one because the
domain is compact, with the Borel -algebra — Mathlib has no measurable-space instance on a
space of continuous maps, so the mission supplies it, and a BorelSpace instance with it.
The polygonal interpolation is written as a finite sum,
which agrees with at integer and is linear in between, and is manifestly continuous,
so walkPath is a genuine element of with no side condition. Both properties were proved
in Lean before publishing rather than assumed. Indexing is from zero, so .
The Brownian limit is brownianPath B, the restriction of the path to . Restriction is a
total function: it returns the zero path for a discontinuous argument. That junk branch is never
reached, because every statement assumes every path of is continuous, not merely almost
every one — one may always modify a Brownian motion on a null set to achieve this, and Durrett's
canonical construction on has it by definition. Without it there would be no
-valued random variable to speak of.
Weak convergence is Mathlib's TendstoInDistribution, the same predicate mission II used for the
Lindeberg–Feller theorem, instantiated at rather than at .
Skorokhod's theorem and the embedding of the walk are stated as existence of a probability space
carrying the Brownian motion, a filtration and the stopping times. This is how Durrett states them
— the construction needs an independent pair alongside the Brownian motion, and he notes
himself that is a stopping time only for the enlarged filtration. The filtration is
therefore an explicit family that is increasing, sits inside the ambient -field, and
contains — the pastSigma of mission V, which this mission imports as a
reference. The stopping-time property is {T ≤ t} ∈ F_t, stated directly rather than through a
bundled filtration structure.
Theorem 8.1.2's conclusion "" is read as equality of the laws of the whole processes: the push-forward of equals the law of the partial-sum process of an i.i.d. sequence with step law , taken on the infinite product measure. The gaps are required to be independent and identically distributed, as the book says.
The counting in Example 8.1.8 is a sum of indicators rather than a filtered cardinality, to keep a decidability side condition out of the statement, and the limit is the Lebesgue measure of as a real number. Example 8.1.6 takes the maximum over , which includes , and the limit is the supremum of over , attained because the path is continuous on a compact interval.
Existence of a Brownian motion is a hypothesis, not a claim, exactly as in mission V, except in Theorems 8.1.1 and 8.1.2 where the existence of a suitable space is the content of the statement and a Brownian motion must be produced; that is Durrett's Theorem 7.1.1, which the library does not yet have, so those two items subsume it.
Contributions welcome beyond the listed items: Lemma 8.1.9 on its own; Theorem 8.1.3, the CLT derived from the embedding; Example 8.1.7, the last zero before time and the arcsine law; continuous-time optional stopping and the exit identities 7.5.3 and 7.5.5 that Skorokhod's theorem rests on; the extension to ; and the martingale, stationary-sequence and empirical-process versions of sections 8.2 to 8.4.
Phase winding is an integer attached to a circle-valued field on a closed spatial cycle. It distinguishes configurations that cannot be continuously deformed into one another while remaining circle-valued and spatially continuous. In oscillator and spin models this integer is often described informally as conserved by smooth evolution, while changes of winding are attributed to phase slips, vortices, singularities, or branch-cut crossings. The purpose of this mission is to turn that informal division into an exact Lean interface.
The continuum and finite-lattice settings must be separated. A jointly continuous field on a spatial circle really does provide a homotopy of circle maps, so its degree is invariant. A finite list of continuously moving vertex phases does not by itself determine a continuous field on the geometric realization of the lattice. Principal shortest-arc interpolation becomes ambiguous at antipodal bonds, and the corresponding discrete winding can jump even though every vertex phase remains continuous. The mission therefore treats winding as a first integral only on the regular sector and records every failure of regularity through an integer reset ledger.
This distinction is relevant to circle-valued reductions of the Kuramoto model, the finite XY model, and Lohe-type dynamics. Kuramoto's original synchronization model concerns coupled phase oscillators, while Lohe's non-Abelian extension replaces phases by group-valued variables. A model-specific conservation theorem is justified only after the dynamics has been connected to an actual circle-valued spatial loop or to the registered finite principal-branch interface.
A circle loop is a continuous map from a closed parameter interval to whose two endpoints agree. Its winding number is the integer obtained from the endpoint of a lift to the universal cover . When the loop's basepoint moves during a deformation, the loop is normalized by the inverse of its value at the chosen spatial basepoint; this produces a based loop without changing its winding.
A continuous Circle-field segment is a jointly continuous map
Each time slice is a spatial loop. Such a segment has no branch-cut convention: it is intrinsic topological data.
For a finite directed edge system (including a finite periodic lattice), a state assigns a real lift to every vertex. Each oriented edge receives an integer principal turn. A state is branch regular when no stored edge is antipodal. A coherent finite reset ledger stores successive principal-turn cochains and defines the reset . For a certified closed integer cycle , the pairing is its registered winding jump.
A Kuramoto, XY, or Lohe consumer must supply the missing model-specific data. For a continuum consumer this is a jointly continuous circle-valued field. For a finite consumer it is a continuous vertex trajectory together with branch regularity away from registered events. A Lohe consumer additionally needs a continuous Circle readout or invariant Circle carrier; preservation of a rotor constraint alone does not provide that reduction.
For every jointly continuous Circle-field segment, the two endpoint loops have equal winding:
The statement must cover moving loop basepoints through explicit normalization. Winding is defined directly from Mathlib's exponential covering map as the floor of the zero-based lift endpoint divided by .
For every finite directed principal-phase trajectory on a preconnected time domain that remains branch regular, every registered integer-chain winding is constant:
Continuity of the vertex phases alone is not a sufficient hypothesis and must not appear as a replacement for branch regularity or spatial interpolation.
For a finite coherent ledger with steps , endpoint winding change equals the sum of the reset periods:
The conservation theorem is the empty-ledger or zero-period special case. The statement is an exact integer identity and does not assert an energy lower bound, vortex separation, or a thermodynamic-limit result.
The generic dynamics adapter requires a jointly continuous ambient-state segment, a registered carrier containing it, closed spatial profiles, and a continuous readout from that carrier to the Circle. Kuramoto/XY or Lohe consumers must separately prove those hypotheses for their model. A second fence states that a global continuous readout from a simply connected carrier maps every loop to a nullhomotopic Circle loop; nonzero Lohe winding therefore requires a separately registered non-simply-connected carrier, such as a preserved orbit, or a different explicit interface.
The resulting theorem family makes precise the statement that winding obstructs unwinding. In the intrinsic continuum setting, winding cannot change while the field remains a continuous -valued map. In the finite principal-branch setting, winding is piecewise constant and every change has an exact integer certificate. This separates a topological conservation law from the physical or analytic question of how much energy is needed to realize a certificate.
For formalization, the mission supplies a reusable boundary between topology and dynamics. A dynamics development can establish continuity and carrier preservation without reimplementing covering-space winding. A lattice development can consume the same integer through reset cochains without claiming that a vertex-only path is a homotopy of spatial loops. Later energy-barrier, vortex, and transport results can depend on the reset balance rather than on an informal conservation principle.
The principal difficulty is that several superficially similar notions of continuity have different consequences. Continuity in time of finitely many vertex phases is continuity into the configuration torus , which is connected and does not preserve a principal-edge winding sector. Continuity of a map on time times the geometric spatial cycle is stronger. A formal statement that confuses them would make the desired theorem false.
There are two additional interface risks. First, the canonical Circle lift is based, whereas a physical phase field normally has a moving value at the chosen spatial origin. Second, the current Lohe development establishes algebraic identities and infinitesimal rotor preservation, not a global continuous flow in a selected Circle subgroup. These distinctions remain visible in the theorem hypotheses.
The mission targets Lean 4.30 with Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, matching the cited LeanProofs development. It reuses Mathlib's unit interval, continuous maps, path homotopies, Circle covering map, local constancy, and finite sums. The continuum statement concerns spatial only. The finite theorem is graph-generic: it uses finite oriented edges, integer edge cochains, certified closed integer cycles, coherent successive reset states, and branch regularity on a preconnected time domain.
The scope excludes ODE or PDE existence and uniqueness, preservation of a Circle carrier by a particular Lohe vector field, extraction of a coherent reset ledger from a physical event trajectory, arbitrary graph interpolation, accumulating reset times, thermodynamic limits, and energetic barriers. Those may be attached later through explicit interfaces. No theorem claims global winding conservation for an unrestricted finite vertex trajectory, and no theorem identifies group-valued Lohe motion with Circle motion without a declared continuous readout.
b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleFundamentalGroupWindingV1.lean#L81b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/StatMech/FiniteTorusPrincipalResetEventV1.lean#L152-L167b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleWindingTranslationHolonomyV1.lean#L107Formalize the corrected theory of flavor mixing angles in the su(3) Cartan sector of Cl(6,0), replacing the retired Killing-form/GUT normalization story. The mechanism: T3 and T8 commute, so mixing is carried not by their commutator but by the complete ordered products retained in grade 4. Milestone path: (M1) the grade-4 projection Pi4: Sym^2(A2) -> span{AB,AC,BC} is an isomorphism, with Pi4(e3^2) = -AB, Pi4(e3 e8) = (BC-AC)/sqrt 3, Pi4(e8^2) = (1/3)AB - (2/3)AC - (2/3)BC and tan(2 theta) = sqrt 3 (w-v)/(2u-v-w) for a retained grade-4 field G4 = u AB + v AC + w BC. (M2) the bridge: the primitive finite-T8 Cartan vector Phi = t e3 + e8 with t = sqrt 5 - 2 (the exact r = 16 closure) has grade-4 image exactly the rank-one family tensor phi phi^T; its traceless part is t[[-2,1],[1,2]], the Cabibbo family tensor up to one family-state sign, giving theta_C = arctan(sqrt 5 - 2) ~ 13.28 degrees; the grade-4 tensor has the same Sym2 structure as a left-handed Yukawa Gram operator M M^dagger. (M3, guarded goal) identify the r = 16 tensor with the relative left-family Yukawa tensor, closing the Sym2/Gram bridge. Foundational lemmas (A2 Cartan plane with [T3,T8] = 0, the complete 7-bracket su(3) table, grade-4 square residuals, grade-6 cubic channel) are landed in the LeanProofs repository and will be contributed as importable platform nodes ahead of the milestones. Recorded provenance: HAM memories #2848 (FullGradeCartanMixingTensorV1, 2026-09-14) and #3099 (CabibboGramSym2BridgeV1, 2026-09-17), proof DAG galaxy.proof-dag.v1 grade4-cartan-mixing.
A real lift of a circle-valued phase records both a principal representative and an integer sheet. This packet isolates the neutral arithmetic of that lifted reading before any physical interpretation as time, dynamics, causality, or a preferred vacuum.
A clock candidate is a function from an arbitrary event type to the real universal cover of the circle. Principalization separates each real value into a representative modulo and an integer sheet. Real origin shifts, integral deck shifts, and orientation reversal are treated as distinct transformations.
The intended packet covers principal-ledger reconstruction, the conditional strict order induced by an injective or monotone lift, affine-origin and deck freedom, orientation reversal, an adapter from separately established circle winding to an integer clock turn, and a scalar power-law integrability boundary.
The exact target statements remain subject to reconciliation with the immutable LeanProofs source before this private draft is submitted. In particular, no arithmetic quotient identity may be presented as the full Circle winding adapter, and no scalar integrability theorem may be interpreted as a PDE blow-up result.
This separates universal-cover bookkeeping from later consumers. A subsequent packet may connect the ledger to reset cochains, null-pair torsors, or dynamics only through explicit adapters.
The main risks are sign conventions at the principal cut, degeneracy on empty event types, confusion between the continuous real origin action and the integral deck action, and circular definitions that manufacture winding from the desired clock integer.
The development targets Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. It makes no claim of monotone physical time, dynamical selection, causal order, global foliation, PDE existence, singularity formation, or a canonical origin or orientation.
b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/WindingProtoTimeV1Targets.leanb656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleFundamentalGroupWindingV1.leanThe first three missions in this programme settle the ordinary magic squares end to end: Mission I proved MacMahon's count , Mission II his semi-magic count , and Mission III classified the normal squares (Lo Shu uniqueness). All three work with the plain magic condition.
This mission counts the two special classes that are singled out by requiring more than magicness, in the opposite directions one expects:
Writing and for the two counting functions, the goal is to determine both for every line sum :
Everything is built on the vocabulary of MagicSquares (Mission I):
IsPanMagic — semi-magic, and every broken diagonal in both directions has
the line sum, indices read modulo ;IsSymmetric — ;panMagicCount, symmetricMagicCount — the cardinalities of the two filtered
finsets of arrays over Fin (t+1), which is lossless because every entry of a
square of line sum is at most .The new definition module MagicSquaresSpecial3 records the two explicit shapes
that the proofs produce: constSquare3 e (the array all of whose entries are
, read over the ambient Fin (3e+1)) and
together with the parameter set symmParamSet e and its
cardinality symmParamCount e.
special_three_count: for every natural number , the pair of equalities
displayed above. The proof splits on and reduces to four child nodes.
pan_three_card). Writing the
array as , the twelve line equations form a linear system
whose only nonnegative solution is . So .symmetric_magic_three_classify).
Symmetry identifies three pairs of entries, leaving five free cells and five
line equations; the anti-diagonal forces , and the rows give
.symm_three_bij). Sending a symmetric magic
square of line sum to is a bijection onto
; hence .pan_three_otherwise,
symm_three_otherwise). Both classes consist of magic squares, and an
order-three magic square has centre (center_of_order_three), so
forces both counts to vanish.The results. The three order-three counts behave completely differently in the same parameter: MacMahon's is quadratic, the symmetric count is linear, and the panmagic count is constant. That contrast is the point of the order-three study — order three is small enough to be completely understood, and the special classes show how differently the two natural strengthenings of the magic condition act. It is also exactly what is lost at order four, where no closed form is known for any of the three.
Formalizing them. The mathematical content is elementary, but the two classes require genuinely different proof techniques, which is what makes the mission worth formalizing:
omega call. The only work is exposing the twelve
equations, which requires reducing the index arithmetic and
on Fin 3.Truncated subtraction, in the admissibility direction. The classification
M = symmMagic3 e (M 0 0) is true for every , without any bound on ;
the bound only appears when asking which members of the family are squares of
line sum . Keeping those two statements apart is what makes the bijection
proof manageable: classification is a pure omega computation, while
admissibility is a one-line argument that forces .
Finite but not decidable. panMagicCount and symmetricMagicCount are
cardinalities of filtered finsets over a function type, so the proofs cannot be
decide or norm_num — the platform forbids native_decide in any case. Both
counting theorems are therefore stated as Finset.card_bij / card_eq_one
arguments over explicit bijections, not as finite evaluations.
center_of_order_three.Fin 3 with a single omega.Central values of twists of elliptic-curve and modular-form -functions govern arithmetic questions ranging from Mordell--Weil ranks to the distribution of nonvanishing twists. Classical Iwasawa theory organizes twists whose conductors grow vertically through powers of one prime. Kriz and Nordentoft introduce a horizontal analogue in which the order of the character is fixed while its conductor acquires new prime factors. Their paper Horizontal p-adic L-functions constructs measures encoding these twists and proves a structure theorem that forces quantitative nonvanishing.
The mission formalizes the paper's common mechanism behind its nonvanishing theorems: Fourier theory of horizontal measures, norm-compatible modular-symbol theta elements, interpolation of central values, and propagation from nonzero measures to logarithmic-power lower bounds. The elliptic-curve statements in Theorems 1.1 and 1.2 are obtained in the paper by specializing this mechanism to weight-two newforms and adding the stated Galois-representation hypotheses.
Fix a prime . The digit group is the compact product
A continuous character of has finite image and factors through a finite product. For a complete algebraically closed nonarchimedean field of residue characteristic , a horizontal measure is represented in Lean by a continuous -linear functional on the Banach space . Its Fourier transform is
The integral measures arising from the digit Iwasawa algebra have Fourier norms in a discrete geometric lattice. This is recorded explicitly by HasDiscreteFourierNorm; it is the norm-language counterpart of the discrete valuation hypothesis used in Corollary 2.9.
On the arithmetic side, modular symbols produce theta elements at finite squarefree conductors. Their projection maps do not initially form a compatible inverse system: an Euler factor appears each time a prime is removed. At an orderly prime this factor is a unit, so normalization produces a compatible system and hence a horizontal -adic -function. Evaluation at a character gives the modified central -value of the corresponding twist.
For every nonzero integral horizontal measure , there is a finite set of characters and a constant such that
for some , for every continuous character . If interpolates modified central values, these corrected values are nonzero and have optimal -adic size. This is Theorem 1.6, equivalently the digit-algebra case of Corollary 2.9, combined with Corollary 5.4.
For a modular elliptic curve over , the normalized theta system is assembled into the horizontal -adic -function of Definition 5.3 and shown to satisfy Corollary 5.4. The final milestones then specialize the structure and propagation theorems to prove Theorems 1.1 and 1.2 (assuming modularity), retaining the three alternative hypotheses of Theorem 1.1 and the jointly-good hypothesis for simultaneous nonvanishing in Theorem 1.2.
If a fixed-order family has counting function bounded below by and every character is related to a nonvanishing one by one of finitely many conductor-bounded corrections, the same lower bound holds for the nonvanishing subfamily. This isolates the formal content of Theorem 5.9 used in the applications of Section 5.4.
The structure theorem replaces one-variable Weierstrass preparation in an infinite-dimensional, non-noetherian Iwasawa algebra. It shows that the zero set of a nonzero horizontal measure is rigid enough that finitely many translations detect an optimal Fourier value everywhere. Through interpolation, this converts a single nonzero horizontal -adic -function into infinitely many nonzero complex central values with a quantitative lower bound.
A formal proof will add reusable infrastructure for nonarchimedean Fourier analysis on profinite products, finite group rings, inverse systems of theta elements, and character-counting asymptotics. None of these results currently has a machine-checked proof in Mathlib. The development is arranged so the analytic structure theorem and the modular-symbol construction can be attacked independently.
The central obstacle is that the horizontal Iwasawa algebra is neither noetherian nor reduced. A direct compactness or finite-generation argument on its spectrum is unavailable. At finite level, Fourier inversion introduces the group order into the valuation estimates; globally, one must control compatible finite quotients while keeping the exceptional correcting set finite. The arithmetic half has a separate normalization problem: raw theta elements satisfy norm relations only up to Euler factors, and interpolation must track imprimitive characters and the removed Euler factors exactly.
The first version works with the exponent- digit group , which is the setting of Theorem 1.6. Characters take values in the unit group of a complete algebraically closed ultrametric field . Measures are continuous linear functionals on , and discreteness of integral Fourier values is an explicit hypothesis. The definition does not assume the finite-correction conclusion.
The modular-form layer is exposed through RawThetaSystem, ThetaSystem, and InterpolationDatum. Milestones must construct these data from genuine modular symbols and prove their norm and interpolation fields; merely postulating the desired nonvanishing values does not satisfy the goal. The quantitative statement uses an explicit eventual lower bound rather than asymptotic notation hidden behind an uninterpreted predicate.
The new definition node isolates the horizontal Iwasawa algebra and the interpolation interface. The first new milestone constructs a nonzero horizontal -adic -function . The second milestone assumes such a pair and combines the horizontal-measure structure theorem, the Friedberg--Hoffstein quadratic seed, Corollary 5.10, and fixed-order character counting to obtain the lower bound in Theorem 1.1(1). The mission goal then follows immediately by applying the existence milestone and passing its witness to the implication milestone.
Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.
Work in an arbitrary abelian group (Lean: AddCommGroup G). For finite
, the additive energy counts quadruples
with ; the trivial maximum is when
. The sumset is , and the difference set
is defined pointwise. A set has small doubling when is
linear in . The Lean development uses Finset.addEnergy and
Finset.addConvolution from Mathlib.
A bipartite graph here is an edge set of type Finset (G × G) with
, not a Mathlib SimpleGraph; solvers should state
graph hypotheses that way. Given such an , the partial sumset
is , following Tao–Vu Definition 2.28.
The mission goal is the two-set (equal-cardinality) form:
This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps and existential; the explicit-constant variant is proved separately in the mission with .
The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.
The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.
Formalizing it matters because the constants are the content: the development
tracks explicit constants through dependent random choice (graph level
and ; energy level
and ),
which paper proofs often leave implicit. Fox–Sudakov state the application for
sets of integers; the formalization is over an arbitrary AddCommGroup, with
no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1)
contains no BSG statement, so this fills a genuine upstream gap.
The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.
Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's and terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.
Sets are Finset G in an AddCommGroup G with DecidableEq; energy is
Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise
sumset and difference operations from open scoped Pointwise. Density
hypotheses are stated with explicit real constants. The counting lemmas at the
bottom of the development (sum_addConvolution_eq_card_product,
path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are
unconditional; the statements that need them carry the nonemptiness,
equal-cardinality and density hypotheses that exclude degenerate zero-energy
configurations. Welcome contributions: the single-set polynomial
Freiman–Ruzsa consequences, and non-abelian variants.
Finset.pluennecke_ruzsa_inequality_nsmul_add;
see G. Petridis, New proofs of Plünnecke-type estimates for product sets in
groups, Combinatorica 32 (2012), 721–733
(arXiv:1101.3507).Combinatorics/Additive/BalogSzemerediGowers and
BSGEnergyToGraph.The first two missions in this programme counted order-three squares. Mission I proved MacMahon's magic count and Mission II his semi-magic count . What neither does is classify: counting tells you how many squares there are, but not what they look like.
This mission closes that gap for the most classical case of all. A normal magic square of order three is a array containing each of exactly once, whose rows, columns and two main diagonals all sum to the magic constant . The statement to be proved is the uniqueness of the Lo Shu square:
every normal magic square of order three is one of the eight images of under the symmetry group of the square.
In particular there are exactly of them, and they form a single orbit under the dihedral group .
MacMahon's parametrization (already formalized in MagicSquaresParam3) writes
every order-three magic square of line sum as
with ranging over the finite admissible set paramSet e. For a normal
square the magic constant is , so and the centre entry is .
Normality (IsNormal) means every entry lies in and the nine entries
are pairwise distinct — equivalently, they are a permutation of .
together with the identification of those eight parameter pairs. By the
bijection magic_three_param_bij this is exactly the statement that there are
eight normal magic squares of order three, i.e. that Lo Shu is unique up to the
symmetry group of the square.
magic_three_normal_classify). Within that range,
is normal exactly when is one ofThe eight surviving pairs are precisely those with distinct corners of
the Lo Shu square; the excluded ones are those with , for which the
entry collides with the centre .
3. Converse (magic_three_normal_converse). Each of the eight pairs really
does give a normal square.
The result itself. The uniqueness of Lo Shu is the oldest non-trivial classification in combinatorics — it is the order-three case of the classification problem for magic squares, and the reason is special: for there are normal squares (up to symmetry) and for no classification is known. Formalizing it shows that the counting machinery of Missions I and II can be turned around and used as a classification tool: the parametrization plus a finite verification give the complete list, not just the cardinality.
Formalizing it. The whole proof is a finite case check over parameter pairs, so the mathematical content is small and the formalization difficulty is concentrated in making the finiteness usable. Two things have to be arranged before automation can see the problem:
IsNormal is stated with a Function.Injective, which is not decidable
as stated; it must first be rewritten into an explicit conjunction of
entrywise bounds and pairwise inequalities over Fin 3.Fin 3 do not unfold by simp alone; one needs
Fin.forall_fin_succ to expand them before norm_num can decide the
resulting ground instances.Finiteness must be manufactured. Nothing in IsNormal mentions a bound on
or , so the first step is to derive from the entrywise
bounds of normality. Skipping it leaves an infinite search that interval_cases
cannot start.
Truncated subtraction. The parametrization is written over , so entries such as and truncate at zero. Every ground instance must be evaluated with the truncation in place — which is why the classification is carried out by evaluating the actual entries rather than by manipulating symbolic inequalities.
IsNormal).MagicSquaresParam3 and the bijection of Mission I.IsNormal for
Fin 3 (and the Fin.forall_fin_succ technique for unfolding finite
quantifiers), the list of the eight Lo Shu parameters, and the order-three
classification itself.The distinct-distances problem asks how few distinct distances a finite planar point set can determine. Guth and Katz proved the near-optimal bound in 2015. Their argument passes through incidence geometry: distances become incidences between points and curves, and the Elekes–Sharir framework converts the problem into an incidence bound for lines in three-space. Pach and de Zeeuw showed the same pipeline works for points on a fixed algebraic curve, replacing line incidences with curve incidences. The algebraic prerequisite for that replacement — that two bounded-degree real plane curves with no shared component meet in finitely many points, with an explicit degree-dependent bound — is what this mission formalizes.
A real plane curve here is the real zero set of a nonzero bivariate polynomial , written . Its total degree is the maximum over monomials with nonzero coefficient. A curve is irreducible when its polynomial is irreducible.
The paper says two curves have a common component when their polynomials
share a nonconstant factor. The Lean development uses a different, weaker
hypothesis, NoCommonCurveComponent: no infinite irreducible real curve lies
inside both sets. A shared factor whose real zero set is finite (for example
) violates the paper's hypothesis but satisfies the Lean one, so the
Lean theorem covers strictly more pairs of curves than the paper's statement.
Currying views as a univariate polynomial in one coordinate whose
coefficients are polynomials in the other. In the Lean code the polynomial
variable is coordinate and the coefficient (base) variable is coordinate ;
this description writes the base coordinate as and the fiber coordinate as
, so a line is called vertical. The resultant of two
curried polynomials is a polynomial in alone. The development uses one
direction of its defining property: if the two specializations at share a
real root, the resultant vanishes at . All Lean statements use
MvPolynomial (Fin 2) ℝ for plane polynomials and EuclideanSpace ℝ (Fin 2)
for points.
The mission's goal is a finite-intersection bound in the spirit of Theorem 2.1 of Pach–de Zeeuw (Bézout's inequality), but it is not that theorem. It differs in both directions:
The six milestones are the algebraic inputs: coefficient-root counting, the two
resultant-nonvanishing criteria, the fiber bound, and the two mixed
vertical/nonvertical pair bounds that carry the constant . The
nonvertical–nonvertical pair bound (primitive_nonvertical_pair_intersection_bound)
carries the cruder constant . Above the
milestones sit the irreducible-pair assembly with constant and
the factorized assembly with constant , from which the goal
follows.
The result is the algebraic input to the Pach–de Zeeuw distinct-distances theorem for points on curves: without a uniform finite-intersection bound, the incidence count that drives the distance bound cannot even be stated. The formalization pins down every constant and every non-degeneracy hypothesis (non-verticality, no shared infinite component, coprimality) that the argument consumes.
The proof composes four toolkits — univariate root counting, Sylvester-matrix
resultant degree bounds, normalized-factor decompositions, and a smooth
implicit-function nonsingularity argument — whose interfaces must agree
exactly. The resulting lemmas (resultant criteria, fiber bounds,
partial-derivative degree bounds) are reusable for other real-algebraic
incidence formalizations over MvPolynomial.
The central difficulty is elimination with explicit constants: the resultant converts a two-variable intersection problem into a one-variable root count, but every step (currying, specialization, factor-pair summation) must preserve a usable degree bound, and the degenerate configurations (vertical fibers, shared factors with finite real zero set, singular points) each need a separate finite bound.
The textbook route — Bézout's inequality over , then observing that real intersection points are complex ones — is not taken, for two reasons. Mathlib has no plane-curve Bézout theorem to invoke. And under the weaker Lean hypothesis the two polynomials may share an irreducible factor with finite real zero set, in which case the complex intersection is infinite and no complex count applies; that branch is closed by bounding the singular points of the shared factor instead.
Points are EuclideanSpace ℝ (Fin 2); curves are MvPolynomial (Fin 2) ℝ
zero sets; finiteness is Set.Finite with Set.ncard bounds. The development
commits to total degree (not weighted degrees) and to the currying order that
eliminates Lean coordinate ; variable-style implicit degree bounds
are explicit {d₁ d₂ : ℕ} binders on the platform. No statement is
vacuous: every intersection bound carries the non-degeneracy hypothesis
(non-associated irreducibles, non-divisibility, nonzero partials) that excludes
the infinite-intersection cases. Contributions welcome: the sharp
general bound (currently an existential constant), the paper's hypothesis form
(no common factor at all), and the incidence assembly that consumes this
mission's output.
PachDeZeeuw.AlgebraicPrelim and PachDeZeeuw.Bezout (mathlib-only,
axiom-clean).Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by . The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most , giving an -approximation.
Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.
An instance consists of a finite type of elements, a finite type indexing available sets, an assignment , and a nonnegative cost . Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are
The frequency of an element is the number of sets containing it, and denotes the maximum frequency over all elements.
The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given covers is strictly stronger than coverability of the family.
Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when is empty, and the -approximation bound reads , which the certificate's tightness clause forces to be rather than anything false.
The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.
A primal-dual certificate is a pair where covers , is dual-feasible, and every has a tight dual constraint, .
For any primal-dual certificate and any fractional cover ,
Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover costs at most times the fractional optimum and a fortiori at most times the integral optimum.
The one substantive step of the goal is split out as its own target: for a primal-dual certificate,
Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most times. With this and weak duality, the goal is two lines.
A greedy certificate at ratio is a cover and a nonnegative with and for every . For such a certificate and any fractional cover ,
Instantiating is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.
Every dual packing is bounded by every fractional cover, ; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.
This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no -approximation result to build on.
The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.
Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.
Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.
This is the second mission in the magic-squares formalization programme, and it takes up the case the first one deliberately left open.
Counting semi-magic squares — arrays of nonnegative integers whose rows and columns all share a common line sum, with the diagonals unconstrained — is the "honest" version of the enumeration problem. For order three the magic count (mission I) is only a quasi-polynomial: it vanishes unless and equals on . The semi-magic count has no such periodicity. MacMahon computed it in 1915:
It is an honest polynomial in of degree , and that degree is not an accident: Ehrhart and Stanley proved that for every order the function is a polynomial of degree satisfying the reciprocity law . The order-three formula above is the smallest nontrivial instance of that theorem, and the only one small enough that every step of the derivation can still be exhibited explicitly.
So this mission is the natural companion to mission I: same objects, same platform vocabulary, but the counting step is genuinely harder — the parameter space is four-dimensional rather than two, and the parametrization is not injective until it is normalized.
Fix and a line sum . A square of order is an array of nonnegative integers.
For the whole family is governed by the six permutation matrices. Split them into the three even ones — the identity and the two -cycles — whose supports are the transversals
and the three odd ones — the transpositions — with supports
Adding them with multiplicities (even) and (odd) gives
whose six line sums all equal ; so this is a semi-magic square of line sum whenever the multiplicities sum to .
This is the goal because it is the weakest statement that still pins down the answer: it asserts the shape of without naming the parametrization, and it survives verbatim as the case of Stanley's theorem that is a polynomial of degree .
sm3_canonical). Every semi-magic
square arises from the display above, and the representation becomes unique
after normalizing: put , , , subtract the
corresponding even permutation matrices, and the residual odd multiplicities
satisfy . The normalization is necessary — without it the
single relationidentifies distinct -tuples — and it is exactly what makes the count a
partition rather than an inclusion–exclusion.
2. Bijection (sm3_bij). The map from normalized coefficient vectors to
semi-magic squares is a bijection, so .
3. Stars and bars (comps_card). The number of -tuples of nonnegative
integers summing to is ; the case is what the
count needs.
4. Evaluating the parameter count (sm3_params_card). Partitioning the
normalized vectors according to the first zero among writes
as
which collapses to by two applications of Pascal's identity.
The result itself. is the case of a theorem that launched a subject: Stanley's proof that counts lattice points in the Birkhoff polytope makes an Ehrhart polynomial, and the order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717) revisited exactly this computation on the way to their quasi-polynomial theorem for the magic counts, and Beck and Zaslavsky later pushed the same technique to the panmagic and symmetric refinements. Getting machine-checked therefore validates the whole hierarchy at its base.
Formalizing it. Nothing here is open; the mathematics is a century old. What is missing is the formalized artifact, and the difficulty is concentrated in two places that are formalization difficulties rather than mathematical ones.
First, surjectivity of the permutation-matrix parametrization. The usual proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem. For order three one can instead do it by hand: subtract the three even transversal minima and show that the residual satisfies . That last step is a six-case argument in linear arithmetic — if then each of the three ways for the transversal to have minimum zero forces — and it is precisely the kind of step that is invisible on paper and must be made explicit in a proof assistant.
Second, the counting step. The parameter set is a filtered finset of
functions Fin 6 → Fin (t+1), while the formula is stated with binomial
coefficients over . Connecting them requires stars-and-bars, proved
from scratch (by induction on the number of parts plus the hockey-stick
identity), because the available library results count sub-multisets rather
than compositions. And the final collapse to MacMahon's form is a chain of
Pascal identities that must be applied in the right order to stay inside
, where subtraction is truncated.
Two traps deserve to be named.
Uniqueness needs the normalization. The representation by six multiplicities is not injective: . Any formalization that counts -tuples directly will overcount, and the correction is not a subtraction but a choice of canonical representative. Deciding "first zero among " is what turns the count into a genuine partition.
Truncated subtraction. The decomposition is expressed over , so every identity — in particular the recovery of the multiplicities from a square — must be stated with the admissibility inequalities as explicit hypotheses. A truncated subtraction is only correct because normalization forbids the truncation, and that side condition has to be discharged rather than assumed.
Fin n; semiMagicCount n t is the cardinality of a
finset of arrays over Fin (t+1) — lossless, since every entry is at most
.Counting magic squares — arrays of nonnegative integers whose rows, columns and two main diagonals all share a common line sum — is one of the oldest problems in enumerative combinatorics, and the testing ground on which the general theory was built. MacMahon computed the order-three count in 1915 by hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717), showed that for general order the counting functions are quasi-polynomials in the line sum, by identifying them with Ehrhart quasi-polynomials of rational polytopes. The order-three case is the oldest nontrivial instance of that theory and the one where every step can still be checked by hand.
The subject therefore has a curious status: the enumerative answer for has been known for over a century, and the structural facts behind it (a magic square is determined by two corner entries; opposite cells sum to twice the centre) are folklore — but none of it has a machine-checked proof. This mission formalizes the classical derivation end to end.
Fix an order and a type of entries. A square of order is an array with entries in ; its row sums, column sums, and the two diagonal sums (main and anti-diagonal) are the sums of the entries along those lines.
No distinctness of entries is required. Let denote the number of semi-magic and the number of magic squares of order with nonnegative integer entries and line sum . Every entry of such a square is at most , so these are finite counts.
For the whole family is parametrized. If has line sum then the centre cell equals , and writing and the eight line identities force
All nine entries are nonnegative exactly when
and substituting , turns these into : the ball of radius in .
together with the companion vanishing when . This is the count of magic squares of line sum with nonnegative integer entries (entries need not be distinct). It is the goal because it is the weakest stable statement: it asserts only the shape of the answer, not the intermediate parametrization, and it survives verbatim as the case of the general quasi-polynomial theorem.
That the map is a bijection from the magic squares of line sum onto the admissible parameter pairs, and that the latter are counted by the -ball cardinality. This is the route the mission actually takes; the count is its corollary.
, the analogous count for semi-magic squares, is a genuinely different and harder quasi-polynomial. It is listed as a stretch target, not a milestone.
The result itself. MacMahon's formula is the base case of the Ehrhart-theory reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's quasi-polynomial theorem for general degenerates to it at , so it is the sanity check any generalization must pass. The parametrization behind it is what makes the "how many" question finite-dimensional at all: it reduces a search over arrays to a count of lattice points in a two-dimensional ball. Downstream, the same parametrization governs the classification of normal magic squares (the Lo Shu square and its symmetries) and the associativity identity .
Formalizing it. The mathematics is classical and proved; nothing here is
open. What is missing is the formalized artifact. The order-three structural
lemmas — the centre identity, the opposite-cell identity, and the two directions
of the parametrization — are already machine-checked on this platform. The
remaining work is the counting step: exhibiting a concrete bijection between
two finsets whose elements live in different types (arrays over Fin (3e+1)
versus pairs of naturals) and evaluating a finite sum. That is where the
formalization, not the mathematics, is hard.
The obvious attack — "each magic square is determined by , so just count
the pairs" — fails at exactly one point, and it is not a mathematical point. The
counting function is defined as the cardinality of a finset of arrays with
entries in Fin (3e+1) (a finite type, so that Finset.univ exists), whereas
the parametrization lives over . Proving the counts agree therefore
requires a honest Finset.card_bij in both directions:
mkMagic3 from an admissible pair, coerce every entry into
Fin (3e+1) using the bound , and show the round trip is
the identity.Neither direction is deep, but the coercions are unforgiving: a truncated
subtraction in mkMagic3 is only correct because admissibility forbids the
truncation, and that side condition must be discharged explicitly rather than
assumed. The second difficulty is the cardinality of the ball: the
identification needs the elementary identity
, after which the count is
.
Fin n; the anti-diagonal uses Fin.rev, and broken
diagonals use addition modulo . Counting functions are cardinalities of
finsets of arrays over Fin (t+1) — lossless, since every entry is at most
— and return natural numbers.mkMagic3 is defined over with truncated subtraction. Every
row/column/diagonal identity therefore carries the admissibility inequalities
as explicit hypotheses; no identity is asserted unconditionally.Square, IsSemiMagic,
IsMagic, IsPanMagic, IsAssociative, IsNormal, magicConstant, and the
four counting functions ), the symmetry/affine toolbox, and
the order-three structural lemmas. Contributions are welcome on the
semi-magic count , on panmagic and associative refinements, and on the
extension to general .An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.
This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs per day and buying costs once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic -competitive algorithm, and a randomized algorithm whose competitive ratio tends to , due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.
An instance is a pair : the purchase price , a positive integer, and the number of ski days, which the online algorithm does not know. An offline solution either buys at once, paying , or rents on every day, paying ; so the offline optimum is
Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable and one rent variable per day :
Its dual is a packing program with one variable per day:
The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.
The fractional primal-dual algorithm maintains , initially . On each new day, while it sets , then raises
and sets ; once has reached it does nothing further. The free parameter is then pinned to the value that makes reach exactly after days,
The coefficient is the exact finite- ratio , left in closed form rather than replaced by a constant. This is deliberate: increases to , so and therefore for every finite . A goal asserting -competitiveness at finite would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.
The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.
Chapter 3's other result, independent of the fractional development.
The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.
On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.
The offline problem is trivial, and a newcomer's first move — prove is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:
The optimum is never observed. The algorithm's cost must be compared against without being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.
The growth law is piecewise. The update fires only while . Summing the per-day increments therefore does not telescope uniformly: days before reaches contribute each and later days contribute nothing, and the index at which the switch happens is exactly — which is a theorem about the recurrence, not an assumption.
The constant is forced, not chosen. is not a free tuning parameter; it is the unique value for which the geometric sequence hits at , which is in turn what makes the dual solution feasible (). Dual feasibility and the choice of are the same fact.
Conventions this development commits to. The purchase price is a natural number with , because Chapter 3 uses simultaneously as a price, as a day index ("buy skis on the th day"), and as the exponent in ; costs are real numbers, with and coerced. Days are indexed from , so day of the prose is index , and Fin k indexes the days. Real division is total, so ; the hypothesis is what keeps every reciprocal in the development genuine, and without it would evaluate to and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day .
A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting and each range over ; Figure 3.1 on p. 18 prints only , . This mission takes the prose version, and , as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value , so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.
Ruling out a trivializing formalization. The offline optimum is defined independently, as , and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to times the number of days on which — so it cannot be weakened into vacuity without becoming false.
Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.
Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold uniformly and buying on the day whose increment of contains . That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.
Bayesian filtering estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.
The Discriminative Kalman Filter (DKF) uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in Theorem 2 of Appendix B.
The historical starting point is the linear Gaussian filter of Kalman (1960). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.
The state space is for a positive finite dimension . Write for the ordinary multivariate Gaussian density with mean and symmetric positive-definite covariance . Densities and their distances are with respect to Lebesgue measure.
The state model has a matrix and positive-definite covariance matrices satisfying
Its stationary density and transition density are
For an integrable density , prediction gives
The discriminative update combines a previous filtering density with a density for the state given the current observation:
This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by is part of the standard DKF under consideration.
For Gaussian inputs with parameters and , define
The DKF step returns mean and covariance when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance , using the current observation's functions and as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the paper.
Fix sequences of probability densities , indexed by positive integers, whose exact normalized updates
are well defined for every index. Fix Gaussian density sequences , a point , and a probability measure . The five assumptions are
Here denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; is the unit point mass at . The measure need not have a density and may be degenerate.
The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:
is a well-defined Gaussian density for all sufficiently large .
A sixth milestone is Lemma 1 (DKF equation): the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to . It includes both the exact equation and the asymptotic assertion from the source.
In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.
The inverse stationary density can grow in the tails, so small errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.
There is a second distinction between convergence to a point mass and approximation in . Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.
Lean represents states as Fin d → ℝ and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.
Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.
All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.
The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.
A foundation model trained on tokenized electronic health record (EHR) timelines can be used to predict clinical outcomes without ever being finetuned for a specific prediction task: condition the model on a patient's observed timeline, autoregressively sample many possible futures, and report the fraction of sampled futures in which the outcome of interest occurs. This generative approach to inference powers a growing family of EHR foundation models— including Event Stream GPT (McDermott et al., 2023), Foresight (Kraljevic et al., 2024), ETHOS (Renc et al., 2024), and Curiosity (Waxler et al., 2025)—and it is attractive for its zero-shot approach to predicting a variety of outcomes.
It is also expensive. Reproducing one published pipeline required more than A100 GPU-hours of inference. Worse, the estimator built from sampled futures takes values in , so its resolution is tied to the sampling budget: for an outcome of prevalence , sampled futures fail more than of the time to rank a patient at ten times average risk above an average one. The most consequential clinical decisions turn on exactly such low-prevalence, high-impact outcomes.
Solo et al. (arXiv:2602.03730) observe that Monte Carlo discards almost everything the model produces: at every step the model emits a full next-token distribution and the sampler keeps only the token it drew. The paper introduces two estimators that consume the discarded probabilities instead, and proves that doing so costs no bias and—for one of them—never costs variance.
Let generate token sequences from a countable vocabulary , with designated outcome token . The next-token probabilities may depend on the complete preceding history. The time threshold is initially unexceeded. Its crossing may depend on several kinds of time-spacing tokens and on their accumulated duration.
For a sampled timeline , is the first position occupied by , or if it never appears. The time is the first position at which the threshold has been exceeded. Assume almost surely. Timelines are retained through the actual threshold crossing, even if the outcome appears earlier. Thus is not reassigned after an outcome.
The threshold is reached almost surely, but the number of tokens required may be arbitrarily large. No deterministic bound or finite expected token count is assumed. For REACH, assume also that removing the outcome token and renormalizing defines a sampler that reaches the same threshold almost surely.
For independent original timelines, the Monte Carlo estimator is
The SCOPE estimator is
For REACH, sample independent outcome-free timelines by setting the next-token probability of to zero and renormalizing the probabilities of the other tokens. Using the original model probabilities along those timelines, define
The targets are:
Expectations and variances use each estimator's specified sampling law.
The claims concern the probability assigned by the generative model. They provide unbiasedness and a comparison of sampling variance. SCOPE is kept unclipped, as in the paper's unbiasedness result. All five target statements have accompanying local Lean proofs.
A pathwise finite stopping time need not have a common finite bound or a finite mean. An expectation involving the stopped SCOPE sum therefore needs justification beyond finite-sum linearity. REACH uses a different sampling law, so its unbiasedness and variance comparison also require a proved connection between the original event and the two-stage experiment. The equal-probabilities milestone records that connection explicitly.
Lean represents each sampled timeline by a finite list ending at its first threshold crossing. Arbitrary finite lengths are included in the same sample space. Path probabilities are products of next-token probabilities, and the laws are countable sums of these path masses. Requiring each law to have total mass one expresses almost-sure termination of that sampler; it is not a uniform length bound. The vocabulary can be finite or countably infinite.
The stopping predicate examines a complete prefix and is not restricted to a single terminal token. The original law continues through outcomes until the threshold. A separate almost-everywhere hypothesis excludes equal outcome and threshold times. The code proves that the actual threshold time is finite almost surely and that the strict event is the event used by the internal calculations.
The two-stage experiment explicitly samples conditionally independent Bernoulli trials using the original hazards. Its conditioning information retains the complete indexed pool of outcome-free timelines. The Rao–Blackwell target uses Mathlib's conditional expectation. The variance target uses Mathlib's variance, and proves square integrability rather than assuming it.
Essentially every quantitative model written as a rate of change — a mechanical system, a chemical reaction network, a population model, a control loop — is an ordinary differential equation (ODE) together with an initial condition. Before anything can be computed about such a model, two questions must be settled: does a solution through the given initial state exist, and is it the only one? The classical answer is the Picard–Lindelöf theorem: a Lipschitz right-hand side yields a unique local solution. Uniqueness is not a technicality — it is what licenses speaking of the trajectory through a point, hence of a flow, and so it underwrites the entire qualitative theory of dynamical systems that the source text builds afterwards (vector fields, tubular flow, -limit sets, Poincaré–Bendixson, Grobman–Hartman, stable manifolds).
This mission is the first in a series formalizing Augusto Armando de Castro Júnior's lecture notes Curso de Equações Diferenciais Ordinárias (2009), a graduate ODE course that develops the theory directly in Banach spaces, not only in . The book proves existence and uniqueness once, in that general setting, and then reuses it throughout; this mission formalizes that foundation.
Let be a real Banach space, , , and . Write for the closed ball and
A map is Lipschitz with respect to the second variable with constant if
the same serving for every (Definição 2.1.1 of the source).
Given , the Cauchy problem (initial value problem) with initial data asks for a curve , defined on a nondegenerate interval , such that for all , , and for all — one-sided derivatives at the endpoints of (Definições 1.0.1 and 1.1.1). Equivalently, by the Fundamental Theorem of Calculus, is continuous with graph in and satisfies the integral equation
Finally, put and .
The goal theorem is Teorema 2.1.2 (Picard) of the source: if is continuous, bounded, and Lipschitz in the second variable, then the Cauchy problem , has a solution on , and any two solutions on that interval whose graphs stay in coincide there:
The milestones are the results the source uses to get there, in its own order: the contraction fixed point theorem (Teorema 0.2.10), the equivalence between the Cauchy problem and the integral equation (Capítulo 2, opening paragraphs), the sufficient condition for Lipschitz dependence via a bounded partial derivative (Proposição 2.1.4), and the global version on a whole interval (Corolário 2.1.3).
Picard's theorem is what makes the initial value problem well posed in the sense of Hadamard's first two requirements. Downstream in the same book it is the hypothesis behind maximal solutions and the escape-from-compacts property (§2.3), continuous and differentiable dependence on initial conditions and parameters (Chapter 3), and the local flow of a vector field (Chapter 4). Without uniqueness none of these statements can even be phrased.
As for formalization status: Mathlib already contains a Picard–Lindelöf development
(IsPicardLindelof, ODE_solution_unique and relatives) and a Banach fixed point theorem
(ContractingWith.exists_fixedPoint). The work this mission asks for is therefore not the
discovery of a proof but a faithful bridge: stating the source's hypotheses as the source states
them — a closed ball, a supremum bound , the radius , Lipschitz in the
second variable with one constant for all times, uniqueness among solutions whose graph stays in
the domain — and deriving them from, or proving them alongside, the library's own formulation.
Such bridges are where unfaithful formalizations usually hide, and they are reusable by every
later mission in the series.
The obvious route is "cite the library and close the goal". It does not go through unchanged, for three reasons. First, the hypothesis shapes differ: the library packages its assumptions in a structure with its own choice of ball, bound and time radius, and matching with a supremum-defined requires the boundedness argument to be redone at the interface. Second, uniqueness here is asserted for solutions in the sense of this mission's definition — derivative within the interval, one-sided at the two endpoints, graph inside — so a Grönwall-type uniqueness statement must be transported to that formulation, including the endpoint cases. Third, the source works with an arbitrary Banach space and only assumes bounded, rather than assuming finite dimension; compactness arguments are unavailable by design.
The remaining genuine mathematical content sits in the milestones: the iterate estimate used by the source to make some iterate of the Picard operator a contraction, and the mean value inequality on a convex open set behind Proposição 2.1.4.
Conventions this proposal fixes, all visible in the definitions item:
A complete development needs the Bochner and interval integrals, the contraction mapping API, the mean value inequality for Fréchet derivatives, and the ODE files. Contributions of independent interest to the series: the Picard iterate factorial estimate, and the conversion between the library's Picard–Lindelöf hypotheses and the ones above.
Mathlib/Analysis/ODE/PicardLindelof.lean and Mathlib/Analysis/ODE/Gronwall.lean,
https://github.com/leanprover-community/mathlib4.In 1918 Emmy Noether published Invariante Variationsprobleme (Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-phys. Klasse, 235–257), answering a question raised by Hilbert and Klein about the status of energy conservation in the general theory of relativity. The paper proves two theorems that tie the symmetries of a variational integral to structural properties of its Euler–Lagrange equations: continuous symmetries depending on finitely many parameters produce divergence identities ("conservation laws"), while symmetries depending on arbitrary functions produce identities among the Euler–Lagrange expressions themselves, so that some of the field equations are consequences of the others. The first theorem is the source of the correspondence between time translation and energy, space translation and momentum, rotation and angular momentum; the second underlies the Bianchi-type identities of generally covariant theories and the gauge identities of field theory.
This mission formalizes the two theorems of §1 of the paper, together with the chain of identities of §2 and §3 by which Noether derives them, in the case of first-order Lagrangians.
Fix integers (independent variables), (dependent variables). Points of the base are , and a field is a map , written componentwise . Write for the derivative of a scalar function on along the -th coordinate direction, and
for the divergence of a vector field on .
A Lagrangian is a function of the point , of the field value , and of the array of first derivatives . Along a field one writes , and the integral under study is . The momenta are
and the Lagrange expressions — the left-hand sides of the Euler–Lagrange equations — are
An infinitesimal transformation is given by generators on the independent variables and on the dependent ones. Noether's equation (9) replaces them by the variation at fixed ,
and the corresponding variation of the Lagrangian is
Two vector fields organise the boundary terms: the partial-integration vector of equation (3), and Noether's
Invariance of enters through Noether's equation (11), the pointwise identity
which the paper derives in §2 from the vanishing of over every region.
The goal theorem is Theorem I of the paper, in the first-order case, in the form Noether states as equation (13). Given generators , , each satisfying the invariance identity (11) with its own from (9), one has for every and every
The milestones are the intermediate statements of the paper, in the order in which it proves them: the central identity (3), the passage from the invariance of the integral to the pointwise identity (11), the single-generator divergence identity (12), the conservation law on solutions of the Euler–Lagrange equations (§3), the converse of Theorem I (§3), and Theorem II in the form of the dependency relations (16) for a group depending on arbitrary functions entering to first order.
Theorem I is the general statement behind every "first integral from a symmetry" argument in mechanics and field theory; Theorem II is the statement that a variational theory invariant under a group of arbitrary functions has field equations that are not independent — of them follow from the rest — which is the group-theoretic form of the failure of a proper energy conservation law in general relativity that Hilbert had asserted. The two theorems are used constantly and stated loosely; a formal version fixes exactly which hypotheses are needed and what the conclusion says.
Mathlib contains the differential-calculus and measure-theoretic infrastructure used here (Fréchet derivatives, integration on , compactly supported test functions, and the standard vanishing lemma for locally integrable functions tested against smooth compactly supported functions), but no calculus of variations: there is no Euler–Lagrange operator, no first-variation formula, and no Noether theorem. This mission supplies the first-order, finite-dimensional-base version of that material, with definitions that later missions (higher-order Lagrangians, the -th order identity (6), mixed groups) can extend.
The algebraic core — the central identity (3) and the passage to (12) — is a product rule plus a reindexing, and the real work is elsewhere.
Two steps are genuinely analytic. First, Noether's inference from "the integral of the integrand vanishes over every region" to "the integrand vanishes pointwise" (equations (10)–(11)) requires the regularity of the integrand to be used explicitly. Second, Theorem II's equation (16) requires integrating by parts against an arbitrary function and then applying the fundamental lemma of the calculus of variations in : the arbitrary functions of the group must be specialized to compactly supported test functions before the boundary terms can be discarded.
The remaining difficulty is bookkeeping: every statement must carry the differentiability hypotheses that make each derivative in it meaningful, since in Lean an undefined derivative silently evaluates to zero rather than failing.
The formalization is in the first-order setting: the Lagrangian depends on , on , and on the first derivatives of only. The base is with fixed but arbitrary, and fields are globally defined maps ; no boundary conditions, no manifolds, and no jet bundles are used. The group is not formalized as a group: as in §2 of the paper, only its infinitesimal generators , enter, and the invariance hypothesis is Noether's identity (11). The linear independence of the divergence relations, which Noether argues from the essentiality of the parameters, is not part of the formal statements.
Derivatives are Fréchet derivatives: is the derivative of at applied to the -th standard basis vector, and partial derivatives of the Lagrangian are derivatives of the corresponding partially applied function. Because Lean's derivative operator returns at points of non-differentiability, each statement carries explicit differentiability hypotheses for exactly the functions whose derivatives it mentions; a solver may not assume more.
The statements are not vacuous: the hypotheses of every milestone are satisfied, for instance, by smooth Lagrangians and smooth fields, and the invariance hypothesis (11) is satisfied by the classical examples (a Lagrangian independent of with , ). Degenerate parameter values are admitted and behave as expected: for or the sums are empty and the identities reduce to , and for the goal quantifies over an empty index set.
Contributions of independent interest that this mission would welcome: a reusable statement of the fundamental lemma of the calculus of variations on in the form needed for (16), and the higher-order analogue of the central identity, Noether's equation (6).
Transformer sequence models modulate attention scores by a function of the relative position between a query and a key: the attention logit between token and token is scaled by a fixed profile . Realizing this modulation the naive way means evaluating once per pair and materializing an adjustment over the whole sequence — quadratic in the sequence length . Rotary Position Embedding (RoPE) Su et al. 2021 avoids this entirely: it rotates the query at position and the key at position independently, each by an angle depending only on its own position, so that the pairwise quantity falls out of the dot product of the two separately rotated vectors — is never evaluated pairwise, and no matrix is ever built. This is what lets RoPE stay a linear, per-token preprocessing step compatible with efficient (sub-quadratic) attention implementations, rather than an modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in one particular profile: a monotone, decaying . That schedule is a poor fit whenever the correlation structure of the data is not monotonically decaying with distance — the leading example being periodicity: in sequential recommendation, interactions separated by exactly one day or one week are more correlated than interactions separated by, say, half a day, and a decaying profile cannot express that "attention comes back" at the period.
Chen, Ainslie, Choromanski et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), ask a more general question first: which attention-modulation profiles can be realized at all by this same per-token, pairwise-iteration-free rotation trick — rotate each token once, on its own, and let the pairwise profile emerge from the dot product — and by what rotation-frequency schedule? Their answer is a random-features construction — sample the rotation frequencies from the kernel's own Fourier transform, rather than fixing them log-linearly — that realizes any continuous, normalized, positive-definite profile in expectation, with a quantified concentration rate, all while keeping the exact same per-token rotate-then-dot-product computation RoPE already uses. ClockRoPE is the periodic instance of this general theory, later deployed in a production-scale generative-retrieval system.
Fix an embedding dimension and group a vector into consecutive feature pairs for . For an angle , let
be the (Givens) rotation matrix. A real kernel is positive definite if for every finite family of points and complex coefficients , has nonnegative real part; it is normalized if . When is also continuous and Lebesgue-integrable, its Fourier transform
is (by Bochner's theorem) a genuine probability density on : this is the distribution the mission's rotation frequencies are sampled from.
Given a query at position , a key at position , and i.i.d. frequencies , the Random Fourier Rotation (RFR) estimator is
is exactly the modulated attention logit computed by rotating query/key feature pairs with per-pair, sampled RoPE frequencies — the same operation standard RoPE performs, but with drawn from instead of fixed by a log-linear schedule.
for every . This is the mission's central target: it upgrades the mean identity below into a quantitative, non-asymptotic guarantee that the sampled estimator is close to the target profile with high probability, at a rate that is exponential in the embedding dimension .
The expectation identity that the concentration bound above sharpens; it is the feasibility half of the claim ("this construction is correct on average") that the convergence half needs as its starting point.
For a continuous, positive-definite, -periodic with and Fourier coefficients ,
The periodic specialization needed to apply the goal and first milestone with a discrete frequency distribution over harmonics — the regime ClockRoPE actually deploys, since daily/weekly routines are periodic rather than merely decaying.
The result gives a general recipe — sample, don't hand-design — for turning any admissible attention-modulation profile into a RoPE-compatible rotation schedule, with a concentration guarantee that says how many feature pairs are needed before the sampled schedule reliably approximates the target profile. Crucially, the recipe changes only which frequencies the per-token rotation uses — it never touches the computational shape of RoPE itself: each query and key is still rotated once, independently, by an angle depending only on its own position, and the target pairwise profile is still recovered purely from the dot product of the two rotated vectors. So realizing an arbitrary positive-definite this way costs exactly what realizing RoPE's own log-linear profile costs — linear in the sequence length, with no pairwise evaluation of and no matrix ever materialized — rather than the quadratic cost a direct, per-pair implementation of an arbitrary modulation function would require. This subsumes standard RoPE's log-linear schedule as one instance and explains, via the periodic corollary, why a schedule built from the kernel's own spectrum (rather than an arbitrary log-linear one) is the right way to encode periodicity: nothing about the construction, or its efficiency, is specific to decay. The paper reports this translated into measured gains in a production-scale generative-retrieval system, which is unusual weight of practical evidence behind a Bochner/Herglotz-style spectral argument.
At the time of writing, none of these three results have a machine-checked proof; this mission asks for the first formalization of all three, together with the shared scaffolding (feature-pair extraction, the rotation estimator, and the notion of a positive-definite kernel) they are stated over.
The natural first attempt at the concentration bound is a direct union bound or a naive variance argument, but the estimator is a sum of terms that are each bounded (each rotated pair lies on a fixed-radius circle) rather than governed by a variance bound that shrinks with under a fixed frequency; the source proof instead applies McDiarmid's bounded-differences inequality, treating each sampled frequency as one coordinate of the input and bounding the one-coordinate change in by via the maximal distance between two points on the unit circle — not by directly bounding a variance term. Establishing Proposition 3.1 itself already requires care: it requires justifying that , defined purely as an integral transform of , is in fact a legitimate probability density (Bochner's theorem), and then a real/complex bookkeeping argument identifying the real inner product of rotated pairs with the real part of a product of complex exponentials.
The mission works over the reals and represents feature pairs as functions
Fin (2 * n) → ℝ sliced into Fin n-indexed pairs, matching the " feature pairs,
dimension " convention used throughout; rotations are ordinary
Matrix (Fin 2) (Fin 2) ℝ values built with Matrix.mulVec/Matrix.dotProduct, and
expectation over i.i.d. -distributed frequencies is formalized as integration
against the product measure MeasureTheory.Measure.pi of n independent copies of
the measure with density (MeasureTheory.Measure.withDensity) — this is
mathematically equivalent to, and more directly usable in Lean than, introducing an
abstract probability space with named i.i.d. random variables.
Since a general continuous positive-definite kernel need not have an
integrable Fourier transform (the periodic case in Corollary 3.3 is exactly the
counterexample: its "Fourier transform" is a discrete measure, not a density) — the
goal and first milestone add Integrable f as an explicit hypothesis beyond what the
paper states in prose, so that is genuinely a density rather than a junk value.
This is not a strengthening of the target profiles the paper cares about in practice
(Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all
integrable) and mirrors the paper's own split between the density case (Propositions
3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that
dropped this hypothesis and instead let the Fourier integral silently evaluate to
Lean's junk value (0 for non-integrable integrands) would make the goal statement
possible to "prove" vacuously and must be avoided.
Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier transform of a kernel, feature-pair extraction, the rotation matrix, and the RFR estimator itself — all reusable by any future mission formalizing RoPE-family positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results. McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a independently reusable contribution.