Motivation

The 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 $J$ is not derived here; it remains a modelling premise. This mission shows only that passivity forces symmetry on every link in every direction.

Setting

Fix natural numbers $q$ (number of axes), $L$ (sites along each axis) and $d$. A site is a point $x \in (\mathbb{Z}/L\mathbb{Z})^q$ of the periodic cubic lattice; $x \pm e_a$ is the site one step forward or back along axis $a$, wrapping around. Each link — a site $x$ together with an axis $a$ — carries its own real $d\times d$ matrix $W(x,a)$, and each site carries a velocity $v(x) \in \mathbb{R}^d$. The force on site $x$ is

$$F(x) = \sum_{a} \Bigl( W(x,a)\, v(x+e_a) - W(x-e_a,a)\, v(x-e_a) \Bigr),$$

where the second term uses the matrix of the link behind $x$. The total power is

$$P_W(v) = \sum_{x} v(x) \cdot F(x).$$

In Lean, sites are Site q L = Fin q → Fin L, the step is shift x a s (update coordinate $a$ by $s$ in Fin L), and the power is PassivityTorus.power q L d W v. The coupling is passive when $P_W(v) = 0$ for every $v$.

Formalization targets

Goal: passive if and only if every link is symmetric ($L \ge 3$)

$$L \ge 3 \;\Longrightarrow\; \Bigl(\forall v,\; P_W(v) = 0\Bigr) \iff \Bigl(\forall x, a,\; W(x,a)^{\mathsf T} = W(x,a)\Bigr).$$

This is PassivityTorus.passive_iff_symm, for every $q$ and $d$.

Milestones

1. M1. Stepping back then forward along an axis returns to the start.
2. M2 (power identity, every $q$, $L$). $P_W(v) = \sum_x \sum_a v(x) \cdot \bigl((W(x,a) - W(x,a)^{\mathsf T})\, v(x+e_a)\bigr)$.
3. M3 (symmetric links are passive, every $L$).
4. M4 (passive forces symmetric, $L \ge 3$).

Significance

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 $\le 3.6\times10^{-14}$ at $(q,L) = (1,3), (2,3), (3,3), (3,4)$). A proof covers every $q$, $L \ge 3$ and $d$.

Difficulty

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 $x$ and $x+e_a$ together with a proof that no other link joins them.

The hypothesis $L \ge 3$ is necessary. At $L = 2$ the step forward and the step back along an axis reach the same site. This is proved (in Lean, locally): for every $q \ge 1$, putting the same non-symmetric matrix $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$ on every link of the $L = 2$ lattice gives exactly zero power for every velocity field, so passivity does not force symmetry there. Weakening the hypothesis makes the goal false.

Formalization scope

• The lattice is periodic in every axis, with the same $L$ along each; [NeZero L] is needed for the literal $1$ in Fin L and is implied by $L \ge 3$ in the goal.
• There is one matrix per site per axis, with no relation assumed between links.
• Passivity is quantified over all velocity fields; everything is real.
• $q = 0$ (a single site, no links) and $d = 0$ are included; both sides of the goal hold trivially there, and this is not a trivialization since the statement is quantified over all $q$ and $d$.

Selected references

• Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
• Wikipedia, Passivity (engineering). https://en.wikipedia.org/wiki/Passivity_(engineering)
• Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

Motivation

The 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 $\beta$, a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way. The predicted difference is

$$\Delta\omega = 2\beta c \sin q,$$

where $c$ is the neighbour coupling and $q$ the wavenumber. The claim is that this difference is pinned: it does not depend on the on-site stiffness $K$, even though each of the two frequencies does. Simulations of the model measured the linear asymmetry at $1.000038$, $1.000033$ and $1.000026$ times the predicted value at stiffness $0.90$, $1.00$ and $1.10$, i.e. protected to about $10^{-5}$. This mission proves the exact statement for a uniform lattice.

What this mission does NOT prove.

• Only the linear, small-amplitude asymmetry. At larger amplitude there is a nonlinear correction whose coefficient $\kappa$ does change with the stiffness; in simulation it swings by about 35% over a ±10% stiffness change. That coefficient is not protected, and this mission says nothing about it.
• Only a uniform lattice, with every site at the same stiffness $K$. When the stiffness varies from site to site, the asymmetry does shift (measured in simulation). This mission covers the uniform case only.

Setting

Fix real numbers $K$ (on-site stiffness), $c$ (neighbour coupling), $\beta$ (gyroscopic strength) and a wavenumber $q$. Write

$$b(q) = \beta c \sin q, \qquad R(q) = \bigl(\beta c \sin q\bigr)^2 + K + 2c\,(1 - \cos q).$$

The upper-branch frequency on a uniform ring is

$$\omega(q) = \beta c \sin q + \sqrt{\bigl(\beta c \sin q\bigr)^2 + K + 2c\,(1 - \cos q)} = b(q) + \sqrt{R(q)}.$$

In the Lean development this is PinnedAsymmetry.omega K c β q, with Real.sqrt for the square root. When $R(q) \ge 0$, $\omega(q)$ is a root of the dispersion relation

$$\omega^2 - 2\beta c \sin q\,\omega - \bigl(K + 2c\,(1 - \cos q)\bigr) = 0 .$$

Formalization targets

Goal: the asymmetry is $2\beta c \sin q$, independent of $K$

$$\omega(q) - \omega(-q) = 2\beta c \sin q \qquad \text{for all real } K, c, \beta, q .$$

This is PinnedAsymmetry.asymmetry. The right-hand side contains no $K$. As an immediate consequence, for any two stiffnesses $K_1$ and $K_2$ the asymmetry is identical.

Milestones

1. M1 (the formula is a branch frequency). If $R(q) \ge 0$, then $\omega(q)$ solves the dispersion relation above.
2. M2 (the radicand is even in $q$). $R(-q) = R(q)$, because $\sin^2(-q) = \sin^2 q$ and $\cos(-q) = \cos q$.

Significance

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 $K$ 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 $\kappa$ and non-uniform stiffness).

Difficulty

The difficulty is low. The asymmetry is a difference of two expressions that each contain a square root depending on $K$; 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.

Formalization scope

• All parameters $K, c, \beta, q$ are arbitrary reals; no sign conditions are imposed in the goal.
• Lean's Real.sqrt returns $0$ on negative inputs. The goal still holds in that regime, because the two radicands $R(q)$ and $R(-q)$ are equal, so the two square roots are equal whatever value they take. For physical parameters ($K \ge 0$, $c \ge 0$) the radicand is always non-negative.
• M1 carries the hypothesis $R(q) \ge 0$, since only then is $\omega(q)$ a genuine root of the dispersion relation.
• The frequency is the upper branch only (the $+$ sign in front of the square root).

The development needs only Mathlib's real trigonometric functions and Real.sqrt.

Selected references

• Wikipedia, Dispersion relation. https://en.wikipedia.org/wiki/Dispersion_relation
• Wikipedia, Gyrator (gyroscopic, non-reciprocal coupling). https://en.wikipedia.org/wiki/Gyrator
• Mathlib, Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning $0$ on negative inputs; Real.sq_sqrt). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.html

Motivation

The 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 $J$ form a space of dimension $n^2 = \dim \mathfrak{u}(n)$. 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

$$\text{passive} \;\Longrightarrow\; \text{every } W_i \text{ symmetric} \qquad\text{(this mission)},$$ $$\text{symmetric} + \text{commutes with } J \;\Longrightarrow\; \dim = n^2 \qquad\text{(companion mission)}.$$

What these two missions do NOT prove. Commuting with $J$ 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 $J$-compatible couplings have the dimension of $\mathfrak{u}(n)$. The $J$-compatibility step remains a modelling premise. In addition, the coupling space consists of the Hermitian matrices, which match $\mathfrak{u}(n)$ in dimension; the Lie algebra $\mathfrak{u}(n)$ itself appears only after multiplying by $i$ (Unitary group).

Setting

Let $N$ and $d$ be natural numbers with $N \ge 1$. A ring has $N$ sites labelled by $\mathbb{Z}/N\mathbb{Z} = \{0, \dots, N-1\}$, so site $N-1$ is next to site $0$; indices $i + 1$ and $i - 1$ are taken modulo $N$. Each site carries a velocity vector $v_i \in \mathbb{R}^d$, and each link $i \to i+1$ carries a real $d \times d$ link matrix $W_i$. The force on site $i$ is

$$F_i = W_i\, v_{i+1} - W_{i-1}\, v_{i-1},$$

where the second term uses the previous link's matrix $W_{i-1}$. The total power delivered by the coupling is

$$P_W(v) = \sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( W_i\, v_{i+1} - W_{i-1}\, v_{i-1} \bigr).$$

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 $N$), vectors in Fin d → ℝ, and $\cdot$ the dot product ⬝ᵥ. The coupling is passive when $P_W(v) = 0$ for every choice of velocities $v$.

Formalization targets

Goal: passive if and only if every link is symmetric (rings of at least 3 sites)

$$N \ge 3 \;\Longrightarrow\; \Bigl( \forall v,\; P_W(v) = 0 \Bigr) \iff \Bigl( \forall i,\; W_i^{\mathsf T} = W_i \Bigr).$$

This is PassivityRing.passive_iff_symm. It holds for every $d$ and every family of link matrices, with no assumption relating different links.

Milestones

1. M1 (power identity, every $N$). $P_W(v) = \sum_i v_i \cdot \bigl((W_i - W_i^{\mathsf T})\, v_{i+1}\bigr)$.
2. M2 (symmetric links are passive, every $N$). If every $W_i$ is symmetric, then $P_W(v) = 0$ for all $v$.
3. M3 (passive forces symmetric, $N \ge 3$). If $P_W(v) = 0$ for all $v$, then every $W_i$ is symmetric.

Significance

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 $n^2$ 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 $1, 2, 3, 4, 7$. A machine-checked proof covers every $N \ge 3$ and every $d$, makes the role of the hypothesis $N \ge 3$ explicit, and separates what is proved (passivity forces symmetry) from what remains a modelling premise ($J$-compatibility).

Difficulty

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 $N \ge 3$ is necessary, not a convenience:

• $N = 1$: the site is its own neighbour on both sides, so the force is $W_0 v_0 - W_0 v_0 = 0$ and the power vanishes for every $W_0$, symmetric or not.
• $N = 2$: the power reduces to $v_0 \cdot (D - D^{\mathsf T})\, v_1$ with $D = W_0 - W_1$, so it depends only on the difference of the two link matrices. Taking both links equal to the same non-symmetric matrix, for example $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$, gives zero power for all velocities.

Weakening the hypothesis to $2 \le N$, or dropping it, makes the goal false.

Formalization scope

• Sites are Fin N with its wrap-around arithmetic, so $i + 1$ and $i - 1$ go around the ring; [NeZero N] is required for the literal $1$ in Fin N and is implied by $N \ge 3$ in the goal.
• There is one matrix per link, W : Fin N → Matrix (Fin d) (Fin d) ℝ, not a single shared matrix, and no relation between different links is assumed.
• Passivity is quantified over all velocity configurations v : Fin N → (Fin d → ℝ).
• Everything is real (ℝ); symmetry is (W i)ᵀ = W i.
• $d = 0$ is included; there both sides of the goal hold trivially. This is not a trivialization, since the statement is quantified over all $d$.

M1 and M2 hold for every $N \ge 1$ and carry no ring-size hypothesis; M3 and the goal require $N \ge 3$. The development needs only Mathlib's finite sums, dot products, matrix–vector products and Fin arithmetic.

Selected references

• B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
• Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
• Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
• Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

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.2, Section 2 and Section 3.

Motivation

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 $\mathbb{R}^3$ 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 $SO(3,\mathbb{R})$ contains a free group of rank two, while the isometry groups of $\mathbb{R}$ and $\mathbb{R}^2$ 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 $EG$ for the elementary amenable groups, $AG$ for the amenable groups and $NF$ for the groups with no free subgroup of rank two, one has $EG \subseteq AG \subseteq NF$, and both inclusions were asked to be equalities. Both are strict. Ol'shanskii (1980) showed $AG \neq NF$, and Grigorchuk (1985) showed $EG \neq AG$ with a group of intermediate growth. Chou (1980) supplied the structural facts about $EG$ that the separation rests on.

Amenability is now basic vocabulary in geometric group theory, ergodic theory and operator algebras.

Setting

Let $G$ be a discrete group. A measure on $G$, in von Neumann's sense, is a function $\mu$ assigning a value to every subset of $G$ — not merely to a distinguished $\sigma$-algebra — such that

$$\mu(G) = 1, \qquad \mu(A \sqcup B) = \mu(A) + \mu(B), \qquad \mu(gA) = \mu(A)$$

for all $g \in G$ and all disjoint $A, B \subseteq G$. Only finite additivity is required; countable additivity together with invariance is impossible for a countably infinite group. $G$ is amenable if such a $\mu$ exists.

Two reformulations matter. A left-invariant mean is a positive linear functional $m$ on the bounded real functions $\ell^\infty(G)$ with $m(\mathbf{1}) = 1$ and $m({}_g f) = m(f)$, where ${}_g f(h) = f(g^{-1}h)$. And $G$ satisfies the Følner condition if for every finite $A \subseteq G$ and every $\varepsilon > 0$ there is a finite nonempty $F \subseteq G$ with

$$\frac{|aF \,\triangle\, F|}{|F|} \le \varepsilon \qquad \text{for every } a \in A,$$

where $\triangle$ is symmetric difference. In the Cayley graph this says $F$ has small boundary relative to its size.

Against amenability stands paradoxicality. Two subsets $A, B$ of a $G$-set $X$ are $G$-equidecomposable, written $A \sim B$, if $A$ can be cut into finitely many pieces which, after each is moved by a single element of $G$, reassemble to $B$; and $E \subseteq X$ is $G$-paradoxical if it has two disjoint proper subsets each equidecomposable with $E$ itself. A group that is paradoxical under left translation admits no invariant measure.

Formalization targets

Goal — Theorem 3.6

$$G \text{ satisfies the Følner condition} \iff G \text{ is amenable}$$

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.

Supporting equivalences — Theorems 1.15 and 2.7

For a group $G$, these four are equivalent: $G$ is amenable; there is a left-invariant mean on $\ell^\infty(G)$; $G$ is not paradoxical; and $G$ has the invariant extension property.

Closure properties — Proposition 2.2

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 $EG \subseteq AG$.

Significance

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.

Difficulty

The Følner-implies-amenable direction is the easier one, and the natural construction almost works: given a Følner sequence $F_n$, set $\mu(B) = \lim_n |B \cap F_n| / |F_n|$. That limit need not exist. It must be replaced by a limit along a non-principal ultrafilter, or the measure obtained by compactness in $[0,1]^{\mathcal{P}(G)}$.

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 $\ell^1(G)$, 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 $\sigma$-additivity.

Formalization scope

Amenability is IsAmenable G: the existence of $m : \mathcal{P}(G) \to [0,\infty]$ with $m(G) = 1$, finitely additive on disjoint pairs, and invariant under left translation. The codomain is the extended nonnegative reals rather than $[0,1]$, to match the conclusion of Mathlib's IsFoelner.amenable — which at $X = G$ with every set measurable is exactly IsAmenable — so that theorem is directly usable; finite additivity and $m(G) = 1$ force $m(s) \le 1$ anyway, so nothing is added or lost.

Committed conventions. Means live on $\ell^\infty(G)$, realised as lp (fun _ : G => ℝ) ∞ — not on all of $G \to \mathbb{R}$, where invariance and normalisation are already contradictory (proved for $\mathbb{Z}$), so every statement about means would be vacuously unprovable. Normalisation is phrased via constantly-$1$ functions, to avoid depending on the ring structure of $\ell^\infty$. 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 $m(G) = 1$ 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 $\ell^\infty$, 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.

What is left out

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 $SO(3,\mathbb{R})$ 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 $2$-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.

Selected references

• A. Garrido, An introduction to amenable groups, lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013. archived PDF
• S. Banach and A. Tarski, Sur la décomposition des ensembles de points en parties respectivement congruentes, Fund. Math. 6 (1924), 244–277. DOI
• J. von Neumann, Zur allgemeinen Theorie des Maßes, Fund. Math. 13 (1929), 73–116. DOI
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. DOI
• E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. DOI
• I. Namioka, Følner's conditions for amenable semi-groups, Math. Scand. 15 (1964), 18–28 — the source of the argument for the goal theorem. DOI
• J. M. Rosenblatt, Invariant measures and growth conditions, Trans. Amer. Math. Soc. 193 (1974), 33–53 — where supramenability is introduced. DOI
• A. Yu. Ol'shanskii, On the problem of the existence of an invariant mean on a group, Russian Math. Surveys 35 (1980), 180–181 — the paper Grigorchuk credits for $AG \neq NF$. DOI
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407. DOI
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izvestiya 25 (1985), 259. DOI
• S. Wagon, The Banach–Tarski Paradox, Cambridge University Press, 1985. DOI

Motivation

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:

• 2006 — Friston, A free energy principle for the brain (J. Physiol. Paris 100): the bound stated for perception as variational inference on a generative model.
• 2010 — Friston, The free-energy principle: a unified brain theory? (Nat. Rev. Neurosci. 11, 127–138): free energy as an upper bound on surprisal, presented as the core of a unified account.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory (Neural Comput. 29(1), 1–49): the same functional drives policy selection through expected free energy.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): textbook treatment; the posterior-form identity $F = D_{\mathrm{KL}}(Q\,\|\,P(s|o)) - \log P(o)$ as the central equation.
• 2026 — 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.

Setting

Everything is finite, and laws are normalized real mass functions.

A finite law on a finite type $\alpha$ is a function $p : \alpha \to \mathbb{R}$ with $p(x) \ge 0$ for every $x$ and $\sum_x p(x) = 1$. A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row over $\beta$. The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence

$$D_{\mathrm{KL}}(p\,\|\,q) \;=\; \sum_{x} q(x)\cdot \mathrm{klFun}\!\left(\frac{p(x)}{q(x)}\right), \qquad \mathrm{klFun}(x) = x\log x + 1 - x,$$

a totalized real-valued divergence that is finite even at zero-mass atoms (the convention $0 \cdot \log 0 = 0$ via Real.negMulLog) and nonnegative on normalized laws.

A finite generative model for active inference (definition Def_fep_generative_model) over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ consists of: an initial state law $P(s)$; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ and the outcome law $P(o \mid \pi)$. A recognition density is any finite law $Q$ over states — the system's internal estimate. At an outcome $o$ with positive predicted mass, the Bayesian posterior $P(\cdot \mid o, \pi)$ is the exact finite Bayes rule. The outcome surprisal is $-\log P(o \mid \pi)$, and the posterior-form variational free energy of a recognition density $Q$ is

$$F[Q, o, \pi] \;=\; D_{\mathrm{KL}}\big(Q \,\|\, P(\cdot \mid o, \pi)\big) \;-\; \log P(o \mid \pi).$$

Formalization targets

Goal: the variational free-energy bound

For every generative model, every policy $\pi$, every outcome $o$ with $P(o\mid\pi) > 0$, and every recognition density $Q$:

$$-\log P(o \mid \pi) \;\le\; F[Q, o, \pi].$$

The recognition density $Q$ is universally quantified — the bound holds for whatever state estimate the system happens to carry.

Exactness, uniqueness, and the ELBO form

Three companions pin down the equality case, ordered weakest to strongest alongside the milestone list:

• Exactness — the Bayesian posterior attains the bound:

$$F\big[P(\cdot \mid o, \pi),\, o,\, \pi\big] = -\log P(o \mid \pi).$$

• Uniqueness — equality characterizes the posterior, with no full-support assumption:

$$F[Q, o, \pi] = -\log P(o \mid \pi) \iff Q = P(\cdot \mid o, \pi).$$

• ELBO form — negating both sides:

$$-F[Q, o, \pi] \;\le\; \log P(o \mid \pi).$$

Measure-theoretic core

Independently of the finite model, in Mathlib's nonnegative extended reals $\mathbb{R}_{\ge0} \cup \{\infty\}$, with $q$, $p$ measures on any measurable space and $s \in \mathbb{R}_{\ge0} \cup \{\infty\}$:

$$s \;\le\; s + D_{\mathrm{KL}}(q \,\|\, p),$$

the unconditional shape of the bound (topic fep-002 of the source catalogue), with the divergence taken as $\infty$ when the log-likelihood ratio is not integrable.

Significance

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.

Difficulty

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:

• The positivity premise $P(o \mid \pi) > 0$ is not decoration: the Bayesian posterior is defined only where the evidence has positive mass, and hiding that in a totalized division would change the statement.
• The uniqueness characterization is not a formality: at zero-mass reference atoms the logarithmic cross-entropy identity degenerates, and the proof needs the normalization lemma $D_{\mathrm{KL}}(p\,\|\,q) = 0 \leftrightarrow p = q$, which forces the recognition law's mass to zero wherever the posterior's is zero. A solver who proves the bound but states equality with a full-support hypothesis has proved something different from the source.
• The measure-theoretic core is deliberately unconditional; adding finiteness side conditions to it would weaken the source's point that $\mathbb{R}_{\ge0} \cup \{\infty\}$ absorbs the degenerate cases.

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 $Q$.

Formalization scope

Committed conventions of this mission's Lean development:

• All model carriers are finite types (Fintype); laws are $\mathbb{R}$-valued normalized mass functions; kernels are normalized rows. No measure-theoretic machinery below the finite substrate except for the measure-theoretic core milestone.
• KL is the totalized real-valued finite divergence $D_{\mathrm{KL}}(p\,\|\,q) = \sum_x q(x)\cdot \mathrm{klFun}(p(x)/q(x))$; entropy uses Real.negMulLog, so $0 \cdot \log 0 = 0$ exactly, not by exception-handling.
• The posterior is the exact finite Bayes rule FiniteKernel.posterior, taken at the explicit hypothesis $0 < P(o \mid \pi)$.
• One mission-wide namespace 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.
• The measure-theoretic core uses Mathlib's InformationTheory.klDiv in ℝ≥0∞ with no finiteness hypotheses.
• Contributions welcome: alternative measure-theoretic renderings of the core bound, the Gaussian instantiation of the same identity, and ports of the source repository's subsequent rows (Bayesian model reduction, expected free energy) onto these definitions.

Selected references

• K. Friston, A free energy principle for the brain, Journal of Physiology (Paris) 100 (2006) 70–87. https://doi.org/10.1016/j.jphysparis.2006.10.001
• K. Friston, The free-energy principle: a unified brain theory?, Nature Reviews Neuroscience 11 (2010) 127–138. https://doi.org/10.1038/nrn2787
• K. Friston, T. FitzGerald, F. Rigoli, P. Schwartenbeck, G. Pezzulo, Active inference: a process theory, Neural Computation 29 (2017) 1–49. https://doi.org/10.1162/neco_a_00912
• T. Parr, G. Pezzulo, K. J. Friston, Active Inference: The Free Energy Principle in Mind, Brain, and Behavior, MIT Press (2022). https://mitpress.mit.edu/9780262045354/active-inference/
• D. A. Friedman, fep_formal: Towards Lean 4 Formalization of the Free Energy Principle (v1.2.0), Active Inference Institute (2026), the formal source of truth for this mission. https://github.com/ActiveInferenceInstitute/fep_formal
• D. A. Friedman, Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, Active Inference Journal (2026). https://doi.org/10.5281/zenodo.19699233

Why control variates matter in federated optimization

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.

Setting: local updates and sampled clients

There are $N\ge1$ clients, with differentiable objectives $f_i:\mathbb R^d\to\mathbb R$. The global objective is $f(x)=N^{-1}\sum_i f_i(x)$. Every client gradient is $\beta$-Lipschitz, where $\beta>0$. A stochastic gradient query is conditionally unbiased and has conditional squared-error expectation at most $\sigma^2$, with $\sigma\ge0$. 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 $T\ge1$ rounds selects a uniform subset $A_r$ of $S$ clients, where $1\le S\le N$. Each selected client takes $K\ge1$ local steps. Let $x^r$ be the server model, $c_i^r$ its stored client control variates, and $c^r=N^{-1}\sum_i c_i^r$. With constant local and global step sizes $\eta_l>0$ and $\eta_g\ge1$, a client starts at $y_{i,0}^r=x^r$ and uses

$$y_{i,k+1}^r=y_{i,k}^r-\eta_l\bigl(g_{i,k}^r-c_i^r+c^r\bigr), \qquad x^{r+1}=x^r+\frac{\eta_g}{S}\sum_{i\in A_r}(y_{i,K}^r-x^r).$$

Option II replaces a participating client's control with $K^{-1}\sum_{k=0}^{K-1}g_{i,k}^r$ and retains every other control. These are Algorithm 1, PDF p. 4, and Appendix E, equations (18)–(21), PDF pp. 25–26. Write $h=K\eta_l\eta_g$ for the effective step size.

Formalization targets

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 $x^\star$,

$$\frac1N\sum_i\|\nabla f_i(x)-\nabla f_i(x^\star)\|^2 \le2\beta\bigl(f(x)-f(x^\star)\bigr).$$

This is Appendix B.1, equation (9), PDF p. 14. PerturbedStrongConvexity states, for each $\mu$-strongly convex client and $\mu\ge0$,

$$\langle\nabla f_i(x),z-y\rangle\ge f_i(z)-f_i(y) +\frac\mu4\|y-z\|^2-\beta\|z-x\|^2,$$

as in Appendix C, Lemma 5, PDF p. 17.

ConvexFiniteRoundConvergence allows arbitrary deterministic initial controls $c_i^0$. Assume all clients are $\mu$-strongly convex with $\mu\ge0$, including ordinary convexity when $\mu=0$, and fix a minimizer $x^\star$ of $f$. Define

$$C_0=\frac1N\sum_i\|c_i^0-\nabla f_i(x^\star)\|^2, \qquad V_0=\|x^0-x^\star\|^2+\frac{9Nh^2}{S}C_0,$$ $$q=1-\frac{\mu h}{2},\qquad w_r=q^{-(r+1)},\qquad W_T=\sum_{r=0}^{T-1}w_r.$$

For $h\le1/(81\beta)$ and $\mu h\le S/(15N)$, the target is

$$\frac1{W_T}\sum_{r=0}^{T-1}w_r\, \mathbb E\bigl[f(x^r)-f(x^\star)\bigr] \le\frac{V_0}{hW_T} +\frac{12h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

This is a finite-round formulation of Appendix E.1, Lemma 15, PDF p. 30; its $\mu=0$ case is the first bound on PDF p. 31.

NonconvexFiniteRoundConvergence assumes a lower bound $f_\mathrm{lower}$ for $f$ and initializes every client control with $K$ fresh gradients at $x^0$. Put $F_0=f(x^0)-f_\mathrm{lower}$. For $h\le(S/N)^{2/3}/(24\beta)$, establish

$$\frac1T\sum_{r=0}^{T-1}\mathbb E\|\nabla f(x^r)\|^2 \le\frac{14F_0}{hT} +\frac{70\beta h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).$$

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 $T$ optimization rounds.

What the result establishes

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.

Where the difficulty lies

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.

Formalization scope

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-$S$ subset is sampled, as permitted by the paragraph after equation (22), PDF p. 26.

The conventions include $S=N$, $K=1$, zero noise, and $\mu=0$. The output indices are precisely $0,\ldots,T-1$. 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.

Selected references

• Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020, PMLR 119:5132–5143; arXiv:1910.06378v4, revised 2021. Primary scope: Theorem III, PDF p. 5; A3–A5 and (9), p. 14; Lemma 5, p. 17; Appendix E, pp. 25–35, especially Lemmas 15 and 19.

Reversible Binary 2D Cellular Automata: Disproof of $R = 18$ and Lower Bound $R \ge 33,076,358$

Problem Statement & Context

A two-dimensional binary cellular automaton (CA) on the infinite grid $\mathbb{Z}^2$ with the standard $3 \times 3$ Moore neighborhood $M = \{-1,0,1\}^2$ updates configurations $c : \mathbb{Z}^2 \to \{0,1\}$ via a local rule $f : \{0,1\}^M \to \{0,1\}$ according to:

$$F_f(c)(z) = f\Big(\big(c(z + u)\big)_{u \in M}\Big)$$

A local rule $f$ is reversible (or bijective) if its global map $F_f$ is a bijection of the configuration space $\{0,1\}^{\mathbb{Z}^2}$.

Let $R$ denote the exact number of reversible binary local rules on the $3 \times 3$ Moore neighborhood. A longstanding open conjecture asserted that $R = 18$, corresponding solely to the 18 trivial single-cell shifts and complemented shifts:

$$f(c) = c(z + u) \quad \text{or} \quad f(c) = 1 - c(z + u) \quad (u \in M)$$

In this mission, we formally disprove $R = 18$ by constructing an explicit non-trivial conserved-landscape rule $f_\star$ whose global map $F_{f_\star}$ is an involution on $\mathbb{Z}^2$, proving $19 \le R$. We further extend this result to establish $R \ge 33,076,358$.

---

Ladder of Proven Bounds

Bound Level	Proven Bound	Description / Mathematical Mechanism
$\mathbf{L_0}$	$R \ge 18$	Trivial single-cell shifts and complemented shifts ($2 \times 9 = 18$).
$\mathbf{L_1}$	$R \ge 19$	Disproof of $R = 18$ via explicit non-trivial conserved-landscape rule $f_\star$.
$\mathbf{L_2}$	$R \ge 33,070,982$	Conserved-landscape marker rule family ($24,576$ centered rules).
$\mathbf{L_3}$	$R \ge 33,076,358$	Incorporation of $5,376$ off-centre marker rules reading center cell $x_0$.
Symmetry	$R_{\text{rot90}} = 74$	Exactly 74 rules invariant under $90^\circ$ spatial rotations.
Torus	$	\mathcal{R}_{2,3}
Upper Limit	$R \le 2^{511}$	Derived from constant divergence condition $f(\mathbf{0}) \ne f(\mathbf{1})$.

---

Key Milestone Theorems

1. Theorem 1 (Trivial Rule Reversibility): All 18 single-cell shift and negated-shift rules are bijective global maps.
2. Theorem 2 (Conserved-Landscape Involution $f_\star$): The rule $f_\star$ complements a cell iff its W and SE neighbors are $1$ and the other six are $0$. $F_{f_\star} \circ F_{f_\star} = \text{id}$.
3. Theorem 3 (Non-Triviality & $19 \le R$): $f_\star$ differs from every trivial rule, establishing $19 \le R$ and disproving $R = 18$.
4. Theorem 4 (Constant Divergence Condition): Every reversible rule satisfies $f(\mathbf{0}) \ne f(\mathbf{1})$.

Why local training needs a convergence guarantee

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.

Setting: full participation with uniform weights

There are $M\ge1$ clients and a parameter vector in $\mathbb R^d$. Client $i$ has a differentiable convex objective $F_i$. The global objective is $F(x)=M^{-1}\sum_{i=1}^M F_i(x)$. Every local gradient is $L$-Lipschitz for the same $L>0$. Fix a global minimizer $x^\star$ of $F$ and a deterministic initial model $x_0$, and write $D=\|x_0-x^\star\|$.

Every client participates in every round. Each of $T\ge1$ rounds consists of $\tau\ge1$ local steps with constant learning rate $\eta$. If $x_i^{t,k}$ is client $i$'s state after $k$ local steps of round $t$, its next state is $x_i^{t,k+1}=x_i^{t,k}-\eta g_i^{t,k}$. At the next round all clients restart from the average of the preceding round's terminal states. The shadow iterate is $\bar x^{t,k}=M^{-1}\sum_i x_i^{t,k}$; it is defined even at local steps where clients do not communicate.

On a probability space $(\Omega,\mathcal A,\mathbb P)$, the history before a step contains all past oracle draws. The stochastic gradients are conditionally unbiased, their conditional squared errors have expectation at most $\sigma^2$, and the different clients' current gradients are conditionally independent. The heterogeneity bound is $\|\nabla F_i(x)-\nabla F(x)\|\le\zeta$ for every client and every point, where $\sigma,\zeta\ge0$. 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.

Formalization targets

The principal goal is Theorem 1, equation (15). For $0<\eta\le1/(4L)$, establish

$$\mathbb E\!\left[\frac1{\tau T}\sum_{t=0}^{T-1}\sum_{k=1}^{\tau} \bigl(F(\bar x^{t,k})-F(x^\star)\bigr)\right] \le \frac{D^2}{2\eta\tau T}+\frac{\eta\sigma^2}{M} +4\tau\eta^2L\sigma^2+18\tau^2\eta^2L\zeta^2.$$

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 $18\tau^2\eta^2\zeta^2+4\tau\eta^2\sigma^2$. 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 $D,\sigma,\zeta>0$. With

$$\eta=\min\left\{\frac1{4L}, \frac{\sqrt M D}{\sqrt\tau\sqrt T\sigma}, \frac{D^{2/3}}{\tau^{2/3}T^{1/3}L^{1/3}\sigma^{2/3}}, \frac{D^{2/3}}{\tau T^{1/3}L^{1/3}\zeta^{2/3}}\right\},$$

the same expected loss is at most

$$\frac{2LD^2}{\tau T}+\frac{2\sigma D}{\sqrt{M\tau T}} +\frac{5L^{1/3}\sigma^{2/3}D^{4/3}}{\tau^{1/3}T^{2/3}} +\frac{19L^{1/3}\zeta^{2/3}D^{4/3}}{T^{2/3}}.$$

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.

What this establishes

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.

Where the difficulty lies

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 $1/M$ noise improvement using independent client sampling. Ignoring the sampling relationship can invalidate the advertised bound even for scalar quadratic objectives.

Formalization scope

The model uses finite-dimensional real Euclidean space, including the harmless zero-dimensional case, and a standard Borel probability space. A filtration indexed by $t\tau+k$ 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.

Selected references

• Jianyu Wang et al., A Field Guide to Federated Optimization, 2021, arXiv:2107.06917v1, Section 6.1.1–6.1.2, PDF pp. 40–41; Appendix D, PDF pp. 86–88.
• H. Brendan McMahan et al., Communication-Efficient Learning of Deep Networks from Decentralized Data, AISTATS 2017, arXiv:1602.05629, the FedAvg algorithm cited by the field guide. This is historical context, not an additional target.

Motivation

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 $\alpha$, the map

$$n\longmapsto e^{i n\alpha}$$

is simultaneously a group character, a faithful encoding of $\mathbb Z$, and a countable dense orbit in the unit circle. Its complex values also form a linearly independent family over the algebraic complex numbers $\overline{\mathbb Q}$.

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.

Setting

Write $S^1\subset\mathbb C$ for the complex unit circle. For a real angle $\alpha$ and integer $n$, define

$$\operatorname{phase}_\alpha(n)=e^{i n\alpha}\in S^1.$$

This is an additive-to-multiplicative character: phase at $0$ is $1$, and phase at $m+n$ is the product of the phases at $m$ and $n$.

A based Circle loop $\gamma$ has a canonical integer $\operatorname{wind}(\gamma)$, obtained from the endpoint of its zero-based lift through the exponential cover. Its real phase readout is $\operatorname{phase}_\alpha(\operatorname{wind}(\gamma))$.

The orbit is dense when every nonempty open subset of $S^1$ contains some $\operatorname{phase}_\alpha(n)$. 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.

Formalization targets

Irrational rotation criterion

For every real $\alpha$,

$$\operatorname{DenseRange}(n\mapsto e^{i n\alpha}) \quad\Longleftrightarrow\quad \frac{\alpha}{2\pi}\notin\mathbb Q.$$

The proof identifies the phase orbit with integer multiples in $\mathbb R/(2\pi\mathbb Z)$ and transports Mathlib's irrational-rotation theorem through the standard homeomorphism with the complex unit circle.

Algebraic angles are nonresonant

If $\alpha\in\mathbb R$ is nonzero and algebraic over $\mathbb Q$, then $\alpha/(2\pi)$ is irrational. Otherwise $\pi$ would be algebraic, contradicting the proved transcendence of $\pi$. Consequently the real phase character has dense range.

Faithfulness and arithmetic rigidity

For the same nonzero algebraic $\alpha$, the character is injective and

$$\bigl(e^{i n\alpha}\bigr)_{n\in\mathbb Z}$$

is linearly independent over $\overline{\mathbb Q}$. The first conclusion says no two winding integers alias. The second says no nontrivial finite algebraic-coefficient linear relation exists among the phase values.

Actual Circle-loop consumer

For based Circle loops $\gamma$ and $\delta$,

$$e^{i\alpha\operatorname{wind}(\gamma)} =e^{i\alpha\operatorname{wind}(\delta)} \quad\Longleftrightarrow\quad \operatorname{wind}(\gamma)=\operatorname{wind}(\delta).$$

This consumes the canonical covering-space winding rather than an arbitrary externally supplied integer.

Resonance control

At the full-turn angle $\alpha=2\pi$, every integer phase is $1$, so the character is not injective. This negative control is outside the algebraic-angle regime because $\pi$ is transcendental. It records exactly why a nonresonance hypothesis is load-bearing.

Significance

The capstone exhibits one object with three complementary properties:

1. topological discreteness — values are indexed by integer winding;
2. dynamical density — the countable orbit visits every Circle neighborhood;
3. arithmetic rigidity — distinct values are faithful and linearly independent over $\overline{\mathbb Q}$.

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.

Difficulty

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 $2\pi$ and transport through the AddCircle–Circle homeomorphism in both directions. Linear independence requires the completed Lindemann–Weierstrass theorem, not merely irrationality or transcendence of $\pi$.

The coercion bridge between the real Circle phase and the complex exponential character is also orientation-sensitive: the formal phase is exactly $\exp(i n\alpha)$. 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.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Circle density is stated only for real $\alpha$. The arithmetic conclusions require both IsAlgebraic ℚ α and $\alpha\ne0$.

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.

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.
• Lean mathematical library, Dense subgroups of the additive circle. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.html
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

Motivation

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 $y^2 = x^3 + f x + g$, each potentially good additive Kodaira type has a fixed discriminant vanishing order $\operatorname{ord}\Delta$ — the entries of Tate's table — and the exceptional types $\mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$ have Dynkin types $E_6, E_7, E_8$ (the gauge algebra in the split/geometric setting; a nonsplit $\mathrm{IV}^*$ instead gives $F_4$). On an elliptically fibered K3 the global discriminant divisor has degree $24 = e(\mathrm{K3}) = 12\,\chi(\mathcal{O}_{\mathrm{K3}})$ (the topological Euler characteristic; the formalized affine statement is $\deg\Delta \le 24$), 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.

Setting

Fix a field $k$; work with $y^2 = x^3 + f x + g$, $f, g \in k[X]$, discriminant $\Delta = 4f^3 + 27g^2$ (up to the unit $-16$). Write $\operatorname{ord}_{t_0}(p)$ for the multiplicity of $t_0$ as a root of $p$; for the $\mathrm{I}_0^*$ row, whenever $(X - t_0)^2 \mid f$ and $(X - t_0)^3 \mid g$, write $f = (X - t_0)^2 F$ and $g = (X - t_0)^3 G$ and set the reduced coefficients $c_2 = F(t_0)$, $d_3 = G(t_0)$ (equivalently the order-$2$ and order-$3$ Taylor coefficients of $f$ and $g$ at $t_0$). The K3 degree data is $\deg f \le 8$, $\deg g \le 12$, $\Delta \ne 0$. The seven potentially good additive types ($\mathrm{II}, \mathrm{III}, \mathrm{IV}, \mathrm{I}_0^*, \mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$) are encoded by their $(\operatorname{ord} f, \operatorname{ord} g)$ signatures (HasKodaira), with lower bounds written as divisibility $(X - t_0)^n \mid \cdot$ and exact orders as rootMultiplicity.

Formalization targets

Goal — the 7-brane budget

For $k$ of characteristic zero and $(f,g)$ satisfying the K3 degree data, any finite set $S$ of base points, and any assignment $\tau$ of a Kodaira type each point genuinely carries,

$$\sum_{t \in S} \operatorname{discOrder}(\tau(t)) \le 24.$$

Milestones — the Tate table (each entry: fibre signature $\Rightarrow$ exact $\operatorname{ord}\Delta$)

1. $\deg\Delta \le 24$ under $\deg f \le 8$, $\deg g \le 12$.
2. Local orders are bounded by the degree: $\sum_{t \in S}\operatorname{ord}_t\Delta \le \deg\Delta$ ($\Delta \ne 0$, $S$ finite).
3. Type $\mathrm{II}$: $(\operatorname{ord} f \ge 1, \operatorname{ord} g = 1) \Rightarrow \operatorname{ord}\Delta = 2$.
4. Type $\mathrm{III}$: $(\operatorname{ord} f = 1, \operatorname{ord} g \ge 2) \Rightarrow \operatorname{ord}\Delta = 3$.
5. Type $\mathrm{IV}$: $(\operatorname{ord} f \ge 2, \operatorname{ord} g = 2) \Rightarrow \operatorname{ord}\Delta = 4$.
6. Type $\mathrm{I}_0^*$ (full row): $(\operatorname{ord} f \ge 2, \operatorname{ord} g \ge 3,\ 4c_2^3+27d_3^2 \ne 0) \Rightarrow \operatorname{ord}\Delta = 6$.
7. Type $\mathrm{IV}^*$ ($E_6$): $(\operatorname{ord} f \ge 3, \operatorname{ord} g = 4) \Rightarrow \operatorname{ord}\Delta = 8$.
8. Type $\mathrm{III}^*$ ($E_7$): $(\operatorname{ord} f = 3, \operatorname{ord} g \ge 5) \Rightarrow \operatorname{ord}\Delta = 9$.
9. Type $\mathrm{II}^*$ ($E_8$): $(\operatorname{ord} f \ge 4, \operatorname{ord} g = 5) \Rightarrow \operatorname{ord}\Delta = 10$.

Corollaries (also milestones)

10. Exceptional-fibre budget: $8 N_{\mathrm{IV}^*} + 9 N_{\mathrm{III}^*} + 10 N_{\mathrm{II}^*} \le 24$ (pairwise-disjoint IV*/III*/II* loci).
11. At most three type $\mathrm{IV}^*$ ($E_6$) points ($4 \times 8 = 32 > 24$).
12. At most two type $\mathrm{III}^*$ ($E_7$) points ($3 \times 9 = 27 > 24$).
13. At most two type $\mathrm{II}^*$ ($E_8$) points ($3 \times 10 = 30 > 24$).
14. Residual budget: for any finite set $E$ of $\mathrm{II}^*$ ($E_8$) points and any finite $S$ disjoint from $E$, $10\,|E| + \sum_{t \in S}\operatorname{ord}_t\Delta \le 24$ (two $E_8$ points leave at most $4$; note $S$ need not be classified by the seven types).

Significance

Every entry of the table is load-bearing for the budget: the goal converts each $\operatorname{discOrder}(\tau(t))$ into the true local order $\operatorname{ord}_t\Delta$ (milestones 3--9), then bounds the sum by $\deg\Delta \le 24$ (milestones 1--2). Corollaries recover the physics: at most two $\mathrm{II}^*$, at most two $\mathrm{III}^*$, and at most three $\mathrm{IV}^*$ fibres (the $E_8, E_7, E_6$ loci in the split/geometric setting -- a nonsplit $\mathrm{IV}^*$ gives $F_4$); the exceptional budget $8 N_{\mathrm{IV}^*} + 9 N_{\mathrm{III}^*} + 10 N_{\mathrm{II}^*} \le 24$; and the residual budget $10\,\#E + \sum_{t \in S} \operatorname{ord}_t\Delta \le 24$, so two $\mathrm{II}^*$ points leave at most $4$ 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.

Difficulty

The six "clean" rows ($\mathrm{II}, \mathrm{III}, \mathrm{IV}, \mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$) sit at unequal orders $3\operatorname{ord} f \ne 2\operatorname{ord} g$, so the order of the sum is the smaller summand's order — an order-of-a-sum computation, valid in characteristic zero where $4, 27$ are units. The genuinely hard row is $\mathrm{I}_0^*$, which needs finer data than the raw orders. Writing $f = (X - t_0)^2 F$, $g = (X - t_0)^3 G$ with $c_2 = F(t_0)$, $d_3 = G(t_0)$, both terms of $\Delta = 4f^3 + 27g^2$ have order at least $6$, and the coefficient of $(X - t_0)^6$ is $4c_2^3 + 27 d_3^2$; its nonvanishing gives $\operatorname{ord}_{t_0}\Delta = 6$. This covers the three branches $(\operatorname{ord} f, \operatorname{ord} g) = (2,3),\ (2, {\ge} 4),\ ({\ge} 3, 3)$ uniformly — only in the $(2,3)$ branch, where $3\operatorname{ord} f = 2\operatorname{ord} g = 6$, can two nonzero order-$6$ contributions cancel. The nonvanishing is the distinct-roots criterion for the reduced cubic $x^3 + c_2 x + d_3$ and, under $\operatorname{ord} f \ge 2$ and $\operatorname{ord} g \ge 3$, characterizes the $\mathrm{I}_0^*$ row; when it vanishes, further valuation data distinguish the $\mathrm{I}_n^*$ series, the higher potentially good types, and nonminimal cases. The budget itself then needs the local-to-global degree bound (milestones 1--2).

Formalization scope

Over a characteristic-zero field $k$ (intended $k = \mathbb{C}$), Mathlib-native Polynomial API only (natDegree, rootMultiplicity, roots, taylor). Lower-bound orders use divisibility $(X - t_0)^n \mid \cdot$, which faithfully includes the $f = 0$ / $g = 0$ ($\operatorname{ord} = +\infty$) 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 $\operatorname{ord} f$, $\operatorname{ord} g$ lies below the non-minimal threshold $\operatorname{ord} f \ge 4 \wedge \operatorname{ord} g \ge 6$). The potentially multiplicative $\mathrm{I}_n$ and $\mathrm{I}_n^*$ series are excluded by design (their discriminant orders form unbounded families, not fixed by $(\operatorname{ord} f, \operatorname{ord} g)$). The budget goal is an upper bound over the fibres one classifies — it assumes a valid type assignment on $S$ but neither constructs it nor proves the existence and uniqueness of the complete Kodaira classification, and $S$ need not exhaust the singular locus. A full exhaustive classification, the $\mathrm{I}_n^*$ series, and the literal $\mathbb{P}^1$ 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 $4, 27 \ne 0$ (characteristic $\ne 2, 3$). Over a non-closed field the classification counts $k$-rational affine points; base-change to $\bar{k}$ recovers the geometric statement. Counts are over the affine chart $\mathbb{A}^1 \subset \mathbb{P}^1$.

Selected references

• J. Tate, Algorithm for determining the type of a singular fiber in an elliptic pencil, in Modular Functions of One Variable IV, LNM 476 (1975), 33--52.
• M. Schuett, T. Shioda, Elliptic Surfaces, Adv. Stud. Pure Math. 60 (2010), 51--160. https://arxiv.org/abs/0907.0298
• T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854 (2018). https://arxiv.org/abs/1806.01854