Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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.
In the mid-1960s the success of as an approximate symmetry of hadrons raised the question whether the Poincaré group and an internal symmetry group could be combined into a larger relativistic symmetry group that is not simply their direct product. A series of no-go theorems for Lie groups (Coleman 1965, Weinberg 1965, Michel–Sakita 1965) relied on artificial assumptions and did not cover infinite-parameter groups. Coleman and Mandula (Phys. Rev. 159, 1251 (1967)) settled the question using information about the S matrix: any connected symmetry group of a non-trivial, Lorentz-invariant S matrix with a reasonable particle spectrum is locally the direct product of the Poincaré group and an internal symmetry group. The theorem is the standard reason why space-time and internal symmetries do not mix in relativistic quantum field theory, and its loopholes (graded Lie algebras, i.e. supersymmetry; conformal symmetry for massless theories) shaped later model building (Haag–Łopuszański–Sohnius 1975).
Momenta are four-vectors with Minkowski product . The one-particle spectrum is organised by mass hyperboloids , , indexed by a set of distinct masses. On there are one-particle states of each momentum, and a Lorentz transformation acts on them through unitary Wigner matrices . The two-particle block of the T matrix, (Eq. (2) of the paper), is a family of matrices defined for , covariant under Lorentz transformations.
A symmetry generator is a Hermitian operator on momentum-space wave functions that acts on two-particle states as and commutes with . A generator commuting with the translations is a multiplication operator : on it multiplies the wave function at by a Hermitian matrix , and on two-particle states it acts by (Eq. (19)). An internal symmetry generator is one commuting with the whole Poincaré group.
The paper's hypotheses are: (1) Lorentz invariance; (2) particle finiteness — finitely many particle types below any mass; (3) weak elastic analyticity of the elastic amplitudes near the physical region, except at normal thresholds ; (4) occurrence of scattering — any two momentum eigenstates scatter, except at isolated energies ; (5) a technical assumption that the generators have distribution kernels.
Assume every particle is massive. Let be a real-linear set of Hermitian generators containing the Poincaré generators (multiplication by ) and (), closed under , whose members act on the hyperboloids as differential operators of one finite order (the same on every hyperboloid), and whose translation-commuting members commute with the S matrix. Then every has the form
with , a constant four-vector, and an infinitesimal internal symmetry transformation. The paper states that this Lemma 9 "is just the infinitesimal form of our theorem".
Correction note (revised draft). An earlier version of this draft stated the goal without the positive-mass hypothesis and with an order bound that could depend on the hyperboloid. That version is false, and the drafter formally disproved it in Lean: take one massless scalar particle with trivial Wigner cocycle and constant non-zero , and let consist of the operators that agree on test functions with a real combination of the translation generators, the Lorentz generators and the dilation generator . All hypotheses hold, but the dilation is not of the form . This is the known conformal loophole of the theorem for massless theories; the paper's hypothesis (2) and its proof implicitly use massive particles. The goal is now
ColemanMandula.coleman_mandula_corrected, which addshmassive : ∀ k, 0 < D.mass kand a single order boundnfor each generator on all hyperboloids (the paper's single finite order in the proof of Lemma 9). Update: in the drafter's local project (Lean 4.28.0, Mathlib8f9d9cf), Lemmas 3–8 and the corrected goal have been proved withoutsorry, using only the standard axioms; this is the drafter's own work, not an independent check. The drafter has not shown that the uniform order bound is needed.
The result rules out any non-trivial relativistic mixing of space-time and internal symmetries for theories with a non-trivial S matrix, covering infinite-parameter groups, and it yields as a corollary that all particles in a supermultiplet have the same mass (a generalisation of O'Raifeartaigh's theorem). The paper itself makes "no claim for corresponding standards of rigor"; a machine-checked version fixes a precise model in which the argument is correct, and exposes exactly which analytic facts (analyticity, continuity of the Wigner cocycle, the structure of compact Lie algebras, the absence of non-trivial finite-dimensional unitary representations of the Lorentz group) carry the proof. To the proposer's knowledge the theorem has not been formalized in Lean before.
The central step is Lemma 6: the traceless parts of the translation-commuting generators restricted to a hyperboloid form a Lie algebra that embeds (via Lemma 5) into , hence is compact reductive; the Lorentz group acts on it by automorphisms. One has to show this action is trivial — on the semisimple part because the Lorentz group has no non-trivial homomorphism into a compact group, and on the Abelian part by a separate argument. None of this infrastructure (compact Lie algebras, their automorphism groups, Lorentz-group representation theory) is currently available in Mathlib in usable form. Lemmas 3–5 in turn need analyticity and connectivity arguments on the manifold of momentum-conserving configurations.
The formalization works in a momentum-space model (definitions ColemanMandula_Kinematics, ColemanMandula_Scattering):
Fin 4 → ℝ with signature ; Lorentz transformations are real matrices with , , . Massless hyperboloids are allowed (the apex is excluded).Shell), each with finitely many states per momentum; all particle types of one mass are grouped together. The Wigner cocycle is an arbitrary continuous cocycle, smooth in .The model is non-vacuous: a single massive scalar particle with a constant non-zero T matrix satisfies all hypotheses, with spanned by the Poincaré generators and the identity. Contributions are welcome on: continuity/analyticity arguments on two-body phase space (Lemmas 3–5), compact Lie algebra structure theory and triviality of finite-dimensional unitary representations of the Lorentz group (Lemma 6), and the functional equation for additive collision invariants (Lemma 7).
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.
This mission formalizes the lower bound on the number of reversible binary cellular automata on the Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.
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.
A convex polytope has both geometric coordinates and a finite pattern of faces. Moving its vertices can change distances and angles while preserving which vertices belong to which faces. Enumeration by combinatorial type asks for those incidence patterns, with geometrically different realizations of the same pattern counted together. Grünbaum’s enumeration theorem establishes that the complete collection can be determined algorithmically when the dimension and number of vertices are prescribed Convex Polytopes, §5.5, p.91.
A d-polytope here is a nonempty convex hull of finitely many points in real d-dimensional coordinate space, with affine span equal to the whole space. A face is obtained by maximizing a linear functional over the polytope; the collection of faces also includes the empty face and the polytope itself. Inclusion orders this collection. Two polytopes have the same combinatorial type when their full face collections admit an order isomorphism. This notion retains the incidence structure and forgets metric measurements.
To describe a type with finite data, label the k vertices by the integers from zero through k−1. Record the set of vertex labels belonging to each nonempty proper face. This family of subsets is the polytope’s scheme. A finite list of finite lists of natural numbers encodes such a family. The order of labels and repeated occurrences of a label do not change the represented subset. A scheme is realized only when its recorded subsets are exactly the vertex sets of the nonempty proper faces: it cannot add faces, omit faces, or introduce labels outside the prescribed range.
The target is a single total computable function
For every dimension d and vertex count k, each scheme in E(d,k) must have a realizing d-polytope with exactly k vertices. Every d-polytope with k vertices must realize some scheme in that output. Finally, if polytopes realizing two output positions have isomorphic full face posets, those positions must be equal. These requirements say that the output contains precisely one representative of every combinatorial type. The existential choice of one function precedes both numerical inputs, so the algorithm must work uniformly for all dimensions and vertex counts.
The result supplies an effective finite classification at each prescribed size. It is stronger than the observation that only finitely many incidence families can be written down: those families need not all arise from real convex polytopes. It also addresses termination, since a total algorithm must return its entire finite answer for every input. The theorem is a known mathematical result in the cited textbook. The present formal target asks for a proof of its stated algorithmic conclusion; no machine-checked proof of that conclusion is asserted here.
The principal difficulty is the connection between finite incidence data and geometric realizability. Combinatorial consistency alone does not supply real coordinates for a convex polytope. The source distinguishes this realizability question from the enumeration conclusion and identifies decidability over the real numbers as relevant to it §5.5, p.91. The mission retains the complete enumeration conclusion, including realizability of each answer, coverage of every type, and absence of duplicate types.
The formal representation uses real coordinates without a rationality restriction and permits nonsimplicial polytopes. Vertices are labelled injectively and exhaustively. The number of vertices is expressed as the number of nonempty zero-dimensional exposed faces. Nonemptiness separates the empty face, whose book dimension is −1, from the natural-valued dimension used to count faces. For finite convex hulls the face collections are finite, so this cardinality has its usual meaning.
Natural-number dimensions include dimension zero. The unique point has one vertex and no nonempty proper faces, and therefore uses an empty scheme. This is an explicit extension of the source’s positive-dimensional scheme convention. Unrealizable dimension and vertex-count pairs require an empty output. Finite-polytope faces, their ordered collection, vertex counts, and finite scheme realizations are the concrete objects needed to state the goal; total computability applies to the complete finite output rather than to individual tests alone.
Reference: Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.5, Theorem 2 (5.5.2), printed p.91, PDF p.117; definitions in §§2.4 and 3.1. Source text.
A vector whose coordinates are all zero or one records a collection of yes-or-no choices. Taking the convex hull of a collection of these vectors gives a 0/1-polytope, also called a binary polytope. Such objects connect discrete choices with geometry: points describe feasible combinations, while supporting inequalities describe restrictions that every feasible combination satisfies. Grünbaum's discussion in §4.9 emphasizes the role of facets of these polytopes in combinatorial optimization and cutting-plane descriptions.
The question here concerns how many facets can occur when the dimension grows. Restricting every generating point to binary coordinates gives a finite, highly structured collection of possible points. Nevertheless, this restriction still allows polytopes with very many distinct boundary faces. The theorem of Bárány and Pór establishes superexponential growth in the largest possible number of facets. The mission concerns the form of this growth asserted in Grünbaum's 2003 notes, printed page 69a, rather than a prescribed numerical constant.
Fix a natural number d. The ambient space is the real coordinate space R^d. A convex hull consists of all convex combinations of the generating points, meaning weighted averages with nonnegative weights whose sum is one. A polytope is the convex hull of a finite set of points. It is full-dimensional when its affine span is all of R^d; this rules out a polytope lying in a proper affine subspace.
For a binary polytope, every generating point belongs to {0,1}^d. A subset of this cube is automatically finite. Nonemptiness and full dimension are imposed separately in the target. Consequently, the dimension in the facet bound is the actual dimension of the polytope as well as the dimension of its coordinate space.
An exposed face is the set of all points of the polytope that maximize a given linear functional. A facet is a face of affine dimension d−1. Facets are counted as geometric sets. Two different inequalities that expose the same face do not contribute two facets. Write f_(d−1)(P) for this number.
The target is the following existence statement:
The constant c and threshold D are chosen before the dimension d. The polytope P may depend on d. The assertion therefore supplies a witness in every sufficiently large dimension. It does not merely assert the existence of one complicated polytope or of witnesses along an unspecified subsequence.
The logarithm is natural. Replacing it by another fixed base greater than one changes the admissible constant c, while preserving the shape of the theorem. The statement leaves both c and D unspecified. The Bárány–Pór paper, Theorem 1.1, supplies the asymptotic context for the book's formulation.
For any fixed c greater than one, the expression c^(d ln d) eventually exceeds A^d for every fixed A greater than one. Thus a single exponential base cannot bound the facet counts of all binary polytopes across dimensions. The binary-coordinate restriction alone does not yield that kind of uniform bound.
The underlying mathematical result is established in the literature. The formalization task is to prove its stated existence conclusion with the precise geometric definitions above. The conclusion concerns actual facets of actual polytopes, so a family of redundant inequalities or a list with repetitions would not satisfy the counting requirement.
A large supply of binary points does not by itself identify the supporting hyperplanes of their convex hull. Counting points and counting facets are different tasks. Moreover, the theorem requires the same growth constant across all sufficiently large dimensions. Verifying individual examples, even examples with many facets, leaves that uniform asymptotic requirement unresolved.
The book describes certain random polytopes as witnesses. Its stated conclusion gives no probability distribution or numerical probability bound. The target records the resulting extremal existence assertion; it imposes no extra probabilistic hypothesis on the witness.
The coordinate model is Fin d → ℝ. IsDPolytope requires a nonempty finite convex hull with full affine span. IsZeroOnePolytope specifies the hull of binary-coordinate points. faceCount P k counts nonempty exposed faces with affine dimension k. These concrete notions also apply to other questions about finite-dimensional polytopes.
Face counts use natural cardinality. On the domain of finite polytopes there are only finitely many faces, so this is the ordinary finite count. Requiring D at least two ensures that d−1 represents the facet dimension without a low-dimensional subtraction convention and that the logarithm's argument is positive. Full dimension excludes the whole polytope from the facet count, and nonemptiness excludes the empty face.
A convex set can be studied through its images in spaces of smaller dimension. Each image records part of the geometry, while losing the information along the directions that are collapsed. A finite convex hull always has finite convex hulls as its affine images. The converse asks whether sufficiently rich projection data can force the original set to have a finite description by points. This mission concerns the recognition theorem attributed to Klee in Grünbaum's Convex Polytopes, §5.1, Theorem 8, printed page 74.
The question concerns all projections into a suitable dimension, rather than an individual view of a set. A single image may conceal directions in which the original set has additional structure. The theorem identifies a condition on the entire family of images that characterizes polytopes among bounded convex sets.
Fix an integer . Real coordinate space consists of vectors with real coordinates. A set is convex if it contains the line segment joining any two of its points. It is bounded if its points remain within some finite distance of the origin. Neither condition requires to fill the ambient space.
The convex hull of a set , written , is the smallest convex set containing . A polytope is the convex hull of a finite set. The generating set need not be a minimal set of vertices. Grünbaum gives this characterization in §3.1, printed page 31. The empty generating set is permitted, as are generating sets contained in a proper affine subspace.
An affine map preserves affine combinations. A surjective affine map has a -dimensional target and reaches every point of that target. When , such a map loses dimensions. This represents the singular affine images called projections in §5.1, printed page 71, with coordinates chosen on the target affine space. Translation of the target is allowed.
For every bounded convex set , the goal is the equivalence
The dimension may depend on , but it is chosen before testing the affine maps. Every surjective affine map with that target dimension is tested. For each such map, the finite set generating the image can be different. No common set of projected vertices or uniform bound on the number of generators is required.
This is one recognition theorem, containing both implications. The selected source grouping does not introduce separate supporting theorem targets.
The theorem characterizes a global finite convex-hull property through lower-dimensional images. In particular, the conclusion concerns the original set itself; it does not merely assert that its closure has a finite generating set. This distinction matters because boundedness and convexity alone do not assert closedness.
The result is a known mathematical theorem in the source. The formalization target is its complete equivalence with the stated domain and quantifier order. A proof of only the preservation of polytopes under affine maps would leave the recognition implication unresolved.
Every tested image can have its own finite generating set. Finiteness of each image does not directly supply a finite generating set that works in the original ambient space. The recognition implication must connect the universal family of images to the geometry of the whole set. Replacing that family by a convenient fixed projection would change the question.
Real -space is represented by functions from Fin d to the real numbers. Boundedness and convexity use the ordinary Mathlib predicates, and being a polytope is expressed directly by existence of a finite set with the specified convex hull. No full-dimensional polytope structure is imposed on .
The hypothesis makes explicit the admissible ambient dimension needed for . In dimension three, the only available target dimension is two. No assertion of the displayed existential criterion is made in dimensions zero, one, or two. Empty sets, singleton sets, and other lower-dimensional subsets remain within the domain in every admissible ambient dimension.
Affine maps are required to be surjective onto the selected coordinate space. Thus their rank is exactly the selected target dimension, rather than an accidentally smaller rank. Closedness, nonemptiness, rational coordinates, and a predetermined number of vertices are not additional hypotheses. The mathematical ingredients are real convex hulls, finite sets, bounded sets, and affine images.
Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003. Theorem 5.1.8, printed page 74 (source.pdf page 100); projection convention, printed page 71 (PDF97); polytope convention, printed page 31 (PDF51). The source pages are included in this package's evidence directory.
A polytope can be represented by cutting a higher-dimensional simplex with an affine flat. The geometry of the cut determines the resulting polytope. Perles's prescribed-point theorem adds a constraint to this representation: the cutting flat must pass through a point chosen in advance inside the simplex. Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition (2003), shows that this requirement can always be met when the simplex has enough facets. The source is §5.1, printed page 74, with the section convention introduced on printed page 71.
A polytope is the convex hull of finitely many points. In this mission it is nonempty and full-dimensional in its ambient real coordinate space. Thus a d-polytope P in R^d contains enough points to span that space affinely. A face is the set of points on which a supporting linear functional attains its maximum; a facet is a face of dimension d−1. Different supporting functionals can describe the same face, so the facet allowance counts geometric faces rather than inequalities used to describe them.
A k-simplex is the convex hull of k+1 affinely independent points. Write its vertices as v₀,…,vₖ in R^k and its convex hull as T. Affine independence means there is no nontrivial affine relation among these vertices. The simplex therefore has dimension k, and its interior is taken in the whole space R^k. No restriction is placed on its side lengths or angles. A d-flat is a translate of a d-dimensional linear subspace. A section of T by such a flat L is the entire intersection T ∩ L.
The target is the following existence assertion. For every d-polytope P with at most k+1 facets, every k-simplex T in R^k, and every p in the interior of T, there is a d-flat L such that
An affine equivalence here preserves affine combinations and is invertible on the affine spans. It can change lengths and angles. In the stated coordinates, it is represented by an injective real affine map A from R^d onto L satisfying
All input data, including the interior point p, are universally quantified before the flat and map are chosen. The flat can depend on these data. The source writes the facet allowance as f and the simplex dimension as f−1; the notation here uses f=k+1.
The prescribed-point conclusion gives control beyond the existence of some simplex section representing P. It permits the simplex and an interior point to be fixed while the cutting flat is selected to recover the given polytope. The conclusion concerns its full affine geometry: the image of every point of P lies in the section, and every point of the section belongs to that image. This is the additional representational constraint discussed immediately before Theorem 10 on printed page 74.
The difficulty lies in meeting these requirements simultaneously. A flat through the chosen point can have an intersection of the wrong affine shape. A section with the correct affine shape need not contain the prescribed point. The theorem requires both properties for every allowed simplex and point, while retaining the original facet bound. Neither a special regular simplex nor a selected interior point captures this quantifier structure.
The formal statement uses real coordinate spaces indexed by finite sets, finite convex hulls, affine spans, exposed faces, and affine maps. Nonempty faces are counted by their affine dimension. In dimension zero the facet allowance is automatic: under the convention counting the empty face it contributes at most one facet, which fits the allowance k+1. This avoids interpreting natural subtraction d−1 as a facet dimension at d=0. The zero-dimensional simplex and zero-dimensional polytope remain within the statement.
This is a known geometric theorem whose formal proof remains to be supplied. The target contains one proof placeholder. The definitions specify the underlying geometry concretely. The mission consists of the single prescribed-section theorem; its definitions support that statement, and no separate supporting theorem is included as a milestone. The source is Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 10, printed page 74 (source.pdf page 100); see also §5.1, printed page 71 (PDF page 97), for the section convention.
A convex polytope has geometric coordinates and a combinatorial structure: its faces, ordered by inclusion. Different coordinates can describe the same combinatorial type. Gale transforms connect these viewpoints by encoding affine dependencies among the vertices as another point configuration, often in a smaller-dimensional space.
Let P and Q be full-dimensional d-polytopes in real coordinate space, each with n vertices. Choose injective lists V and W containing all their vertices and fix a permutation θ of the n indices. The question is whether this prescribed vertex correspondence extends to an isomorphism between the full face posets of P and Q. The empty face and the whole polytope are included in these posets.
An affine dependency of V is a list of real coefficients a whose sum is zero and whose weighted sum of the vertices is zero. These coefficient lists form a vector space of dimension n−d−1. Choose any basis and put its vectors into the columns of a matrix. The n rows of this matrix form a Gale transform G of V. A Gale transform H of W is constructed in the same way, with its own choice of basis. The rows may repeat and may be zero; there is no general-position assumption.
Theorem 5.4.5 states that the prescribed correspondence extends to an isomorphism of face posets exactly when it preserves every relative-interior test on the Gale configurations. For every subset J of vertex indices, the origin belongs to the relative interior of the convex hull of the rows G(J) if and only if it belongs to the relative interior of the convex hull of H(θ(J)). Relative interior means interior within the affine span of the selected convex hull, not interior in the whole coordinate space.
The equivalence concerns every subset of indices and both directions of implication. It retains the prescribed permutation rather than merely asking whether the polytopes have some combinatorial equivalence. Indexing the Gale points also keeps track of which original vertices they represent when several Gale rows coincide. Taking a set image does not change the convex hull of a chosen subconfiguration.
The empty subset is included: its convex hull has empty relative interior, so both membership tests are false. For a simplex, n=d+1 and the Gale space has dimension zero. Its nonempty row subconfigurations consist of the zero vector, and the relative-interior formulation still applies. Zero-dimensional polytopes are also retained.
This mission is the equivalence criterion itself, with the concrete definitions of a full-dimensional polytope, its face poset, and a Gale transform. The grouping keeps transform construction within the vocabulary of the criterion. The neighboring results on affine and projective equivalence have different conclusions and are outside this goal.
Source: Branko Grünbaum, Convex Polytopes, second edition (2003), §5.4, Theorem 5, printed page 89 (PDF page 115). The affine-dependence construction appears on printed pages 85–86 (PDF pages 111–112).
The ordinary chain rule describes how a smooth function changes along a differentiable path. A continuous stochastic path can have fluctuations whose accumulated squared increments remain visible even when the time partition becomes arbitrarily fine. The change of variables formula must account for these fluctuations as well as the part of the path with finite variation. Ethier and Kurtz give this identity for time-dependent functions of multidimensional continuous semimartingales in Chapter 5, Theorem 2.9, equations (2.40)–(2.41), of Markov Processes: Characterization and Convergence.
Work on a complete probability space with a filtration, an increasing family of sigma algebras describing the information available at each nonnegative time. The initial sigma algebra contains every ambient null set. For each coordinate, a continuous semimartingale has a decomposition
The initial vector is measurable with respect to the initial information. Each process is continuous and adapted, starts at zero, and has bounded variation on every bounded time interval. Each is a continuous adapted local martingale, initially zero almost surely: stopping along a suitable sequence of stopping times tending to infinity gives martingales. No Brownian driver or diffusion coefficient is specified.
Let be a real-valued function of nonnegative time and a vector in . The regularity class requires joint continuity of the function, its first time derivative, all first spatial derivatives, and all second spatial derivatives. The time derivative at zero is interpreted from the right. The hypotheses impose no compact support, global derivative bound, or second time derivative.
The goal is the complete identity
It holds almost surely simultaneously for every nonnegative time. The quadratic covariation records the limit of sums of products of increments. Both diagonal and off-diagonal contributions occur. The bracket processes and integral versions are supplied by the conclusion, rather than imposed as additional restrictions on the input processes.
The formula determines how a smooth observation of the evolving state changes. Its terms separate explicit time dependence, finite-variation motion, martingale fluctuations, and their second-order correction. This is the calculus result for a given continuous semimartingale; existence or uniqueness of solutions to a stochastic differential equation is a separate mathematical question. The target is the known theorem in the cited book. Its mathematical assertion includes existence of the integral versions appearing in the displayed identity.
Continuity of the sample paths does not imply bounded variation of the martingale component. Consequently, ordinary pathwise integration against that component does not supply the needed calculus. The stochastic integral requires a probabilistic limiting interpretation. A further issue is the exceptional set: an identity established separately at each time does not by itself provide one event of full probability on which it holds at every time. The continuous versions and the order of the quantifiers address that distinction.
Coordinates are indexed by Fin d, and time is nonnegative. Allowing zero coordinates also includes the consistent case of a function of time alone. A dyadic partition has intervals, so the denominators in the defining sums are nonzero, including at partition level zero. At time zero all increments vanish.
The finite-variation integrals are characterized pathwise by limits of left dyadic sums. The stochastic integrals are continuous adapted processes characterized by convergence of those sums in probability at each fixed time. The cross brackets are characterized by the corresponding increment-product sums and are required to have continuous adapted versions of locally bounded variation. These predicates do not assume the change of variables identity. The ordinary time integral has a continuous integrand on each compact interval, so its integrability follows from the stated hypotheses. The source's almost-sure version conventions are retained; right continuity of the filtration is not an additional hypothesis.
Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. Chapter 5, Stochastic Integral Equations, §2, Theorem 2.9, printed p.287 (held PDF p.296). Probability-space and version conventions: printed pp.279–280 and 286 (PDF pp.288–289 and 295).