Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
An integer winding label is discrete, but its exponential readout lies on a continuous circle. This mission makes that relationship exact. For a nonzero real algebraic angle , the map
is simultaneously a group character, a faithful encoding of , and a countable dense orbit in the unit circle. Its complex values also form a linearly independent family over the algebraic complex numbers .
The result welds three previously completed interfaces. Circle covering theory produces canonical integer winding. Irrational-rotation theory classifies when an integer orbit is dense. Lindemann–Weierstrass gives the arithmetic rigidity that excludes resonance and algebraic linear relations. The point is not that topology alone proves transcendence, or that transcendence constructs winding: the theorem records the precise composition of the three layers.
The foundations are the completed private missions Winding Dynamics I, Lindemann–Weierstrass I, and Winding Arithmetic II. The transcendence layer is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.
Write for the complex unit circle. For a real angle and integer , define
This is an additive-to-multiplicative character: phase at is , and phase at is the product of the phases at and .
A based Circle loop has a canonical integer , obtained from the endpoint of its zero-based lift through the exponential cover. Its real phase readout is .
The orbit is dense when every nonempty open subset of contains some . It is faithful when distinct integers have distinct phases. These properties are compatible: a countable subset may be dense without being all of the circle.
For every real ,
The proof identifies the phase orbit with integer multiples in and transports Mathlib's irrational-rotation theorem through the standard homeomorphism with the complex unit circle.
If is nonzero and algebraic over , then is irrational. Otherwise would be algebraic, contradicting the proved transcendence of . Consequently the real phase character has dense range.
For the same nonzero algebraic , the character is injective and
is linearly independent over . The first conclusion says no two winding integers alias. The second says no nontrivial finite algebraic-coefficient linear relation exists among the phase values.
For based Circle loops and ,
This consumes the canonical covering-space winding rather than an arbitrary externally supplied integer.
At the full-turn angle , every integer phase is , so the character is not injective. This negative control is outside the algebraic-angle regime because is transcendental. It records exactly why a nonresonance hypothesis is load-bearing.
The capstone exhibits one object with three complementary properties:
This is a precise version of the intuitive claim that winding creates an integer coordinate whose phase representation explores a continuum. The continuum statement is density, not surjectivity: the image remains countable. The arithmetic statement is linear independence, not algebraic independence of the separate phase variables; the character law itself supplies multiplicative relations.
Together with Winding Arithmetic II, continuous homotopy preserves these readouts and a registered reset ledger factorizes their changes. This mission isolates the extra fact that the resulting character is both faithful and dense for every nonzero real algebraic angle.
No single layer implies the capstone by itself. The Circle exponential is periodic, so injectivity requires a genuine nonresonance argument. Density requires the exact normalization by and transport through the AddCircle–Circle homeomorphism in both directions. Linear independence requires the completed Lindemann–Weierstrass theorem, not merely irrationality or transcendence of .
The coercion bridge between the real Circle phase and the complex exponential character is also orientation-sensitive: the formal phase is exactly . Reversing the sign would still define a dense faithful character, but it would not be the registered convention used by the prior winding arithmetic mission.
All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Circle density is stated only for real . The arithmetic conclusions require both IsAlgebraic ℚ α and .
The actual-loop theorem proves equality of phase values if and only if equality of canonical winding integers. It does not claim that the loops themselves are equal, and it does not add a new classification of homotopy classes. That classification remains the responsibility of the Circle covering-space layer.
The theorem proves a faithful representation of winding values, not the existence of winding in an arbitrary physical model. A Kuramoto, XY, or Lohe consumer must still provide a jointly continuous Circle field or a preserved non-simply-connected carrier and readout. No particle–wave or quantum-mechanical interpretation is asserted.
In F-theory, the non-abelian gauge algebra of an elliptic fibration is read off from the Kodaira/Tate type of the singular fibres over the discriminant locus, via the fibre--gauge-algebra dictionary (T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854). For a locally minimal short Weierstrass model , each potentially good additive Kodaira type has a fixed discriminant vanishing order — the entries of Tate's table — and the exceptional types have Dynkin types (the gauge algebra in the split/geometric setting; a nonsplit instead gives ). On an elliptically fibered K3 the global discriminant divisor has degree (the topological Euler characteristic; the formalized affine statement is ), so the total discriminant charge of the singular fibres is capped. This mission formalizes the potentially good additive rows of the Tate table and the resulting 7-brane budget.
Fix a field ; work with , , discriminant (up to the unit ). Write for the multiplicity of as a root of ; for the row, whenever and , write and and set the reduced coefficients , (equivalently the order- and order- Taylor coefficients of and at ). The K3 degree data is , , . The seven potentially good additive types () are encoded by their signatures (HasKodaira), with lower bounds written as divisibility and exact orders as rootMultiplicity.
For of characteristic zero and satisfying the K3 degree data, any finite set of base points, and any assignment of a Kodaira type each point genuinely carries,
Every entry of the table is load-bearing for the budget: the goal converts each into the true local order (milestones 3--9), then bounds the sum by (milestones 1--2). Corollaries recover the physics: at most two , at most two , and at most three fibres (the loci in the split/geometric setting -- a nonsplit gives ); the exceptional budget ; and the residual budget , so two points leave at most for the other fibres. Mathlib has a single-curve WeierstrassCurve/EllipticCurve library but no elliptic-fibration theory: this mission builds a machine-checked slice of the Kodaira/Tate fibre-order table over Mathlib's Polynomial API. The results are classical (Kodaira; Tate's algorithm; Schuett--Shioda, arXiv:0907.0298), so the work is the formalization.
The six "clean" rows () sit at unequal orders , so the order of the sum is the smaller summand's order — an order-of-a-sum computation, valid in characteristic zero where are units. The genuinely hard row is , which needs finer data than the raw orders. Writing , with , , both terms of have order at least , and the coefficient of is ; its nonvanishing gives . This covers the three branches uniformly — only in the branch, where , can two nonzero order- contributions cancel. The nonvanishing is the distinct-roots criterion for the reduced cubic and, under and , characterizes the row; when it vanishes, further valuation data distinguish the series, the higher potentially good types, and nonminimal cases. The budget itself then needs the local-to-global degree bound (milestones 1--2).
Over a characteristic-zero field (intended ), Mathlib-native Polynomial API only (natDegree, rootMultiplicity, roots, taylor). Lower-bound orders use divisibility , which faithfully includes the / () corner that a rootMultiplicity-only encoding drops; exact orders use rootMultiplicity. No global minimality predicate is assumed; at every point classified by HasKodaira, the stated signature implies local minimality (one of , lies below the non-minimal threshold ). The potentially multiplicative and series are excluded by design (their discriminant orders form unbounded families, not fixed by ). The budget goal is an upper bound over the fibres one classifies — it assumes a valid type assignment on but neither constructs it nor proves the existence and uniqueness of the complete Kodaira classification, and need not exhaust the singular locus. A full exhaustive classification, the series, and the literal statement (fibre at infinity via homogeneous forms) are natural future extensions. Characteristic zero is assumed for uniformity, not necessity: the degree bound is characteristic-free and the local order lemmas only need (characteristic ). Over a non-closed field the classification counts -rational affine points; base-change to recovers the geometric statement. Counts are over the affine chart .
Winding number is a topological integer: continuous deformation preserves it, while crossing a branch cut or registering a reset can change it by an integer amount. Transcendence theory gives a different kind of rigidity. For a nonzero algebraic coupling , the phases attached to distinct integers are linearly independent over the field of algebraic complex numbers. This mission joins those statements at their exact formal interfaces.
The result is useful wherever a model first produces an integer winding label and then represents that label by a complex phase. Topology supplies the discrete coordinate, dynamics determines when it is conserved or reset, and Lindemann–Weierstrass supplies arithmetic distinguishability. None of those layers is asked to manufacture the others.
The foundation comes from three completed private missions: Winding Dynamics I: Homotopy Conservation and Reset Balance, Integer Winding Transcendence I: Exponential Phase Independence, and Lindemann–Weierstrass I: Exponential Independence. The transcendence proof is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.
Let be the complex unit circle. A based Circle loop is a continuous path in that starts and ends at . Its canonical real lift through the exponential covering starts at ; the lift endpoint determines an integer .
For and , define the integer exponential character
The arithmetic consumer uses , where is nonzero and algebraic over . Thus a loop carries the phase .
A closed Circle field is a jointly continuous map on the time/spatial square whose two spatial endpoints agree at every time. Each spatial slice is normalized by its moving basepoint, producing a based loop. A carrier/readout segment generalizes this: an ambient trajectory remains in a registered carrier subspace and is observed through a continuous map from that carrier to .
The discontinuous branch is represented separately by a finite reset ledger. It stores successive integer edge-turn cochains. Pairing those cochains with a certified closed edge cycle produces integer winding values and reset periods.
For a family of loops with pairwise-distinct windings,
If the initial windings of a family of closed Circle fields are distinct, then the initial phase family is linearly independent, every phase is unchanged between endpoint times, and the final phase family remains linearly independent. The same conclusion is exposed through the carrier/readout interface.
If a reset ledger has endpoint winding change and registered reset periods , then
This is the multiplicative image of the exact additive ledger balance.
For nonzero algebraic , the character is injective on . Consequently, two actual Circle loops have equal algebraic phase readouts exactly when they have equal canonical winding. On the reset branch,
Thus the multiplicative reset record detects zero net winding change without losing integer information.
The main theorem upgrades conservation of a single integer to conservation of an arithmetic basis. Distinct homotopy classes do not merely retain distinct integer labels: after the algebraic exponential readout, the corresponding phases admit no nontrivial finite linear relation with algebraic coefficients. This lets downstream consumers treat a family of winding sectors as a linearly independent family over .
The reset theorem provides the matching event law. Continuous evolution preserves the basis, whereas a registered reset multiplies phases according to the reset periods. The two branches share one character but retain different hypotheses, so a discontinuous ledger event is not misrepresented as a continuous homotopy.
The algebraic readout is also faithful: despite taking values on the complex exponential curve, it neither aliases two winding sectors nor hides a nonzero net reset behind total phase under the stated algebraic hypothesis.
This does not establish a particle–wave duality or a quantum-mechanical interpretation. It establishes a precise mathematical analogy: an integer topological label has a complex character representation whose distinct values enjoy a strong arithmetic independence theorem under an algebraic nonresonance condition.
The individual deductions are short only because three difficult interfaces have already been proved. Replacing an arbitrary integer map by actual Circle winding requires using the canonical covering lift rather than postulating labels. Preserving the phase basis requires transporting injectivity and linear independence through a jointly continuous moving-basepoint normalization. The reset branch requires respecting the sign convention and mapping a finite sum to a finite product, including the empty ledger.
Several tempting statements would be false. Duplicate winding labels cannot give a linearly independent family. The exponent collapses every phase to . Continuity of finitely many vertex phases does not by itself define a continuous spatial Circle field, and crossing the principal cut can change a discrete principal-turn winding. A global readout from a simply connected carrier such as all of cannot support nonzero loop winding without a separately registered non-simply-connected subcarrier or channel.
For a general complex coupling, exponential resonance can destroy injectivity. The nonzero algebraic hypothesis excludes that resonance here through the proved Lindemann--Weierstrass theorem; it is not merely a convenient side condition.
All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The Circle winding is the floor of the canonical zero-based lift endpoint divided by . Closed fields live on and are normalized at spatial coordinate zero. The coupling is an arbitrary complex algebraic number, not necessarily real, and must be nonzero.
The main carrier/readout theorem is conditional on an explicit continuous carrier-valued trajectory, closed spatial slices, and continuous Circle readout. It does not prove existence of a Kuramoto, XY, or Lohe solution, nor preservation of a particular carrier by such an ODE. Those are model-specific successors.
The reset factorization consumes the registered coherent ledger and certified closed cycle. It is an exact algebraic event law, not an energy estimate and not a claim that every physical trajectory realizes such a ledger. Its vertex and edge types retain the universe-zero scope of the existing reset interface.
What this mission proves, and what it does not. The goal theorem is the explicit upper bound of Erdős, Lev, Rauzy, Sándor and Sárközy (1999) — a published result, now formally verified here. Erdős problem #131 itself is NOT solved by this mission. Erdős asked for the order of growth of , which is known only to lie between and and remains open. A goal theorem reading
Provedtherefore means the 1999 bound is formalized, nothing more.
Call a finite set of positive integers non-dividing if no element of it divides the sum of any nonempty collection of the other elements. The condition is easy to state and immediately restrictive: taking the collection to be a single element already forbids , so a non-dividing set is primitive, and taking larger collections forbids a great deal more. Paul Erdős asked, with Lev, Rauzy, Sándor and Sárközy, how large such a set can be inside . Writing for that maximum, the question is to determine the order of growth of . It remains unanswered, and the gap between what is known from above and from below is a full factor of .
The problem sits at the meeting point of divisibility and additive combinatorics. Its upper bounds come from the theory of non-averaging sets, since every non-dividing set is non-averaging; its lower bounds come from explicit constructions. The two sides have been improved independently for twenty-five years without meeting.
Work inside . For a finite and , write for with removed. Say that is non-dividing when
Two conventions are forced. First, ranges over all nonempty subsets, singletons included, so primitivity is part of the property rather than an extra assumption. Second, must be nonempty: the empty sum is and every divides , so admitting would leave no non-dividing sets at all.
Define the extremal function
A set is non-averaging if no element equals the average of some nonempty collection of the others. Every non-dividing set is non-averaging, which is the link through which the strongest upper bounds arrive.
The goal is the explicit upper bound of Erdős, Lev, Rauzy, Sándor and Sárközy:
The question Erdős actually posed is stronger and remains open:
The bound above is the sharpest explicit constant in the literature, and it is the natural formalization target: it is a clean closed-form inequality valid for every , with a self-contained combinatorial proof, and nothing about it is asymptotic.
Beyond it lies the open question. What is known:
So the truth lies between and , and which end is right is unknown.
The obvious argument gives almost nothing. Pigeonhole on partial sums shows : order the other elements arbitrarily, form the running sums, and if there are more of them than residues modulo then two agree, making a contiguous block sum divisible by . That is genuinely all the elementary argument yields, and it is compatible with as large as .
The difficulty is that the constraint is a statement about exponentially many subset sums, while the conclusion is about a single cardinality. Every strong bound known proceeds by discarding almost all of that information and keeping a structured fragment — contiguous blocks, or the averaging condition — and the loss at that step is exactly what separates from . Improving either side appears to require using the divisibility conditions for several elements simultaneously, which no current argument does.
Sets are Finset ℕ. The forbidden subsets are drawn from A.erase a, so the tested element never appears in the sum it is tested against, and they are quantified as members of (A.erase a).powerset rather than by the subset relation, which makes the property decidable — this is what allows an explicit finite witness to be checked by the kernel rather than asserted. is a Finset.sup of cardinalities over the filtered powerset of Finset.Icc 1 N, so it is a total function with no junk-value caveats and lower bounds on it follow from exhibiting a single set.
The target inequality is stated over ℝ with Real.sqrt, matching the source's rather than any integer rounding of it.
F-theory geometrizes the strongly coupled regime of type IIB string theory by encoding the varying axio-dilaton as the complex structure of an elliptic curve fibered over a base. Non-abelian gauge symmetry is read off from the Kodaira/Tate type of the singular fibres over the discriminant locus, following the fibre--gauge-algebra dictionary of the classification of singular fibres (T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854). The simplest compact example is an elliptically fibered K3 surface, the arena of 8d F-theory and its duality with the heterotic string on ; there the global discriminant divisor has degree ("24 seven-branes", equal to the topological Euler characteristic ; the formalized affine statement is ), and an elliptic K3 can contain at most two type II* fibres. A configuration with two such fibres realizes the enhancement familiar from eight-dimensional heterotic/F-theory duality.
Fix a field and work with the (short) Weierstrass model whose coefficients are polynomials on the affine base line. Its discriminant is (the usual discriminant up to the unit ). For write for the multiplicity of as a root of , and for its degree. A base point is an point when and (the vanishing orders of a Kodaira type II*). The Calabi--Yau/K3 degree data condition is , , and .
for of characteristic zero and satisfying the K3 degree data, together with finiteness of that set.
The count of points controls the maximal non-abelian enhancement of an elliptic K3: two disjoint type II* fibres consume of the global discriminant budget of (), leaving at most units for the remaining singular fibres, and realize ; a third is obstructed (). This is the F-theory count underlying the two factors of the 8d heterotic string, and a prerequisite for classifying 8d gauge groups. (It bounds the number of factors; it is not by itself the full rank- statement, which additionally involves the Shioda--Tate/Neron--Severi lattice.)
On the formalization side, Mathlib has a substantial single-curve WeierstrassCurve/EllipticCurve library but no theory of elliptic surfaces or elliptic fibrations: discriminants as sections over a base, vanishing orders, and fibre counting are absent. This mission builds the first fibration-level results directly on top of Mathlib's Polynomial API. The results are established classically (Kodaira; Tate's algorithm; the Euler-number/discriminant-degree identity in M. Schuett and T. Shioda, Elliptic Surfaces, arXiv:0907.0298), so the work here is the machine-checked formalization, not new mathematics.
Two things are worth separating.
The cardinality bound itself is elementary. An point forces , so distinct points contribute coprime factors of ; then already caps their number at two (). This uses neither the discriminant, nor , nor characteristic zero. The goal is stated in the finiteness-and-cardinality form precisely so it cannot be satisfied vacuously.
The fibration-level content is the milestones, which are the genuine Kodaira/Tate statements and are independently meaningful: that an point contributes exactly to the discriminant order (milestone 2 -- an order-of-a-sum computation valid because and are units in characteristic zero); the global degree bound (milestone 1); and the local-to-global inequality (milestone 3). These are the load-bearing steps for the stronger statements about points coexisting with other fibres -- e.g. that fixing two points leaves only degree of discriminant for all remaining singular fibres () -- which is the natural next goal and cannot be shortcut through .
Everything is stated over a characteristic-zero field (the intended model is ) using only Mathlib's Polynomial API: natDegree, rootMultiplicity, roots. The discriminant is (up to the unit ). An point is IsE8Point: and . The predicate IsK3Data fixes , , -- the degree bound characterizing the maximal (K3) elliptic surface and below; it is not a full surface-theoretic K3 hypothesis. To rule out a trivializing reading: the goal asserts finiteness of the -point set conjoined with the cardinality bound, so it cannot be satisfied vacuously through the convention that an infinite set has cardinality ; and is assumed wherever is used as a bound.
Convention note. Mathlib's rootMultiplicity is at the zero polynomial, so IsE8Point implicitly forces and ; in particular the degenerate type II* locus (where morally holds) is excluded by this encoding. This only shrinks the -point set, so it does not affect the bound; a faithful -inclusive definition is a candidate refinement.
Characteristic zero is assumed for uniformity rather than necessity: the degree bound is characteristic-free, and the local order calculation only needs (characteristic ). Over a non-closed field the count is of -rational affine points; base-change to recovers the geometric statement. The count is taken over the affine chart ; the literal statement (adding the fibre at infinity via homogeneous forms) is a natural extension and a welcome future contribution, as are the remaining Kodaira/Tate fibre-order lemmas.
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.
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.Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.
Work in an arbitrary abelian group (Lean: AddCommGroup G). For finite
, the additive energy counts quadruples
with ; the trivial maximum is when
. The sumset is , and the difference set
is defined pointwise. A set has small doubling when is
linear in . The Lean development uses Finset.addEnergy and
Finset.addConvolution from Mathlib.
A bipartite graph here is an edge set of type Finset (G × G) with
, not a Mathlib SimpleGraph; solvers should state
graph hypotheses that way. Given such an , the partial sumset
is , following Tao–Vu Definition 2.28.
The mission goal is the two-set (equal-cardinality) form:
This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps and existential; the explicit-constant variant is proved separately in the mission with .
The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.
The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.
Formalizing it matters because the constants are the content: the development
tracks explicit constants through dependent random choice (graph level
and ; energy level
and ),
which paper proofs often leave implicit. Fox–Sudakov state the application for
sets of integers; the formalization is over an arbitrary AddCommGroup, with
no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1)
contains no BSG statement, so this fills a genuine upstream gap.
The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.
Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's and terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.
Sets are Finset G in an AddCommGroup G with DecidableEq; energy is
Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise
sumset and difference operations from open scoped Pointwise. Density
hypotheses are stated with explicit real constants. The counting lemmas at the
bottom of the development (sum_addConvolution_eq_card_product,
path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are
unconditional; the statements that need them carry the nonemptiness,
equal-cardinality and density hypotheses that exclude degenerate zero-energy
configurations. Welcome contributions: the single-set polynomial
Freiman–Ruzsa consequences, and non-abelian variants.
Finset.pluennecke_ruzsa_inequality_nsmul_add;
see G. Petridis, New proofs of Plünnecke-type estimates for product sets in
groups, Combinatorica 32 (2012), 721–733
(arXiv:1101.3507).Combinatorics/Additive/BalogSzemerediGowers and
BSGEnergyToGraph.The first two missions in this programme counted order-three squares. Mission I proved MacMahon's magic count and Mission II his semi-magic count . What neither does is classify: counting tells you how many squares there are, but not what they look like.
This mission closes that gap for the most classical case of all. A normal magic square of order three is a array containing each of exactly once, whose rows, columns and two main diagonals all sum to the magic constant . The statement to be proved is the uniqueness of the Lo Shu square:
every normal magic square of order three is one of the eight images of under the symmetry group of the square.
In particular there are exactly of them, and they form a single orbit under the dihedral group .
MacMahon's parametrization (already formalized in MagicSquaresParam3) writes
every order-three magic square of line sum as
with ranging over the finite admissible set paramSet e. For a normal
square the magic constant is , so and the centre entry is .
Normality (IsNormal) means every entry lies in and the nine entries
are pairwise distinct — equivalently, they are a permutation of .
together with the identification of those eight parameter pairs. By the
bijection magic_three_param_bij this is exactly the statement that there are
eight normal magic squares of order three, i.e. that Lo Shu is unique up to the
symmetry group of the square.
magic_three_normal_classify). Within that range,
is normal exactly when is one ofThe eight surviving pairs are precisely those with distinct corners of
the Lo Shu square; the excluded ones are those with , for which the
entry collides with the centre .
3. Converse (magic_three_normal_converse). Each of the eight pairs really
does give a normal square.
The result itself. The uniqueness of Lo Shu is the oldest non-trivial classification in combinatorics — it is the order-three case of the classification problem for magic squares, and the reason is special: for there are normal squares (up to symmetry) and for no classification is known. Formalizing it shows that the counting machinery of Missions I and II can be turned around and used as a classification tool: the parametrization plus a finite verification give the complete list, not just the cardinality.
Formalizing it. The whole proof is a finite case check over parameter pairs, so the mathematical content is small and the formalization difficulty is concentrated in making the finiteness usable. Two things have to be arranged before automation can see the problem:
IsNormal is stated with a Function.Injective, which is not decidable
as stated; it must first be rewritten into an explicit conjunction of
entrywise bounds and pairwise inequalities over Fin 3.Fin 3 do not unfold by simp alone; one needs
Fin.forall_fin_succ to expand them before norm_num can decide the
resulting ground instances.Finiteness must be manufactured. Nothing in IsNormal mentions a bound on
or , so the first step is to derive from the entrywise
bounds of normality. Skipping it leaves an infinite search that interval_cases
cannot start.
Truncated subtraction. The parametrization is written over , so entries such as and truncate at zero. Every ground instance must be evaluated with the truncation in place — which is why the classification is carried out by evaluating the actual entries rather than by manipulating symbolic inequalities.
IsNormal).MagicSquaresParam3 and the bijection of Mission I.IsNormal for
Fin 3 (and the Fin.forall_fin_succ technique for unfolding finite
quantifiers), the list of the eight Lo Shu parameters, and the order-three
classification itself.The distinct-distances problem asks how few distinct distances a finite planar point set can determine. Guth and Katz proved the near-optimal bound in 2015. Their argument passes through incidence geometry: distances become incidences between points and curves, and the Elekes–Sharir framework converts the problem into an incidence bound for lines in three-space. Pach and de Zeeuw showed the same pipeline works for points on a fixed algebraic curve, replacing line incidences with curve incidences. The algebraic prerequisite for that replacement — that two bounded-degree real plane curves with no shared component meet in finitely many points, with an explicit degree-dependent bound — is what this mission formalizes.
A real plane curve here is the real zero set of a nonzero bivariate polynomial , written . Its total degree is the maximum over monomials with nonzero coefficient. A curve is irreducible when its polynomial is irreducible.
The paper says two curves have a common component when their polynomials
share a nonconstant factor. The Lean development uses a different, weaker
hypothesis, NoCommonCurveComponent: no infinite irreducible real curve lies
inside both sets. A shared factor whose real zero set is finite (for example
) violates the paper's hypothesis but satisfies the Lean one, so the
Lean theorem covers strictly more pairs of curves than the paper's statement.
Currying views as a univariate polynomial in one coordinate whose
coefficients are polynomials in the other. In the Lean code the polynomial
variable is coordinate and the coefficient (base) variable is coordinate ;
this description writes the base coordinate as and the fiber coordinate as
, so a line is called vertical. The resultant of two
curried polynomials is a polynomial in alone. The development uses one
direction of its defining property: if the two specializations at share a
real root, the resultant vanishes at . All Lean statements use
MvPolynomial (Fin 2) ℝ for plane polynomials and EuclideanSpace ℝ (Fin 2)
for points.
The mission's goal is a finite-intersection bound in the spirit of Theorem 2.1 of Pach–de Zeeuw (Bézout's inequality), but it is not that theorem. It differs in both directions:
The six milestones are the algebraic inputs: coefficient-root counting, the two
resultant-nonvanishing criteria, the fiber bound, and the two mixed
vertical/nonvertical pair bounds that carry the constant . The
nonvertical–nonvertical pair bound (primitive_nonvertical_pair_intersection_bound)
carries the cruder constant . Above the
milestones sit the irreducible-pair assembly with constant and
the factorized assembly with constant , from which the goal
follows.
The result is the algebraic input to the Pach–de Zeeuw distinct-distances theorem for points on curves: without a uniform finite-intersection bound, the incidence count that drives the distance bound cannot even be stated. The formalization pins down every constant and every non-degeneracy hypothesis (non-verticality, no shared infinite component, coprimality) that the argument consumes.
The proof composes four toolkits — univariate root counting, Sylvester-matrix
resultant degree bounds, normalized-factor decompositions, and a smooth
implicit-function nonsingularity argument — whose interfaces must agree
exactly. The resulting lemmas (resultant criteria, fiber bounds,
partial-derivative degree bounds) are reusable for other real-algebraic
incidence formalizations over MvPolynomial.
The central difficulty is elimination with explicit constants: the resultant converts a two-variable intersection problem into a one-variable root count, but every step (currying, specialization, factor-pair summation) must preserve a usable degree bound, and the degenerate configurations (vertical fibers, shared factors with finite real zero set, singular points) each need a separate finite bound.
The textbook route — Bézout's inequality over , then observing that real intersection points are complex ones — is not taken, for two reasons. Mathlib has no plane-curve Bézout theorem to invoke. And under the weaker Lean hypothesis the two polynomials may share an irreducible factor with finite real zero set, in which case the complex intersection is infinite and no complex count applies; that branch is closed by bounding the singular points of the shared factor instead.
Points are EuclideanSpace ℝ (Fin 2); curves are MvPolynomial (Fin 2) ℝ
zero sets; finiteness is Set.Finite with Set.ncard bounds. The development
commits to total degree (not weighted degrees) and to the currying order that
eliminates Lean coordinate ; variable-style implicit degree bounds
are explicit {d₁ d₂ : ℕ} binders on the platform. No statement is
vacuous: every intersection bound carries the non-degeneracy hypothesis
(non-associated irreducibles, non-divisibility, nonzero partials) that excludes
the infinite-intersection cases. Contributions welcome: the sharp
general bound (currently an existential constant), the paper's hypothesis form
(no common factor at all), and the incidence assembly that consumes this
mission's output.
PachDeZeeuw.AlgebraicPrelim and PachDeZeeuw.Bezout (mathlib-only,
axiom-clean).Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by . The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most , giving an -approximation.
Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.
An instance consists of a finite type of elements, a finite type indexing available sets, an assignment , and a nonnegative cost . Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are
The frequency of an element is the number of sets containing it, and denotes the maximum frequency over all elements.
The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given covers is strictly stronger than coverability of the family.
Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when is empty, and the -approximation bound reads , which the certificate's tightness clause forces to be rather than anything false.
The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.
A primal-dual certificate is a pair where covers , is dual-feasible, and every has a tight dual constraint, .
For any primal-dual certificate and any fractional cover ,
Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover costs at most times the fractional optimum and a fortiori at most times the integral optimum.
The one substantive step of the goal is split out as its own target: for a primal-dual certificate,
Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most times. With this and weak duality, the goal is two lines.
A greedy certificate at ratio is a cover and a nonnegative with and for every . For such a certificate and any fractional cover ,
Instantiating is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.
Every dual packing is bounded by every fractional cover, ; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.
This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no -approximation result to build on.
The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.
Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.
Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.
This is the second mission in the magic-squares formalization programme, and it takes up the case the first one deliberately left open.
Counting semi-magic squares — arrays of nonnegative integers whose rows and columns all share a common line sum, with the diagonals unconstrained — is the "honest" version of the enumeration problem. For order three the magic count (mission I) is only a quasi-polynomial: it vanishes unless and equals on . The semi-magic count has no such periodicity. MacMahon computed it in 1915:
It is an honest polynomial in of degree , and that degree is not an accident: Ehrhart and Stanley proved that for every order the function is a polynomial of degree satisfying the reciprocity law . The order-three formula above is the smallest nontrivial instance of that theorem, and the only one small enough that every step of the derivation can still be exhibited explicitly.
So this mission is the natural companion to mission I: same objects, same platform vocabulary, but the counting step is genuinely harder — the parameter space is four-dimensional rather than two, and the parametrization is not injective until it is normalized.
Fix and a line sum . A square of order is an array of nonnegative integers.
For the whole family is governed by the six permutation matrices. Split them into the three even ones — the identity and the two -cycles — whose supports are the transversals
and the three odd ones — the transpositions — with supports
Adding them with multiplicities (even) and (odd) gives
whose six line sums all equal ; so this is a semi-magic square of line sum whenever the multiplicities sum to .
This is the goal because it is the weakest statement that still pins down the answer: it asserts the shape of without naming the parametrization, and it survives verbatim as the case of Stanley's theorem that is a polynomial of degree .
sm3_canonical). Every semi-magic
square arises from the display above, and the representation becomes unique
after normalizing: put , , , subtract the
corresponding even permutation matrices, and the residual odd multiplicities
satisfy . The normalization is necessary — without it the
single relationidentifies distinct -tuples — and it is exactly what makes the count a
partition rather than an inclusion–exclusion.
2. Bijection (sm3_bij). The map from normalized coefficient vectors to
semi-magic squares is a bijection, so .
3. Stars and bars (comps_card). The number of -tuples of nonnegative
integers summing to is ; the case is what the
count needs.
4. Evaluating the parameter count (sm3_params_card). Partitioning the
normalized vectors according to the first zero among writes
as
which collapses to by two applications of Pascal's identity.
The result itself. is the case of a theorem that launched a subject: Stanley's proof that counts lattice points in the Birkhoff polytope makes an Ehrhart polynomial, and the order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717) revisited exactly this computation on the way to their quasi-polynomial theorem for the magic counts, and Beck and Zaslavsky later pushed the same technique to the panmagic and symmetric refinements. Getting machine-checked therefore validates the whole hierarchy at its base.
Formalizing it. Nothing here is open; the mathematics is a century old. What is missing is the formalized artifact, and the difficulty is concentrated in two places that are formalization difficulties rather than mathematical ones.
First, surjectivity of the permutation-matrix parametrization. The usual proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem. For order three one can instead do it by hand: subtract the three even transversal minima and show that the residual satisfies . That last step is a six-case argument in linear arithmetic — if then each of the three ways for the transversal to have minimum zero forces — and it is precisely the kind of step that is invisible on paper and must be made explicit in a proof assistant.
Second, the counting step. The parameter set is a filtered finset of
functions Fin 6 → Fin (t+1), while the formula is stated with binomial
coefficients over . Connecting them requires stars-and-bars, proved
from scratch (by induction on the number of parts plus the hockey-stick
identity), because the available library results count sub-multisets rather
than compositions. And the final collapse to MacMahon's form is a chain of
Pascal identities that must be applied in the right order to stay inside
, where subtraction is truncated.
Two traps deserve to be named.
Uniqueness needs the normalization. The representation by six multiplicities is not injective: . Any formalization that counts -tuples directly will overcount, and the correction is not a subtraction but a choice of canonical representative. Deciding "first zero among " is what turns the count into a genuine partition.
Truncated subtraction. The decomposition is expressed over , so every identity — in particular the recovery of the multiplicities from a square — must be stated with the admissibility inequalities as explicit hypotheses. A truncated subtraction is only correct because normalization forbids the truncation, and that side condition has to be discharged rather than assumed.
Fin n; semiMagicCount n t is the cardinality of a
finset of arrays over Fin (t+1) — lossless, since every entry is at most
.Counting magic squares — arrays of nonnegative integers whose rows, columns and two main diagonals all share a common line sum — is one of the oldest problems in enumerative combinatorics, and the testing ground on which the general theory was built. MacMahon computed the order-three count in 1915 by hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717), showed that for general order the counting functions are quasi-polynomials in the line sum, by identifying them with Ehrhart quasi-polynomials of rational polytopes. The order-three case is the oldest nontrivial instance of that theory and the one where every step can still be checked by hand.
The subject therefore has a curious status: the enumerative answer for has been known for over a century, and the structural facts behind it (a magic square is determined by two corner entries; opposite cells sum to twice the centre) are folklore — but none of it has a machine-checked proof. This mission formalizes the classical derivation end to end.
Fix an order and a type of entries. A square of order is an array with entries in ; its row sums, column sums, and the two diagonal sums (main and anti-diagonal) are the sums of the entries along those lines.
No distinctness of entries is required. Let denote the number of semi-magic and the number of magic squares of order with nonnegative integer entries and line sum . Every entry of such a square is at most , so these are finite counts.
For the whole family is parametrized. If has line sum then the centre cell equals , and writing and the eight line identities force
All nine entries are nonnegative exactly when
and substituting , turns these into : the ball of radius in .
together with the companion vanishing when . This is the count of magic squares of line sum with nonnegative integer entries (entries need not be distinct). It is the goal because it is the weakest stable statement: it asserts only the shape of the answer, not the intermediate parametrization, and it survives verbatim as the case of the general quasi-polynomial theorem.
That the map is a bijection from the magic squares of line sum onto the admissible parameter pairs, and that the latter are counted by the -ball cardinality. This is the route the mission actually takes; the count is its corollary.
, the analogous count for semi-magic squares, is a genuinely different and harder quasi-polynomial. It is listed as a stretch target, not a milestone.
The result itself. MacMahon's formula is the base case of the Ehrhart-theory reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's quasi-polynomial theorem for general degenerates to it at , so it is the sanity check any generalization must pass. The parametrization behind it is what makes the "how many" question finite-dimensional at all: it reduces a search over arrays to a count of lattice points in a two-dimensional ball. Downstream, the same parametrization governs the classification of normal magic squares (the Lo Shu square and its symmetries) and the associativity identity .
Formalizing it. The mathematics is classical and proved; nothing here is
open. What is missing is the formalized artifact. The order-three structural
lemmas — the centre identity, the opposite-cell identity, and the two directions
of the parametrization — are already machine-checked on this platform. The
remaining work is the counting step: exhibiting a concrete bijection between
two finsets whose elements live in different types (arrays over Fin (3e+1)
versus pairs of naturals) and evaluating a finite sum. That is where the
formalization, not the mathematics, is hard.
The obvious attack — "each magic square is determined by , so just count
the pairs" — fails at exactly one point, and it is not a mathematical point. The
counting function is defined as the cardinality of a finset of arrays with
entries in Fin (3e+1) (a finite type, so that Finset.univ exists), whereas
the parametrization lives over . Proving the counts agree therefore
requires a honest Finset.card_bij in both directions:
mkMagic3 from an admissible pair, coerce every entry into
Fin (3e+1) using the bound , and show the round trip is
the identity.Neither direction is deep, but the coercions are unforgiving: a truncated
subtraction in mkMagic3 is only correct because admissibility forbids the
truncation, and that side condition must be discharged explicitly rather than
assumed. The second difficulty is the cardinality of the ball: the
identification needs the elementary identity
, after which the count is
.
Fin n; the anti-diagonal uses Fin.rev, and broken
diagonals use addition modulo . Counting functions are cardinalities of
finsets of arrays over Fin (t+1) — lossless, since every entry is at most
— and return natural numbers.mkMagic3 is defined over with truncated subtraction. Every
row/column/diagonal identity therefore carries the admissibility inequalities
as explicit hypotheses; no identity is asserted unconditionally.Square, IsSemiMagic,
IsMagic, IsPanMagic, IsAssociative, IsNormal, magicConstant, and the
four counting functions ), the symmetry/affine toolbox, and
the order-three structural lemmas. Contributions are welcome on the
semi-magic count , on panmagic and associative refinements, and on the
extension to general .An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.
This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs per day and buying costs once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic -competitive algorithm, and a randomized algorithm whose competitive ratio tends to , due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.
An instance is a pair : the purchase price , a positive integer, and the number of ski days, which the online algorithm does not know. An offline solution either buys at once, paying , or rents on every day, paying ; so the offline optimum is
Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable and one rent variable per day :
Its dual is a packing program with one variable per day:
The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.
The fractional primal-dual algorithm maintains , initially . On each new day, while it sets , then raises
and sets ; once has reached it does nothing further. The free parameter is then pinned to the value that makes reach exactly after days,
The coefficient is the exact finite- ratio , left in closed form rather than replaced by a constant. This is deliberate: increases to , so and therefore for every finite . A goal asserting -competitiveness at finite would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.
The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.
Chapter 3's other result, independent of the fractional development.
The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.
On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.
The offline problem is trivial, and a newcomer's first move — prove is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:
The optimum is never observed. The algorithm's cost must be compared against without being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.
The growth law is piecewise. The update fires only while . Summing the per-day increments therefore does not telescope uniformly: days before reaches contribute each and later days contribute nothing, and the index at which the switch happens is exactly — which is a theorem about the recurrence, not an assumption.
The constant is forced, not chosen. is not a free tuning parameter; it is the unique value for which the geometric sequence hits at , which is in turn what makes the dual solution feasible (). Dual feasibility and the choice of are the same fact.
Conventions this development commits to. The purchase price is a natural number with , because Chapter 3 uses simultaneously as a price, as a day index ("buy skis on the th day"), and as the exponent in ; costs are real numbers, with and coerced. Days are indexed from , so day of the prose is index , and Fin k indexes the days. Real division is total, so ; the hypothesis is what keeps every reciprocal in the development genuine, and without it would evaluate to and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day .
A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting and each range over ; Figure 3.1 on p. 18 prints only , . This mission takes the prose version, and , as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value , so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.
Ruling out a trivializing formalization. The offline optimum is defined independently, as , and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to times the number of days on which — so it cannot be weakened into vacuity without becoming false.
Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.
Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold uniformly and buying on the day whose increment of contains . That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.
Bayesian filtering estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.
The Discriminative Kalman Filter (DKF) uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in Theorem 2 of Appendix B.
The historical starting point is the linear Gaussian filter of Kalman (1960). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.
The state space is for a positive finite dimension . Write for the ordinary multivariate Gaussian density with mean and symmetric positive-definite covariance . Densities and their distances are with respect to Lebesgue measure.
The state model has a matrix and positive-definite covariance matrices satisfying
Its stationary density and transition density are
For an integrable density , prediction gives
The discriminative update combines a previous filtering density with a density for the state given the current observation:
This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by is part of the standard DKF under consideration.
For Gaussian inputs with parameters and , define
The DKF step returns mean and covariance when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance , using the current observation's functions and as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the paper.
Fix sequences of probability densities , indexed by positive integers, whose exact normalized updates
are well defined for every index. Fix Gaussian density sequences , a point , and a probability measure . The five assumptions are
Here denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; is the unit point mass at . The measure need not have a density and may be degenerate.
The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:
is a well-defined Gaussian density for all sufficiently large .
A sixth milestone is Lemma 1 (DKF equation): the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to . It includes both the exact equation and the asymptotic assertion from the source.
In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.
The inverse stationary density can grow in the tails, so small errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.
There is a second distinction between convergence to a point mass and approximation in . Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.
Lean represents states as Fin d → ℝ and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.
Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.
All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.
The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.
A foundation model trained on tokenized electronic health record (EHR) timelines can be used to predict clinical outcomes without ever being finetuned for a specific prediction task: condition the model on a patient's observed timeline, autoregressively sample many possible futures, and report the fraction of sampled futures in which the outcome of interest occurs. This generative approach to inference powers a growing family of EHR foundation models— including Event Stream GPT (McDermott et al., 2023), Foresight (Kraljevic et al., 2024), ETHOS (Renc et al., 2024), and Curiosity (Waxler et al., 2025)—and it is attractive for its zero-shot approach to predicting a variety of outcomes.
It is also expensive. Reproducing one published pipeline required more than A100 GPU-hours of inference. Worse, the estimator built from sampled futures takes values in , so its resolution is tied to the sampling budget: for an outcome of prevalence , sampled futures fail more than of the time to rank a patient at ten times average risk above an average one. The most consequential clinical decisions turn on exactly such low-prevalence, high-impact outcomes.
Solo et al. (arXiv:2602.03730) observe that Monte Carlo discards almost everything the model produces: at every step the model emits a full next-token distribution and the sampler keeps only the token it drew. The paper introduces two estimators that consume the discarded probabilities instead, and proves that doing so costs no bias and—for one of them—never costs variance.
Let generate token sequences from a countable vocabulary , with designated outcome token . The next-token probabilities may depend on the complete preceding history. The time threshold is initially unexceeded. Its crossing may depend on several kinds of time-spacing tokens and on their accumulated duration.
For a sampled timeline , is the first position occupied by , or if it never appears. The time is the first position at which the threshold has been exceeded. Assume almost surely. Timelines are retained through the actual threshold crossing, even if the outcome appears earlier. Thus is not reassigned after an outcome.
The threshold is reached almost surely, but the number of tokens required may be arbitrarily large. No deterministic bound or finite expected token count is assumed. For REACH, assume also that removing the outcome token and renormalizing defines a sampler that reaches the same threshold almost surely.
For independent original timelines, the Monte Carlo estimator is
The SCOPE estimator is
For REACH, sample independent outcome-free timelines by setting the next-token probability of to zero and renormalizing the probabilities of the other tokens. Using the original model probabilities along those timelines, define
The targets are:
Expectations and variances use each estimator's specified sampling law.
The claims concern the probability assigned by the generative model. They provide unbiasedness and a comparison of sampling variance. SCOPE is kept unclipped, as in the paper's unbiasedness result. All five target statements have accompanying local Lean proofs.
A pathwise finite stopping time need not have a common finite bound or a finite mean. An expectation involving the stopped SCOPE sum therefore needs justification beyond finite-sum linearity. REACH uses a different sampling law, so its unbiasedness and variance comparison also require a proved connection between the original event and the two-stage experiment. The equal-probabilities milestone records that connection explicitly.
Lean represents each sampled timeline by a finite list ending at its first threshold crossing. Arbitrary finite lengths are included in the same sample space. Path probabilities are products of next-token probabilities, and the laws are countable sums of these path masses. Requiring each law to have total mass one expresses almost-sure termination of that sampler; it is not a uniform length bound. The vocabulary can be finite or countably infinite.
The stopping predicate examines a complete prefix and is not restricted to a single terminal token. The original law continues through outcomes until the threshold. A separate almost-everywhere hypothesis excludes equal outcome and threshold times. The code proves that the actual threshold time is finite almost surely and that the strict event is the event used by the internal calculations.
The two-stage experiment explicitly samples conditionally independent Bernoulli trials using the original hazards. Its conditioning information retains the complete indexed pool of outcome-free timelines. The Rao–Blackwell target uses Mathlib's conditional expectation. The variance target uses Mathlib's variance, and proves square integrability rather than assuming it.
Essentially every quantitative model written as a rate of change — a mechanical system, a chemical reaction network, a population model, a control loop — is an ordinary differential equation (ODE) together with an initial condition. Before anything can be computed about such a model, two questions must be settled: does a solution through the given initial state exist, and is it the only one? The classical answer is the Picard–Lindelöf theorem: a Lipschitz right-hand side yields a unique local solution. Uniqueness is not a technicality — it is what licenses speaking of the trajectory through a point, hence of a flow, and so it underwrites the entire qualitative theory of dynamical systems that the source text builds afterwards (vector fields, tubular flow, -limit sets, Poincaré–Bendixson, Grobman–Hartman, stable manifolds).
This mission is the first in a series formalizing Augusto Armando de Castro Júnior's lecture notes Curso de Equações Diferenciais Ordinárias (2009), a graduate ODE course that develops the theory directly in Banach spaces, not only in . The book proves existence and uniqueness once, in that general setting, and then reuses it throughout; this mission formalizes that foundation.
Let be a real Banach space, , , and . Write for the closed ball and
A map is Lipschitz with respect to the second variable with constant if
the same serving for every (Definição 2.1.1 of the source).
Given , the Cauchy problem (initial value problem) with initial data asks for a curve , defined on a nondegenerate interval , such that for all , , and for all — one-sided derivatives at the endpoints of (Definições 1.0.1 and 1.1.1). Equivalently, by the Fundamental Theorem of Calculus, is continuous with graph in and satisfies the integral equation
Finally, put and .
The goal theorem is Teorema 2.1.2 (Picard) of the source: if is continuous, bounded, and Lipschitz in the second variable, then the Cauchy problem , has a solution on , and any two solutions on that interval whose graphs stay in coincide there:
The milestones are the results the source uses to get there, in its own order: the contraction fixed point theorem (Teorema 0.2.10), the equivalence between the Cauchy problem and the integral equation (Capítulo 2, opening paragraphs), the sufficient condition for Lipschitz dependence via a bounded partial derivative (Proposição 2.1.4), and the global version on a whole interval (Corolário 2.1.3).
Picard's theorem is what makes the initial value problem well posed in the sense of Hadamard's first two requirements. Downstream in the same book it is the hypothesis behind maximal solutions and the escape-from-compacts property (§2.3), continuous and differentiable dependence on initial conditions and parameters (Chapter 3), and the local flow of a vector field (Chapter 4). Without uniqueness none of these statements can even be phrased.
As for formalization status: Mathlib already contains a Picard–Lindelöf development
(IsPicardLindelof, ODE_solution_unique and relatives) and a Banach fixed point theorem
(ContractingWith.exists_fixedPoint). The work this mission asks for is therefore not the
discovery of a proof but a faithful bridge: stating the source's hypotheses as the source states
them — a closed ball, a supremum bound , the radius , Lipschitz in the
second variable with one constant for all times, uniqueness among solutions whose graph stays in
the domain — and deriving them from, or proving them alongside, the library's own formulation.
Such bridges are where unfaithful formalizations usually hide, and they are reusable by every
later mission in the series.
The obvious route is "cite the library and close the goal". It does not go through unchanged, for three reasons. First, the hypothesis shapes differ: the library packages its assumptions in a structure with its own choice of ball, bound and time radius, and matching with a supremum-defined requires the boundedness argument to be redone at the interface. Second, uniqueness here is asserted for solutions in the sense of this mission's definition — derivative within the interval, one-sided at the two endpoints, graph inside — so a Grönwall-type uniqueness statement must be transported to that formulation, including the endpoint cases. Third, the source works with an arbitrary Banach space and only assumes bounded, rather than assuming finite dimension; compactness arguments are unavailable by design.
The remaining genuine mathematical content sits in the milestones: the iterate estimate used by the source to make some iterate of the Picard operator a contraction, and the mean value inequality on a convex open set behind Proposição 2.1.4.
Conventions this proposal fixes, all visible in the definitions item:
A complete development needs the Bochner and interval integrals, the contraction mapping API, the mean value inequality for Fréchet derivatives, and the ODE files. Contributions of independent interest to the series: the Picard iterate factorial estimate, and the conversion between the library's Picard–Lindelöf hypotheses and the ones above.
Mathlib/Analysis/ODE/PicardLindelof.lean and Mathlib/Analysis/ODE/Gronwall.lean,
https://github.com/leanprover-community/mathlib4.In 1918 Emmy Noether published Invariante Variationsprobleme (Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-phys. Klasse, 235–257), answering a question raised by Hilbert and Klein about the status of energy conservation in the general theory of relativity. The paper proves two theorems that tie the symmetries of a variational integral to structural properties of its Euler–Lagrange equations: continuous symmetries depending on finitely many parameters produce divergence identities ("conservation laws"), while symmetries depending on arbitrary functions produce identities among the Euler–Lagrange expressions themselves, so that some of the field equations are consequences of the others. The first theorem is the source of the correspondence between time translation and energy, space translation and momentum, rotation and angular momentum; the second underlies the Bianchi-type identities of generally covariant theories and the gauge identities of field theory.
This mission formalizes the two theorems of §1 of the paper, together with the chain of identities of §2 and §3 by which Noether derives them, in the case of first-order Lagrangians.
Fix integers (independent variables), (dependent variables). Points of the base are , and a field is a map , written componentwise . Write for the derivative of a scalar function on along the -th coordinate direction, and
for the divergence of a vector field on .
A Lagrangian is a function of the point , of the field value , and of the array of first derivatives . Along a field one writes , and the integral under study is . The momenta are
and the Lagrange expressions — the left-hand sides of the Euler–Lagrange equations — are
An infinitesimal transformation is given by generators on the independent variables and on the dependent ones. Noether's equation (9) replaces them by the variation at fixed ,
and the corresponding variation of the Lagrangian is
Two vector fields organise the boundary terms: the partial-integration vector of equation (3), and Noether's
Invariance of enters through Noether's equation (11), the pointwise identity
which the paper derives in §2 from the vanishing of over every region.
The goal theorem is Theorem I of the paper, in the first-order case, in the form Noether states as equation (13). Given generators , , each satisfying the invariance identity (11) with its own from (9), one has for every and every
The milestones are the intermediate statements of the paper, in the order in which it proves them: the central identity (3), the passage from the invariance of the integral to the pointwise identity (11), the single-generator divergence identity (12), the conservation law on solutions of the Euler–Lagrange equations (§3), the converse of Theorem I (§3), and Theorem II in the form of the dependency relations (16) for a group depending on arbitrary functions entering to first order.
Theorem I is the general statement behind every "first integral from a symmetry" argument in mechanics and field theory; Theorem II is the statement that a variational theory invariant under a group of arbitrary functions has field equations that are not independent — of them follow from the rest — which is the group-theoretic form of the failure of a proper energy conservation law in general relativity that Hilbert had asserted. The two theorems are used constantly and stated loosely; a formal version fixes exactly which hypotheses are needed and what the conclusion says.
Mathlib contains the differential-calculus and measure-theoretic infrastructure used here (Fréchet derivatives, integration on , compactly supported test functions, and the standard vanishing lemma for locally integrable functions tested against smooth compactly supported functions), but no calculus of variations: there is no Euler–Lagrange operator, no first-variation formula, and no Noether theorem. This mission supplies the first-order, finite-dimensional-base version of that material, with definitions that later missions (higher-order Lagrangians, the -th order identity (6), mixed groups) can extend.
The algebraic core — the central identity (3) and the passage to (12) — is a product rule plus a reindexing, and the real work is elsewhere.
Two steps are genuinely analytic. First, Noether's inference from "the integral of the integrand vanishes over every region" to "the integrand vanishes pointwise" (equations (10)–(11)) requires the regularity of the integrand to be used explicitly. Second, Theorem II's equation (16) requires integrating by parts against an arbitrary function and then applying the fundamental lemma of the calculus of variations in : the arbitrary functions of the group must be specialized to compactly supported test functions before the boundary terms can be discarded.
The remaining difficulty is bookkeeping: every statement must carry the differentiability hypotheses that make each derivative in it meaningful, since in Lean an undefined derivative silently evaluates to zero rather than failing.
The formalization is in the first-order setting: the Lagrangian depends on , on , and on the first derivatives of only. The base is with fixed but arbitrary, and fields are globally defined maps ; no boundary conditions, no manifolds, and no jet bundles are used. The group is not formalized as a group: as in §2 of the paper, only its infinitesimal generators , enter, and the invariance hypothesis is Noether's identity (11). The linear independence of the divergence relations, which Noether argues from the essentiality of the parameters, is not part of the formal statements.
Derivatives are Fréchet derivatives: is the derivative of at applied to the -th standard basis vector, and partial derivatives of the Lagrangian are derivatives of the corresponding partially applied function. Because Lean's derivative operator returns at points of non-differentiability, each statement carries explicit differentiability hypotheses for exactly the functions whose derivatives it mentions; a solver may not assume more.
The statements are not vacuous: the hypotheses of every milestone are satisfied, for instance, by smooth Lagrangians and smooth fields, and the invariance hypothesis (11) is satisfied by the classical examples (a Lagrangian independent of with , ). Degenerate parameter values are admitted and behave as expected: for or the sums are empty and the identities reduce to , and for the goal quantifies over an empty index set.
Contributions of independent interest that this mission would welcome: a reusable statement of the fundamental lemma of the calculus of variations on in the form needed for (16), and the higher-order analogue of the central identity, Noether's equation (6).