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?
This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 4, the (first) Grigorchuk group and its solution of half of the von Neumann–Day problem.
The first two Garrido missions, Amenable Groups I and Amenable Groups II (the Banach–Tarski paradox), established the inclusions between the elementary amenable groups, the amenable groups, and the groups with no free subgroup of rank two. "The von Neumann–Day problem asks whether these inclusions are strict" (p. 12). Ol'shanskii settled ; "The other part of the problem was solved in 1985 by Grigorchuk" (p. 12), with the theorem this mission targets.
Chou's theorem that every torsion group in is locally finite "traces a clear route for solving the Day problem. Namely, it suffices to find an amenable torsion group which is not locally finite" (p. 13). The Grigorchuk group is such a group: a finitely generated, infinite group of automorphisms of the binary tree in which every element has order a power of , and whose growth is subexponential, so that it is amenable.
The infinite rooted binary tree has as vertices the finite words in , and its automorphisms are the permutations of the vertices that preserve length and prefixes. The Grigorchuk group is generated by four of them: exchanges the two subtrees below the root, and , , fix the first level and are defined recursively by , , , meaning that acts on the subtree below as and on the subtree below as , and so on.
is the subgroup of fixing every vertex of level . An element acts on each of the subtrees below level as a tree automorphism, its section there. sends to the tuple of these sections, and for , is its section below the vertex . is the word length with respect to .
"The (first) Grigorchuk group is amenable but not elementary amenable" (p. 12). This is the goal because it is the theorem the section proves and the one that separates from .
Conjugation by exchanges the two sections of an element of ; is a Klein four-group and is generated by ; is infinite, since maps onto it; and the maps are monomorphisms.
Every element of has order a power of , so is an infinite finitely generated torsion group and, by Chou's Theorem 4.2, not in . The notes omit the proof of Proposition 4.7 and refer to de la Harpe's book; it is a milestone to be proved here.
The length contraction for , the index , and a general inequality comparing the balls of a group with those of a subgroup of finite index give subexponential growth (Theorem 4.9); Theorem 3.8 of the first Garrido mission then gives amenability.
The Grigorchuk group is one of the central examples of geometric group theory: the first group of intermediate growth, a finitely generated infinite torsion group, and the separation of amenable from elementary amenable groups. Neither Mathlib nor the platform has it, and a search of Lean Pool, Tau Ceti and the Palomar registry found no formalization; Mathlib's only mention is a bibliography entry in its Schreier-graph file. The tree-automorphism definitions here are reusable for other groups acting on the binary tree. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.
Lemma 4.8 is the hard step: a careful count, over three levels of sections, of how a shortest word shrinks and how many cancellations occur. Proposition 4.7 has no proof in the notes; the standard argument is an induction on word length through the sections. The growth argument of Theorem 4.9 is an estimate on built from Lemma 4.8 and the ball inequality.
The tree is modelled by its vertices, List Bool, and is a subgroup of the group of
tree automorphisms, following the notes' "a group of automorphisms of ". The generators are
defined by Garrido's recursion, and the bundle proves that each is an involutive automorphism;
sections are defined for every automorphism and every vertex, with a proof that they are
automorphisms. The sections of and are shown to lie in as part of the
milestone rather than assumed.
One trivialising formalization is ruled out: is not taken to be an abstract group given by a presentation or by fiat, but the concrete group of tree automorphisms the notes define, so that the finiteness, torsion and growth statements are about that group.
Definition 4.4 and Lemma 4.5, the ordinal hierarchy , and Theorem 4.3 are covered by the Chou 1980 mission, which proved Theorem 4.3 with an inductive predicate in place of the ordinals; Theorem 4.2 enters as a reference. Ol'shanskii's is outside the notes' scope ("beyond the scope of these talks", p. 12) and is not formalized.
The Shape Zero model reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route: C1 Formal Proofs, §3, Theorem 3.6 ("Roles Force Fano") states that any Steiner triple system admitting a role colouring is the Fano plane. Its proof derives only that there are points, and takes the last step on trust: C1 §3 asserts "the unique STS(7) (the Fano plane PG(2, 2))" in Theorem 3.3 and justifies it with one sentence, "Uniqueness of STS(7) is classical."
The companion mission The role postulates force exactly seven points proved the point count and deliberately stopped there. This mission supplies the missing step and completes the chain:
The attack path is the standard textbook proof of the uniqueness of STS(7), supplying the step C1 §3 calls classical. The proof goes through three milestones: a normal form around one point, exactly two completions of it, and an explicit relabelling of each completion onto the Fano plane. The line count (seven lines, three through each point) and the meeting property (any two lines meet in exactly one point) then follow as corollaries of the goal. C1 gives no argument for this step; the milestones below are that classical argument, not C1's.
What this mission does NOT prove.
A Steiner triple system on the points is a family of -point subsets, called lines, such that every pair of distinct points lies on exactly one line. A role colouring gives each point of each line one of three roles so that the three points of a line get different roles and every point takes every role exactly once.
The Fano plane is the Steiner triple system on with lines modulo :
This is the companion mission's published definition RolesForceSeven.fano, labelled . (C1 §5 writes the same lines on ; this mission uses the companion mission's labelling.)
The definitions RolesForceSeven.STS, RolesForceSeven.RoleColouring and RolesForceSeven.fano are imported from the companion mission, not restated, so both missions refer to the same objects. The one new definition is FanoUnique.IsFano S: there is a bijection from the points of to with the Fano lines.
This is FanoUnique.sts7_is_fano.
The goal follows from M1, M2 and M3. (These are M3, M4 and M5 in the draft's original numbering.)
Both hold in the Fano plane and are preserved by relabelling, so they follow from the goal.
For , a Steiner triple system on points with a role colouring is the Fano plane up to relabelling (FanoUnique.roles_force_fano). The companion mission's goal gives ; the goal of this mission does the rest. The hypothesis is kept, following the erratum to C1 §3: the empty system satisfies every other condition and is not the Fano plane.
The result itself. Together with the companion mission, it makes C1 Theorem 3.6 fully machine-verified: the role postulates force not only seven points but the Fano plane itself, up to relabelling.
Formalizing it. C1 cites the uniqueness of STS(7) as classical. It was checked numerically — exhaustively over labelled systems — but never proved in the C1 package; this mission proves it.
| check | result |
|---|---|
| Steiner triple systems on 7 labelled points | 30 (classical count ) |
| of those, isomorphic to the Fano plane | 30 of 30 |
| any two distinct lines meet in exactly one point | true in all 30 |
| completions of | exactly 2 (A and B) |
| swapping points 1 and 2 carries A to B | true |
Moderate. M3 is a finite computation. The work is in M1 — building the relabelling bijection from the three lines through a point — and M2, the case analysis on the line through points and , which forces the remaining lines. Corollaries A and B follow from the goal by relabelling. Exhaustive search over all line families () is not feasible, so the structured proof is needed.
Fin n; lines are Finset (Fin n); the definitions are the companion mission's, imported unchanged.Fin n ≃ Fin 7; it forces and exactly lines.This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.1, the Banach–Tarski paradox, together with the inclusion that the notes draw from it.
The notes open with the theorem that started the subject. In 1924, they recall, Banach and Tarski "proved a remarkable theorem which is nowadays stated as 'given a ball in 3-dimensional space, there is a way of decomposing it into finitely many disjoint pieces that can be rearranged to form two balls of the same size as the original one'" (p. 1). As the notes put it, "This counterintuitive result is essentially a statement about measure theory": no finitely additive, isometry-invariant measure defined on every subset of can give the unit ball a finite nonzero measure, so Lebesgue measure cannot be extended that way.
The reason is group-theoretic. The free group decomposes paradoxically under its own left multiplication, the rotation group contains a copy of , and a free action transports the decomposition to the sphere; Hausdorff's paradox and a countable correction give the sphere, and radial projection the ball. The same argument shows that a group containing cannot carry an invariant finitely additive probability measure — the inclusion of amenable groups into groups without free subgroups of rank two, whose converse was von Neumann's question.
This mission is the companion of the first Garrido mission, which formalized the measure-theoretic half of Section 1 (equidecomposability, the Banach–Schröder–Bernstein theorem, Tarski's theorem) and Sections 2 and 3.
A group acting on a set makes two subsets -equidecomposable, ,
when can be cut into finitely many pieces which, each moved by one element of ,
reassemble into ; a subset is -paradoxical when it contains two
disjoint proper subsets each equidecomposable with . Both are the published definitions from
the first Garrido mission, Equidecomposable and IsParadoxical, and paradoxicality is
defined for an arbitrary subset because the notes use it for and for
a ball.
The groups and spaces are the classical ones. is the unit sphere in
(Sphere n), with — Mathlib's
Matrix.specialOrthogonalGroup — acting by matrix-vector multiplication. is the group of
all isometries of (EuclideanGroup 3), acting by evaluation; it contains the
translations, the rotations and the reflections. A group acts freely (ActsFreely) when no
element other than the identity fixes a point. is FreeGroup (Fin 2), and "no free
subgroup of rank two" is the published Chou.NoFreeSubgroupOfRankTwo. The rotations and
of Proposition 1.6 are defined in the bundle with their matrices.
Every closed ball of positive radius in , and itself, is -paradoxical: "Any solid ball in is -paradoxical. Furthermore, is -paradoxical" (p. 3).
This is the goal because it is the theorem the section is named for and the one the notes build to.
is paradoxical, and so is every nonempty set on which it acts freely (Proposition 1.5); contains a free group of rank two (Proposition 1.6); the sphere minus a countable set is paradoxical (Theorem 1.7, Hausdorff's paradox); a countable set can be absorbed (Proposition 1.8); so the sphere is -paradoxical for (Corollary 1.9). The steps that the notes state inside proofs are milestones of their own: the two rotations and generate a free group, a nontrivial rotation fixes exactly two points of , and a countable subset of has a rotation whose positive powers move it off itself.
No rotation-invariant finitely additive probability measure lives on all subsets of for ; no isometry-invariant finitely additive measure on all subsets of gives the unit ball a finite nonzero value; and an amenable group has no free subgroup of rank two.
The Banach–Tarski paradox is one of the best-known theorems of twentieth-century mathematics,
and it is the reason finitely additive measure theory and amenability exist as subjects.
Neither Mathlib nor the platform has it. It has been formalized in Lean outside both:
aetilley/banach-tarski, following Tomkowicz and Wagon,
proves that the closed unit ball in is paradoxical under its isometry group, and is a
candidate for inclusion in
Lean Pool. This mission follows Garrido's statements instead,
and publishes each step as a theorem other work can import. Mathlib has the equidecomposition machinery in
Equidecomp.lean
and the ping-pong lemma, which is the natural tool for Proposition 1.6, but no paradoxical
decomposition of anything.
The inclusion completes, with the first Garrido mission's , the display on p. 11 of the notes. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.
Three steps carry the weight. The freeness of and is a computation the notes defer to Wagon's book: a nonempty reduced word is shown to move a suitable vector, by tracking coordinates of the form with integers reduced modulo . The absorption of a countable set needs a rotation whose powers move the set off itself, which is a countability argument about angles. And the passage to for is only sketched in the notes ("by the same arguments as in Proposition 1.8"): the induction lifts a paradoxical decomposition of to minus two poles, and the poles must then be absorbed by a rotation of .
Transferring the sphere to the ball needs radial projection and the absorption of the center, again by a rotation of infinite order, this time about an axis that misses the center.
Rotations are matrices: is Matrix.specialOrthogonalGroup (Fin (n + 1)) ℝ,
acting on the sphere by mulVec; the bundle proves that an orthogonal matrix preserves the
Euclidean norm, so the action is well defined. is the full group of isometries
EuclideanSpace ℝ (Fin 3) ≃ᵢ EuclideanSpace ℝ (Fin 3), as in the first Garrido mission's
Corollary 2.5, with an action by evaluation defined in the bundle.
Committed conventions. "Solid ball" is read as a closed ball Metric.closedBall c r with
, for every center . "Countable" is Set.Countable, which includes finite sets.
Proposition 1.5's second part assumes the set nonempty, since the empty set carries a free
action and is not paradoxical. The p. 1 consequence asks for a finite nonzero value on the
unit ball: the notes say only "non-zero", and the measure that is on every nonempty set
satisfies that. Both departures are named in the statements' descriptions.
One trivialising formalization is ruled out: equidecomposability with the whole group allowed to
act on each piece by an arbitrary bijection would make every two sets of the same cardinality
equidecomposable. Here each piece is moved by a single group element, through Mathlib's
Equidecomp, and paradoxicality needs two disjoint proper subsets.
A complete development needs the sphere and its rotation action, the isometry group of , and the combinatorics of paradoxical decompositions; the definitions are reusable for any later work on the paradox. Contributions are welcome on any milestone. Proposition 1.5 and the step on fixed points of rotations are the most self-contained entry points.
The locally compact and measurable versions of the paradox, and the questions of how few pieces suffice, are not in the notes and are not formalized. Tarski's theorem, the converse that a non-paradoxical set carries an invariant measure, is proved in the first Garrido mission and is not restated here.
The Shape Zero model (Shape Zero LLC, unpublished) predicts a propagation asymmetry: with a gyroscopic coupling of strength , a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way, and the difference, , does not depend on the on-site stiffness . The companion mission The propagation asymmetry does not depend on the on-site stiffness proves this on a one-dimensional uniform lattice. The model's base is three-dimensional, where a wave also carries transverse wavenumbers. This mission extends the result to a uniform lattice with any number q ≥ 1 of axes, and shows that the asymmetry is independent of both the stiffness and every transverse wavenumber.
What this mission does NOT prove.
Fix real numbers (on-site stiffness), (neighbour coupling) and (gyroscopic strength), and a wavevector . The upper-branch frequency is
with the sum over all axes. Reversing the wave along axis 0 gives . In Lean these are PinnedAsymmetryQ.omega q K c β k (with Real.sqrt) and flip0 q k. The formula has been checked against the eigenvalues of the actual q = 3 lattice generator to across 216 wavevectors and three parameter sets.
This is PinnedAsymmetryQ.asymmetry. Neither nor any transverse wavenumber appears on the right.
The result itself. The goal isolates the part of the frequency that is exactly independent of the stiffness and of the transverse wavenumbers on a lattice of any dimension. At q = 3 it is the statement relevant to the model's actual base; at q = 1 it reduces to the companion mission.
Formalizing it. The q-dimensional statement had been checked numerically only (3,000 random parameter sets at q = 3: goal to ). A proof covers every , every wavevector and all real parameters.
Low. The asymmetry is a difference of two expressions whose square-root parts depend on and on every ; the point is that reversing axis 0 leaves the radicand unchanged, so the square roots cancel. M1 needs the radicand non-negative in order to square the square root.
[NeZero q]), so axis 0 exists. All parameters are arbitrary reals, with no sign conditions in the goal.Real.sqrt returns on negative inputs. The goal still holds there, because the two radicands are equal, so the two square roots are equal whatever value they take.Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning on negative inputs). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.htmlThe Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes through a velocity-dependent force, one coupling matrix per link. The companion mission Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites) proves that a coupling doing no net work (a passive coupling) must have every link matrix symmetric — but only on a one-dimensional ring. The model's base is three-dimensional. This mission extends the result to a periodic cubic lattice with any number q of spatial axes, so it covers q = 3 directly and reduces exactly to the ring result at q = 1.
What this mission does NOT prove. As with the companion missions, commuting with the complex structure is not derived here; it remains a modelling premise. This mission shows only that passivity forces symmetry on every link in every direction.
Fix natural numbers (number of axes), (sites along each axis) and . A site is a point of the periodic cubic lattice; is the site one step forward or back along axis , wrapping around. Each link — a site together with an axis — carries its own real matrix , and each site carries a velocity . The force on site is
where the second term uses the matrix of the link behind . The total power is
In Lean, sites are Site q L = Fin q → Fin L, the step is shift x a s (update coordinate by in Fin L), and the power is PassivityTorus.power q L d W v. The coupling is passive when for every .
This is PassivityTorus.passive_iff_symm, for every and .
The result itself. It is the dimension-independent form of the passivity theorem: whatever the number of spatial axes, a per-link coupling does no net work for every motion exactly when every link matrix is symmetric. It removes the one-dimensional restriction from the step that justifies restricting the model's coupling class to symmetric matrices.
Formalizing it. The ring result has been machine-checked; the lattice extension had been checked numerically only (identity error at ). A proof covers every , and .
The algebra is the ring argument; the difficulty is bookkeeping. The incoming term must be reindexed by the one-step shift, which is a bijection of the torus, and the converse needs a test motion supported on two neighbouring sites and together with a proof that no other link joins them.
The hypothesis is necessary. At the step forward and the step back along an axis reach the same site. This is proved (in Lean, locally): for every , putting the same non-symmetric matrix on every link of the lattice gives exactly zero power for every velocity field, so passivity does not force symmetry there. Weakening the hypothesis makes the goal false.
[NeZero L] is needed for the literal in Fin L and is implied by in the goal.Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.htmlThe Shape Zero model (Shape Zero LLC, unpublished) makes one experimentally testable prediction: a propagation asymmetry. In a ring of oscillators with a gyroscopic coupling of strength , a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way. The predicted difference is
where is the neighbour coupling and the wavenumber. The claim is that this difference is pinned: it does not depend on the on-site stiffness , even though each of the two frequencies does. Simulations of the model measured the linear asymmetry at , and times the predicted value at stiffness , and , i.e. protected to about . This mission proves the exact statement for a uniform lattice.
What this mission does NOT prove.
Fix real numbers (on-site stiffness), (neighbour coupling), (gyroscopic strength) and a wavenumber . Write
The upper-branch frequency on a uniform ring is
In the Lean development this is PinnedAsymmetry.omega K c β q, with Real.sqrt for the square root. When , is a root of the dispersion relation
This is PinnedAsymmetry.asymmetry. The right-hand side contains no . As an immediate consequence, for any two stiffnesses and the asymmetry is identical.
The result itself. The goal isolates the one quantity in the model's prediction that is exactly independent of the on-site stiffness: the direction-dependent part of the frequency. Each branch frequency depends on through the square root, but the difference between the two directions does not. M1 is what makes this a statement about the physical frequency rather than about an arbitrary expression, by showing the formula solves the model's dispersion relation.
Formalizing it. The algebra is elementary; the content is that the stiffness provably drops out, for every value of the parameters rather than at the sampled stiffnesses of a simulation. The formal statement also records precisely what is covered (the linear asymmetry on a uniform lattice) and what is not (the nonlinear coefficient and non-uniform stiffness).
The difficulty is low. The asymmetry is a difference of two expressions that each contain a square root depending on ; the point to establish is that the two square roots coincide, so that no stiffness dependence survives the subtraction. M1 requires squaring the square root, which is valid only when the radicand is non-negative.
Real.sqrt returns on negative inputs. The goal still holds in that regime, because the two radicands and are equal, so the two square roots are equal whatever value they take. For physical parameters (, ) the radicand is always non-negative.The development needs only Mathlib's real trigonometric functions and Real.sqrt.
Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning on negative inputs; Real.sq_sqrt). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.htmlThe Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes on a ring through a velocity-dependent force, with one coupling matrix per link. A companion mission, The passivity-admissible couplings have dimension n² = dim u(n), shows that real matrices which are symmetric and commute with a complex structure form a space of dimension . That mission deliberately takes symmetry as given. This mission supplies the reason for it: a coupling that never does net work (a passive coupling) must have every link matrix symmetric, provided the ring has at least three sites.
Together the two missions give the chain
What these two missions do NOT prove. Commuting with is not derived here. It is the requirement that the coupling respect each node's complex structure, and in the model it is imposed, not forced by passivity. After both missions the proved content is: passivity forces symmetry, and symmetric -compatible couplings have the dimension of . The -compatibility step remains a modelling premise. In addition, the coupling space consists of the Hermitian matrices, which match in dimension; the Lie algebra itself appears only after multiplying by (Unitary group).
Let and be natural numbers with . A ring has sites labelled by , so site is next to site ; indices and are taken modulo . Each site carries a velocity vector , and each link carries a real link matrix . The force on site is
where the second term uses the previous link's matrix . The total power delivered by the coupling is
In the Lean development this is PassivityRing.power N d W v, with sites indexed by Fin N (whose addition and subtraction wrap around modulo ), vectors in Fin d → ℝ, and the dot product ⬝ᵥ. The coupling is passive when for every choice of velocities .
This is PassivityRing.passive_iff_symm. It holds for every and every family of link matrices, with no assumption relating different links.
The result itself. The goal turns a physical requirement — no net work for any motion — into an exact algebraic condition on each link separately. It is the step that justifies restricting the companion mission's coupling class to symmetric matrices, so that the dimension count applies to the passive couplings of the model rather than to an assumed class.
Formalizing it. The model's claim has so far been checked numerically at ring sizes . A machine-checked proof covers every and every , makes the role of the hypothesis explicit, and separates what is proved (passivity forces symmetry) from what remains a modelling premise (-compatibility).
The forward direction and the power identity are finite-sum bookkeeping. The central difficulty is the converse: the hypothesis constrains a single scalar quantity summed around the ring, and it must be shown to constrain each link matrix individually. On small rings this fails because distinct terms of the sum coincide, so the argument depends on the ring being large enough that neighbouring sites are genuinely distinct, and in Lean that is modular arithmetic on Fin N.
The hypothesis is necessary, not a convenience:
Weakening the hypothesis to , or dropping it, makes the goal false.
Fin N with its wrap-around arithmetic, so and go around the ring; [NeZero N] is required for the literal in Fin N and is implied by in the goal.W : Fin N → Matrix (Fin d) (Fin d) ℝ, not a single shared matrix, and no relation between different links is assumed.v : Fin N → (Fin d → ℝ).ℝ); symmetry is (W i)ᵀ = W i.M1 and M2 hold for every and carry no ring-size hypothesis; M3 and the goal require . The development needs only Mathlib's finite sums, dot products, matrix–vector products and Fin arithmetic.
Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.htmlThis mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.2, Section 2 and Section 3.
A group is amenable when its subsets can be measured in a way that translation does not disturb. Von Neumann isolated the notion in 1929 to explain the Banach–Tarski paradox: a solid ball in can be cut into finitely many pieces and reassembled into two balls of the original size, and the reason is group-theoretic rather than geometric — the rotation group contains a free group of rank two, while the isometry groups of and do not. No paradox is possible for a group carrying a translation-invariant finitely additive probability measure.
Mahlon Day proved in the 1950s that von Neumann's definition agrees with the existence of an invariant mean on bounded functions, moving the theory into functional analysis, and coined the word "amenable" as a pun on "mean"; the problem below was first stated in print, with von Neumann's name attached, in Day's 1957 paper. Følner gave a combinatorial criterion — a group is amenable exactly when it has finite subsets almost invariant under translation — now usually taken as the definition, and the link to growth.
The organizing question of the classical theory was the von Neumann–Day problem: writing for the elementary amenable groups, for the amenable groups and for the groups with no free subgroup of rank two, one has , and both inclusions were asked to be equalities. Both are strict. Ol'shanskii (1980) showed , and Grigorchuk (1985) showed with a group of intermediate growth. Chou (1980) supplied the structural facts about that the separation rests on.
Amenability is now basic vocabulary in geometric group theory, ergodic theory and operator algebras.
Let be a discrete group. A measure on , in von Neumann's sense, is a function assigning a value to every subset of — not merely to a distinguished -algebra — such that
for all and all disjoint . Only finite additivity is required; countable additivity together with invariance is impossible for a countably infinite group. is amenable if such a exists.
Two reformulations matter. A left-invariant mean is a positive linear functional on the bounded real functions with and , where . And satisfies the Følner condition if for every finite and every there is a finite nonempty with
where is symmetric difference. In the Cayley graph this says has small boundary relative to its size.
Against amenability stands paradoxicality. Two subsets of a -set are -equidecomposable, written , if can be cut into finitely many pieces which, after each is moved by a single element of , reassemble to ; and is -paradoxical if it has two disjoint proper subsets each equidecomposable with itself. A group that is paradoxical under left translation admits no invariant measure.
This is the goal because it bridges the combinatorial and measure-theoretic sides of the subject, and every later application of amenability to growth uses it in one direction or the other.
For a group , these four are equivalent: is amenable; there is a left-invariant mean on ; is not paradoxical; and has the invariant extension property.
Amenability passes to subgroups and quotients, is closed under extensions, and is closed under directed unions; hence all abelian and all virtually solvable groups are amenable, and .
Each of the three equivalent pictures serves a different purpose: the measure gives non-paradoxicality, the mean gives access to functional analysis and fixed-point arguments, and the Følner condition is what one can verify for a concrete group. Theorem 3.8 is the typical consequence — a group of subexponential growth is amenable — proved by exhibiting the balls of the word metric as a Følner sequence, which only the equivalence licenses.
Mathlib has very little of this. It names no definition of amenability:
FoelnerFilter.lean
says one "has not yet been given" for want of "a general consensus" on the right generality, and
writes the property out inline in the conclusion of IsFoelner.amenable, which is one direction
of the goal. Equidecomp.lean
has the equidecomposition machinery, with a TODO asking for the Schröder–Bernstein theorem for
equidecomposability that is Theorem 1.2 here.
This mission supplies the missing definitions, that Schröder–Bernstein theorem, the closure properties, and the direction of the Følner equivalence that is genuinely open. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.
The Følner-implies-amenable direction is the easier one, and the natural construction almost works: given a Følner sequence , set . That limit need not exist. It must be replaced by a limit along a non-principal ultrafilter, or the measure obtained by compactness in .
The converse — amenable implies Følner — is where the content is, and no averaging argument reaches it. One has to produce, from a mean, finite sets that are almost invariant; the passage runs through a separation theorem in , the only step here needing a genuinely infinite-dimensional tool. The classical arguments provide no combinatorial route.
Two smaller obstructions are worth naming. Tarski's theorem — an invariant measure giving a set measure one exists precisely when that set is not paradoxical — is quoted without proof in the source and is the hardest single statement in the mission. And Theorem 2.6 rests on a finitely additive extension theorem for measures on a Boolean algebra, which is not the Carathéodory construction in Mathlib; Mathlib's is about outer measures and -additivity.
Amenability is IsAmenable G: the existence of with
, finitely additive on disjoint pairs, and invariant under left translation. The
codomain is the extended nonnegative reals rather than , to match the conclusion of
Mathlib's IsFoelner.amenable — which at with every set measurable is exactly
IsAmenable — so that theorem is directly usable; finite additivity and
force anyway, so nothing is added or lost.
Committed conventions. Means live on , realised as lp (fun _ : G => ℝ) ∞ —
not on all of , where invariance and normalisation are already
contradictory (proved for ),
so every statement about means would be vacuously unprovable. Normalisation is phrased via constantly- functions, to avoid depending
on the ring structure of . Cardinalities use Set.ncard, so no DecidableEq
instance propagates into the statements.
Paradoxicality is defined for an arbitrary subset, recovering the source's whole-space notion as
a special case, because the source states it for the whole space but uses it for subsets
throughout. Equidecomposability builds on Mathlib's Equidecomp, and growth on the published
Chou_Growth bundle, rather than either being redefined.
One trivialising formalization is ruled out: amenability requiring only and
additivity, without invariance, is satisfied by any normalised counting density and would make
the mission vacuous. Left-invariance is part of every definition here, and IsAmenable is
exhibited non-vacuously for finite groups.
A complete development needs finitely additive measures on a power set, invariant means on , the Følner condition and sequences, paradoxical decompositions, and a finitely additive extension theorem on a Boolean algebra; the definitions and the last of these are reusable beyond this mission. Contributions are welcome on any milestone. Proposition 2.2's closure properties are the most self-contained entry points, and Theorem 1.2 is the one Mathlib has explicitly asked for.
Two bodies of material from the source are deliberately out of scope, left for later missions in this series.
The geometric construction of the Banach–Tarski paradox — that contains a free group of rank two, the Hausdorff paradox, and the paradoxical decompositions of the sphere and the ball. This mission takes the measure-theoretic half of Section 1 and leaves the half about the -sphere. Tarski's theorem and the Banach–Schröder–Bernstein theorem are in scope despite being printed alongside that material, because both are equidecomposability combinatorics and both are needed by results that are in scope.
The Grigorchuk group — its construction on the binary rooted tree, the proof that it is amenable but not elementary amenable, and its subexponential growth. Theorem 4.2 and Theorem 4.3 are the exceptions, and they enter as references rather than targets.
Also out of scope: the locally compact case. The source gives most definitions for both discrete and locally compact groups, then says it will "mostly focus on discrete groups"; only the discrete case is formalized. Følner nets for uncountable groups are likewise omitted, as is the extension of Example 3.5 to finitely generated abelian groups, which the source leaves as an exercise.
The free energy principle (FEP) proposes that a self-organizing system — a brain, an organism, an agent — persists by minimizing one quantity: the variational free energy of its sensory states under an internal generative model. Introduced by Karl Friston as a principle of brain function [Friston 2006] and stated in its unified form [Friston 2010], the principle makes a precise mathematical claim at its core: whatever internal state estimate the system holds, the free energy of incoming data is never below the data's surprisal (negative log marginal likelihood), and the excess is exactly the Kullback–Leibler divergence between the system's recognition density and the Bayesian posterior implied by the model. Active inference extends the same functional from perception to action and planning [Friston et al. 2017], and the same bound is known in machine learning as the evidence lower bound (ELBO) of variational inference [Parr et al. 2022].
Timeline of the mathematical content this mission formalizes:
fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 Free Energy Principle topics, compiled with zero proof holes against a pinned Mathlib. This mission transcribes the catalogue's core-free-energy chain — topic fep-002 and the foundation module active_inference — onto the platform, turning the first link of the FEP development into solvable community infrastructure.Everything is finite, and laws are normalized real mass functions.
A finite law on a finite type is a function with for every and . A finite kernel from to assigns to each a normalized row over . The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence
a totalized real-valued divergence that is finite even at zero-mass atoms (the convention via Real.negMulLog) and nonnegative on normalized laws.
A finite generative model for active inference (definition Def_fep_generative_model) over finite types consists of: an initial state law ; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy the model predicts the state law and the outcome law . A recognition density is any finite law over states — the system's internal estimate. At an outcome with positive predicted mass, the Bayesian posterior is the exact finite Bayes rule. The outcome surprisal is , and the posterior-form variational free energy of a recognition density is
For every generative model, every policy , every outcome with , and every recognition density :
The recognition density is universally quantified — the bound holds for whatever state estimate the system happens to carry.
Three companions pin down the equality case, ordered weakest to strongest alongside the milestone list:
Independently of the finite model, in Mathlib's nonnegative extended reals , with , measures on any measurable space and :
the unconditional shape of the bound (topic fep-002 of the source catalogue), with the divergence taken as when the log-likelihood ratio is not integrable.
The result itself. This inequality is the load-bearing step of the FEP: it converts "minimize free energy" into "move recognition toward the posterior," and it is the exact statement whose continuous, dynamic, and policy-selecting extensions (expected free energy, Markov blankets, non-equilibrium thermodynamics) form the rest of the FEP literature. Without it, the principle's variational step has no mathematical content.
Formalizing it. The mathematics here is classical — Gibbs' inequality — and the source development already proves every row with no proof holes. What the mission adds is faithful, reusable infrastructure: the definitions are published as platform nodes in the shared namespace FreeEnergyPrinciple, so later missions in this programme (expected free energy and policy selection, Markov blankets, Gaussian and continuous-time variants, already proved in the source repository) can import them instead of re-deriving the substrate. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.
The bound itself is a one-line consequence of KL nonnegativity — the naive idea "prove it by simp on the KL sum" is essentially right, and the source proofs are correspondingly short. The actual difficulty is boundary precision, where plausible renderings go silently wrong:
A vacuous formalization — quantifying over a single distinguished recognition law, or taking "posterior" as an arbitrary variable — would trivialize the goal; the targets below rule this out by fixing the exact finite Bayes rule and universally quantifying .
Committed conventions of this mission's Lean development:
Fintype); laws are -valued normalized mass functions; kernels are normalized rows. No measure-theoretic machinery below the finite substrate except for the measure-theoretic core milestone.Real.negMulLog, so exactly, not by exception-handling.FiniteKernel.posterior, taken at the explicit hypothesis .FreeEnergyPrinciple; definitions live in the published definition files Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model, and every theorem item imports them. A Free Energy Principle II mission (expected free energy) is expected to reuse the same namespace and definitions.InformationTheory.klDiv in ℝ≥0∞ with no finiteness hypotheses.Federated optimization trains one model using objectives held by many clients. Performing several local updates between communication rounds saves communication, but clients with different objectives can move in different directions. SCAFFOLD maintains a correction for each client to address this disagreement, including when only some clients participate. Karimireddy et al. establish convergence without a bound on how similar the client objectives are. The relevant result is Theorem III, Section 5, PDF p. 5.
SCAFFOLD: Convergence with Client Sampling concerns that known result's formalization. Its exact targets are finite-round bounds from the Appendix E analysis, covering strongly convex, general convex, and nonconvex objectives. The paper's FedAvg results and its separate quadratic-acceleration theorem are outside this scope.
There are clients, with differentiable objectives . The global objective is . Every client gradient is -Lipschitz, where . A stochastic gradient query is conditionally unbiased and has conditional squared-error expectation at most , with . Current queries on different clients are conditionally independent given the full history. These make precise the fresh-oracle interpretation of A4–A5, Appendix B.1, PDF p. 14.
Each of rounds selects a uniform subset of clients, where . Each selected client takes local steps. Let be the server model, its stored client control variates, and . With constant local and global step sizes and , a client starts at and uses
Option II replaces a participating client's control with and retains every other control. These are Algorithm 1, PDF p. 4, and Appendix E, equations (18)–(21), PDF pp. 25–26. Write for the effective step size.
Four milestones support a root goal that is the conjunction of the two convergence statements below.
GradientGrowth states, for convex clients and a global minimizer ,
This is Appendix B.1, equation (9), PDF p. 14. PerturbedStrongConvexity states, for each -strongly convex client and ,
as in Appendix C, Lemma 5, PDF p. 17.
ConvexFiniteRoundConvergence allows arbitrary deterministic initial controls . Assume all clients are -strongly convex with , including ordinary convexity when , and fix a minimizer of . Define
For and , the target is
This is a finite-round formulation of Appendix E.1, Lemma 15, PDF p. 30; its case is the first bound on PDF p. 31.
NonconvexFiniteRoundConvergence assumes a lower bound for and initializes every client control with fresh gradients at . Put . For , establish
This is the explicit finite-round consequence targeted from Appendix E.2, Lemma 19, PDF p. 34, with the initialization specified on PDF pp. 31 and 35. The full-client warm start's communication cost is separate from these optimization rounds.
The bounds quantify optimization progress under stochastic gradients, several local steps, and partial participation. They permit arbitrarily different client objectives within the stated smoothness and convexity assumptions. Their output is a weighted random server iterate, represented by its expected loss, or a uniform random server iterate for the squared-gradient guarantee; this follows the output convention in equation (22), PDF p. 26.
The mathematical convergence analysis is published. The open work here is a Lean proof under the explicit stochastic-run model. The proposed statements do not themselves supply a machine-checked convergence proof. A completed development would provide reusable results about sampled finite averages, adaptive gradient queries, and optimization with stored noisy controls.
Local gradients are evaluated at different client states, and inactive clients retain controls computed in earlier rounds. Consequently, treating the server update as a centralized stochastic-gradient step discards both local disagreement and stale-control error. The challenge is to control these quantities while preserving their dependence on earlier randomness, as reflected in Appendix E.1–E.2, PDF pp. 26–35.
The source also needs careful transcription. The printed Theorem VII nonconvex noise term on PDF p. 25 differs from Lemma 19 in its smoothness and sampling factors, while output indices differ between equation (22) and the finite sum on p. 31. The exact targets above use the proof's finite-round constants and explicit indexing; they do not claim a verbatim formalization of every printed asymptotic rate.
SCAFFOLD.Space is finite-dimensional real Euclidean space;
SCAFFOLD.Problem records differentiable client objectives and smoothness.
SCAFFOLD.Run records a standard Borel probability space, full-history
filtration, measurable square-integrable iterates and oracle samples, and
the concrete updates. Virtual local paths are generated before a fresh
uniform size- subset is sampled, as permitted by the paragraph after
equation (22), PDF p. 26.
The conventions include , , zero noise, and . The output indices are precisely . Convex initial controls are deterministic; the nonconvex branch uses the specified stochastic warm start. The run definition assumes no descent inequality or convergence conclusion. Contributions should establish the four named propositions and necessary analysis/probability infrastructure while retaining these semantics.
A two-dimensional binary cellular automaton (CA) on the infinite grid with the standard Moore neighborhood updates configurations via a local rule according to:
A local rule is reversible (or bijective) if its global map is a bijection of the configuration space .
Let denote the exact number of reversible binary local rules on the Moore neighborhood. A longstanding open conjecture asserted that , corresponding solely to the 18 trivial single-cell shifts and complemented shifts:
In this mission, we formally disprove by constructing an explicit non-trivial conserved-landscape rule whose global map is an involution on , proving . We further extend this result to establish .
| Bound Level | Proven Bound | Description / Mathematical Mechanism |
|---|---|---|
| Trivial single-cell shifts and complemented shifts (). | ||
| Disproof of via explicit non-trivial conserved-landscape rule . | ||
| Conserved-landscape marker rule family ( centered rules). | ||
| Incorporation of off-centre marker rules reading center cell . | ||
| Symmetry | Exactly 74 rules invariant under spatial rotations. | |
| Torus | $ | \mathcal{R}_{2,3} |
| Upper Limit | Derived from constant divergence condition . |
Federated optimization studies learning when data and computation are spread across clients. Communicating after every stochastic gradient step can be costly, so clients often take several steps before averaging their models. The difficulty is that different clients can optimize different objective functions. Their models then move apart between communication rounds. A convergence guarantee must account for both stochastic gradient noise and this disagreement. Wang et al. give an explicit analysis of this tradeoff in A Field Guide to Federated Optimization, Section 6.1.
The relevant historical sequence is the introduction of FedAvg by McMahan et al.
in 2017, the development of local-SGD convergence analyses reviewed by Wang et al.,
and the unified illustrative analysis in the 2021 field guide. The present target
is that guide's known convex convergence theorem, rather than a new conjecture
about arbitrary federated learning. The remaining open task is a Lean proof of
the stated result. The mission is categorized as ResearchPaper: it formalizes a specific known
result rather than proposing a new mathematical conjecture.
There are clients and a parameter vector in . Client has a differentiable convex objective . The global objective is . Every local gradient is -Lipschitz for the same . Fix a global minimizer of and a deterministic initial model , and write .
Every client participates in every round. Each of rounds consists of local steps with constant learning rate . If is client 's state after local steps of round , its next state is . At the next round all clients restart from the average of the preceding round's terminal states. The shadow iterate is ; it is defined even at local steps where clients do not communicate.
On a probability space , the history before a step contains all past oracle draws. The stochastic gradients are conditionally unbiased, their conditional squared errors have expectation at most , and the different clients' current gradients are conditionally independent. The heterogeneity bound is for every client and every point, where . These are the assumptions of Section 6.1.1, PDF p. 40, equations (11)–(14), with the history and independence convention used explicitly in Appendix D.1 immediately after equation (27), PDF p. 87.
The principal goal is Theorem 1, equation (15). For , establish
Two source milestones describe the intermediate results. Lemma 1 bounds the conditional average loss within a round by the decrease of squared distance to the minimizer, plus a noise term and a sum of client disagreements. Lemma 2 bounds each conditional squared disagreement by . Both are stated on PDF p. 41, Section 6.1.2, with proofs in Appendix D, PDF pp. 86–88. They remain genuine open proof obligations; the algorithm model does not assume either estimate.
An additional milestone records the same theorem's tuned-step consequence, equations (16)–(17), in the regime . With
the same expected loss is at most
The principal goal includes zero-noise and zero-heterogeneity cases. The extra positivity conditions apply only to the printed tuned-step formula, whose denominators otherwise require separate conventions.
The bound separates an initial-distance term, a noise term improved by the number of clients, and two costs of local updates. It quantifies how local work interacts with stochastic noise and differing client objectives. Its conclusion concerns the average objective gap along the post-update shadow sequence; it does not assert the same bound for every last iterate or for the average of client losses. These distinctions follow directly from the quantity defined in equation (14).
A completed formalization would provide reusable checked components for stochastic optimization: finite client averages, history-conditioned oracle assumptions, per-round potential estimates, and disagreement bounds. The paper supplies the mathematical proof; this draft supplies checked statements and definitions. No convergence proof is claimed by creating or compiling the proposal.
The average update evaluates each gradient at its own client's state. It therefore does not directly equal a centralized stochastic-gradient step at the shadow iterate. A proof must control that discrepancy quantitatively, preserve the conditioning on the round's starting history, and justify the noise improvement using independent client sampling. Ignoring the sampling relationship can invalidate the advertised bound even for scalar quadratic objectives.
The model uses finite-dimensional real Euclidean space, including the harmless zero-dimensional case, and a standard Borel probability space. A filtration indexed by records the full past. Local states and gradients carry explicit measurability and finite-second-moment conditions. These probability conventions support actual Bochner and conditional expectations; integrals are not treated as arbitrary total functions without analytic obligations.
The local objectives, global objective, gradients, iterates, and shadow averages are concrete functions. The model assumes neither a drift bound nor a progress bound. Source hypotheses are uniform in the model point, and the minimizer is an actual minimizer of the averaged objective. Unequal weighting, partial client participation, nonconvex objectives, adaptive step sizes, and privacy mechanisms are outside this particular theorem. Contributions should prove the named source lemmas or their necessary analytic infrastructure while retaining these statements.
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.lean