Group Theory

Motivation

A braid on $n$ strands is the everyday object it sounds like: $n$ strings hanging between two horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned this picture into algebra in 1925 by showing that braids form a group under concatenation and that this group has a finite presentation with $n-1$ generators. The braid groups sit at the crossroads of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free and orderable), and of representation theory and mathematical physics through the Burau, Lawrence– Krammer and Temperley–Lieb representations.

This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander Andrey Gomes Tarcha's Um Estudo Introdutório da Teoria de Tranças (UNESP, Rio Claro), whose capstone is Teorema 3.15: the braid group on $n$ strands admits Artin's presentation. The dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9), shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two structural properties: the full twist is central (Proposição 3.16) and $B_m$ embeds in $B_n$ for $m \le n$ (Proposição 3.17).

Setting

Work in the plane $E^2 = \mathbb{C}$. The ordered configuration space

$$F_{0,n}E^2 = \{(z_1,\dots,z_n) \in \mathbb{C}^n : z_k \neq z_l \text{ for } k \neq l\}$$

carries the subspace topology of $\mathbb{C}^n$, and the symmetric group $\Sigma_n$ acts on it by permuting coordinates. The unordered configuration space $B_{0,n}E^2 = F_{0,n}E^2/\Sigma_n$ carries the quotient topology; its points are the $n$-element subsets of the plane. The base configuration is $(1,2,\dots,n)$, and $*$ denotes its class in $B_{0,n}E^2$. The geometric braid group is

$$\pi_1\bigl(B_{0,n}E^2, *\bigr),$$

a loop of $n$-point configurations being exactly a geometric braid, and homotopy of loops being exactly the equivalence by elementary moves used in the dissertation.

The elementary half-twist $\sigma_{i+1}$, for $0 \le i \le n-2$, is the loop that rotates the two base points $i+1$ and $i+2$ by the angle $\pi$ about their midpoint $i + \tfrac32$, leaving the other $n-2$ points fixed:

$$t \;\longmapsto\; \Bigl\{\, i+\tfrac32 \pm \tfrac12 e^{\pi i t} \,\Bigr\} \;\cup\; \{\,k+1 : k \neq i,\, i+1 \,\}, \qquad t \in [0,1].$$

It returns to the base configuration at $t = 1$ with the two moving points interchanged, so it is a loop in $B_{0,n}E^2$ and defines a class in $\pi_1(B_{0,n}E^2,*)$.

The abstract braid group $B_n$ is the group presented by generators $\sigma_1,\dots,\sigma_{n-1}$ subject to

$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$

Formalization targets

Goal — Teorema 3.15, with the isomorphism pinned on generators

$$\exists\, \varphi : B_n \;\xrightarrow{\ \sim\ }\; \pi_1\bigl(B_{0,n}E^2,*\bigr), \qquad \varphi(\sigma_{i+1}) = \bigl[\text{half-twist}_i\bigr] \ \ (0 \le i \le n-2).$$

This is the statement the dissertation actually proves: the map $\varphi$ of its proof is defined on generators by $\varphi(x_i) = [\sigma_i]$, and the work consists in showing that it is a well-defined homomorphism which is surjective and injective. Asking only for an abstract isomorphism would leave the generators unconstrained; naming their images is what makes the presentation usable downstream.

Milestones

$$\langle\,[\text{half-twist}_i]\,\rangle = \pi_1\bigl(B_{0,n}E^2,*\bigr) \qquad \text{(Teorema 3.11)}$$ $$[\text{half-twist}_i][\text{half-twist}_j] = [\text{half-twist}_j][\text{half-twist}_i]\ (|i-j|\ge 2), \qquad [\text{ht}_i][\text{ht}_{i+1}][\text{ht}_i] = [\text{ht}_{i+1}][\text{ht}_i][\text{ht}_{i+1}]$$ $$\forall b \in B_2,\ \exists m \in \mathbb{Z},\ b = \sigma_1^m \qquad \text{(Proposição 3.13)}$$ $$\forall b \in B_3,\ b = \sigma_1^{a_1}\sigma_2^{b_1}\cdots\sigma_1^{a_m}\sigma_2^{b_m} \qquad \text{(Proposição 3.14)}$$ $$(\sigma_1\sigma_2\cdots\sigma_{n-1})^n \in Z(B_n) \qquad \text{(Proposição 3.16)}$$ $$B_m \hookrightarrow B_n \ \ (m \le n) \qquad \text{(Proposição 3.17)}$$

Significance

Artin's presentation is what makes the braid groups computable: the word problem, the Burau and Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form all start from generators and relations, while the topological side supplies the meaning of those generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute with a given geometric braid; the version stated here transports each half-twist loop to a generator word, which is what downstream work needs.

On the formalization side, the geometric model (configuration spaces and their fundamental groups) and the algebraic model (a presented group) are already available on the platform in this environment, and the abstract form of Artin's theorem is already stated there as an open problem. What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in $B_{0,n}E^2$ — this definition is proved sorry-free here, including the injectivity of the moving configuration at every time and the continuity of the path; the sharpened goal that fixes the isomorphism on generators; and the dissertation's supporting results, none of which is currently on the platform. None of the milestones or the goal has a machine-checked proof yet.

Difficulty

Surjectivity of $\varphi$ — every braid is a product of half-twists — is a compactness-and-general- position argument in the dissertation: cut the braid into finitely many slabs in which a single crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since "general position" is not available for free: a loop of configurations must be subdivided and each piece pushed to a standard crossing.

Injectivity is harder and is the step where a naive approach fails. It is not enough to check that the relations hold; one has to know that they are all the relations, i.e. that a word whose braid is null-homotopic is a consequence of the braid relations. The dissertation follows the classical route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with an induction on $n$; its inductive step needs the exact sequence of the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$, which is itself substantial work.

Formalization scope

The plane is $\mathbb{C}$; configurations are injective tuples indexed by Fin n; the unordered configuration space is the quotient by the coordinate-permutation action with the quotient topology; the base configuration is $(1,2,\dots,n)$ (not $(0,1,\dots,n-1)$). Braid generators are indexed by Fin (n-1), the index $i$ standing for the book generator $\sigma_{i+1}$; truncated natural subtraction means the degenerate values $n = 0, 1$ give the trivial group, and the statements are asserted for all $n$ including those cases. The abstract braid group is the presented group on Fin (n-1) modulo the normal closure of the commutation and braid relators.

The half-twist rotates counterclockwise. The mirror symmetry $z \mapsto \bar z$ fixes the base configuration and exchanges the two orientations, so the goal statement does not depend on this choice; a solver may use either convention internally.

The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the generators are the prescribed classes of explicit loops, so neither the identity on a presented group nor an abstract counting argument suffices.

Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the pure braid group as the kernel of the map to $\Sigma_n$, the exponent-sum homomorphism, and torsion-freeness of $B_n$. The half-twist definition published with this mission is reusable for any further work on braids in this environment.

Selected references

• Alexsander Andrey Gomes Tarcha, Um Estudo Introdutório da Teoria de Tranças, master's dissertation, UNESP Rio Claro, 2023. https://repositorio.unesp.br/items/9d2ffbf0-8bd2-4ec7-9e45-e2cee8a1b202
• Emil Artin, Theorie der Zöpfe, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
• Joan S. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
• Edward Fadell and Lee Neuwirth, Configuration spaces, Mathematica Scandinavica 10 (1962), 111–118. https://doi.org/10.7146/math.scand.a-10517

Motivation

The braid group is one of the places where group theory, low-dimensional topology and knot theory meet. Artin introduced it in 1925 (E. Artin, Theorie der Zöpfe, Abh. Math. Sem. Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard equipment in the study of links (closed braids and Markov's theorem), of mapping class groups of punctured surfaces, and of configuration spaces. Birman's Braids, Links, and Mapping Class Groups (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical reference that develops all three subjects from the braid group outwards, and its Chapter 1 is the foundation on which the rest of the book rests.

The chapter's structure is itself the reason to formalize it first: everything later in the book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the mapping class group of the punctured sphere — is phrased in terms of the group $\pi_1 B_{0,n}E^2$ and of the presentation established here. A mission that fixes faithful Lean definitions of the configuration spaces and of the abstract braid group therefore fixes the vocabulary for the whole series.

Timeline of the results collected here: Artin (1925) gave the presentation and the characterization of braid automorphisms of a free group; Chow (1948) determined the centre; Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk (1962) used them to give the proof of the presentation reproduced by Birman.

Setting

Write $E^2$ for the Euclidean plane, identified throughout with the complex numbers $\mathbb{C}$. For $n \ge 0$ let

$$F_{0,n}E^2 = \{\,(z_1,\dots,z_n) \in \mathbb{C}^n : z_i \neq z_j \text{ for } i \neq j\,\}$$

be the ordered configuration space of $n$ points in the plane, topologized as a subspace of $\mathbb{C}^n$. The symmetric group $\Sigma_n$ acts on it by permuting coordinates; the quotient

$$B_{0,n}E^2 = F_{0,n}E^2 / \Sigma_n,$$

with the quotient topology, is the unordered configuration space. A point of $B_{0,n}E^2$ is an unordered set of $n$ distinct points of the plane. The base configuration is $\bar z^{\,0} = (1,2,\dots,n)$, and all fundamental groups below are taken at $\bar z^{\,0}$ or at its image.

The braid group of the plane is $\pi_1 B_{0,n}E^2$: a loop is a motion of $n$ points of the plane returning to the same set of points, and homotopy classes of such motions compose as braids. The pure braid group is $P_n = \pi_1 F_{0,n}E^2$, the subgroup of motions returning each point to its own starting position.

Separately, let $B_n$ denote the abstract group given by generators $\sigma_1,\dots,\sigma_{n-1}$ subject to

$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$

These are equations (1-1) and (1-2) of the book (p. 11). Geometrically $\sigma_i$ interchanges the $i$-th and $(i+1)$-st points along a semicircle.

Formalization targets

Goal — Theorem 1.8 (Artin, 1925; Birman p. 18)

$$B_n \;\cong\; \pi_1 B_{0,n} E^2 .$$

The group of motions of $n$ points of the plane is the group with generators $\sigma_1,\dots,\sigma_{n-1}$ and the two families of relations above: the relations are not only valid but defining.

Milestones

The milestone list follows the chapter: the covering-space description of the projection $F_{0,n}E^2 \to B_{0,n}E^2$ (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence (Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group (Corollary 1.8.1, p. 24), the faithful representation of $B_n$ by automorphisms of a free group (Corollary 1.8.3, p. 25), the centre of $B_n$ (Corollary 1.8.4, p. 28, due to Chow), and Artin's algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).

Significance

Theorem 1.8 is what makes the braid group computable: with defining relations in hand one can combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2 and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids into concrete data — a braid is determined by what it does to the generators of a free group — and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine behind the conjugacy-problem and Magnus-representation chapters.

For formalization the state of play is that Mathlib has free groups, presented groups, the fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid groups and no configuration spaces: nothing here can be assembled from existing declarations. The mission therefore produces reusable infrastructure — configuration spaces of the plane, the symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as machine-checked proofs of results that are classical but, as far as the mission's search of the library showed, not yet formalized in Mathlib.

Difficulty

The generators and relations are easy to write down and easy to verify in $\pi_1 B_{0,n}E^2$; what is hard is completeness, i.e. that no further relations are needed. The naive route — draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do. The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on $n$ driven by the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$: its homotopy exact sequence gives a split extension of $P_{n-1}$ by a free group, presentations are assembled along the extension, and finally the covering $F_{0,n}E^2 \to B_{0,n}E^2$ with deck group $\Sigma_n$ transfers the answer from the pure braid group to the full braid group. Each of those steps needs genuine algebraic topology — local triviality of the projection, exactness of the homotopy sequence, freeness of $\pi_1$ of a punctured plane — which is where the formalization work actually lies.

Formalization scope

The plane is $\mathbb{C}$. $F_{0,n}E^2$ is the subtype of injective functions $\mathrm{Fin}\,n \to \mathbb{C}$; $B_{0,n}E^2$ is its quotient by the equivalence "differ by precomposition with a permutation", with the quotient topology. Base point: the configuration $i \mapsto i+1$, i.e. $(1,2,\dots,n)$, and its image. Fundamental groups are Mathlib's FundamentalGroup at those base points. Braid generators are indexed by $\mathrm{Fin}(n-1)$ with $0$-based indices ($i$ stands for $\sigma_{i+1}$), and free-group generators by $\mathrm{Fin}\,n$; the abstract braid group is a PresentedGroup on that index set. Truncated subtraction makes the generator set empty for $n \le 1$, so $B_0$ and $B_1$ are trivial, as intended. Two milestones are stated with the shift $n \mapsto n+1$ (i.e. for the projection $F_{0,n+1}E^2 \to F_{0,n}E^2$) to avoid truncated subtraction in the maps.

Two conventions are worth flagging because they weaken what the Lean text asserts relative to the prose. First, the goal asserts the existence of some isomorphism $B_n \cong \pi_1B_{0,n}E^2$; it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops are not part of the formal development. Second, Artin's representation is formalized as the existence of a homomorphism $\xi$ from $B_n$ to the automorphism group of the free group whose value on each $\sigma_i$ is the explicit endomorphism of equation (1-14), together with its injectivity; Theorem 1.9 is then stated for an arbitrary such $\xi$, given as a hypothesis, and is non-vacuous precisely because Corollary 1.8.3 supplies one.

No trivializing formalization is available: the goal is an isomorphism statement between two groups that are both defined independently of it, and the degenerate cases $n \le 1$ (both sides trivial) are genuine special cases of it, not the content.

Infrastructure a complete development needs, all reusable: freeness of $\pi_1$ of a punctured plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a fibration in the range needed, presentations of split extensions, and the transfer of a presentation along a regular covering. Contributions of any of these as standalone lemmas are welcome, as is a formalization of the geometric generators (1-9) that would let the goal be strengthened to pin the isomorphism on $\sigma_i$.

Selected references

• E. Artin, Theorie der Zöpfe, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
• E. Artin, Theory of braids, Annals of Mathematics 48 (1947), 101–126. https://doi.org/10.2307/1969218
• W.-L. Chow, On the algebraical braid group, Annals of Mathematics 49 (1948), 654–658. https://doi.org/10.2307/1969333
• E. Fadell, L. Neuwirth, Configuration spaces, Mathematica Scandinavica 10 (1962), 111–118. https://doi.org/10.7146/math.scand.a-10517
• E. Fadell, J. Van Buskirk, The braid groups of $E^2$ and $S^2$, Duke Mathematical Journal 29 (1962), 243–257. https://doi.org/10.1215/S0012-7094-62-02925-3
• J. S. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, Princeton University Press, 1974. https://doi.org/10.1515/9781400881420

Motivation

A basic question of additive combinatorics asks how a set grows under repeated addition. If a finite set $A$ in an abelian group satisfies $|A + B| \le \alpha |A|$ for some finite set $B$, how large can the iterated sumsets $hB = B + \cdots + B$ be? Plünnecke's inequality gives the answer used throughout the subject: some nonempty part of $A$ grows by at most a factor $\alpha$ per added copy of $B$. Combined with Ruzsa's triangle inequality it becomes the Plünnecke–Ruzsa inequality $|mB - nB| \le \alpha^{m+n}|A|$, which underlies Freĭman-type structure theorems, sum–product estimates and the polynomial Freĭman–Ruzsa programme.

Timeline.

• 1970: H. Plünnecke proves the inequality for iterated sumsets in abelian groups with a graph-theoretic method (commutative layered graphs and Menger's theorem).
• 1989: I. Z. Ruzsa simplifies Plünnecke's argument and combines it with the triangle inequality to bound $|mB - nB|$.
• 2011: G. Petridis gives a short elementary proof, without graphs (arXiv:1101.3507, Combinatorica 32, 2012). His argument also shows that one subset $X \subseteq A$ works for every number of summands $h$, and it extends to triple products $CXB$ in non-abelian groups.

Setting

Let $G$ be a group with finite subsets $A$, $B$, $C$. The product set is $AB = \{ab : a \in A,\ b \in B\}$, and $|\cdot|$ denotes cardinality. In an abelian group, written additively, the sumset is $A + B = \{a + b : a \in A,\ b \in B\}$, and for $h \ge 0$ the iterated sumset $hB$ is $B + \cdots + B$ with $h$ summands, $0B = \{0\}$. It is not the dilate $\{hb : b \in B\}$.

A nonempty subset $X \subseteq A$ has minimal growth under $B$ if

$$\frac{|XB|}{|X|} \le \frac{|ZB|}{|Z|} \quad\text{for every nonempty } Z \subseteq A.$$

Such an $X$ exists whenever $A$ is nonempty, since $A$ has finitely many subsets. In Lean, $G$ is a Group or AddCommGroup with decidable equality, the sets are Finset G with the pointwise operations of Mathlib (A * B, A + B, h • B), and cardinalities are #A cast to ℝ.

Formalization targets

Goal: Theorem 3.1

For finite $A$, $B$ in an abelian group with $A$ nonempty and $|A + B| \le \alpha|A|$, there is a nonempty $X \subseteq A$ with

$$|X + hB| \le \alpha^h |X| \qquad \text{for every } h \ge 0.$$

The point is the order of quantifiers: one $X$ serves all $h$.

Milestones

1. Proposition 2.1 (p. 5). If $|XB|/|X| \le |ZB|/|Z|$ for every $Z \subseteq X$, then $|CXB| \le \frac{|XB|}{|X|}\,|CX|$ for every finite $C$, in any group. This is already on the platform, proved, as FamousTheorems.pluennecke_petridis (additive notation, cross-multiplied), and enters the mission as a reference.
2. Theorem 1.5 (p. 3). In any group, $|AB| \le \alpha|A|$ with $A$ nonempty gives a nonempty $X \subseteq A$ with

$$|CXB| \le \alpha |CX| \quad\text{for every finite } C.$$

3. Inductive step of Theorem 3.1 (p. 7). For $X \subseteq A$ of minimal growth and $|A+B| \le \alpha|A|$:

$$|X + hB| \le \alpha\,|X + (h-1)B| \quad (h \ge 1).$$

Significance

Theorem 3.1 is the form of Plünnecke's inequality used in applications. Two consequences follow directly. Taking $A = B$ gives $|hB| \le \alpha^h|B|$ whenever $|2B| \le \alpha|B|$. Combining one $X$ for all $h$ with Ruzsa's triangle inequality gives $|mB - nB| \le \alpha^{m+n}|A|$ (Theorem 1.2 of the paper). With a separate $X$ for each $h$, the second step would need the same set for $m$ and $n$, and that is exactly what Theorem 3.1 provides. Theorem 1.5 is the non-abelian ingredient: missions 2 and 3 of this series apply it to obtain explicit Plünnecke-type bounds for $|B^h|$ and $|SB^h|$ in arbitrary groups.

Formalizing it. The results are proved and classical. Mathlib already contains Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul) and the Plünnecke–Ruzsa inequality Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add. Its proof runs through a private lemma that bounds $|X + hB|$ for one fixed minimiser, but no public statement in Mathlib or on the platform asserts Theorem 3.1 or Theorem 1.5 in the form "there exists a nonempty $X$ for all $h$" (respectively "for all $C$"). This mission adds those statements as reusable, citable nodes in the paper's numbering.

Difficulty

A first attempt iterates the hypothesis directly: $|A + 2B| \le \alpha|A + B|$ would follow if $A + B$ again grew by a factor $\alpha$ under $B$, but nothing controls the growth of $A + B$. The ratio $|ZB|/|Z|$ is not monotone in $Z$, and passing to subsets of $A$ can only help if the subset is chosen correctly. Choosing a different good subset for each $h$ gives Theorem 1.1 but loses the uniformity. The work is to show that one fixed subset controls all the products $CXB$ simultaneously, and in the non-abelian Theorem 1.5 to keep the order of the factors $C$, $X$, $B$ throughout.

Formalization scope

• Theorem 3.1 and the inductive step are stated in an AddCommGroup with DecidableEq. Theorem 1.5 is stated in a Group, with no commutativity, as on the page. The factor order $C \cdot X \cdot B$ is preserved.
• $hB$ is h • B (the $h$-fold sumset; 0 • B = {0}), and "for all $h$" ranges over all natural numbers, including the true case $h = 0$.
• $\alpha$ is an arbitrary real number; cardinalities are cast to ℝ. No hypothesis $\alpha \ge 1$ is added: it follows from the hypotheses once $A$ and $B$ are nonempty (with $B$ empty they force only $\alpha \ge 0$, and every conclusion is still true).
• Nonempty witness. The page says "there exists $X \subseteq A$". Since $\emptyset + hB = \emptyset$, the empty set would satisfy the printed statements trivially, and that formalization is ruled out: the goal and Theorem 1.5 assume $A$ nonempty and assert $X$ nonempty, matching the paper's choice of $X$ as a minimiser of a ratio defined on nonempty sets.
• Minimal growth in the step milestone is written cross-multiplied, $|X+B|\,|Z| \le |Z+B|\,|X|$, over nonempty $Z \subseteq A$; the step is stated for $h \ge 1$ with natural-number subtraction guarded by that hypothesis.
• Ruzsa's covering lemma and Ruzsa's triangle inequality, quoted in §4, are in Mathlib (Finset.ruzsa_covering_mul, Finset.ruzsa_triangle_inequality_mul_mulInv_mul) and are not items of this mission.
• No new definitions are needed. Welcome contributions: proofs of the three draft statements, and, separately, the deduction of Theorem 1.2 from Theorem 3.1.

Selected references

• G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, arXiv:1101.3507v3, 2011; Combinatorica 32 (2012). https://arxiv.org/abs/1101.3507 , https://doi.org/10.1007/s00493-012-2818-5
• H. Plünnecke, Eine zahlentheoretische Anwendung der Graphentheorie, J. Reine Angew. Math. 243 (1970) 171–183. https://doi.org/10.1515/crll.1970.243.171
• I. Z. Ruzsa, An application of graph theory to additive number theory, Scientia, Ser. A 3 (1989) 97–109 (no online version).
• T. Tao, V. Vu, Additive Combinatorics, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511755149

Motivation: Saxl's conjecture on the staircase tensor square

The irreducible complex representations of the symmetric group $S_n$ are the Specht modules $S^\lambda$, indexed by partitions $\lambda\vdash n$. How a tensor product $S^\alpha\otimes S^\beta$ (with diagonal action) decomposes is recorded by the Kronecker coefficients

$$g(\alpha,\beta,\lambda)=\dim\operatorname{Hom}_{S_n}\!\big(S^\lambda,\,S^\alpha\otimes S^\beta\big),$$

for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase $\rho_m=(m,m-1,\dots,1)$, a partition of $N_m=m(m+1)/2$, has a tensor square containing every irreducible representation of $S_{N_m}$.

Timeline

• 2012 — Saxl proposes the conjecture at the UCLA Combinatorics Seminar (20 March 2012), as recorded by Pak, Panova and Vallejo.
• 2010 — Brown, van Willigenburg and Zabrocki show that $S^{(m,m-1)}\otimes S^{(m,m-1)}$ is the multiplicity-free sum of all irreducibles with at most four rows (BWZ 2010, Cor. 4.1).
• 2013 — Heide, Saxl, Tiep and Zalesski prove that the Steinberg square of most finite simple groups of Lie type contains every irreducible, a motivating precedent (HSTZ 2013, Thm 1.2).
• 2015 — Ikenmeyer proves positivity for all $\lambda$ comparable with $\rho_m$ in dominance order, and all hooks (Ikenmeyer 2015).
• 2016 — Pak, Panova and Vallejo formulate the conjecture in print, give a character-nonvanishing criterion, and handle hooks and two-row shapes for large $m$ (PPV 2016).
• 2017 — Luo and Sellke: almost every partition occurs (uniform and Plancherel measures) (Luo–Sellke 2017).
• 2018–2021 — Bessenrodt: double hooks (2018); Bessenrodt, Bowman and Sutton: all 2-height-zero constituents and framed staircases (2021); Li: triple hooks (2021).
• 2023 — Harman and Ryba: the staircase tensor cube contains everything (Harman–Ryba 2023).
• 2025 — Letellier and Nam prove the staircase-square statement for unipotent characters of $\mathrm{GL}_n(q)$, a different character theory (Letellier–Nam 2025).
• 2026 — An OpenAI preprint, A Cyclic Polytabloid Proof of Saxl's Conjecture (OpenAI Math Release, September 24, 2026), claims a proof of the full conjecture. It has not been peer reviewed and the theorem is not formally verified.

Setting

A partition is a Mathlib YoungDiagram. The Lean development builds $S^\lambda$ concretely: for a tableau $t$ (a bijection between $\{0,\dots,n-1\}$ and the cells), the polytabloid $e_t$ is the signed sum over the column group of $t$ of the permuted indicator of the row word of $t$, inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$; Specht t is the $\mathbb C$-span of the $S_n$-orbit of $e_t$. The coefficient kronecker a b t is the complex dimension of the space of $S_n$-intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells $(i,j)$ with $i+j<m$, i.e. $\rho_m$.

Formalization targets

Goal: Saxl's conjecture

For every integer $m\ge1$ and every partition $\lambda\vdash N_m$,

$$g(\rho_m,\rho_m,\lambda)>0 ,$$

equivalently $S^{\rho_m}\otimes S^{\rho_m}$ contains every irreducible representation of $S_{N_m}$. This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram $\mu$ with as many cells as staircase m). The goal is published on the platform with status Open.

Significance

The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every $S^\lambda$ already occurs in the submodule $W_m$ generated by one explicit tensor $v_{R_m}\otimes v_{C_m}$ of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every $n\notin\{2,4,9\}$, an irreducible representation of $S_n$ whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).

Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of $S_n$.

Difficulty

Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all $\lambda$) or higher powers (cube, fourth power) leave exceptional constituents. An induction on $m$ must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.

Formalization scope

• staircase m has cells $\{(i,j): i+j<m\}$, with $m(m+1)/2$ cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.
• kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map $S^\lambda\to S^{\rho_m}\otimes S^{\rho_m}$ exists.
• The case $m\ge1$ matches the source; $m=0$ is excluded.
• Needed infrastructure: Specht modules and polytabloid bases, Young's rule and dominance, sign twists, induction and restriction, Littlewood–Richardson branching. The definitions are shared verbatim with the companion universal-tensor-square mission.

Selected references

• I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
• G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
• A. A. H. Brown, S. van Willigenburg and M. Zabrocki, Expressions for Catalan Kronecker products, Pacific J. Math. 248 (2010), 31–48. https://doi.org/10.2140/pjm.2010.248.31
• C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
• S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
• C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
• C. Bessenrodt, C. Bowman and L. Sutton, Kronecker positivity and 2-modular representation theory, Trans. Amer. Math. Soc. Ser. B 8 (2021), 1024–1055. https://doi.org/10.1090/btran/70
• X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
• N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
• E. Letellier and G. Nam, The Saxl conjecture and the tensor square of unipotent characters of GL_n(q), Algebr. Comb. 8 (2025), 1119–1140. https://doi.org/10.5802/alco.434
• OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf

Motivation

Every pure integer program $\min\{c\cdot x : Ax = b,\ x \ge 0 \text{ integer}\}$ can be relaxed, by dropping the nonnegativity of the basic variables of an optimal linear-programming basis, to a problem over a finite Abelian group: find nonnegative integers $t(g)$, one for each nonzero group element, with $\sum t(g)\cdot g = g_0$. R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969) 451–558) studies the convex hulls of the solutions of these group equations, the corner polyhedra, and the master polyhedron $P(\mathcal G, g_0)$ that contains all of them as faces. These polyhedra are the source of the group-theoretic approach to cutting planes: their faces are valid inequalities for every integer program with the same group, and their vertices are the candidate optimal solutions of the group relaxation.

The paper's first section shows that every vertex of such a polyhedron is an irreducible solution, and remarks (p. 460) that the converse fails in general: a typical group has many irreducible solutions that are not vertices. Section 3F identifies a family of groups where the two notions coincide, which is what makes the vertices of these polyhedra countable in closed form.

Setting

Let $\mathcal G$ be a finite Abelian group written additively, with zero $\bar 0$, and $\mathcal G^+ = \mathcal G\setminus\{\bar 0\}$. For $g_0 \in \mathcal G$ the group equation is

$$\sum_{g\in\mathcal G^+} t(g)\cdot g = g_0, \qquad t(g) \in \{0, 1, 2, \ldots\}.$$

The master polyhedron $P(\mathcal G, g_0)$ is the convex hull in $\mathbb R^{\mathcal G^+}$ of its nonnegative integer solutions (for $g_0 = \bar 0$ the solution $t = 0$ is excluded). A vertex is an extreme point of $P(\mathcal G, g_0)$.

A nonnegative integer vector $t$ is irreducible if any two integer vectors $r, s$ with $0 \le r, s \le t$ and $\sum r(g)\cdot g = \sum s(g)\cdot g$ are equal. A finite set $S$ of group elements is independent if $\sum_{g\in S} s_g g = \bar 0$ with integers $s_g$ forces $s_g g = \bar 0$ for each $g$.

The groups of §3F are those in which every nonzero element has order 2, the groups $\mathcal G_2, \mathcal G_{2,2}, \ldots$, or every nonzero element has order 3, the groups $\mathcal G_3, \mathcal G_{3,3}, \ldots$.

Formalization targets

Goal: THEOREM 23 (p. 505)

If every nonzero element of $\mathcal G$ has order $p$, with $p = 2$ or $p = 3$, and $g_0 \ne \bar 0$, then for every nonnegative integer solution $t$ of the group equation

$$t \text{ irreducible} \iff t \in \operatorname{vert} P(\mathcal G, g_0),$$

and the support $\{g : t(g) > 0\}$ of such a vertex is an independent set.

Milestones

1. THEOREM 2 (p. 460), for $P(\mathcal G, g_0)$ with $g_0 \ne \bar 0$: every vertex is an irreducible integer solution.
2. The LEMMA of p. 505: for $p \in \{2, 3\}$, $p > t > 0$ and $p > s \ge 0$ there are $0 \le t', t'' \le t$ with $t' + s \equiv t'' \pmod p$.
3. The support of an irreducible solution is independent (p. 506).
4. A solution vanishing off the support of an irreducible $t$ agrees with $t$ modulo $p$ and dominates it (p. 506, corrected).
5. An irreducible $t$ minimizes $\pi$, the indicator of the complement of its support, every minimizer dominates $t$, and $t$ is a vertex (p. 506, corrected).
6. The vertex characterization (p. 506): a nonzero $t$ is a vertex of some $P(\mathcal G, g_0)$, $g_0 \ne \bar 0$, iff its support is independent and $t(g) < p$ for all $g$.

Significance

THEOREM 23 turns a polyhedral question into a combinatorial one for the elementary Abelian 2- and 3-groups: the vertices of $P(\mathcal G, g_0)$ are read off from independent subsets of the group and residues below $p$. Gomory uses this on pp. 506–507 to count all vertices of all $P(\mathcal G_{s^n}, g_0)$ exactly and to derive their asymptotic number. It also marks the boundary of the general picture: groups with elements of other orders have irreducible solutions that are not vertices.

The result has been proved since 1969; no machine-checked proof exists. The mission produces a Lean statement and, once solved, a verified proof of the theorem together with the general fact that vertices of the master polyhedron are irreducible, a reusable layer for the other group-polyhedron results of the same paper. Two sentences of the printed proof (p. 506) are false as written (see Formalization scope); formalization records their corrected forms.

Difficulty

The direction "vertex $\Rightarrow$ irreducible" holds in every group and is a midpoint argument. The difficulty is the converse: showing that an irreducible solution cannot be written as a proper convex combination of other solutions, which are infinitely many and unbounded. The natural route, exhibiting a linear objective that $t$ uniquely minimizes, does not work with the objective printed on the page: solutions with the same support as $t$ but larger entries are tied with it. The argument must control those solutions through the arithmetic of residues modulo $p$, and this is where the exponent 2 or 3 is used; the analogous residue statement fails for $p = 5$.

Formalization scope

• T-space vectors are functions on the subtype {g : G // g ≠ 0}; integer solutions are $\mathbb N$-valued and cast to $\mathbb R$; vertices are Set.extremePoints ℝ of the convex hull of the cast solutions.
• "All elements of $\mathcal G$ are of order 2 or all of order 3" is read as: there is $p \in \{2, 3\}$ with every nonzero element of order $p$. Groups mixing orders 2 and 3 are excluded, as on the page.
• $g_0 \ne \bar 0$ is a hypothesis of the whole of THEOREM 23 (the page attaches it to the second sentence only). At $g_0 = \bar 0$ the solution $t = 0$ is excluded (footnote p. 474) and every nonzero solution is reducible, so the first sentence would fail. THEOREM 2 is restated for $P(\mathcal G, g_0)$, $g_0 \ne \bar 0$, for the same reason.
• "Independent" is the page's definition with integer coefficients; the gloss "part of a group basis" is not formalized.
• The letter $T$ on pp. 505–506 is the support of $t$, not the solution set.
• The page's claim that $t$ is the only solution vanishing off its support, and the unique minimizer of $\pi$, fail literally (in $\mathbb Z_2$ with $g_0 = 1$, $t = (1)$ and $u = (3)$). Milestones 4 and 5 state the corrected conclusions; the goal theorem is unaffected.
• The vertex characterization adds $t \ne 0$, which the page leaves implicit.
• Ruled out: stating the order hypothesis for all elements including $\bar 0$ (unsatisfiable, so the theorem would be vacuous), dropping $g_0 \ne \bar 0$ (false statement), or replacing the master polyhedron by a bounded truncation (a different polyhedron with extra vertices).
• Needed: convex hulls of infinite sets of lattice points and their extreme points (Mathlib's convexHull, extremePoints_convexHull_subset), and finite sums in Abelian groups. Contributions welcome: any of the milestones, and a general lemma that a unique minimizer of a nonnegative linear function over the integer solutions is a vertex.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53 (1965), 260–265. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. https://doi.org/10.1007/BF01584976

Motivation

A cellular automaton over a group $G$ with a finite alphabet $A$ is a map on configurations $x : G \to A$ that updates every cell by the same finite local rule, read off from a finite neighbourhood of that cell. Cellular automata over $\mathbb{Z}^d$ go back to von Neumann and Ulam and are a standard model in symbolic dynamics; replacing $\mathbb{Z}^d$ by an arbitrary group links the theory to geometric group theory.

In 1973 Gottschalk asked which groups $G$ have the property that every injective cellular automaton over $G$ is automatically surjective, and called such groups surjunctive. For a finite group this is the pigeonhole principle, since $A^G$ is then a finite set. For infinite groups the configuration space is an uncountable compact space and the pigeonhole principle is no longer available. Gottschalk's surjunctivity conjecture states that every group is surjunctive. It is open.

Timeline

• 1962–1963 — Moore and Myhill prove the Garden of Eden theorem for $\mathbb{Z}^2$ (and, in the same way, $\mathbb{Z}^d$): a cellular automaton is surjective if and only if it is pre-injective. In particular $\mathbb{Z}^d$ is surjunctive.
• 1969 — Hedlund (crediting Curtis and Lyndon) characterises cellular automata over $\mathbb{Z}$ as the continuous shift-commuting self-maps of $A^{\mathbb{Z}}$ (the Curtis–Hedlund–Lyndon theorem); the characterisation extends to every group.
• 1973 — Gottschalk introduces surjunctivity and states the conjecture; he records Lawton's result that residually finite groups are surjunctive.
• 1999 — Ceccherini-Silberstein, Machì and Scarabotti prove the Garden of Eden theorem for amenable groups, which implies that amenable groups are surjunctive.
• 1999–2000 — Gromov introduces what Weiss names sofic groups, and both show that sofic groups are surjunctive. Sofic groups include all residually finite groups and all amenable groups.
• Today — no group is known to be non-sofic, and no group is known to be non-surjunctive.

Setting

Fix a group $G$ and a finite nonempty set $A$ (the alphabet). A configuration is a function $x : G \to A$; the set of configurations is $A^G$. It carries the product topology, where $A$ has the discrete topology; this makes $A^G$ compact.

The left shift of $x$ by $g \in G$ is the configuration

$$(g \cdot x)(h) = x(g^{-1}h), \qquad h \in G,$$

written shift G g x in the Lean development. A map $\tau : A^G \to A^G$ is shift-equivariant (IsShiftEquivariant) if $\tau(g\cdot x) = g\cdot\tau(x)$ for all $g$ and $x$.

The group $G$ is surjunctive (IsSurjunctive) if, for every finite nonempty alphabet $A$, every map $\tau : A^G \to A^G$ that is continuous, shift-equivariant and injective is also surjective.

A map $\tau$ is a cellular automaton (IsCellularAutomaton) if there are a finite memory set $S \subseteq G$ and a local rule $\mu : A^S \to A$ with

$$\tau(x)(g) = \mu\big(s \mapsto x(gs)\big) \qquad \text{for all } x \in A^G,\ g \in G.$$

Three classes of groups appear in the milestones:

1. $G$ is residually finite (IsResiduallyFinite) if every $g \neq 1$ lies outside some normal subgroup of finite index.
2. $G$ is amenable if there is a finitely additive, left-invariant probability measure defined on all subsets of $G$ (the existing platform definition Garrido.IsAmenable).
3. $G$ is sofic (IsSofic) if for every finite $K \subseteq G$ and every $\varepsilon > 0$ there are a finite nonempty set $X$ and a map $\sigma : G \to \mathrm{Sym}(X)$ such that $\sigma_{gh}(x) = \sigma_g(\sigma_h(x))$ for at least a $(1-\varepsilon)$ fraction of the points $x \in X$ whenever $g, h \in K$, and $\sigma_g(x) \neq x$ for at least a $(1-\varepsilon)$ fraction of the points whenever $g \in K \setminus \{1\}$.

Formalization targets

Goal: Gottschalk's conjecture

$$\forall\, G \text{ group}: \quad G \text{ is surjunctive.}$$

Milestones

1. Curtis–Hedlund–Lyndon: for finite $A$, a map $\tau : A^G \to A^G$ is continuous and shift-equivariant if and only if it is a cellular automaton.
2. Subgroups: every subgroup of a surjunctive group is surjunctive.
3. Local character: if every finitely generated subgroup of $G$ is surjunctive, then $G$ is surjunctive.
4. Finite groups are surjunctive.
5. Residually finite groups are surjunctive (Lawton).
6. Amenable groups are surjunctive (Ceccherini-Silberstein–Machì–Scarabotti).
7. Sofic groups are surjunctive (Gromov; Weiss).

Significance

The result itself. A positive answer would make the implication "injective $\Rightarrow$ surjective" for cellular automata hold unconditionally, extending the pigeonhole principle from finite sets to all shift spaces $A^G$. Surjunctivity is also tied to Kaplansky's direct finiteness conjecture: for a surjunctive group $G$ and any finite field $K$, the group ring $K[G]$ is directly finite ($ab = 1 \Rightarrow ba = 1$). A counterexample would be the first known non-sofic group, since sofic groups are surjunctive.

Formalizing it. Milestones 4–7 are proved results in the literature; milestones 1–3 are standard facts of the theory. At the time of writing, none of milestones 1–3 and 5–7 is known to exist as a machine-checked proof on this platform. Formalizing them requires building the basic theory of cellular automata over groups (memory sets, local rules, induced automata on subgroups), which can be reused by other work in symbolic dynamics. The goal theorem itself is open.

Difficulty

For infinite $G$ the space $A^G$ is infinite, so no counting argument applies directly. All known proofs approximate $G$ by finite objects: finite quotients (residually finite case), Følner sets with an entropy count (amenable case), or approximate finite permutation models (sofic case). No such approximation is known to exist for every group, and it is not known whether every group is sofic. A proof of the full conjecture therefore needs either a proof that every group is sofic or an argument that does not go through finite approximations.

Formalization scope

• Groups $G$ and alphabets $A$ live in Type (universe $0$). Alphabets are finite (Fintype) and nonempty; their topology is an arbitrary topology assumed to be discrete, and $A^G$ carries Lean's product topology.
• The shift is a plain function shift, not a MulAction instance, to avoid a clash with Mathlib's pointwise action on function types.
• Amenability is taken from the existing platform definition Garrido.IsAmenable (finitely additive invariant probability measure on all subsets). Residual finiteness and soficity are defined in GottschalkSurjunctivity_Defs.
• Soficity is stated with a normalised count of points; the conditions are required for every $\varepsilon > 0$, so small $\varepsilon$ is where the content lies.
• Surjunctivity is not trivialised by the nonemptiness assumption: for a nonempty group and a nonempty alphabet, $A^G$ is nonempty and, when $G$ is infinite, uncountable.

Contributions welcome: the Curtis–Hedlund–Lyndon theorem, restriction and induction of cellular automata along subgroups, and the residually finite case are natural first steps.

Selected references

• W. H. Gottschalk, Some general dynamical notions, Recent Advances in Topological Dynamics, Lecture Notes in Math. 318, Springer, 1973, pp. 120–125. https://doi.org/10.1007/BFb0061728
• G. A. Hedlund, Endomorphisms and automorphisms of the shift dynamical system, Math. Systems Theory 3 (1969), 320–375. https://doi.org/10.1007/BF01691062
• T. Ceccherini-Silberstein, A. Machì, F. Scarabotti, Amenable groups and cellular automata, Ann. Inst. Fourier 49 (1999), 673–685. https://doi.org/10.5802/aif.1686
• M. Gromov, Endomorphisms of symbolic algebraic varieties, J. Eur. Math. Soc. 1 (1999), 109–197. https://doi.org/10.1007/PL00011162
• B. Weiss, Sofic groups and dynamical systems, Sankhyā Ser. A 62 (2000), 350–359.
• T. Ceccherini-Silberstein, M. Coornaert, Cellular Automata and Groups, Springer Monographs in Mathematics, 2010. https://doi.org/10.1007/978-3-642-14034-1
• Wikipedia, Surjunctive group. https://en.wikipedia.org/wiki/Surjunctive_group

Motivation

Rotations of three-dimensional space are the most frequently used nontrivial Lie group in physics. Quantum mechanics requires more than the rotation group $SO(3)$ itself: particles of half-integer spin, such as the electron, transform under a group in which a rotation by $2\pi$ acts as $-1$. That group is $SU(2)$, the double covering group of $SO(3)$. W. Siegel's graduate text Fields (arXiv:hep-th/9912205) introduces spin through this covering in Chapter II, Section A ("Two components", pp. 110–116). It encodes a 3-vector as a traceless hermitian $2\times2$ matrix, reads the dot and cross products off the matrix product, and realizes rotations as conjugation by unitary matrices.

This mission is the first in a series formalizing results from Fields. It covers the algebra of §IIA1–IIA3, which ends with the statement that the map $SU(2)\to SO(3)$ is two-to-one.

Setting

Let $M_2(\mathbb C)$ be the complex $2\times2$ matrices, $V^\dagger$ the conjugate transpose, $V^T$ the transpose and $V^*$ the entrywise complex conjugate.

• A 3-vector is a matrix $V\in M_2(\mathbb C)$ with $V^\dagger=V$ and $\operatorname{tr}V=0$. These matrices form a real vector space $\mathcal V$ of dimension three.
• The book's basis: for $v=(v_1,v_2,v_3)\in\mathbb R^3$,

$$V(v)=\frac1{\sqrt2}\begin{pmatrix}v_1&v_2-iv_3\\ v_2+iv_3&-v_1\end{pmatrix},\qquad E_i=V(e_i).$$

• The norm is $|V|^2=-2\det V=\operatorname{tr}(V^2)$, and the inner product is $V\cdot W=\operatorname{tr}(VW)$.
• The matrix $C=\begin{pmatrix}0&-i\\ i&0\end{pmatrix}$.
• A rotation acts by $V\mapsto UVU^\dagger$ with $U\in SU(2)$, i.e. $U^\dagger=U^{-1}$ and $\det U=1$. Its matrix in the basis $E_i$ is

$$R(U)_{ij}=\operatorname{Re}\operatorname{tr}\big(E_i\,U\,E_j\,U^\dagger\big).$$

In the Lean development these are SiegelFields.IsThreeVector, vecToMatrix, basisMatrix, matC and rotationOf. Components are indexed by $\{0,1,2\}$.

Formalization targets

Goal: $SU(2)$ is a double covering of $SO(3)$

$$R:\ SU(2)\to SO(3)\ \text{ is a surjective homomorphism, and } R(U)=R(W)\iff W=\pm U\quad(U,W\in SU(2)).$$

Concretely: $R(U)\in SO(3)$ for all $U\in SU(2)$; $R(UW)=R(U)R(W)$; every element of $SO(3)$ is some $R(U)$; and $R(U)=R(W)$ exactly when $W=U$ or $W=-U$.

Milestones (in the book's order)

1. $-2\det M=\operatorname{tr}(M^2)-(\operatorname{tr}M)^2$ (p. 111).
2. $|V|^2=-2\det V=\operatorname{tr}(V^2)$ is real, non-negative and vanishes only at $V=0$ (p. 111).
3. The 3-vectors are exactly the matrices $V(v)$, and $v$ is unique (p. 111).
4. $\det V(v)=-\tfrac12\sum v_i^2$ and $\operatorname{tr}(V(v)^2)=\sum v_i^2$ (pp. 111–112).
5. $V\cdot W=\det V+\det W-\det(V+W)=\operatorname{tr}(VW)$ and $\{V,W\}=(V\cdot W)I$ (pp. 111–112).
6. $MCM^TC=I\det M$, $M+CM^TC=I\operatorname{tr}M$, and $\operatorname{tr}M=0\iff(MC)^T=MC$ (pp. 111–112).
7. $M^2=M\operatorname{tr}M-I\det M$, hence $V^2=-I\det V=\tfrac12|V|^2I$ (p. 112).
8. $[V(v),V(w)]=\sqrt2\,i\,V(v\times w)$ (p. 112).
9. Unitary conjugation preserves 3-vectors and their determinant (p. 114).
10. Reality conditions $V^*=-CVC$ and $U^*=CUC$ for $U\in SU(2)$ (pp. 114–115).
11. $cI\in SU(2)\iff c=\pm1$ (p. 115).
12. $U,W\in SU(2)$ act identically on all 3-vectors iff $W=\pm U$ (p. 115).
13. $U\,V(v)\,U^\dagger=V(R(U)v)$ for unitary $U$ (p. 114, component form).

Significance

The covering $SU(2)\to SO(3)$ is the basic reason spinors exist. It gives the spin-$\tfrac12$ representation, explains why a $2\pi$ rotation acts as $-1$ on fermions, and is the first instance of the low-dimensional Lie algebra identifications that Siegel lists in §IC5 (such as $SO(3,1)=SL(2,\mathbb C)$ and $SO(6)=SU(4)$). Later chapters of Fields build spinor index notation, the Lorentz group and supersymmetry on this material.

The mathematics is classical and fully proved. What this mission adds is a machine-checked version stated in the book's own conventions: its basis, its normalization of the norm ($|V|^2=-2\det V$) and its matrix $C$. The result is a dictionary between Siegel's matrix notation and Mathlib's matrix groups that later missions in the series can import.

Difficulty

Most milestones are identities about $2\times2$ matrices and can be checked entrywise. The substantive parts of the goal are surjectivity onto $SO(3)$ and the kernel computation. Showing that every rotation is some $R(U)$ requires constructing $U$ from $R$, for example from an axis and an angle or by generating $SO(3)$ from simpler rotations. It cannot be done by an entrywise identity. Pinning the kernel to $\{\pm I\}$ requires showing that a unitary matrix commuting with all of $\mathcal V$ is scalar, and then combining this with $\det U=1$. Showing $\det R(U)=+1$ rather than $\pm1$ needs either a connectedness argument or an explicit formula.

Formalization scope

• $SU(2)$ is Matrix.specialUnitaryGroup (Fin 2) ℂ and $SO(3)$ is Matrix.specialOrthogonalGroup (Fin 3) ℝ. Unitary matrices are Matrix.unitaryGroup (Fin 2) ℂ.
• rotationOf U is defined for every matrix $U$ and takes the real part of a trace. The statements restrict $U$ to the unitary or special unitary group, where that trace is real.
• The cross product is Mathlib's crossProduct on Fin 3 → ℝ. The book's basis corresponds to the cyclically relabelled Pauli matrices $(\sigma_3,\sigma_1,\sigma_2)$, which preserves orientation.
• Surjectivity appears in the goal because a covering map is onto. The book asserts it through the phrase "double covering" rather than proving it.
• All statements use the same definition file, and nothing in it is assumed through hypotheses. The goal therefore cannot be satisfied by a vacuous or trivializing choice.

Contributions welcome: proofs of the matrix identities, a proof of surjectivity, and connections to Mathlib's quaternion and unit-sphere API.

Selected references

• W. Siegel, Fields, arXiv:hep-th/9912205v3, 2005. https://arxiv.org/abs/hep-th/9912205 (Chapter II A, pp. 110–116; Chapter I C5, pp. 107–108)