All missions

Motivation

How few distinct distances can a planar point set determine? The near enemies of this mission are the closest competitors to the extremal configuration: points in no-three-collinear position (no line through three of them) and points lying on a common sphere — the lattice-sphere slice of Erdős–Füredi–Pach–Ruzsa is the motivating example. The bisector energy of a set counts ordered quadruples $(a,b,c,d)$ of points for which the pair $a,b$ and the pair $c,d$ have the same perpendicular bisector; it measures how far the set is from generic. Lund–Sheffer–de Zeeuw fixed the floor of this statistic: $2n(n-1)$ is a universal lower bound, and bisector injectivity is sufficient for equality. The Near Enemy theorem is the projection statement on top of it — every admissible set admits one generic projection whose image attains that floor, sits in general position, has zero rotation energy, and carries the whole distance-transport package.

Setting

Work with finite sets $P$ of points in the Euclidean plane (EuclideanSpace ℝ (Fin 2)), and in the transport direction with points in EuclideanSpace ℝ ι for a general finite index type. Following Lund–Sheffer–de Zeeuw, the bisector energy is

The rotation energy counts the ordered congruent quadruples whose difference vectors are neither equal nor opposite, so it discards the translation and half-turn channels and isolates the proper-rotation one. A linear map $T$ is projection-generic for a set $G$ when exactly two conditions hold: $T$ sends the difference of any two distinct points of $G$ to a nonzero vector, and for two distinct unordered pairs of $G$ the images never combine a parallel pair of differences with an orthogonal midpoint difference. Perpendicular bisectors, difference classes and distance images are all Finset operations.

Target

The mission goal is the spherical complete profile: for every finite set $G$ lying on a common sphere, in any dimension, there is a linear map $T$ to the plane whose image satisfies six conclusions at once —

together with injectivity of $T$ on $G$, general position of the image (no three collinear, no four cospherical), and exact distance transport. The projection is chosen per set — its very type depends on the ambient dimension — but a single projection delivers all six conclusions together, and that bundled form is what downstream incidence arguments consume.

Milestones ascend in five steps: the universal energy floor, the bisector-injectivity equality case, the attainment of the floor by projection-generic maps, the existence of such a map for every no-three-collinear set, and the no-three-collinear transport bundle that the goal then specialises to the spherical case.

Significance

Lund–Sheffer–de Zeeuw introduced the extremal picture for bisector energy at the level of the exact constant. In footnote 1 on p. 538 of the SoCG 2015 version (LIPIcs vol. 34, 537–552) they state that $\mathcal{E}(P) = 2n(n-1)$ when every distinct pair determines a distinct bisector, with the enumeration of the trivial quadruples that proves the floor. The universal asymptotic form $\mathcal{E}(P) = \Omega(n^2)$ is a remark in their §3.4.

This mission builds a complete machine-checked development of the floor, its attainment and the sufficiency direction, from first principles in Lean 4 over mathlib; the rotationEnergy statistic together with the rotationEnergy = 0 certificate for the projected image, where rotationEnergy(P) = 0 follows from the published "distance Sidon set" property; and a single generic projection of a given set that carries the bisector floor at the same time as the Erdős–Füredi–Pach–Ruzsa general-position package. Four of that bundle's six conjuncts are already in Erdős–Füredi–Pach–Ruzsa 1993, whose Theorem 3.1 supplies them.

Formalizing it matters because the argument composes analysis (generic projections obtained from nonvanishing of circle determinants), algebra (inner-product and determinant polynomial witnesses carrying linear_combination certificates) and counting (fiberwise difference-class tallies) — and the interfaces between the three must agree exactly. The projection-genericity and polynomial-witness lemmas are reusable for any Euclidean extremal formalization.

Difficulty

The hard step is keeping the projection generic through every predicate at once: a projection that preserves no-three-collinearity can still kill a circle determinant, or create a coincidence that the counting needs to keep distinct. The naive first idea — project along a random direction and hope — fails because each predicate forbids a different algebraic hypersurface of directions; the fix is a single simultaneous-avoidance argument over the union, with each forbidden set shown proper by an explicit polynomial witness. That step is the largest proof in the mission and carries its own milestone.

Formalization scope

Points are EuclideanSpace; finite sets are Finset; energies are ℕ-valued statistics. Generic projections are linear maps carrying the explicit two-clause ProjectionGeneric predicate, so there is no hidden regularity assumption. Dimension is a general ι with [Fintype ι] wherever the transport needs it. The goal's only hypothesis is membership of a common sphere; no-three-collinearity is derived from it rather than assumed, because a line meets a sphere at most twice. No statement is vacuous: explicit witnesses were checked in the kernel for the goal and for every milestone.

Welcome contributions: the converse of the equality case — bisector injectivity is proved here to be sufficient for the floor, and necessity is open in this development; sharpness examples beyond the Erdős–Füredi–Pach–Ruzsa configuration; and the incidence assembly that consumes this mission's output.

Selected references

• B. Lund, A. Sheffer and F. de Zeeuw, Bisector energy and few distinct distances, Proc. 31st SoCG 2015, LIPIcs vol. 34, 537–552, DOI 10.4230/LIPIcs.SOCG.2015.537; journal version Discrete Comput. Geom. 56 (2016), no. 2, 337–356, DOI 10.1007/s00454-016-9783-5, arXiv:1411.6868. Source of the bisector-energy statistic and its upper bounds. Footnote 1 on p. 538 of the SoCG version gives $\mathcal{E}(P) = 2n(n-1)$ for every set whose pairs have distinct bisectors, with the count of trivial quadruples that proves the floor; §3.4 (p. 545) gives $\mathcal{E}(P) = \Omega(n^2)$ for every set. The footnote is not in arXiv:1411.6868v1.
• P. Erdős, Z. Füredi, J. Pach and I. Z. Ruzsa, The grid revisited, Discrete Math. 111 (1993), 189–196, DOI 10.1016/0012-365X(93)90155-M — the lattice-sphere-slice configuration that gives this mission its name, and (proof of Theorem 3.1, p. 193) the generic planar projection that is injective, keeps general position and transports distances.
• J. Solymosi and T. Tao, An incidence theorem in higher dimensions, Discrete Comput. Geom. 48 (2012), no. 2, 255–280, DOI 10.1007/s00454-012-9420-x, arXiv:1103.2926, §5.1 — the canonical statement of the generic-projection trick this construction borrows. The same trick is used in J. Pach and F. de Zeeuw, Distinct distances on algebraic curves in the plane, Combin. Probab. Comput. 26 (2017), no. 1, 99–117, arXiv:1308.0177.
• McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, module Geometry.Euclidean.NearEnemyTheorem.

Motivation

A set of integers is sum-free when no two of its members add up to a third. Schur's theorem (1916) says that for every $k$ there is a largest interval $[1,N]$ that can be split into $k$ sum-free classes, and the resulting Schur numbers $S(k)$ are notoriously hard to compute: $S(5) = 160$ was settled only in 2018, by a SAT computation with a machine-checked proof certificate.

Replacing "adds up to" by "adds up to, modulo $m$" gives a family that behaves very differently. Modular Schur numbers were introduced by Chappelon, Revuelta Marchena and Sanz Domínguez, who settled the moduli $m \in \{1,2,3\}$ and proved the universal bound $S_m(k,\ell) \le m-1$ (Electron. J. Combin. 20(2) (2013) #P61). D'orville, Sim, Wong and Ho then closed $m \in \{4,5,6,7\}$ by residue case analysis and posed the general modulus as an open problem (Integers 25 (2025) #A62, their Problem 1). Each additional modulus had cost a separate case analysis, and the case analysis grew with $m$.

The timeline matters for reading what follows. The 2013 paper supplies the universal cap. The 2025 paper supplies a singleton criterion (its Theorem 4) and a divisibility obstruction (its Corollary 3), and applies the latter only in the coprime case $\gcd(m,\ell-1)=1$ (its Corollary 5). What remained was to optimise that obstruction over every residue rather than only in the coprime case, which is what collapses the whole family to one formula.

Setting

Fix integers $m \ge 2$, $\ell \ge 2$ and $k \ge 1$. A set $S$ of integers is $\ell$-sum-free modulo $m$ when there are no $x_1, \dots, x_\ell \in S$ and $y \in S$, repetitions among the $x_i$ allowed, with

The repetition clause is not a technicality: a single element can make its whole class unsafe. The modular Schur number $S_m(k,\ell)$ is the greatest $N \ge 0$ such that the interval $[1,N]$ can be partitioned into at most $k$ classes, each $\ell$-sum-free modulo $m$. A partition into such classes is called valid.

Two derived quantities carry the whole story. Write

Then $dn = m$ exactly, and $d \mid (\ell - 1)$ by construction. All Lean statements in this mission use these same names.

Formalization targets

Goal: the closed form in the many-colours regime

Closed form here means something precise: the value is produced from $m$ and $\ell$ by one gcd, one division and one subtraction, with no search over colourings, no recursion, and no case split on $\ell \bmod m$. The statement fixes no constants and no modulus, so it is not invalidated by any later refinement of the threshold in $k$.

The single-colour value

together with the complementary regime $m < \ell$, where the value is $0$ if $\ell \equiv 1 \pmod m$ and $1$ otherwise. The two together give a value for every admissible pair $(m,\ell)$ at $k=1$, and the tree carries that combined formula at the residue level and at the integer level.

Significance

What the results give. One expression replaces an open-ended sequence of per-modulus case analyses. The moduli $m \in \{1,2,3\}$ of the 2013 paper and $m \in \{4,5,6,7\}$ of the 2025 paper are specialisations, and every remaining modulus is covered at once in the stated range of $k$.

The mechanism is a single self-defeating value. Take $\ell$ copies of $n$: they sum back to $n$ modulo $m$, so the lone class $\{n\}$ already breaks the rule, while every smaller value is safe. That one observation supplies a matching upper and lower bound.

• The upper bound is uniform in $k$. Adding colours never raises the value past $n-1$, which is what makes the formula stable.
• The lower bound costs $n-1$ colours, one per safe residue. Identifying the least sufficient number of colours is where the subject is still open.

Status of the tree, stated precisely. Everything listed under Formalization targets is both proved and machine-checked.

• 21 theorems and 3 definition bundles, each with a complete Lean proof verified by this platform.
• Axiom-clean: each closure is contained in {propext, Classical.choice, Quot.sound}.
• This mission therefore publishes a finished development rather than an open call on its stated goal.
• What is genuinely open is listed under Difficulty below, and is not part of the verified tree.

Relation to the accompanying paper. The paper states the single-colour value only under $2 \le \ell \le m$. Three results in the tree go beyond it: the complementary regime $m < \ell$, and the combined formula covering every $m \ge 2$ and $\ell \ge 2$, stated once at the residue level and again at the integer level. Two further results, the coset-cardinality bounds, are supporting work of the Lean development and are not numbered results of the paper. Each theorem's source field records which of these it is.

Difficulty

The threshold in $k$ is not $n-1$

The obvious attack on the general modulus is to guess that only singletons can be safe classes. The threshold in $k$ would then be exactly $n-1$, and the problem would close for all $k$ at once. That guess is false.

Take $m = 12$ and $\ell \equiv 11 \pmod{12}$, so $d = 2$ and $n = 6$. The two-element set $\{1,5\}$ is $\ell$-sum-free modulo $12$, and three colours then suffice where the singleton count would demand five.

So the least $k$ at which the closed form takes hold, written $k_0(m,\ell)$, is not $n-1$ in general. What is known about it:

• Prime moduli. $k_0(p,\ell) = p-1$ for every $\ell \ge p-1$ with $\ell \not\equiv 1 \pmod p$.
• Composite moduli. Bracketed above and below, but not determined.

A correction to the published prime-power formula

Theorem 8 of D'orville, Sim, Wong and Ho gives a three-branch formula at prime-power moduli. Its middle branch is false. The correction is stated here in full because it bears directly on the threshold.

• The counterexample. At $p = 2$, $i = 3$, $k = 3$ and $\ell = 8$ that branch gives $S_8(3,8) = 5$, while the correct value is $S_8(3,8) = 7$.
• Where the proof fails. In the supporting Lemma 2(2) of that paper. The pair $a = 2$, $b = 6$ satisfies every hypothesis of that lemma at $p = 2$, $i = 3$, $\ell = 8$, yet $\{2,6\}$ is $8$-sum-free modulo $8$.
• The replacement result.

It is proved from a valuation-layer colouring that consumes $i(p-1)$ classes, together with the universal cap. The hypothesis $p \nmid (\ell-1)$ forces $d = 1$ and $n = p^i$, so the replacement reaches the goal theorem's value at $k \ge i(p-1)$ in place of $k \ge p^i - 1$, and it contradicts the printed middle branch for infinitely many triples $(p, i, \ell)$.

Status of that correction, stated precisely.

• It is a prose proof in a draft note, listed under Selected references below and readable in full there.
• It is not formalized, and it is not part of this mission's verified tree.
• Nothing in the verified tree depends on it.
• It is recorded here because a reader who compares this mission against the 2025 paper will otherwise meet the contradiction with no explanation. Formalizing it is the subject of a separate mission.

The intermediate regime

For $1 < k < n-1$ the classes must be simultaneously large and $\ell$-sum-free, and no formula is known. The value is empirically eventually periodic in $\ell \bmod m$ for fixed $k$, verified through $m \le 13$.

None of these open directions is weakened by the goal theorem, which deliberately assumes enough colours to avoid the question.

Formalization scope

Two levels of statement

Two levels appear in the tree, and the distinction between them is the first thing to fix.

• At the integer level the objects are the integers $1, \dots, N$ themselves.
• At the residue level they are their classes modulo $m$, which in Lean is the type ZMod m: Mathlib's type of residues modulo $m$, a commutative ring with exactly $m$ elements for $m \ge 1$, carrying the reduction map from $\mathbb{Z}$ and the arithmetic that map preserves.

Working in ZMod m turns "adds up to, modulo $m$" into a plain equation instead of a divisibility side condition, and it makes every colour class a subset of a finite type.

Conventions

The development works residue-by-residue in ZMod m and commits to the following conventions, all of which are silent in the prose and load-bearing in Lean.

• $\ell$-tuples are functions Fin ℓ → ZMod m valued in the class. This builds in "repetitions allowed" rather than leaving it to a side condition.
• Classes are Finsets, so finiteness is structural.
• A valid partition is a structure with four fields: covering, pairwise disjointness, containment in the target set, and $\ell$-sum-freeness of each class.
• Empty classes are permitted. This is what makes "at most $k$" and "exactly $k$" interchangeable once any colouring exists.

The two numbers, and the cap in their definition

Both a residue-level and an integer-level number are defined, and a reduction theorem proves them equal for every $m \ge 2$. Bounds are proved on the residue side and quoted on the integer side.

Both are defined with Nat.findGreatest against the bound $m-1$. That cap is neither an approximation nor a trivialising choice: a separate theorem shows any $N$ admitting a valid partition satisfies $N \le S_m(k,\ell)$ with no hypothesis on $N$, because $N \ge m$ admits no valid partition at all. A reader checking for a vacuous formalization should also note that the goal is an equality, not a bound, so it cannot be satisfied by weakening a hypothesis.

Reusable beyond this mission

• the residue-reduction bridge;
• the singleton criterion;
• the two coset-cardinality bounds, which are pure counting statements about subsets of a cyclic group whose differences lie in a proper subgroup.

Contributions welcome on the open directions named under Difficulty, in particular any lowering of the threshold in $k$ toward $k_0$, and a closed form for $k_0$ at composite moduli.

Selected references

• J. Chappelon, M. P. Revuelta Marchena, M. I. Sanz Domínguez, Modular Schur numbers, Electron. J. Combin. 20(2) (2013) #P61. https://doi.org/10.37236/2374 (also arXiv:1306.5635)
• J. D'orville, K. A. Sim, K. B. Wong, C. K. Ho, Modular generalizations of Schur numbers, Integers 25 (2025) #A62. https://math.colgate.edu/~integers/z62/z62.pdf
• M. J. H. Heule, Schur number five, AAAI 2018. arXiv:1711.08076
• A. McKenna, A correction to a prime-power formula for modular Schur numbers, 2026. Draft note, not submitted for publication. Released in the repository below on 2026-09-20: PDF · Markdown source
• A. McKenna, Prime-power structure of the stable regime for modular Schur numbers, 2026. Lean development and paper: https://github.com/mysticflounder/modular-schur

Motivation

This mission formalizes John Milnor's Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968) 447–449 (doi:10.4310/jdg/1214428659), a three-page addendum to J. A. Wolf's Growth of finitely generated solvable groups and curvature of Riemannian manifolds, which precedes it in the same issue (421–446, doi:10.4310/jdg/1214428658). Milnor's note has one theorem and three lemmas, and "for definitions and explanations the reader is referred to" Wolf.

Wolf proved that a polycyclic group "either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial growth, or has no such subgroup and is of exponential growth" (p. 421). Milnor's Theorem closes the gap between polycyclic and solvable: "Let $\Gamma$ be a solvable group which is not polycyclic, and $S$ a finite set of generators for $\Gamma$. Then there exists an exponential lower bound $g_S(m) \ge (\text{constant})^m > 1$ for the growth function $g_S$ of $\Gamma$." Together the two papers give the Milnor–Wolf theorem, "that a finitely generated solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth" (Wolf, p. 421). Milnor notes that Wolf's results "provide a partial answer to a problem which was posed by the author in Amer. Math. Monthly 75 (1968) 685–686", and Wolf raises "the question of whether every finitely generated group $\Gamma$, which is not of exponential growth, necessarily has a nilpotent subgroup of finite index" (p. 422); Grigorchuk's groups of intermediate growth (1984) later answered that in the negative, while Gromov (1981) proved that polynomial growth does force a nilpotent subgroup of finite index. Chou's 1980 extension of the Milnor–Wolf theorem to elementary amenable groups, the mission Chou: elementary amenable groups on this platform, cites exactly this theorem. Wolf's paper is the subject of a companion mission.

Setting

Growth. For a finite subset $S$ of a group $\Gamma$, Wolf's growth function $g_S(m)$ (p. 426) is the number of elements expressible as words of length $\le m$ based on $S$, a word $s_1^{a_1} \cdots s_r^{a_r}$ having length $|a_1| + \cdots + |a_r|$. MilnorWolf.growthFunction S m takes $g_S(m)$ as the size of the ball Chou.wordBall S m of the published growth bundle, the set of products of at most $m$ factors from $S \cup S^{-1}$. $\Gamma$ has exponential growth, the published Chou.HasExponentialGrowth, if for some finite generating set $S$ there is $c > 1$ with $g_S(m) \ge c^m$ for all $m$; Wolf shows (p. 434) that this does not depend on $S$.

Polycyclic groups. Wolf's Proposition 4.1 (p. 433) gives eleven equivalent conditions; the definition used here is condition (1): "There is a normal series $\Gamma = A_0 \supset A_1 \supset \cdots \supset A_t = \{1\}$ with every quotient $A_i/A_{i+1}$ finite or infinite cyclic." This is MilnorWolf.IsPolycyclic. A solvable group is Mathlib's Group.IsSolvable: the derived series reaches the trivial subgroup.

Milnor's standing assumptions. The three lemmas concern a group extension $1 \to A \to B \to C \to 1$ where "we will always assume that $A$ is abelian and that $B$ is finitely generated." In the statements, $B$ is a finitely generated group, $A$ an abelian normal subgroup, and $C$ the quotient $B/A$.

Formalization targets

Milnor's Theorem (p. 447)

"Let $\Gamma$ be a solvable group which is not polycyclic, and $S$ a finite set of generators for $\Gamma$. Then there exists an exponential lower bound $g_S(m) \ge (\text{constant})^m > 1$ for the growth function $g_S$ of $\Gamma$." Stated for an arbitrary finite generating set $S$:

This is the goal. The constant is existentially quantified, so a sharper bound does not change the statement. The milestones are Milnor's three lemmas, in order, followed by one published Open theorem of the Chou mission that they prove: Chou's form of Lemmas 1 and 2, where the normal subgroup need not be abelian.

Significance

Milnor's Theorem is the half of the Milnor–Wolf theorem that reaches beyond polycyclic groups: with Wolf's polycyclic dichotomy it says that a finitely generated solvable group is either almost nilpotent, of polynomial growth, or of exponential growth, with nothing in between. That statement is what Chou's Theorem 3.2 extends to elementary amenable groups, and it is the reason a group of intermediate growth cannot be solvable or elementary amenable, the fact that placed Grigorchuk's groups outside those classes.

Formalizing it produces, besides the Theorem, the three lemmas as reusable library results: the subgroup spanned by the conjugates $\beta^k \alpha \beta^{-k}$ is finitely generated when $B$ is not of exponential growth; a normal subgroup with finitely presented quotient is normally generated by finitely many elements; and polycyclic-by-abelian without exponential growth is polycyclic. The proof is complete in the paper; nothing here is open mathematics. On this platform the Theorem and the lemmas are stated and unproved; Chou's mission holds the Open non-abelian form of Lemmas 1 and 2 and two Open reductions that resolve once this mission and the Wolf mission close their externals.

Difficulty

The obvious attempt, to bound the growth of $B$ below by the growth of a free subsemigroup found inside it, is not what Milnor does and does not obviously work for an arbitrary abelian-by-solvable extension. Milnor's argument turns the growth hypothesis into finite generation: among the $2^m$ expressions $\beta\alpha^{i_1} \cdots \beta\alpha^{i_m}$ two must coincide, and the resulting relation expresses $\alpha_m = \beta^m \alpha \beta^{-m}$ in terms of $\alpha_1, \ldots, \alpha_{m-1}$. The delicate step is running this over a whole set of normal generators of $A$ and over each of finitely many $\beta$'s in turn, so that $A$ itself comes out finitely generated (Lemma 3), and then up the derived series of $\Gamma$. In Lean the work is in Lemma 2, which needs the finite presentation of $C$ transported to a presentation on the images of chosen generators of $B$, and in Lemma 3, which needs that a polycyclic group is finitely presented and that an extension of polycyclic groups is polycyclic.

Formalization scope

Growth is measured on the closed balls of the published bundle Chou_Growth: Chou.wordBall S m is the set of products of at most $m$ letters from $S \cup S^{-1}$, and $g_S(m)$ is its cardinality (a Nat.card, finite because $S$ is a Finset). "Not of exponential growth" is the negation of the existential definition, so it is a statement about every finite generating set. Polycyclic is Wolf's condition (1); the definition fixes the reading of "normal series". The abelian hypothesis on $A$ is Mathlib's IsMulCommutative on the subgroup; finite generation and finite presentation are Mathlib's Group.FG and Group.IsFinitelyPresented.

The Theorem's hypotheses are satisfiable: the trivial group is polycyclic, so "not polycyclic" excludes it, and a solvable non-polycyclic finitely generated group exists (the lamplighter group $\mathbb Z/2 \wr \mathbb Z$). No hypothesis is vacuous and no definition makes a target trivially true.

The definitions of polycyclic group, polynomial growth and Wolf's growth exponents $E_1, E_2$ are stated in the bundle MilnorWolf_Growth here because Milnor defers all definitions to Wolf; the results of Wolf's paper, in particular the polycyclic dichotomy that combines with this Theorem into the Milnor–Wolf theorem, belong to the companion mission. Nothing of Milnor's note is omitted. Contributions welcome: proofs of the three lemmas and the Theorem, and general library results they need, such as finite presentability of polycyclic groups.

Selected references

• J. Milnor, Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968), 447–449. doi:10.4310/jdg/1214428659
• J. A. Wolf, Growth of finitely generated solvable groups and curvature of Riemannian manifolds, J. Differential Geometry 2 (1968), 421–446. doi:10.4310/jdg/1214428658
• J. Milnor, A note on curvature and fundamental group, J. Differential Geometry 2 (1968), 1–7.
• A. G. Kurosh, Theory of groups, vol. II, Chelsea, 1956.
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985), 259–300 (Russian original 1984). doi:10.1070/IM1985v025n02ABEH001281
• M. Gromov, Groups of polynomial growth and expanding maps, Publ. Math. IHÉS 53 (1981), 53–78. doi:10.1007/BF02698687
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407 (p. 400). doi:10.1215/ijm/1256047608

Motivation

The exponential function turns addition into multiplication. When its inputs are algebraic numbers, that elementary identity meets a rigid arithmetic boundary: distinct algebraic exponents cannot produce an algebraic linear relation among their exponentials. This principle is the Lindemann–Weierstrass theorem, one of the central results of transcendence theory. Its familiar consequences include the transcendence of Euler's number $e$ and of $\pi$, and therefore the impossibility of squaring the circle with straightedge and compass.

The historical line runs from Hermite's 1873 proof that $e$ is transcendental, through Lindemann's 1882 proof that $\pi$ is transcendental, to Weierstrass's general formulation in 1885. Modern algebraic presentations organize the theorem around conjugates, Galois symmetry, algebraic integers, and an auxiliary-polynomial estimate. The Lean development formalized here follows Yuyang Zhao's mathlib contribution PR #28013, whose mathematical reference is Jacobson's Basic Algebra I, §4.12, Theorem 4.22.

Setting

A complex number is algebraic if it is a root of a nonzero polynomial with rational, equivalently integer, coefficients. A complex number is transcendental if it is not algebraic. Write $\overline{\mathbb Q}\subset\mathbb C$ for the field of algebraic complex numbers and $\exp(z)=e^z$ for the complex exponential.

For a family $(u_i)_{i\in I}$ in $\overline{\mathbb Q}$, injectivity means that distinct indices carry distinct exponents. A family $(x_i)$ is linearly independent over $\overline{\mathbb Q}$ when every finite relation $\sum_i a_i x_i=0$ with algebraic coefficients has all $a_i=0$. It is algebraically independent over $\overline{\mathbb Q}$ when no nonzero multivariate polynomial with algebraic coefficients vanishes on the family.

The strongest target uses natural-number linear independence of $(u_i)$: distinct finitely supported tuples of natural coefficients give distinct sums $\sum_i n_i u_i$. This is exactly the condition needed to distinguish the exponent attached to every monomial.

Formalization targets

Exponential linear independence

For every injective algebraic family $(u_i)$,

This includes the finite Lindemann–Weierstrass relation as its load-bearing finite core.

Hermite–Lindemann and classical constants

For every nonzero algebraic $a\in\mathbb C$,

The same development records the transcendence of $e$, the transcendence of $\pi$, and the transcendence of every nonzero principal logarithm of an algebraic complex number.

Integer winding consumer

Let $\alpha\ne0$ be algebraic and let $w:I\to\mathbb Z$ be injective. The proved Hermite–Lindemann theorem discharges the formerly conditional winding interface and gives

The integer labels are inputs to this arithmetic theorem. A separate topological or dynamical development is responsible for producing them as winding numbers.

Algebraic independence capstone

If $(u_i)$ is a natural-number-linearly-independent family in $\overline{\mathbb Q}$, then

This is the mission's capstone because it turns the linear theorem into a reusable multivariate interface: polynomial monomials become exponentials of distinct natural combinations.

Significance

The theorem separates two kinds of structure that otherwise coexist in the exponential map. The character law $e^{x+y}=e^xe^y$ supplies exact multiplicative relations, but the theorem rules out unintended linear relations over algebraic coefficients. For integer winding consumers, one algebraic nonzero generator $a$ produces the two-sided phase family $(e^{na})_{n\in\mathbb Z}$; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over $\overline{\mathbb Q}$. Winding supplies the discrete labels, while transcendence supplies arithmetic distinguishability.

The formalization contributes more than the named corollaries. It exposes a finite exponential-relation theorem, the algebraic orbit-sum reduction used by it, and general infinite-family interfaces. These components can be reused in later work on exponential polynomials, logarithms of algebraic numbers, and arithmetic representations of topological charges.

This mission formalizes a known theorem; it is not presented as an open mathematical problem. The private theorem graph is already machine-checked against Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The mission records that proof as an independently inspectable dependency graph before any later upstream integration.

Difficulty

The analytic approximation alone is insufficient. It produces a small complex error, but smallness does not imply vanishing, and taking a field norm does not repair the gap because the other embeddings have no corresponding analytic bound. Likewise, a field automorphism of $\overline{\mathbb Q}$ cannot be moved through the complex exponential as an algebraic operation.

The formal statement therefore requires both an analytic and an arithmetic layer. The arithmetic layer must replace a hypothetical algebraic relation by a Galois-stable relation with integer data and a genuinely nonzero integer contribution. The analytic layer must then make the absolute value of that integer strictly less than one. Managing conjugacy classes, root multisets, denominator clearing, finite supports, and the asymptotic prime choice in one kernel-checked chain is the central formalization difficulty.

Formalization scope

The development is pinned to Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Algebraic complex numbers are represented by integralClosure ℚ ℂ; transcendence corollaries are stated with Transcendental ℤ, which is equivalent to the usual absence of a nonzero integer polynomial relation. The finite theorem uses Fintype; the general linear and algebraic independence theorems permit arbitrary universe-zero index types and reduce relations to finite support internally.

The auxiliary algebraic theorem is stated over an arbitrary algebraically closed field over $\mathbb Q$ and a multiplicative character on its additive group. The analytic consumer specializes this character to the complex exponential. Two small support modules provide quotient lifting for finitely supported functions and evaluation identities for symmetric multivariate polynomials.

The condition $a\ne0$ in Hermite–Lindemann is load-bearing: $e^0=1$ is algebraic. Injectivity of the exponent family is load-bearing for linear independence: duplicate exponents duplicate vectors. The capstone's natural-number linear independence is not algebraic independence of the exponents and must not be silently strengthened or weakened.

The source is an attributed, compatibility-preserving port of the May 2026 Lean 4.30 snapshot of mathlib PR #28013. Platform packaging uses the conservative ASCII rename linearIndependent_exp_finite for the upstream private helper and phi for one Greek binder. The elaborated theorem types were compared against the upstream source; these are naming changes only.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Mathlib contributors, AnalyticalPart: the analytic estimate for Lindemann–Weierstrass. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.html

Motivation

Integer winding is one of the simplest ways that continuous geometry produces discrete arithmetic. A loop in the circle has an integer winding number, while the complex exponential turns an additive parameter into a multiplicative phase. This mission asks what arithmetic information survives when those two constructions are combined. Its answer is a conditional but exact bridge: once Hermite--Lindemann supplies one transcendental phase, distinct integer winding labels produce a linearly independent family over the algebraic numbers.

The transcendence input is classical. Lindemann proved in 1882 that the exponential of a nonzero algebraic number is transcendental, and Weierstrass subsequently established the broader theorem now called Lindemann--Weierstrass. A modern statement appears as Theorem 1.1 of Javier Fresán's notes on the Hermite--Lindemann--Weierstrass theorem: exponentials of rationally linearly independent algebraic numbers are algebraically independent. The present mission deliberately does not formalize that analytic theorem. It isolates and formalizes the algebraic consumer that becomes available immediately after its one-variable consequence is supplied.

Setting

Let $K\subseteq E$ be a field extension and let $z\in E$. For every integer $n$, the Laurent power $z^n$ is defined when $z\ne0$. An element $z$ is transcendental over $K$ when no nonzero polynomial with coefficients in $K$ vanishes at $z$. The first target proves that transcendence rules out every finite $K$-linear relation among the two-sided family

For a complex parameter $\beta$, define the integer exponential character

It satisfies $\chi_\beta(n)=\exp(\beta)^n$ and the character law $\chi_\beta(m+n)=\chi_\beta(m)\chi_\beta(n)$. The mission registers the Hermite--Lindemann assertion as an explicit proposition: for every nonzero complex number $\beta$ algebraic over $\mathbb Q$, $\exp(\beta)$ is transcendental over $\mathbb Q$.

Write $\overline{\mathbb Q}$ for the subfield of complex numbers algebraic over $\mathbb Q$. If $\alpha\ne0$ is algebraic, then $i\alpha$ is nonzero and algebraic. Hermite--Lindemann therefore makes $z=\exp(i\alpha)$ transcendental, first over $\mathbb Q$ and then over $\overline{\mathbb Q}$. Integer phases are exactly the Laurent powers $z^n$.

Formalization targets

Laurent-power independence

For every field extension $E/K$ and every $z\in E$ transcendental over $K$,

Integer exponential character

For every $\beta\in\mathbb C$ and $m,n\in\mathbb Z$,

Conditional all-integer phase independence

Assuming Hermite--Lindemann, if $\alpha\in\mathbb C$ is nonzero and algebraic over $\mathbb Q$, then

Winding-labelled capstone

For any injective integer label $w:I\to\mathbb Z$ under the same hypotheses,

The label $w$ may be supplied downstream by a winding-number construction, a self-linking number, or another independently proved integer invariant. This packet consumes the integer; it does not manufacture winding from continuous data.

Significance

The result separates topology from arithmetic cleanly. A geometric or dynamical development is responsible for producing an integer label and proving when labels are distinct. The present mission then turns that discrete distinction into a strong arithmetic conclusion about the corresponding complex phases. Because the Laurent-power theorem is stated over an arbitrary field extension, it is reusable outside circle topology and transcendence theory.

The formalization also records the exact limits of the conclusion. The phase with label zero is $1$ and is not individually transcendental. Repeated winding labels force repeated vectors and therefore destroy linear independence. At zero coupling every phase collapses to $1$. Finally, the character law supplies multiplicative relations, so the indexed phases are not being claimed algebraically independent as separate variables. The theorem is linear independence over $\overline{\mathbb Q}$, not algebraic independence of an unconstrained family.

Difficulty

The main algebraic difficulty is the presence of negative exponents. Ordinary polynomial evaluation detects finite relations among nonnegative powers, but an integer-indexed relation is a Laurent polynomial. The formal statement must ensure that evaluation of Laurent polynomials at a nonzero transcendental element is injective. It must also transport transcendence from $\mathbb Q$ to the algebraic closure embedded in $\mathbb C$ without replacing the registered field by an informal copy.

The transcendence theorem itself is a much larger analytic and algebraic-number-theoretic development. Treating it as an explicit hypothesis is therefore load-bearing: no unproved axiom or hidden instance may assert Hermite--Lindemann. Full Lindemann--Weierstrass is stronger than needed for this one-parameter family, since all exponents are integer multiples of a single algebraic generator.

Formalization scope

The mission targets Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f with Lean 4.30. Laurent polynomials are Mathlib's finitely supported integer-indexed monoid algebra. The algebraic numbers are represented by algebraicClosure ℚ ℂ, the subtype of complex numbers algebraic over the rationals. Linear independence is the ordinary Mathlib module-theoretic predicate.

The reusable core proves Laurent-power independence for arbitrary fields and arbitrary field extensions. The complex consumer uses Mathlib's complex exponential, the algebraicity of $i$, and the algebraic-closure transcendence transfer. The mission includes explicit degenerate controls for zero coupling and duplicate labels. It does not prove Hermite--Lindemann, Lindemann--Weierstrass, transcendence of $\pi$, a topological winding theorem, or algebraic independence of the phase family.

Selected references

• Javier Fresán, Gevrey Arithmetic and E-functions, Chapter 1, Theorem 1.1 (Hermite--Lindemann--Weierstrass), 2023. https://javier.fresan.perso.math.cnrs.fr/gevrey.pdf
• Encyclopedia of Mathematics, Lindemann theorem. https://encyclopediaofmath.org/wiki/Lindemann_theorem
• Mathlib, Mathlib.Algebra.Polynomial.Laurent, Laurent-polynomial definitions and evaluation. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Laurent.html

Motivation

Phase winding is an integer attached to a circle-valued field on a closed spatial cycle. It distinguishes configurations that cannot be continuously deformed into one another while remaining circle-valued and spatially continuous. In oscillator and spin models this integer is often described informally as conserved by smooth evolution, while changes of winding are attributed to phase slips, vortices, singularities, or branch-cut crossings. The purpose of this mission is to turn that informal division into an exact Lean interface.

The continuum and finite-lattice settings must be separated. A jointly continuous field on a spatial circle really does provide a homotopy of circle maps, so its degree is invariant. A finite list of continuously moving vertex phases does not by itself determine a continuous field on the geometric realization of the lattice. Principal shortest-arc interpolation becomes ambiguous at antipodal bonds, and the corresponding discrete winding can jump even though every vertex phase remains continuous. The mission therefore treats winding as a first integral only on the regular sector and records every failure of regularity through an integer reset ledger.

This distinction is relevant to circle-valued reductions of the Kuramoto model, the finite XY model, and Lohe-type dynamics. Kuramoto's original synchronization model concerns coupled phase oscillators, while Lohe's non-Abelian extension replaces phases by group-valued variables. A model-specific conservation theorem is justified only after the dynamics has been connected to an actual circle-valued spatial loop or to the registered finite principal-branch interface.

Setting

A circle loop is a continuous map from a closed parameter interval to $S^1$ whose two endpoints agree. Its winding number is the integer obtained from the endpoint of a lift to the universal cover $\mathbb R\to S^1$. When the loop's basepoint moves during a deformation, the loop is normalized by the inverse of its value at the chosen spatial basepoint; this produces a based loop without changing its winding.

A continuous Circle-field segment is a jointly continuous map

Each time slice $U_t$ is a spatial loop. Such a segment has no branch-cut convention: it is intrinsic topological data.

For a finite directed edge system (including a finite periodic lattice), a state assigns a real lift to every vertex. Each oriented edge receives an integer principal turn. A state is branch regular when no stored edge is antipodal. A coherent finite reset ledger stores successive principal-turn cochains $T_i$ and defines the reset $k_i=T_{i+1}-T_i$. For a certified closed integer cycle $C$, the pairing $\langle k_i,C\rangle$ is its registered winding jump.

A Kuramoto, XY, or Lohe consumer must supply the missing model-specific data. For a continuum consumer this is a jointly continuous circle-valued field. For a finite consumer it is a continuous vertex trajectory together with branch regularity away from registered events. A Lohe consumer additionally needs a continuous Circle readout or invariant Circle carrier; preservation of a rotor constraint alone does not provide that reduction.

Formalization targets

Continuous-field conservation

For every jointly continuous Circle-field segment, the two endpoint loops have equal winding:

The statement must cover moving loop basepoints through explicit normalization. Winding is defined directly from Mathlib's exponential covering map as the floor of the zero-based lift endpoint divided by $2\pi$.

Branch-regular finite conservation

For every finite directed principal-phase trajectory on a preconnected time domain that remains branch regular, every registered integer-chain winding is constant:

Continuity of the vertex phases alone is not a sufficient hypothesis and must not appear as a replacement for branch regularity or spatial interpolation.

Exact reset balance

For a finite coherent ledger with steps $i=0,\ldots,N-1$, endpoint winding change equals the sum of the reset periods:

The conservation theorem is the empty-ledger or zero-period special case. The statement is an exact integer identity and does not assert an energy lower bound, vortex separation, or a thermodynamic-limit result.

Dynamics adapters

The generic dynamics adapter requires a jointly continuous ambient-state segment, a registered carrier containing it, closed spatial profiles, and a continuous readout from that carrier to the Circle. Kuramoto/XY or Lohe consumers must separately prove those hypotheses for their model. A second fence states that a global continuous readout from a simply connected carrier maps every loop to a nullhomotopic Circle loop; nonzero Lohe winding therefore requires a separately registered non-simply-connected carrier, such as a preserved $U(1)$ orbit, or a different explicit interface.

Significance

The resulting theorem family makes precise the statement that winding obstructs unwinding. In the intrinsic continuum setting, winding cannot change while the field remains a continuous $S^1$-valued map. In the finite principal-branch setting, winding is piecewise constant and every change has an exact integer certificate. This separates a topological conservation law from the physical or analytic question of how much energy is needed to realize a certificate.

For formalization, the mission supplies a reusable boundary between topology and dynamics. A dynamics development can establish continuity and carrier preservation without reimplementing covering-space winding. A lattice development can consume the same integer through reset cochains without claiming that a vertex-only path is a homotopy of spatial loops. Later energy-barrier, vortex, and transport results can depend on the reset balance rather than on an informal conservation principle.

Difficulty

The principal difficulty is that several superficially similar notions of continuity have different consequences. Continuity in time of finitely many vertex phases is continuity into the configuration torus $(S^1)^V$, which is connected and does not preserve a principal-edge winding sector. Continuity of a map on time times the geometric spatial cycle is stronger. A formal statement that confuses them would make the desired theorem false.

There are two additional interface risks. First, the canonical Circle lift is based, whereas a physical phase field normally has a moving value at the chosen spatial origin. Second, the current Lohe development establishes algebraic identities and infinitesimal rotor preservation, not a global continuous flow in a selected Circle subgroup. These distinctions remain visible in the theorem hypotheses.

Formalization scope

The mission targets Lean 4.30 with Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, matching the cited LeanProofs development. It reuses Mathlib's unit interval, continuous maps, path homotopies, Circle covering map, local constancy, and finite sums. The continuum statement concerns spatial $S^1$ only. The finite theorem is graph-generic: it uses finite oriented edges, integer edge cochains, certified closed integer cycles, coherent successive reset states, and branch regularity on a preconnected time domain.

The scope excludes ODE or PDE existence and uniqueness, preservation of a Circle carrier by a particular Lohe vector field, extraction of a coherent reset ledger from a physical event trajectory, arbitrary graph interpolation, accumulating reset times, thermodynamic limits, and energetic barriers. Those may be attached later through explicit interfaces. No theorem claims global winding conservation for an unrestricted finite vertex trajectory, and no theorem identifies group-valued Lohe motion with Circle motion without a declared continuous readout.

Selected references

• Monumental Systems, CircleFundamentalGroupWindingV1, LeanProofs commit b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleFundamentalGroupWindingV1.lean#L81
• Monumental Systems, FiniteTorusPrincipalResetEventV1, LeanProofs commit b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/StatMech/FiniteTorusPrincipalResetEventV1.lean#L152-L167
• Monumental Systems, CircleWindingTranslationHolonomyV1, LeanProofs commit b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleWindingTranslationHolonomyV1.lean#L107
• Y. Kuramoto, “Self-entrainment of a population of coupled non-linear oscillators,” in International Symposium on Mathematical Problems in Theoretical Physics, Lecture Notes in Physics 39, 1975, pp. 420–422. https://doi.org/10.1007/BFb0013365
• M. A. Lohe, “Non-Abelian Kuramoto models and synchronization,” Journal of Physics A: Mathematical and Theoretical 42 (2009), 395101. https://doi.org/10.1088/1751-8113/42/39/395101
• A. Hatcher, Algebraic Topology, Chapter 1, Cambridge University Press, 2002. https://pi.math.cornell.edu/~hatcher/AT/ATch1.pdf

Formalize the corrected theory of flavor mixing angles in the su(3) Cartan sector of Cl(6,0), replacing the retired Killing-form/GUT normalization story. The mechanism: T3 and T8 commute, so mixing is carried not by their commutator but by the complete ordered products retained in grade 4. Milestone path: (M1) the grade-4 projection Pi4: Sym^2(A2) -> span{AB,AC,BC} is an isomorphism, with Pi4(e3^2) = -AB, Pi4(e3 e8) = (BC-AC)/sqrt 3, Pi4(e8^2) = (1/3)AB - (2/3)AC - (2/3)BC and tan(2 theta) = sqrt 3 (w-v)/(2u-v-w) for a retained grade-4 field G4 = u AB + v AC + w BC. (M2) the bridge: the primitive finite-T8 Cartan vector Phi = t e3 + e8 with t = sqrt 5 - 2 (the exact r = 16 closure) has grade-4 image exactly the rank-one family tensor phi phi^T; its traceless part is t[[-2,1],[1,2]], the Cabibbo family tensor up to one family-state sign, giving theta_C = arctan(sqrt 5 - 2) ~ 13.28 degrees; the grade-4 tensor has the same Sym2 structure as a left-handed Yukawa Gram operator M M^dagger. (M3, guarded goal) identify the r = 16 tensor with the relative left-family Yukawa tensor, closing the Sym2/Gram bridge. Foundational lemmas (A2 Cartan plane with [T3,T8] = 0, the complete 7-bracket su(3) table, grade-4 square residuals, grade-6 cubic channel) are landed in the LeanProofs repository and will be contributed as importable platform nodes ahead of the milestones. Recorded provenance: HAM memories #2848 (FullGradeCartanMixingTensorV1, 2026-09-14) and #3099 (CabibboGramSym2BridgeV1, 2026-09-17), proof DAG galaxy.proof-dag.v1 grade4-cartan-mixing.

Motivation

A real lift of a circle-valued phase records both a principal representative and an integer sheet. This packet isolates the neutral arithmetic of that lifted reading before any physical interpretation as time, dynamics, causality, or a preferred vacuum.

Setting

A clock candidate is a function from an arbitrary event type to the real universal cover of the circle. Principalization separates each real value into a representative modulo $2\pi$ and an integer sheet. Real origin shifts, integral deck shifts, and orientation reversal are treated as distinct transformations.

Formalization targets

The intended packet covers principal-ledger reconstruction, the conditional strict order induced by an injective or monotone lift, affine-origin and deck freedom, orientation reversal, an adapter from separately established circle winding to an integer clock turn, and a scalar power-law integrability boundary.

The exact target statements remain subject to reconciliation with the immutable LeanProofs source before this private draft is submitted. In particular, no arithmetic quotient identity may be presented as the full Circle winding adapter, and no scalar integrability theorem may be interpreted as a PDE blow-up result.

Significance

This separates universal-cover bookkeeping from later consumers. A subsequent packet may connect the ledger to reset cochains, null-pair torsors, or dynamics only through explicit adapters.

Difficulty

The main risks are sign conventions at the principal cut, degeneracy on empty event types, confusion between the continuous real origin action and the integral deck action, and circular definitions that manufacture winding from the desired clock integer.

Formalization scope

The development targets Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. It makes no claim of monotone physical time, dynamical selection, causal order, global foliation, PDE existence, singularity formation, or a canonical origin or orientation.

Selected references

• Monumental Systems, WindingProtoTimeV1Targets, LeanProofs commit b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/WindingProtoTimeV1Targets.lean
• Monumental Systems, CircleFundamentalGroupWindingV1, LeanProofs commit b656238b73d5f0f74515f6574a1dcb4e0216129f, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleFundamentalGroupWindingV1.lean

Motivation

The first three missions in this programme settle the ordinary $3\times3$ magic squares end to end: Mission I proved MacMahon's count $M_{3}(3e)=2e^{2}+2e+1$, Mission II his semi-magic count $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$, and Mission III classified the normal squares (Lo Shu uniqueness). All three work with the plain magic condition.

This mission counts the two special classes that are singled out by requiring more than magicness, in the opposite directions one expects:

• the panmagic (pandiagonal) squares, whose broken diagonals must also have the magic sum — a strengthening so strong that for order three the whole family collapses;
• the symmetric magic squares, whose array must equal its transpose — a symmetry that only removes a few conditions and leaves a genuine family.

Writing $P_{3}(t)$ and $S_{3}(t)$ for the two counting functions, the goal is to determine both for every line sum $t$:

Setting

Everything is built on the vocabulary of MagicSquares (Mission I):

• IsPanMagic — semi-magic, and every broken diagonal in both directions has the line sum, indices read modulo $n$;
• IsSymmetric — $M_{ij}=M_{ji}$;
• panMagicCount, symmetricMagicCount — the cardinalities of the two filtered finsets of arrays over Fin (t+1), which is lossless because every entry of a square of line sum $t$ is at most $t$.

The new definition module MagicSquaresSpecial3 records the two explicit shapes that the proofs produce: constSquare3 e (the array all of whose entries are $e$, read over the ambient Fin (3e+1)) and

together with the parameter set symmParamSet e $=\{0,\dots,2e\}$ and its cardinality symmParamCount e.

Formalization targets

Goal — the complete count

special_three_count: for every natural number $t$, the pair of equalities displayed above. The proof splits on $3\mid t$ and reduces to four child nodes.

The route

1. Panmagic collapses to the constant square (pan_three_card). Writing the array as $a,b,c;d,m,f;g,h,i$, the twelve line equations form a linear system whose only nonnegative solution is $a=b=\dots=i=e$. So $P_{3}(3e)=1$.
2. Symmetry is classified by a corner (symmetric_magic_three_classify). Symmetry identifies three pairs of entries, leaving five free cells and five line equations; the anti-diagonal $2c+m=3e$ forces $c=m=e$, and the rows give $M=\mathrm{symmMagic3}(e, M_{00})$.
3. A bijection onto an interval (symm_three_bij). Sending a symmetric magic square of line sum $3e$ to $M_{00}$ is a bijection onto $\{0,1,\dots,2e\}$; hence $S_{3}(3e)=2e+1$.
4. The divisibility obstruction (pan_three_otherwise, symm_three_otherwise). Both classes consist of magic squares, and an order-three magic square has centre $t/3$ (center_of_order_three), so $3\nmid t$ forces both counts to vanish.

Significance

The results. The three order-three counts behave completely differently in the same parameter: MacMahon's $M_{3}$ is quadratic, the symmetric count is linear, and the panmagic count is constant. That contrast is the point of the order-three study — order three is small enough to be completely understood, and the special classes show how differently the two natural strengthenings of the magic condition act. It is also exactly what is lost at order four, where no closed form is known for any of the three.

Formalizing them. The mathematical content is elementary, but the two classes require genuinely different proof techniques, which is what makes the mission worth formalizing:

• For the panmagic case the six broken diagonals together with the rows and columns give a subtraction-free linear system over $\mathbb{N}$, so the uniqueness step is a single omega call. The only work is exposing the twelve equations, which requires reducing the index arithmetic $i+k$ and $\mathrm{rev}(i)+k$ on Fin 3.
• For the symmetric case the answer is a family, and the admissibility bound $a\le 2e$ is a statement about truncated subtraction: the entry $2e-a$ is computed in $\mathbb{N}$, so the row identity $a+(2e-a)+e=3e$ is satisfiable precisely for $a\le 2e$. Formalizing the bijection therefore needs an honest treatment of that truncation, where the panmagic case needs none.

Difficulty

Truncated subtraction, in the admissibility direction. The classification M = symmMagic3 e (M 0 0) is true for every $M$, without any bound on $M_{00}$; the bound only appears when asking which members of the family are squares of line sum $3e$. Keeping those two statements apart is what makes the bijection proof manageable: classification is a pure omega computation, while admissibility is a one-line argument that $a+(2e-a)=2e$ forces $a\le 2e$.

Finite but not decidable. panMagicCount and symmetricMagicCount are cardinalities of filtered finsets over a function type, so the proofs cannot be decide or norm_num — the platform forbids native_decide in any case. Both counting theorems are therefore stated as Finset.card_bij / card_eq_one arguments over explicit bijections, not as finite evaluations.

Formalization scope

• The in-scope statements are the two closed forms for all $t$, together with the classification of the symmetric family that the bijection is built on.
• Parametrization follows MacMahon; the symmetric shape is the diagonal slice $c=e$ of his two-parameter family, which is why the count drops from quadratic to linear.
• Nothing here re-proves Mission I: the divisibility obstruction is inherited from the already-proved center_of_order_three.
• Reusable beyond this mission: the order-three classification of symmetric magic squares, the observation that panmagic order-three squares are exactly the constant ones, and the technique of discharging twelve-index linear systems over Fin 3 with a single omega.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916.
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• W. S. Andrews, Magic Squares and Cubes, 2nd ed., Dover, 1960.
• H. Behforooz, Symmetric and panmagic squares (survey of the symmetry properties of magic squares), and the standard pandiagonal literature.

Motivation

Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.

Setting

Work in an arbitrary abelian group $G$ (Lean: AddCommGroup G). For finite $X, Y \subseteq G$, the additive energy $E(X,Y)$ counts quadruples $(x,x',y,y')$ with $x + y = x' + y'$; the trivial maximum is $|X|^3$ when $|X| = |Y|$. The sumset $X + Y$ is $\{x + y\}$, and the difference set $X - Y$ is defined pointwise. A set has small doubling when $|X + X|$ is linear in $|X|$. The Lean development uses Finset.addEnergy and Finset.addConvolution from Mathlib.

A bipartite graph here is an edge set $E$ of type Finset (G × G) with $E \subseteq A \times^s B$, not a Mathlib SimpleGraph; solvers should state graph hypotheses that way. Given such an $E$, the partial sumset $A +_E B$ is $\{a + b : (a,b) \in E\}$, following Tao–Vu Definition 2.28.

Target

The mission goal is the two-set (equal-cardinality) form:

This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps $c$ and $C$ existential; the explicit-constant variant is proved separately in the mission with $c = \eta/16$.

The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.

Significance

The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.

Formalizing it matters because the constants are the content: the development tracks explicit constants through dependent random choice (graph level $c = \delta/8$ and $C = 2^{13}K^3/\delta^5 + 2^{12}/\delta^5$; energy level $c_0 = \eta/16$ and $C_0 = 2^{13}(4/\eta)^3/(\eta/2)^5 + 2^{12}/(\eta/2)^5$), which paper proofs often leave implicit. Fox–Sudakov state the application for sets of integers; the formalization is over an arbitrary AddCommGroup, with no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1) contains no BSG statement, so this fills a genuine upstream gap.

Difficulty

The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.

Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's $a' \ne a$ and $b' \ne b$ terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.

Formalization scope

Sets are Finset G in an AddCommGroup G with DecidableEq; energy is Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise sumset and difference operations from open scoped Pointwise. Density hypotheses are stated with explicit real constants. The counting lemmas at the bottom of the development (sum_addConvolution_eq_card_product, path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are unconditional; the statements that need them carry the nonemptiness, equal-cardinality and density hypotheses that exclude degenerate zero-energy configurations. Welcome contributions: the single-set polynomial Freiman–Ruzsa consequences, and non-abelian variants.

Selected references

• A. Balog and E. Szemerédi, A statistical theorem of set addition, Combinatorica 14 (1994), 263–268.
• W. T. Gowers, A new proof of Szemerédi's theorem for arithmetic progressions of length four, Geom. Funct. Anal. 8 (1998), 529–551.
• J. Fox and B. Sudakov, Dependent random choice, Random Structures & Algorithms 38 (2011), 68–99 (Lemmas 5.1/5.2 and §5.1 BSG application).
• T. Tao and V. Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Definition 2.28 (partial sumsets), Theorem 2.29 (BSG, p. 79) and Lemma 2.30 (energy to partial sumset, p. 80).
• C. Reiher and T. Schoen, Note on the theorem of Balog, Szemerédi, and Gowers, Combinatorica 44 (2024), no. 3, 691–698 (arXiv:2308.10245).
• I. Ruzsa's inequalities via Mathlib's Finset.pluennecke_ruzsa_inequality_nsmul_add; see G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, Combinatorica 32 (2012), 721–733 (arXiv:1101.3507).
• McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, modules Combinatorics/Additive/BalogSzemerediGowers and BSGEnergyToGraph.

Motivation

The first two missions in this programme counted order-three squares. Mission I proved MacMahon's magic count $M_{3}(3e)=2e^{2}+2e+1$ and Mission II his semi-magic count $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$. What neither does is classify: counting tells you how many squares there are, but not what they look like.

This mission closes that gap for the most classical case of all. A normal magic square of order three is a $3\times3$ array containing each of $1,2,\dots,9$ exactly once, whose rows, columns and two main diagonals all sum to the magic constant $15$. The statement to be proved is the uniqueness of the Lo Shu square:

every normal magic square of order three is one of the eight images of $\begin{pmatrix}4&9&2\\3&5&7\\8&1&6\end{pmatrix}$ under the symmetry group of the square.

In particular there are exactly $8$ of them, and they form a single orbit under the dihedral group $D_{4}$.

Setting

MacMahon's parametrization (already formalized in MagicSquaresParam3) writes every order-three magic square of line sum $3e$ as

with $(a,c)$ ranging over the finite admissible set paramSet e. For a normal square the magic constant is $15$, so $e=5$ and the centre entry is $5$.

Normality (IsNormal) means every entry lies in $[1,9]$ and the nine entries are pairwise distinct — equivalently, they are a permutation of $1,\dots,9$.

Formalization targets

Goal — Lo Shu uniqueness

together with the identification of those eight parameter pairs. By the bijection magic_three_param_bij this is exactly the statement that there are eight normal magic squares of order three, i.e. that Lo Shu is unique up to the symmetry group of the square.

The route

1. Normality bounds the parameters. If $\mathrm{mkMagic3}(5,a,c)$ is normal then $1\\le a\\le 9$ and $1\\le c\\le 9$, because $a$ and $c$ are corner entries. This reduces the classification to a finite search over $81$ pairs.
2. Classification (magic_three_normal_classify). Within that range, $\mathrm{mkMagic3}(5,a,c)$ is normal exactly when $(a,c)$ is one of

The eight surviving pairs are precisely those with $a,c$ distinct corners of the Lo Shu square; the excluded ones are those with $a+c=10$, for which the $(2,1)$ entry $a+c-5$ collides with the centre $5$. 3. Converse (magic_three_normal_converse). Each of the eight pairs really does give a normal square.