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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Markov processes with jumps model changes that cannot be represented by continuous diffusion paths: arrivals in queueing systems, sudden failures, population events, and discontinuous changes in financial or physical systems. Their infinitesimal descriptions are nonlocal generators, because the value of the operator at a state depends on test-function values at displaced states rather than only on derivatives at the current point. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), treats three complementary regimes. Theorem 3.1 covers finite-rate jumps on a general locally compact state space. Theorem 3.4 treats homogeneous Lévy operators on Euclidean space, including infinite jump activity and degenerate covariance. Theorem 3.3 gives the main target here: well-posedness for a time- and state-dependent compensated Lévy-type martingale problem.
These results connect concrete jump kernels and integro-differential operators to two standard descriptions of stochastic dynamics. Autonomous operators are realized as generators of conservative Feller semigroups, while time-dependent operators are characterized through martingale identities. Keeping all three source results in one mission records the nonlocal-generator theme without claiming that their distinct hypotheses imply one another.
For the Euclidean results, the state space is , represented in Lean as EuclideanSpace ℝ (Fin d), with . A covariance field is a continuous linear endomorphism, a drift field is a vector, and is a measure of jump displacements. For a smooth compactly supported test function , the compensated Lévy-type operator is
The denominator in the compensation term is part of the source convention. The covariance factor applies only to the second-order term; the drift is unscaled. The weighted moment permits measures with infinite total mass while controlling the compensated integral.
A solution of the Lévy-type martingale problem is a jointly measurable process with the prescribed initial pushforward law whose integrated-generator increments have zero expectation against every bounded continuous function of any finite history. Smooth compactly supported functions are the spatial tests. This definition imposes no path-continuity requirement.
The finite-rate model uses a locally compact, noncompact, separable metric space , a nonnegative rate , and a weakly continuous probability transition kernel . Its operator is . Positive weights and specify the graph domain and control behavior at infinity.
The main target is Chapter 8, Section 3, Theorem 3.3. The covariance is continuous, symmetric, bounded, and strictly positive definite at every nonzero vector, without a uniform ellipticity constant. The drift is measurable and bounded. The weighted jump measure is integrable, and for every measurable set its weighted mass is a bounded continuous function of time and state.
For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every solution on every probability space. Setwise continuity is retained exactly; it is not replaced by weak convergence of measures or by finite total jump intensity.
Theorem 3.4 freezes the coefficients in time and space. The covariance may be degenerate but is symmetric and nonnegative, and the jump measure needs only the finite weighted integral. The full graph consists of functions, first derivatives, and second derivatives that vanish at infinity. Its closure is the exact generator of a positive conservative strongly continuous contraction semigroup on , and smooth compactly supported functions form a core.
Theorem 3.1 retains the general-state-space jump model. The transition kernel is both setwise measurable and weakly continuous; the rate and weights satisfy the source's vanishing and signed integral bounds. The weighted graph closes to a single-valued conservative Feller generator, and compactly supported continuous functions form a core.
The main theorem says that the displayed nonlocal characteristics determine stochastic dynamics in distribution even when the drift is only measurable and jump activity need not be finite. The two autonomous theorems identify concrete domains whose closures are genuine Feller generators, including positivity, contraction, strong continuity, conservativity, and core statements. Together they distinguish finite-rate kernels, homogeneous compensated Lévy dynamics, and nonautonomous Lévy-type dynamics while sharing the same generator language.
The formal contribution is a machine-checkable statement layer, not a proof claim. It exposes the exact compensation, weighted-integrability, graph-domain, semigroup, and finite-history conventions on which later proofs depend. The common diffusion operator, bounded-pointwise closure, and strongly continuous contraction-semigroup predicate are reused from earlier private missions in the same textbook series rather than duplicated under conflicting identifiers.
The obvious finite-jump approximation does not by itself preserve the full conclusions. Infinite jump activity requires compensation near zero, and convergence of the associated operators must still identify the intended martingale problem or the exact closed Feller generator. In the nonautonomous theorem, setwise continuity of weighted jump masses must coexist with merely measurable drift, while uniqueness ranges over arbitrary probability-space realizations and all finite-dimensional laws. Strengthening to continuous drift, imposing finite total jump intensity, assuming uniform ellipticity, or comparing only continuous-path solutions would materially weaken or alter the source theorem.
Nonnegative real time is represented by ℝ≥0; Euclidean coordinates use Fin d. Fréchet derivatives express both gradient and Hessian terms. The jump measure is a measure of displacements , so the operator evaluates . Integrable hypotheses prevent Lean's totalized integral from silently assigning zero to a divergent positive weighted moment. Positive dimension is explicit through [NeZero d].
The martingale predicate includes empty finite histories and repeated observation times. Its bounded continuous history tests determine the same finite-dimensional identities used by the source, and no sample-path regularity is inserted. The autonomous graphs live in ; bounded-pointwise closure means closure under uniformly bounded pointwise sequential limits, not ordinary norm closure. The finite-rate theorem preserves its restriction of the additional integrability clause to states with positive rate. No vacuous solution predicate, unweighted moment assumption, hidden nonzero-rate condition, or proof-only theorem dependency is introduced.
Finite-dimensional simplices are the natural state spaces for proportions: allele frequencies, population shares, and other collections of nonnegative coordinates whose total cannot exceed one. A diffusion on such a space must do more than solve an unconstrained stochastic equation. Its covariance degenerates on the boundary, and its drift must respect every face so that the process remains in the simplex. Chapter 8 of Ethier and Kurtz develops generator results for this setting as part of the analytic foundation for Markov-process models with constrained state spaces Ethier and Kurtz, Chapter 8, §2.
This mission formalizes their Theorem 2.8, a known generation theorem rather than an open conjecture. The theorem treats arbitrary Lipschitz drift satisfying the inward boundary inequalities. It identifies the closed diffusion graph as a Feller generator and also states that polynomial restrictions form a core. The generality of the drift distinguishes this result from later population-model applications with particular mutation or selection coefficients.
For a positive integer , the simplex state space is
The missing mass may be viewed as an additional coordinate. In Lean, WFState d is the subtype of functions Fin d → ℝ satisfying precisely nonnegativity and the upper bound on the coordinate sum. These conditions already imply for every coordinate.
Let be the drift. The boundary conditions say that whenever , while whenever . Thus the drift cannot point outward through a coordinate face or through the top face. No mutation–selection formula or extra smoothness condition is imposed: global Lipschitz continuity and these face inequalities are the complete drift hypotheses retained here.
The covariance matrix is
and the associated simplex diffusion operator is
Only the second-order sum is multiplied by . The covariance becomes singular on boundary faces, so this is not an immediate instance of a uniformly elliptic whole-space theorem.
The formal target asserts that the uniform graph closure of
is single-valued and is exactly the generator graph of a positive, conservative, strongly continuous contraction semigroup on . Conservativity is expressed by preservation of the constant function . The generator is identified by the right derivative at time zero, not merely by containment of a convenient operator restriction.
The final clause says that polynomials restricted to are a core: closing the graph obtained from polynomial first coordinates gives the same full generator graph. This is a graph-closure statement and is stronger than uniform density of polynomials as functions.
Single-valuedness shows that the closed graph behaves as an operator rather than a multivalued relation. Generation supplies a Feller semigroup whose positivity and preservation of constants give the Markov interpretation. The exact generator biconditional fixes the full infinitesimal domain, while the polynomial-core conclusion permits generator questions to be reduced to algebraically structured test functions without changing the closed operator.
The source theorem is already proved in the book. The formalization task is to recover its generator statement and core conclusion in Lean with all boundary, closure, and semigroup conventions explicit. The current mission contributes a source-reviewed statement and its expression-level definitions; it does not claim a completed Lean proof.
The obvious route through standard elliptic diffusion generation does not apply because degenerates as coordinates approach the boundary. It is also insufficient to prove only that the displayed differential operator is contained in some generator: the theorem identifies the closure of the entire graph and separately asserts the polynomial core.
Boundary semantics create another source of possible weakening. Dropping either inward condition would permit outward drift at a face. Replacing the arbitrary Lipschitz drift by a special population-genetics formula would narrow the theorem. Replacing graph equality by inclusion, or polynomial graph density by ordinary function density, would lose a stated conclusion. These distinctions are all preserved in the target.
The Lean development uses the book-wide namespace EthierKurtz. The compact space is represented by real-valued bounded continuous functions on WFState d; compactness makes this the intended continuous-function space with the uniform norm. A function is represented through a globally twice continuously differentiable extension on the ambient finite-coordinate space, following the book’s Appendix 6 extension convention for closed convex sets.
The operator uses Fréchet derivatives evaluated on coordinate vectors, which represent the first and second partial derivatives in the finite-dimensional ambient space. The graph is closed in the product uniform norm. IsStronglyContinuousContractionSemigroup records identity at zero, the nonnegative-time semigroup law, contraction, and strong right continuity at zero. The target additionally records positivity, preservation of one, and equality between its derivative graph and the closed diffusion graph.
The scope excludes the zero-dimensional case, as required by 0 < d. It does not introduce a continuous-path hypothesis, a special drift parameterization, or uniform ellipticity. The only packaged declarations beyond the goal are the state space, operator, graph, and the already published semigroup predicate needed to state it. Proof-only lemmas and unrelated Chapter 8 results are outside this mission.
A one-dimensional diffusion is governed in the interior by a second-order differential operator, but the interior coefficients alone do not determine what happens when the process approaches the edge of its state space. An endpoint may be reachable from the interior or inaccessible; after arrival it may absorb, reflect, or retain the process according to a boundary parameter. The same issue persists when an endpoint is infinite. Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), organizes these alternatives through scale and speed integrals and identifies the exact operator domain that generates the corresponding Feller evolution. This mission formalizes Chapter 8, Section 1, Theorem 1.1, printed page 367.
Let . The real state interval is , its interior is , and is the closed interval in the extended real line. A function in is represented by a continuous function on that compact extended interval, so finite endpoint limits are part of the object even when an endpoint is infinite.
The interior diffusion operator is
where and are continuous on and there. Choose an interior reference point . Define
The corresponding endpoint tests and are nonnegative extended-real integrals. Their values may be ; preserving that possibility is essential because the four boundary classes are distinguished precisely by which of the two tests are finite.
At either endpoint, the pair gives the Feller boundary class:
Entrance and natural endpoints are inaccessible, so the generator domain imposes no boundary equation there. At an exit endpoint the limiting generator value must be zero. At a regular endpoint , a parameter determines the boundary condition
The target states that the graph consisting of that are twice continuously differentiable in the interior, whose extends continuously to , and that satisfy the applicable condition at both endpoints is exactly the infinitesimal generator of a Feller semigroup on . The conclusion includes the semigroup law, contraction, strong right continuity at zero, positivity, preservation of the constant function , and a biconditional identifying the complete generator graph rather than merely an included core or its closure.
The theorem translates local coefficients into a global Markov evolution while retaining every possible finite or infinite endpoint type. The endpoint tests determine which boundary behavior is available, and the regular-boundary parameter records absorbing, reflecting, and intermediate behavior in one equation. Without the classification, writing down the differential expression does not specify a unique Feller generator because distinct domains can encode different stochastic behavior at the same endpoint.
The formal contribution is a machine-checkable statement layer for the source theorem. It makes the compactified state space, improper endpoint integrals, one-sided endpoint filters, and exact generator graph explicit. The theorem itself remains an open proof obligation in this statement-only mission. The definitions can also support later formal work on hitting distributions, killed or reflected diffusions, and comparison of boundary regimes.
The main difficulty is that the classification cannot be reduced to ordinary finite integrals or to boundary values at finite real points. Infinite endpoints and divergent scale or speed tests carry mathematical information; replacing extended-real integrals by totalized real integrals would collapse boundary classes. A second difficulty is identifying the full closed generator domain. Showing that the differential expression is meaningful on smooth interior functions is insufficient: the proof must connect its endpoint asymptotics to positivity, conservativity, strong continuity, and exact generation on the uniform-norm space.
Endpoints use EReal, and the state space is Set.Icc r₀ r₁ in the extended line. Coefficients are constrained only on the open real interior; no boundedness or uniform ellipticity is added. The drift primitive and scale/speed tests use oriented interval integrals internally and ENNReal endpoint integrals externally, retaining . Absolute values correct the orientation on the left of the reference point.
The graph stores continuous endpoint extensions of both and . Interior regularity is expressed by ContDiffOn ℝ 2, and endpoint limits use the one-sided neighborhood filter induced from the extended interval. The regular parameter is required to lie in only when both boundary tests are finite. The mission does not replace the four cases by an opaque classifier, assume finite endpoints, add a pathwise stochastic differential equation, or weaken exact generation to graph inclusion. The shared book definition of a strongly continuous contraction semigroup is reused from the earlier semigroup-generation mission rather than redeclared.
Diffusion processes connect stochastic differential equations, partial differential equations, and Markov semigroups. On Euclidean space, their local behavior is encoded by a second-order operator built from a covariance field and a drift field. A central question is whether those local coefficients determine an actual Markov evolution, and whether the resulting evolution is unique. Ethier and Kurtz organize these questions through generator graphs and martingale problems, which allow the same language to cover smooth elliptic diffusions, degenerate models, and coefficients that vary measurably with time. This mission formalizes three complementary whole-space regimes from Chapter 8 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), principally Theorems 1.6, 1.7, and 2.5.
The state space is the finite-dimensional Euclidean space , represented in Lean as EuclideanSpace ℝ (Fin d), with . A covariance operator is a continuous linear endomorphism of this space, while a drift is a vector. For a smooth scalar test function , the diffusion operator is
The factor multiplies only the covariance-weighted second-order term. The formalization uses Fréchet derivatives evaluated in the standard coordinate directions. In the time-homogeneous cases, the smooth compactly supported graph consists of pairs viewed in , and its uniform closure is the candidate generator.
For time-dependent coefficients, a measurable process solves the time-inhomogeneous martingale problem when its initial pushforward law is prescribed and the integrated generator identity holds against every smooth compactly supported spatial test and every bounded continuous finite-history test. This formulation records the natural-past moment identities without imposing continuity of sample paths as an extra hypothesis.
The main target is Chapter 8, Section 1, Theorem 1.7. The covariance and drift are jointly Borel measurable and locally bounded. The covariance is symmetric and nonnegative. At each fixed spatial point it is uniformly elliptic over every bounded positive time interval, and its spatial continuity is uniform over that interval. A common quadratic bound controls the covariance norm and the one-sided radial drift quantity .
For every initial probability measure, the conclusion asserts existence of a measurable-process solution on some probability space and uniqueness of all finite-dimensional distributions among every such solution on any probability space. The drift is not assumed continuous, and no stronger norm-growth condition on the drift or moment condition on the initial law is inserted.
Chapter 8, Section 1, Theorem 1.6 treats bounded Hölder continuous time-homogeneous coefficients with symmetric, globally uniformly elliptic covariance. It concludes that the closure of the smooth compactly supported graph is single-valued and is exactly the generator of a positive, strongly continuous contraction semigroup on . Conservativity is retained through membership of the constant graph pair in the bounded-pointwise closure.
Chapter 8, Section 2, Theorem 2.5 permits degenerate and unbounded covariance fields. Its assumptions are symmetry, nonnegativity, twice continuous differentiability of the matrix entries, bounded second partial derivatives, and a globally Lipschitz drift. Its conclusion is the same full Feller generation and conservativity statement. This regime is related to, but not implied by, the bounded uniformly elliptic regime.
Together the three statements separate distinct mechanisms for obtaining Markov dynamics from local diffusion data. The two autonomous theorems identify when a concrete smooth core closes to a Feller generator, including positivity, contraction, strong continuity, and conservativity. The nonautonomous theorem establishes existence and uniqueness in distribution under substantially rougher temporal behavior and merely measurable drift. Keeping the regimes together exposes the common operator while preserving their incompatible regularity hypotheses.
The formal contribution is a machine-checkable statement layer for these source results and their expression-essential definitions. It does not claim proofs of the theorems. The definitions make explicit the coordinate form of the generator, the graph, the bounded-pointwise closure convention, and the complete finite-history martingale identities. These components can support later formal proofs and other diffusion or martingale-problem developments.
The source conclusions are not consequences of a single elementary continuity argument. In the Feller cases, identifying the closure of a graph with the generator requires simultaneous control of the operator domain, the semigroup properties, positivity, and conservativity. In the time-dependent case, measurability of the drift is deliberately weaker than continuity, while uniqueness must cover all measurable-process realizations and all finite collections of observation times. Replacing that conclusion by uniqueness only among continuous processes, or strengthening the drift hypotheses until a standard smooth theory applies, would change the theorem.
The development uses nonnegative real time and finite-dimensional real Euclidean space. Covariance matrices act as continuous linear maps; their entries are recovered in the standard orthonormal basis. Smoothness is expressed with ContDiff, compact support with HasCompactSupport, and autonomous generator graphs in C₀. The bounded-pointwise closure is the smallest set closed under uniformly bounded pointwise sequential limits, not merely the set of one-step limits.
The martingale-problem predicate requires joint measurability of the process, equality of the initial pushforward measure, and all bounded continuous finite-history identities. Empty histories and repeated observation times are included. The goal compares the complete finite-dimensional laws of any two solutions. No vacuous solution predicate, arbitrary extension of the generator, chosen matrix square root, hidden path-continuity assumption, or proof-only theorem dependency is used.
Classical central limit theorems begin with independent observations. Many stochastic models instead produce observations whose dependence persists across time: measurements from an equilibrium process, functions of a stationary Markov chain, and noise sequences in time-series models are standard examples. For such data, the variance of a long sum contains covariance terms from every lag, and independence cannot be used to discard them. Chapter 7, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), gives a functional central limit theorem under a quantitative mixing condition. The conclusion is stronger than convergence of one normalized sum: the whole partial-sum path converges to Brownian motion.
Fix a probability space and a two-sided real sequence . Strict stationarity means that shifting every integer index by the same amount leaves the joint law of the entire sequence unchanged. Each is measurable and centered, so .
For a nonnegative lag , let the past be the sigma-algebra generated by all with , and let the future be generated by all with . For , the book's mixing coefficient is the supremum, over future events , of
Thus measures how far events at least time units in the future remain from being independent of the complete past. The Lean definition constructs both coordinate-generated sigma-algebras explicitly and represents conditional probability as the conditional expectation of an indicator.
For , define the scaled partial-sum process
The Lean sequence uses the index because Lean's natural numbers begin at zero; this is only a reindexing of the same positive scaling sequence. Suppose there is such that every coordinate has a finite moment. Set
The target is Theorem 3.1: the ordered covariance series converges and
is nonnegative, while converges to centered Brownian motion with variance parameter . The variance is allowed to be zero. The covariance sum is encoded as convergence of its ordered partial sums, not as the stronger and unrequested assertion of absolute summability.
The result identifies the macroscopic fluctuation process of a stationary dependent sequence. It supplies both the long-run variance, including every lag covariance, and a Brownian path limit. Consequently, continuous functionals of the accumulated process can be studied through the limiting Brownian motion rather than only through one-time normal approximations.
The formal statement preserves the book's functional interpretation. ConvergesToContinuousGaussian records the complete prelimit path laws, centered Gaussian finite-dimensional laws with covariance , and convergence to a continuous limit through a common realization. This avoids weakening the theorem to convergence of a single terminal sum or to separate finite-dimensional marginals. The declaration is a statement-only formalization: the theorem remains an open Lean goal, while the mixing coefficient and partial-sum process are concrete definitions.
The usual independent-sum argument does not apply because blocks of observations are not independent and their covariance terms need not vanish. Merely showing that dependence becomes small at large lags is insufficient: the decay must interact with the available moment so that the total contribution of distant dependence is summable. A scalar central limit theorem would also leave tightness of the path sequence unresolved. The theorem packages both issues into the summability condition on the precise coefficient and concludes a path-level Brownian limit.
The formalization uses a two-sided sequence indexed by , matching the source's convenient stationary extension. Stationarity is equality of the laws of the whole shifted and unshifted sequence, which entails every finite-dimensional shift identity without adding Markov or independence assumptions. The probability measure is explicit, and every coordinate has an explicit measurability hypothesis.
stationaryLpMixing uses the past through zero and the future beginning at lag . Its codomain is the extended nonnegative reals, so an infinite norm or supremum is not silently totalized to an ordinary real. The summability hypothesis is an extended-real infinite sum strictly below infinity. stationaryPartialSums embeds the real sum in one-dimensional Euclidean space so it can reuse the book-wide continuous-Gaussian path-convergence definition. The exact floor, positive indexing, square-root normalization, covariance order, and degenerate zero-variance case are retained. No interpolation, absolute covariance summability, positive-variance assumption, Markov property, or independence condition is introduced.
The expression-essential infrastructure consists of the two definitions introduced here and the compatible book-wide ConvergesToContinuousGaussian definition already staged for the preceding diffusion-limit mission. The latter is imported rather than duplicated under a conflicting name. Useful future work includes proving the theorem from martingale approximation and developing reusable results relating concrete mixing bounds to the required summability hypothesis.
Many stochastic models are built from small random changes occurring at high frequency. Queue lengths, population counts, particle systems, and numerical schemes may be discrete or have jumps at every finite scale, yet their large-scale behavior is often described by a continuous diffusion. A diffusion approximation replaces the detailed microscopic model by a process whose drift and covariance depend on its current state. This can make asymptotic probabilities and qualitative behavior accessible without claiming that the original model itself has continuous paths.
Chapter 7 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, develops general limit theorems for this passage. The retained results in this mission are Theorem 1.4, a martingale functional central limit theorem with deterministic covariance, and Theorem 4.1, a state-dependent diffusion approximation from localized characteristics. They are related limit regimes, but the former is not presented here as a literal specialization of the latter: its covariance may vary deterministically with time, whereas the state-dependent theorem uses time-homogeneous coefficient fields evaluated along the evolving state.
A càdlàg process is right-continuous and has a finite left limit at every positive time. For each index , the state process and its finite-variation characteristic have càdlàg paths in . A symmetric matrix process has càdlàg entries and positive-semidefinite increments. The natural filtration records the histories of , , and jointly.
The centered process is required to be a local martingale coordinatewise. Its quadratic characteristic is represented by requiring every product
to be a local martingale as well. These conditions identify as the approximate drift and as the approximate covariance accumulation. They do not impose independence of the coordinates or of the prelimit processes.
Localization uses the first time at which either the current value or its left limit reaches radius . The jump and characteristic conditions are checked only up to , for each radius and time horizon . This is essential when coefficients are controlled locally but not globally.
Let be a continuous symmetric positive-semidefinite matrix field and let be a continuous vector field. For smooth compactly supported , define
Assume the continuous-path martingale problem for this operator is well posed for every initial probability law. The goal states that if the stopped squared jumps of and vanish in expected supremum, the stopped first-power jumps of each vanish, and the stopped characteristics converge in probability to
then weak convergence of the initial laws implies convergence of the complete path laws to the unique continuous diffusion law.
The retained milestone treats vector local martingales with deterministic limiting covariance . It preserves both alternatives in the source: either first-power martingale jumps vanish and is the actual cross variation, or the jumps of and the squared jumps of the martingale vanish while is locally martingale. Pointwise convergence in probability of to then yields the centered continuous Gaussian limit with covariance .
The state-dependent theorem packages a common diffusion-limit argument into conditions on observable local characteristics. It separates model-specific work—identifying the drift, covariance, localization, and jump bounds—from the general conclusion that the entire trajectory converges. The martingale theorem records the important deterministic-covariance regime without erasing either of its two source alternatives.
For formalization, the mission provides concrete predicates for càdlàg paths, stopped maximum jumps, localized characteristic discrepancies, the diffusion generator, continuous martingale-problem laws, and Gaussian process convergence. The result is statement-only: the theorem bodies remain open with sorry, while every expression dependency is a concrete definition. No theorem proof, adapter-equivalence proof, or claim of completed formal verification is included.
Finite-dimensional convergence alone does not control whole trajectories. The central obstacle is simultaneous control of oscillations, jumps, and characteristics after localization. A naive argument that replaces and by their limiting integrals pointwise misses the uniform stopped discrepancies and does not justify tightness of path laws. Likewise, ignoring the left limit in the exit rule can miss a jump that crosses the localization boundary.
Well-posedness is also substantive. Identifying every subsequential limit with a solution of the martingale problem gives uniqueness only when that problem is well posed for the relevant initial law. The formal statement therefore retains existence and uniqueness for every initial probability law rather than silently assuming a distinguished solution.
Time is nonnegative and the sequence is indexed from zero rather than one. Expectations of jump suprema take values in , so no unmentioned integrability assumption is introduced. Matrix positivity is Matrix.PosSemidef, which includes the real symmetric positive-semidefinite condition used by the source. The exit time includes both the current value and the positive-time left limit, and an empty exit set gives infinity.
The diffusion law uses continuous canonical paths, smooth compactly supported tests, and bounded measurable functions of finitely many past states to express the natural-filtration martingale identities. Full process convergence is encoded by a joint realization that preserves every complete prelimit path law and converges almost surely uniformly on each compact interval to a continuous limit. This is the source-reviewed continuous-limit Skorohod representation convention, not merely convergence of finitely many observations.
The two shared definitions EthierKurtz.IsSourceLocalMartingale and EthierKurtz.HasCrossVariation are imported from the earlier book-wide stochastic-calculus package. All other definitions needed to state these two results are included here. Contributions should preserve the localization quantifiers, both central-limit jump alternatives, the full martingale-problem well-posedness hypothesis, and the complete path-law conclusions.
A Brownian stochastic equation describes a state that changes through a deterministic drift and random fluctuations. Such equations are basic models for diffusions and connect probabilistic sample paths with analytic operators. Chapter 5, Section 3 of Stewart Ethier and Thomas Kurtz's Markov Processes: Characterization and Convergence develops this connection in both directions and then separates three questions: whether a solution exists, whether it is unique when driven by fixed noise, and whether all solutions have the same distribution. The mission records four central results from that section as one coherent formalization target. The principal goal is the fixed-driver existence theorem, Theorem 3.11. Theorems 3.3, 3.6, and 3.10 retain the representation, uniqueness, and weak-existence variants without treating one as a consequence of another.
Fix a dimension . The state space is the Euclidean space , represented in Lean as EuclideanSpace ℝ (Fin d). A diffusion coefficient
controls the random fluctuations, and a drift coefficient
controls the finite-variation part. Given a -dimensional Brownian motion and initial state , a solution satisfies, componentwise,
The formal statement does not postulate an opaque stochastic-integral operator. The predicate HasBrownianItoIntegral uses bounded predictable dyadic step approximations, integrated squared-error convergence in probability, and convergence in probability of the corresponding stochastic sums. SolvesBrownianSDE requires continuous paths, adaptation to the completed natural past of and , integrability of the drift, and one almost-sure equation holding for every time and coordinate.
A weak solution may choose its probability space, filtration, and Brownian driver. Its Brownian future increments are independent of the entire filtration past, its state process is adapted after completion, and its initial distribution is prescribed. Pathwise uniqueness compares two solutions on the same space with the same filtration and driver. Distribution uniqueness compares solutions that may live on different spaces and asks for equality of their whole coordinate-path laws.
For locally bounded Borel coefficients, a given continuous solution of the diffusion martingale problem can be lifted to the completed product with an auxiliary Brownian space. On that specific extension there exists a Brownian motion making the lifted original process a weak solution of the stochastic equation. The generator is
This target retains the factor , the complete drift term, possibly singular diffusion matrices, the given process, and the exact completed product filtration.
For locally bounded Borel and and any initial probability law , pathwise uniqueness implies uniqueness in distribution. No existence, Lipschitz, ellipticity, or moment assumption is added.
When both coefficients are continuous and a constant satisfies
there is a weak solution for every initial probability law. The drift hypothesis is one-sided and does not bound .
The main goal assumes locally bounded Borel coefficients, the preceding one-sided growth condition locally in time, and local Lipschitz control on each bounded state ball. For every Brownian motion and every independent square-integrable initial variable already given on a probability space, there exists solving the equation with respect to the completed natural past of and . The quantifier order preserves the fixed driver and original probability space.
The representation theorem connects the analytic martingale problem with the pathwise stochastic-integral formulation while preserving a given process on a prescribed extension. The uniqueness theorem explains when the apparently stronger same-noise comparison controls the law of arbitrary weak solutions. The weak-existence theorem supplies solutions under continuity and one-sided growth without local Lipschitz assumptions. The strong-existence theorem supplies a solution driven by noise and initial data that are fixed in advance, under local Lipschitz regularity.
Formalizing the group creates reusable definitions for completed filtrations, Brownian drivers, local Itô integration, weak solutions, pathwise uniqueness, and time-dependent diffusion generators. The source results are classical theorems, and this proposal records their reviewed Lean statements as open proof obligations. It does not claim machine-checked proofs.
The central difficulty is keeping the probabilistic quantifiers and filtrations exact. Replacing the local stochastic integral by an unconstrained witness would make the equation too weak. Replacing weak existence by existence on a fixed space would make Theorem 3.10 too strong. Conversely, existentially choosing a new driver in Theorem 3.11 would lose its fixed-noise content. The representation theorem also cannot be reduced to equality in law: it must retain the original process through first projection and use the completed product past specified in the source.
Time is ℝ≥0, states are finite-dimensional real Euclidean spaces, and diffusion matrices use the Frobenius norm. Brownian motion is represented by independent scalar Brownian coordinates with measurable evaluations and continuous paths. Completion adds every subset of an ambient measurable null set. The local Itô relation uses left-endpoint dyadic step functions, interval integrability, and convergence in probability. Equality of path laws is expressed on the coordinate function space; for continuous Euclidean paths this matches the usual continuous-path law.
The main theorem keeps Borel measurability, compact-set local boundedness, one-sided drift growth, squared diffusion growth, local Lipschitz bounds, independence of and , and the second moment of . The weak theorem keeps continuity and an arbitrary initial law. The representation target keeps compactly supported smooth tests and the exact covariance contraction. These conditions rule out vacuous solution predicates and default-valued integrals. Contributions may prove the four theorem statements or establish reusable lemmas for the concrete integral, completion, martingale, and path-law infrastructure.
A continuous stochastic process may combine a finite-variation drift with a local martingale fluctuation. To understand a function of that process, one needs a change-of-variables rule that accounts for both parts and for their quadratic covariation. The ordinary chain rule has no term for covariation. The result here is the time-dependent, multidimensional Itô formula in Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986), Chapter 5, Section 2, Theorem 2.9, printed page 287 (PDF page 296). It applies to arbitrary continuous semimartingales satisfying the stated decomposition; its input is not restricted to a particular stochastic differential equation.
Time is the nonnegative real half-line and the state has d real coordinates, indexed by Fin d. The sample space Ω has a complete probability measure P and a filtration ℱ. The initial sigma algebra contains every ambient measurable null set. For each coordinate i, V_i is a continuous adapted finite-variation process, zero at time zero; M_i is a continuous adapted local martingale, zero at time zero almost surely. The process X_i has an ℱ₀-measurable initial value and satisfies X_i(t)=X_i(0)+V_i(t)+M_i(t) for all times and samples.
The test function f(t,x) has a continuous first time derivative, continuous first spatial derivatives, and continuous second spatial derivatives. At time zero, the time derivative is taken within the nonnegative-time domain. The notation f_t, f_{x_i}, and f_{x_i x_j} denotes these derivative witnesses. The conclusion supplies processes representing the continuous cross variations and integrals; their existence is part of the theorem. The Stieltjes relations use pathwise left dyadic sums for continuous finite-variation integrators. Martingale integrals and cross variations use convergence in probability of their corresponding dyadic sums. The integral versions are continuous and adapted where the theorem requires those properties.
For every t ≥ 0, outside one null set independent of t, the target is
The goal is EthierKurtz.ito_formula. It retains every term and both coordinate indices in the cross-variation sum. The bracket and integral witnesses are existential conclusions, so the statement does not require their existence as an extra hypothesis on X.
The formula identifies the effect of a smooth, time-dependent transformation on any process with the stated continuous semimartingale decomposition. In particular, it exposes the second-order correction that distinguishes stochastic change of variables from deterministic calculus. This makes it a general calculus result that can later be applied to diffusion equations, martingale problems, and transformed processes, independently of how the input process was constructed.
The cited theorem is established in the source book. This mission provides a compiled Lean statement and concrete expression dependencies; it does not provide a Lean proof. Formalizing the proof would require the stochastic-integral and covariation infrastructure to support the source's continuous local-martingale setting and version conventions. A solver's result should prove this full statement or develop reusable infrastructure that supports it without changing its hypotheses or conclusion.
The ordinary deterministic chain rule cannot account for the double sum of cross variations. A statement limited to Brownian motion, an absolutely continuous bracket, or a fixed stochastic differential equation would omit cases covered by the source. The local-martingale integral also needs a continuous adapted version with a common almost-sure interpretation over all times; merely obtaining a separate fixed-time limit does not by itself supply that final identity. These requirements make the exact scope of the integral and bracket relations central to the formalization.
The Lean declaration uses ℝ≥0 for time, Fin d → ℝ for state vectors, Measure Ω for the probability law, and Filtration ℝ≥0 for the filtration. It includes completeness of P, the initial-null-set condition on ℱ 0, continuity and adaptation of V and M, local bounded variation of V, stopping-time localization for M, the full decomposition of X, and continuous derivative witnesses for f. The final almost-everywhere quantifier precedes the universal time quantifier. There is no Brownian driver, global square-integrability requirement, right-continuity assumption on the filtration, or diagonal-only bracket simplification.
Five definitions are expression dependencies: IsSourceLocalMartingale, HasCrossVariation, itoStepSum, HasContinuousStieltjesIntegral, and HasContinuousMartingaleIntegral. Their staged declarations retain the reviewed source definitions under a consistent EthierKurtz namespace. The dyadic-sum definitions do not embed the change-of-variables identity, so the theorem cannot be discharged by unfolding a definition of the desired answer. The mission asks for a proof of the stated result, not a weakened special case. The empty-coordinate case is admitted consistently; no positive-dimensional source case is excluded.
Continuous-time Markov processes are often studied through operators that describe how observables evolve. The generation question asks when an operator specified on a domain actually determines a strongly continuous family of contractions. Ethier and Kurtz place this question at the start of Markov Processes: Characterization and Convergence because the resulting semigroup language supports their later treatment of processes and convergence. This mission records the full generation characterization in Chapter 1, Theorem 2.6, and retains the related perturbation result in Theorem 7.1.
Let (E) be a real Banach space. A linear operator (A) has a linear domain (D(A)\subseteq E), which need not equal (E). A family (T(t)), for nonnegative real (t), consists of bounded linear maps (E\to E). It is a strongly continuous contraction semigroup when (T(0)) is the identity, (T(s+t)=T(s)T(t)), every (T(t)) has norm at most one, and (T(t)x\to x) as (t\downarrow0) for every (x\in E). Its infinitesimal generator has exactly those (x) for which the right-hand difference quotient (t^{-1}(T(t)x-x)) converges, and sends each such (x) to the limit.
An operator is dissipative here when
The range condition for a positive (r) says every vector in (E) is (rx-Ax) for some (x\in D(A)). Density means that vectors in (D(A)) approximate every vector in (E). These are independent requirements in the formal statement; neither the domain nor the operator is assumed closed or bounded.
For the related perturbation theorem, (A) and (B) may have different domains. Their sum uses the intersection of those domains. Closure is closure of the graph in (E\times E). A graph closure is required to be the graph of a single-valued operator before it can be called a generator.
The goal is the equivalence
The left side uses the full infinitesimal-generator domain, rather than agreement with a generator only on a smaller subdomain. The right side includes dissipativity for every positive parameter and full surjectivity for at least one positive parameter.
The retained related result assumes that the closure of (A) is single-valued and generates a strongly continuous contraction semigroup, (D(A)\subseteq D(B)), and (B) is dissipative. It further assumes
It concludes that the closure of (A+B) is single-valued and generates such a semigroup, and that its entire graph equals the sum of the graph closures of (A) and (B). This theorem is a related generation variant within the same mission, not a separate main goal.
The equivalence turns an existence question about a family of operators into conditions on a single potentially unbounded operator. In particular, it preserves the exact-domain requirement: proving only that a semigroup generator extends (A) would answer a weaker question. The perturbation theorem then identifies circumstances under which an already generating operator remains useful after adding a dissipative term that need not itself be bounded.
The textbook proves both statements. The Lean files supplied here are statements with intentional proof holes; they do not claim machine-checked proofs. A completed formalization would supply proofs of these source results while keeping the domain, range, closure, and relative-bound conditions shown in the statements.
The hypotheses describe a linear map on only part of the Banach space, while the conclusion requires bounded operators on all of (E) at every nonnegative time. Checking a semigroup law on a convenient subspace is insufficient unless the resulting operators and generator have the stated full domains. For perturbations, graph closure can enlarge a domain. An equality of formulas on (D(A)) alone would therefore omit the theorem's graph and domain conclusion.
Lean uses NormedAddCommGroup E, NormedSpace ℝ E, and CompleteSpace E for the real Banach space; Submodule ℝ E for each domain; D →ₗ[ℝ] E for an operator that need not be bounded; and E →L[ℝ] E for each semigroup operator. Semigroup values at negative real times are unconstrained. The derivative is the right limit through positive times. Graph closure is topological closure in the ambient product, and graph sum requires a common input. The strict relative bound (\alpha<1) and positive resolvent parameter remain explicit.
The reusable definitions are the semigroup predicate, full generator predicate, operator graph, and graph sum. The mission welcomes proofs of the two stated theorems and genuinely source-based supporting lemmas. A model with an empty operator domain, an operator restricted from a larger generator, or a conclusion that drops the graph equality would not satisfy the target.
How few distinct distances can a planar point set determine? The near enemies of this mission are the closest competitors to the extremal configuration: points in no-three-collinear position (no line through three of them) and points lying on a common sphere — the lattice-sphere slice of Erdős–Füredi–Pach–Ruzsa is the motivating example. The bisector energy of a set counts ordered quadruples of points for which the pair and the pair have the same perpendicular bisector; it measures how far the set is from generic. Lund–Sheffer–de Zeeuw fixed the floor of this statistic: is a universal lower bound, and bisector injectivity is sufficient for equality. The Near Enemy theorem is the projection statement on top of it — every admissible set admits one generic projection whose image attains that floor, sits in general position, has zero rotation energy, and carries the whole distance-transport package.
Work with finite sets of points in the Euclidean plane
(EuclideanSpace ℝ (Fin 2)), and in the transport direction with points in
EuclideanSpace ℝ ι for a general finite index type. Following
Lund–Sheffer–de Zeeuw, the bisector energy is
The rotation energy counts the ordered congruent quadruples whose difference
vectors are neither equal nor opposite, so it discards the translation and
half-turn channels and isolates the proper-rotation one. A linear map is
projection-generic for a set when exactly two conditions hold: sends
the difference of any two distinct points of to a nonzero vector, and for
two distinct unordered pairs of the images never combine a parallel pair of
differences with an orthogonal midpoint difference. Perpendicular bisectors,
difference classes and distance images are all Finset operations.
The mission goal is the spherical complete profile: for every finite set lying on a common sphere, in any dimension, there is a linear map to the plane whose image satisfies six conclusions at once —
together with injectivity of on , general position of the image (no three collinear, no four cospherical), and exact distance transport. The projection is chosen per set — its very type depends on the ambient dimension — but a single projection delivers all six conclusions together, and that bundled form is what downstream incidence arguments consume.
Milestones ascend in five steps: the universal energy floor, the bisector-injectivity equality case, the attainment of the floor by projection-generic maps, the existence of such a map for every no-three-collinear set, and the no-three-collinear transport bundle that the goal then specialises to the spherical case.
Lund–Sheffer–de Zeeuw introduced the extremal picture for bisector energy at the level of the exact constant. In footnote 1 on p. 538 of the SoCG 2015 version (LIPIcs vol. 34, 537–552) they state that when every distinct pair determines a distinct bisector, with the enumeration of the trivial quadruples that proves the floor. The universal asymptotic form is a remark in their §3.4.
This mission builds a complete machine-checked development of the
floor, its attainment and the sufficiency direction, from first principles in
Lean 4 over mathlib; the rotationEnergy statistic together with the
rotationEnergy = 0 certificate for the projected image, where
rotationEnergy(P) = 0 follows from the published "distance Sidon set"
property; and a single generic projection of a given set that carries the
bisector floor at the same time as the Erdős–Füredi–Pach–Ruzsa general-position
package. Four of that bundle's six conjuncts are already in
Erdős–Füredi–Pach–Ruzsa 1993, whose Theorem 3.1 supplies them.
Formalizing it matters because the argument composes analysis (generic
projections obtained from nonvanishing of circle determinants), algebra
(inner-product and determinant polynomial witnesses carrying
linear_combination certificates) and counting (fiberwise difference-class
tallies) — and the interfaces between the three must agree exactly. The
projection-genericity and polynomial-witness lemmas are reusable for any
Euclidean extremal formalization.
The hard step is keeping the projection generic through every predicate at once: a projection that preserves no-three-collinearity can still kill a circle determinant, or create a coincidence that the counting needs to keep distinct. The naive first idea — project along a random direction and hope — fails because each predicate forbids a different algebraic hypersurface of directions; the fix is a single simultaneous-avoidance argument over the union, with each forbidden set shown proper by an explicit polynomial witness. That step is the largest proof in the mission and carries its own milestone.
Points are EuclideanSpace; finite sets are Finset; energies are ℕ-valued
statistics. Generic projections are linear maps carrying the explicit
two-clause ProjectionGeneric predicate, so there is no hidden regularity
assumption. Dimension is a general ι with [Fintype ι] wherever the transport
needs it. The goal's only hypothesis is membership of a common sphere;
no-three-collinearity is derived from it rather than assumed, because a line
meets a sphere at most twice. No statement is vacuous: explicit witnesses were
checked in the kernel for the goal and for every milestone.
Welcome contributions: the converse of the equality case — bisector injectivity is proved here to be sufficient for the floor, and necessity is open in this development; sharpness examples beyond the Erdős–Füredi–Pach–Ruzsa configuration; and the incidence assembly that consumes this mission's output.
Geometry.Euclidean.NearEnemyTheorem.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.
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.htmlPhase 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
.