Winding Dynamics I: Homotopy Conservation and Reset BalanceTextbook
## Motivation
Phase winding is an integer attached to a circle-valued field on a closed spatial cycle. It distinguishes configurations that cannot be continuously deformed into one another while remaining circle-valued and spatially continuous. In oscillator and spin models this integer is often described informally as conserved by smooth evolution, while changes of winding are attributed to phase slips, vortices, singularities, or branch-cut crossings. The purpose of this mission is to turn that informal division into an exact Lean interface.
The continuum and finite-lattice settings must be separated. A jointly continuous field on a spatial circle really does provide a homotopy of circle maps, so its degree is invariant. A finite list of continuously moving vertex phases does not by itself determine a continuous field on the geometric realization of the lattice. Principal shortest-arc interpolation becomes ambiguous at antipodal bonds, and the corresponding discrete winding can jump even though every vertex phase remains continuous. The mission therefore treats winding as a first integral only on the regular sector and records every failure of regularity through an integer reset ledger.
This distinction is relevant to circle-valued reductions of the Kuramoto model, the finite XY model, and Lohe-type dynamics. Kuramoto's original synchronization model concerns coupled phase oscillators, while Lohe's non-Abelian extension replaces phases by group-valued variables. A model-specific conservation theorem is justified only after the dynamics has been connected to an actual circle-valued spatial loop or to the registered finite principal-branch interface.
## Setting
A **circle loop** is a continuous map from a closed parameter interval to $S^1$ whose two endpoints agree. Its **winding number** is the integer obtained from the endpoint of a lift to the universal cover $\mathbb R\to S^1$. When the loop's basepoint moves during a deformation, the loop is normalized by the inverse of its value at the chosen spatial basepoint; this produces a based loop without changing its winding.
A **continuous Circle-field segment** is a jointly continuous map
$$
U:[t_0,t_1]\times S^1\longrightarrow S^1.
$$
Each time slice $U_t$ is a spatial loop. Such a segment has no branch-cut convention: it is intrinsic topological data.
For a finite directed edge system (including a finite periodic lattice), a state assigns a real lift to every vertex. Each oriented edge receives an integer principal turn. A state is **branch regular** when no stored edge is antipodal. A coherent finite reset ledger stores successive principal-turn cochains $T_i$ and defines the reset $k_i=T_{i+1}-T_i$. For a certified closed integer cycle $C$, the pairing $\langle k_i,C\rangle$ is its registered winding jump.
A Kuramoto, XY, or Lohe consumer must supply the missing model-specific data. For a continuum consumer this is a jointly continuous circle-valued field. For a finite consumer it is a continuous vertex trajectory together with branch regularity away from registered events. A Lohe consumer additionally needs a continuous Circle readout or invariant Circle carrier; preservation of a rotor constraint alone does not provide that reduction.
## Formalization targets
### Continuous-field conservation
For every jointly continuous Circle-field segment, the two endpoint loops have equal winding:
$$
\operatorname{wind}(U_{t_1})=\operatorname{wind}(U_{t_0}).
$$
The statement must cover moving loop basepoints through explicit normalization. Winding is defined directly from Mathlib's exponential covering map as the floor of the zero-based lift endpoint divided by $2\pi$.
### Branch-regular finite conservation
For every finite directed principal-phase trajectory on a preconnected time domain that remains branch regular, every registered integer-chain winding is constant:
$$
W_C(t_1)=W_C(t_0).
$$
Continuity of the vertex phases alone is not a sufficient hypothesis and must not appear as a replacement for branch regularity or spatial interpolation.
### Exact reset balance
For a finite coherent ledger with steps $i=0,\ldots,N-1$, endpoint winding change equals the sum of the reset periods:
$$
W_C(T_N)-W_C(T_0)
=\sum_{i=0}^{N-1}\langle k_i,C\rangle.
$$
The conservation theorem is the empty-ledger or zero-period special case. The statement is an exact integer identity and does not assert an energy lower bound, vortex separation, or a thermodynamic-limit result.
### Dynamics adapters
The generic dynamics adapter requires a jointly continuous ambient-state segment, a registered carrier containing it, closed spatial profiles, and a continuous readout from that carrier to the Circle. Kuramoto/XY or Lohe consumers must separately prove those hypotheses for their model. A second fence states that a global continuous readout from a simply connected carrier maps every loop to a nullhomotopic Circle loop; nonzero Lohe winding therefore requires a separately registered non-simply-connected carrier, such as a preserved $U(1)$ orbit, or a different explicit interface.
## Significance
The resulting theorem family makes precise the statement that winding obstructs unwinding. In the intrinsic continuum setting, winding cannot change while the field remains a continuous $S^1$-valued map. In the finite principal-branch setting, winding is piecewise constant and every change has an exact integer certificate. This separates a topological conservation law from the physical or analytic question of how much energy is needed to realize a certificate.
For formalization, the mission supplies a reusable boundary between topology and dynamics. A dynamics development can establish continuity and carrier preservation without reimplementing covering-space winding. A lattice development can consume the same integer through reset cochains without claiming that a vertex-only path is a homotopy of spatial loops. Later energy-barrier, vortex, and transport results can depend on the reset balance rather than on an informal conservation principle.
## Difficulty
The principal difficulty is that several superficially similar notions of continuity have different consequences. Continuity in time of finitely many vertex phases is continuity into the configuration torus $(S^1)^V$, which is connected and does not preserve a principal-edge winding sector. Continuity of a map on time times the geometric spatial cycle is stronger. A formal statement that confuses them would make the desired theorem false.
There are two additional interface risks. First, the canonical Circle lift is based, whereas a physical phase field normally has a moving value at the chosen spatial origin. Second, the current Lohe development establishes algebraic identities and infinitesimal rotor preservation, not a global continuous flow in a selected Circle subgroup. These distinctions remain visible in the theorem hypotheses.
## Formalization scope
The mission targets Lean 4.30 with Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, matching the cited LeanProofs development. It reuses Mathlib's unit interval, continuous maps, path homotopies, Circle covering map, local constancy, and finite sums. The continuum statement concerns spatial $S^1$ only. The finite theorem is graph-generic: it uses finite oriented edges, integer edge cochains, certified closed integer cycles, coherent successive reset states, and branch regularity on a preconnected time domain.
The scope excludes ODE or PDE existence and uniqueness, preservation of a Circle carrier by a particular Lohe vector field, extraction of a coherent reset ledger from a physical event trajectory, arbitrary graph interpolation, accumulating reset times, thermodynamic limits, and energetic barriers. Those may be attached later through explicit interfaces. No theorem claims global winding conservation for an unrestricted finite vertex trajectory, and no theorem identifies group-valued Lohe motion with Circle motion without a declared continuous readout.
## Selected references
- Monumental Systems, *CircleFundamentalGroupWindingV1*, LeanProofs commit `b656238b73d5f0f74515f6574a1dcb4e0216129f`, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleFundamentalGroupWindingV1.lean#L81
- Monumental Systems, *FiniteTorusPrincipalResetEventV1*, LeanProofs commit `b656238b73d5f0f74515f6574a1dcb4e0216129f`, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/StatMech/FiniteTorusPrincipalResetEventV1.lean#L152-L167
- Monumental Systems, *CircleWindingTranslationHolonomyV1*, LeanProofs commit `b656238b73d5f0f74515f6574a1dcb4e0216129f`, 2026. https://github.com/MonumentalSystems/LeanProofs/blob/b656238b73d5f0f74515f6574a1dcb4e0216129f/LeanProofs/Rosetta/CircleWindingTranslationHolonomyV1.lean#L107
- Y. Kuramoto, “Self-entrainment of a population of coupled non-linear oscillators,” in *International Symposium on Mathematical Problems in Theoretical Physics*, Lecture Notes in Physics 39, 1975, pp. 420–422. https://doi.org/10.1007/BFb0013365
- M. A. Lohe, “Non-Abelian Kuramoto models and synchronization,” *Journal of Physics A: Mathematical and Theoretical* 42 (2009), 395101. https://doi.org/10.1088/1751-8113/42/39/395101
- A. Hatcher, *Algebraic Topology*, Chapter 1, Cambridge University Press, 2002. https://pi.math.cornell.edu/~hatcher/AT/ATch1.pdf
6 thms1 active userReviewed
Captain: Lucas
Local Connectivity of the Mandelbrot Set (MLC)Open Problem
## The set
For a complex parameter $c$, iterate the quadratic map
$$f_c(z) = z^2 + c$$
starting at the critical point $z = 0$. The **Mandelbrot set** is the set of parameters for which this orbit stays bounded:
$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$
Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.
$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism
$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$
between the complement of $M$ and the exterior of the closed unit disk.
## The question
**MLC conjecture.** *$M$ is locally connected*: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.
By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the *pinched disk* model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the **density of hyperbolicity** in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and **zero area for $\partial M$**.
MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.
## Timeline
- **1982** -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
- **1984/85** -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
- **1990** -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
- **1997** -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
- **1997** -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the *real* quadratic family.
- **1998** -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive *area* remains open.
- **2005** -- Buff and Cheritat construct quadratic *Julia* sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
- **Today** -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.
## What this mission asks for
The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".
The milestones are of three kinds, and are ordered accordingly:
1. **Foundations provable today** -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. **Known theorems from the literature** -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. **The open companions** -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.
All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.
16 thms4 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA IV: ContinuityTextbook
## Motivation
Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4
of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) is
about what continuity gives once the domain is compact or connected. Three of its theorems are
used in nearly every later argument of the book: a continuous function on a compact set has
compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a
connected set has connected image (4.22), hence takes intermediate values (4.23); and a
continuous function on a *compact* metric space is **uniformly continuous** (Theorem 4.19) —
the $\delta$ can be chosen independently of the point.
The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to
prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place
where compactness upgrades a pointwise hypothesis into a global one with a quantitative
conclusion.
This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric
topology of Mission II and is a prerequisite for Missions V–VII.
## Setting
Let $X, Y$ be metric spaces, $E \subseteq X$, $f : E \to Y$, and let $p$ be a limit point of
$E$. Rudin writes $\lim_{x \to p} f(x) = q$ when for every $\varepsilon > 0$ there is
$\delta > 0$ with $d_Y(f(x), q) < \varepsilon$ for all $x \in E$ satisfying
$0 < d_X(x,p) < \delta$; the exclusion of $x = p$ is deliberate, and it is what makes the
notion agree with continuity only when $f(p) = q$ (Theorem 4.6). $f$ is **continuous at** $p$
if the same holds with the condition $0 < d_X(x,p)$ dropped, and **continuous** if it is
continuous at every point.
$f$ is **uniformly continuous** on $X$ if for every $\varepsilon > 0$ there is a single
$\delta > 0$ such that $d_Y(f(p), f(q)) < \varepsilon$ for *all* $p, q \in X$ with
$d_X(p,q) < \delta$. A real function on $(a,b)$ is **monotonically increasing** if $x < y$
implies $f(x) \le f(y)$; its one-sided limits are written $f(x-)$ and $f(x+)$, and it has a
**discontinuity of the first kind** at $x$ when both exist but do not agree with $f(x)$.
## Formalization targets
### Goal — uniform continuity on compacta (Theorem 4.19)
$$
X \text{ compact metric space},\ f : X \to Y \text{ continuous}
\;\Longrightarrow\;
\forall \varepsilon > 0\ \exists \delta > 0\ \forall p, q \in X,\
d(p,q) < \delta \Rightarrow d(f(p), f(q)) < \varepsilon .
$$
### Milestones
$$f \text{ continuous at } p \iff \lim_{x \to p} f(x) = f(p) \qquad (4.6)$$
$$f \text{ continuous} \iff f^{-1}(V) \text{ open for every open } V \qquad (4.8)$$
$$K \text{ compact} \Rightarrow f(K) \text{ compact} \qquad (4.14)$$
$$\text{a continuous real } f \text{ on a compact } X \text{ attains } \sup f \text{ and } \inf f \qquad (4.16)$$
$$f : X \to Y \text{ continuous bijection, } X \text{ compact} \Rightarrow f^{-1} \text{ continuous} \qquad (4.17)$$
$$E \text{ connected} \Rightarrow f(E) \text{ connected} \qquad (4.22)$$
$$f(a) < c < f(b) \Rightarrow f(x) = c \text{ for some } x \in (a,b) \qquad (4.23)$$
$$f \text{ monotone} \Rightarrow f(x-),\, f(x+) \text{ exist and } f(x-) \le f(x) \le f(x+) \qquad (4.29)$$
$$\text{the discontinuity set of a monotone function is at most countable} \qquad (4.30)$$
## Significance
Uniform continuity is the hypothesis that converts local approximation into global
approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower
Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the
equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a $C'$
mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the
two existence theorems of elementary analysis, and both come from this chapter by combining
Chapter 2's compactness and connectedness with continuity.
Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result
that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book
where a countability argument (Chapter 2) pays off analytically.
Mathlib has continuity, compactness and connectedness in general topological spaces, and most
of the milestones can be matched to library results after the statements are put in Rudin's
metric form. The formalization value is again in the dictionary: Rudin's punctured-limit
definition versus `ContinuousWithinAt`, and his $\varepsilon$–$\delta$ uniform continuity versus
the library's uniformity-filter definition.
## Difficulty
There is no single hard step; the difficulty is in the hypotheses being weaker than they look.
In Theorem 4.6 the limit is taken through $E \setminus \{p\}$, so the equivalence with
continuity genuinely needs $p \in E$ *and* $p$ a limit point; dropping the second hypothesis
makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick $\delta_p$
at each point by continuity and take the infimum — fails because the infimum over infinitely
many points can be $0$; compactness is used to reduce to finitely many, and the factor of two
in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the
discontinuity set into $\mathbb{Q}$, built from the gap between $f(x-)$ and $f(x+)$.
## Formalization scope
Conventions fixed by this mission:
* Continuity is Mathlib's `Continuous`, `ContinuousOn`, `ContinuousWithinAt`; Rudin's
$\lim_{x\to p} f(x) = q$ along $E$ is `Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q)`.
* Uniform continuity is `Rudin.UniformlyContinuous`, stated with explicit $\varepsilon$ and
$\delta$ as in Definition 4.18, rather than through the uniformity filter.
* Limit points are `Rudin.IsLimitPoint` from the Chapter 2 mission, so the two missions share
one notion.
* Compactness of the domain in 4.16, 4.17 and 4.19 is the typeclass `[CompactSpace X]`, matching
Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is
the form later missions use.
* Monotone functions are `MonotoneOn f (Set.Ioo a b)`; one-sided limits are `𝓝[<] x` and
`𝓝[>] x` filters, and 4.29 also identifies them with the supremum and infimum of the
corresponding one-sided images, as Rudin does.
The goal is not vacuous and does not follow by unfolding: uniform continuity fails for
continuous functions on non-compact domains (e.g. $x \mapsto x^2$ on $\mathbb{R}$, or
$x \mapsto 1/x$ on $(0,1)$), so compactness is doing the work.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 4 (pp. 83–101).
11 thms2 active usersReviewed
🏆Completed
Captain: dbenbenn
Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than oneResearch Paper
## Motivation
[Von Neumann introduced amenability in 1929](http://eudml.org/doc/211921) in response to the
Banach–Tarski paradox: a group is **amenable** when it carries a finitely additive,
translation-invariant probability measure on its subsets, and no amenable group contains a free
subgroup of rank $2$ — which is exactly what the paradox needs. The converse is the **von
Neumann conjecture**, and it is false: [Ol'shanskii](https://doi.org/10.1070/rm1980v035n04abeh001876) in 1980 and
[Adyan](https://doi.org/10.1070/im1983v021n03abeh001799) in 1982 produced finitely generated
counterexamples. A *finitely
presented* counterexample was harder, and one candidate stood out — **Richard Thompson's group
$F$**, finitely presented, with nobody able to decide whether it was amenable.
Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that
$F$, and more generally the group $\mathrm{PLF}(\mathbb{R})$ of piecewise-linear homeomorphisms
of the line with finitely many breakpoints, contains no free subgroup of rank greater than $1$.
Whether $F$ is amenable they could not determine, and it is still open today; claimed proofs
have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes
([Ol'shanskii–Sapir 2002](https://doi.org/10.1007/s10240-002-0006-7);
[Lodha–Moore 2016](https://doi.org/10.4171/ggd/347)), so $F$
is no longer needed as a candidate. This mission formalizes the half that *was* settled.
## Setting
Let $\mathrm{Homeo}_+(\mathbb{R})$ be the **group of orientation-preserving homeomorphisms** of
the line: the strictly increasing bijections $\mathbb{R}\to\mathbb{R}$ under composition. The
**support** of $f$ is the set of points it moves, $\operatorname{supp} f = \{\,t : f(t)\neq t\,\}$, an open subset of $\mathbb{R}$.
A continuous $f$ is **piecewise linear** when there is a *discrete* set $B$ of **breakpoints**
with $f$ differentiable off $B$ and $f'$ constant on each component of $\mathbb{R}\setminus B$;
for finite $B$ this is the same as $f$ being affine on a neighbourhood of every point outside
$B$. Nothing is required at the points of $B$, so the two affine pieces meeting at a breakpoint
may disagree — that is what makes such an $f$ more than an affine map. Write
$\mathrm{PL}(\mathbb{R})$ for the piecewise-linear elements of $\mathrm{Homeo}_+(\mathbb{R})$
and
$$\mathrm{PLF}(\mathbb{R}) = \{\, f \in \mathrm{PL}(\mathbb{R}) : f \text{ has a finite
breakpoint set} \,\}$$
for the subgroup this mission is about. The distinction matters: the goal below holds in
$\mathrm{PLF}(\mathbb{R})$ and fails in $\mathrm{PL}(\mathbb{R})$, where Brin and Squier build
free subgroups of rank $2$ by lifting them from the circle. Write $\mathrm{PLF}'(\mathbb{R})$ for the commutator subgroup, which Brin and Squier identify
as the elements whose **slope at each end** is $1$ — an element has slope $a$ at an end when it
agrees with a single affine map of slope $a$ on a ray out to that end. **Thompson's group $F$** — the piecewise-linear homeomorphisms of $[0,1]$ with dyadic
breakpoints and power-of-two slopes — is realized inside $\mathrm{PLF}(\mathbb{R})$.
## Formalization targets
### Goal — no two elements generate freely
$$\text{for } f,g \in \mathrm{PLF}(\mathbb{R}), \quad F_2 \to \mathrm{PLF}(\mathbb{R}),\
a \mapsto f,\ b \mapsto g \quad\text{is never injective.}$$
Since a free group of rank greater than $1$ contains one of rank $2$, this is Brin and Squier's
Theorem (3.1).
### The dichotomy it rests on
$$G \le \mathrm{PLF}'(\mathbb{R}) \implies G \text{ abelian, or } G \text{ contains a free
abelian subgroup of rank } 2.$$
Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is
infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the
full-strength (3.2) are milestones of their own here. The goal itself only ever uses the
rank-two form.
### The twenty-four milestones
Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in
its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and
published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2)
both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3),
likewise in both strengths. Five are piecewise-linear infrastructure the source treats as
routine: closure of $\mathrm{PLF}(\mathbb{R})$ under composition and under inverse, the same two
for slope $1$ at each end, and finiteness of the number of components of a support. Five more are
steps the source asserts without proof — that the line carries no non-fixed periodic points, that
a map fixing a set's complement preserves its components, that the iterated images of a
pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays
inside the union of the two supports (p. 495), and that the derived subgroup of a free group of
rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian
subgroup of a free group is cyclic, which is what lets the goal finish through
Nielsen–Schreier.
## Significance
The theorem closes the standard route to proving a group **non**-amenable. To show a group
amenable the classical routes are elementary amenability and subexponential growth, and $F$ is
neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth,
having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route
is to exhibit a free subgroup of rank $2$ — the route this theorem closes. $F$ sits in the gap,
which is why its status has survived sustained attention.
The result reaches past $F$. Monod's groups of piecewise *projective* homeomorphisms are
counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no
non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the
corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof
that paper says it will "largely follow [Brin–Squier, § 3]".
**What formalizing it adds.** Mathlib has no piecewise-linear maps and no [amenability predicate for
groups](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Group/FoelnerFilter.lean). This mission builds the piecewise-linear layer: a workable $\mathrm{PLF}(\mathbb{R})$, its
closure properties, and the structure of supports.
## Difficulty
The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the
breakpoint set is what gives an element slopes at $\pm\infty$ at all, and what makes two elements
affine on each side of a common fixed point. Compactness is the other — throughout, $[f,g] = fgf^{-1}g^{-1}$ — and it splits: that the closure of $\operatorname{supp}[f,g]$ is
compact needs only slope $1$ at each end, with no piecewise linearity at all, which is why
(2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays
inside $\operatorname{supp} f \cup \operatorname{supp} g$ is what reaches back to finiteness. Keeping straight which
fact does which job is most of the work.
The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that
makes them commute: only their intersections with one chosen component are disjoint, and
commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.
## Formalization scope
**What the Lean fixes.** Elements are order isomorphisms of $\mathbb{R}$ — strictly increasing
bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows
Mathlib's convention $(f\cdot g)(x) = f(g(x))$, the opposite of the source's right action, so the
conjugation identity reads $\operatorname{supp}(fgf^{-1}) = f(\operatorname{supp} g)$ here;
getting this backwards states a different theorem that still compiles. A support is the bare
moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with
local affineness off it — the set need not be minimal and may be empty.
A copy of $\mathbb{Z}^2$ is an injectivity statement about $(m,n)\mapsto u^m v^n$, not a subgroup
isomorphism, and the goal is about a single pair $f,g$ rather than a subgroup. The dichotomy
hypothesises slope $1$ at both ends directly, not membership in a derived subgroup — that these
coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and
the identification asserted on p. 493 gives the other.
Beyond a workable $\mathrm{PLF}(\mathbb{R})$, the development needs Nielsen–Schreier, already
in Mathlib as `subgroupIsFreeOfIsFree`: it is what lets an abelian subgroup of a free group be
cyclic, and so lets the goal finish without the source's metabelian ending. That ending is
formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a
free group of rank two is non-abelian; the goal simply does not route through it.
**One trivializing reading is ruled out.** Slope $1$ at both ends is not a compact-support
condition — every translation satisfies it — so (3.2) is not secretly a statement about
compactly supported maps.
**Nothing is built for $F$ specifically**, and amenability is not touched. That is the one piece
deliberately omitted, and contributions are welcome on it: modelling $F$ and embedding it in
$\mathrm{PLF}(\mathbb{R})$. The piecewise-linear layer is reusable beyond this theorem — Thompson's groups $T$ and
$V$, and piecewise-linear topology generally, need exactly it.
## Selected references
- M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line,
Invent. math. **79** (1985), 485–498, [doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519). Theorem (3.1) is the goal.
- J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups,
L'Enseignement Mathématique **42** (1996), 215–256. Theorem 4.10 and Corollary 4.7.
- N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA **110**
(2013), 4524–4527, [arXiv:1209.5229](https://arxiv.org/abs/1209.5229).
- A. Yu. Ol'shanskii and M. V. Sapir, Non-amenable finitely presented torsion-by-cyclic groups,
Publ. Math. IHÉS **96** (2002), 43–169, [doi:10.1007/s10240-002-0006-7](https://doi.org/10.1007/s10240-002-0006-7).
- Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective
homeomorphisms, Groups Geom. Dyn. **10** (2016), 177–200, [doi:10.4171/ggd/347](https://doi.org/10.4171/ggd/347).
- V. Guba, Amenability problem for Thompson's group $F$: state of the art, J. Groups Complex.
Cryptol. **15** (2023), [arXiv:2305.07113](https://arxiv.org/abs/2305.07113).
32 thms2 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA II: Basic TopologyTextbook
## Motivation
Convergence, continuity and integration are all statements about *nearness*, and Chapter 2 of
Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) isolates
the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a
single theorem, **Heine–Borel** (Theorem 2.41), which says that in $\mathbb{R}^k$ — and, as the
chapter's examples show, only in spaces resembling it — three very different-looking finiteness
conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every
infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a
continuous function on $[a,b]$ attains its maximum, is uniformly continuous, is
Riemann-integrable) is an application of that equivalence.
This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the
number systems of Mission I and supplies the topological input for Missions III–VII.
## Setting
A **metric space** is a set $X$ with a distance $d : X \times X \to \mathbb{R}$ that is
positive for distinct points, symmetric, and satisfies the triangle inequality. The
**neighbourhood** $N_r(p)$ is the set of $q$ with $d(p,q) < r$. A point $p$ is a **limit
point** of $E \subseteq X$ if every neighbourhood of $p$ contains a point of $E$ different
from $p$; $E$ is **closed** if it contains all its limit points, **open** if each of its points
has a neighbourhood inside $E$, and its **closure** $\bar E$ is $E$ together with its limit
points. $E$ is **perfect** if it is closed and every point of $E$ is a limit point of $E$, and
**bounded** if it is contained in some neighbourhood.
An **open cover** of $E$ is a family of open sets whose union contains $E$; $K$ is **compact**
if every open cover of $K$ has a finite subcover. A **$k$-cell** is a product
$\{x \in \mathbb{R}^k : a_j \le x_j \le b_j \text{ for all } j\}$. Two sets $A, B$ are
**separated** if $\bar A \cap B = A \cap \bar B = \varnothing$, and $E$ is **connected** if it
is not the union of two nonempty separated sets.
## Formalization targets
### Goal — Heine–Borel (Theorem 2.41)
For $E \subseteq \mathbb{R}^k$, the following are equivalent:
$$
\text{(a) } E \text{ closed and bounded} \quad\Longleftrightarrow\quad
\text{(b) } E \text{ compact} \quad\Longleftrightarrow\quad
\text{(c) every infinite } S \subseteq E \text{ has a limit point in } E .
$$
### Milestones
$$\textstyle\bigcup_n E_n \text{ countable when each } E_n \text{ is} \qquad (2.12)$$
$$\{0,1\}^{\mathbb{N}} \text{ is uncountable} \qquad (2.14)$$
$$\text{arbitrary unions of open sets, finite intersections of open sets, and the closed duals} \qquad (2.24)$$
$$\bar E = E \cup E', \quad \bar E \text{ closed}, \quad \bar E = E \Leftrightarrow E \text{ closed}, \quad E \subseteq F \text{ closed} \Rightarrow \bar E \subseteq F \qquad (2.27)$$
$$\sup E \in \bar E \qquad (2.28)$$
$$\text{open-cover compactness} \Leftrightarrow \text{compactness} \qquad (2.32)$$
$$F \subseteq K,\ F \text{ closed},\ K \text{ compact} \Rightarrow F \text{ compact} \qquad (2.35)$$
$$\text{finite intersection property for compact sets} \qquad (2.36)$$
$$\text{infinite } E \subseteq K \text{ compact} \Rightarrow E \text{ has a limit point in } K \qquad (2.37)$$
$$\text{nested } k\text{-cells have a common point} \qquad (2.39)$$
$$\text{every } k\text{-cell is compact} \qquad (2.40)$$
$$\text{nonempty perfect } P \subseteq \mathbb{R}^k \text{ is uncountable} \qquad (2.43)$$
$$E \subseteq \mathbb{R} \text{ connected} \Leftrightarrow (x,y \in E,\ x<z<y \Rightarrow z \in E) \qquad (2.47)$$
## Significance
Heine–Borel is the bridge between the order completeness of $\mathbb{R}$ established in
Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves
$k$-cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass,
Theorem 2.42), and compactness is what converts local information into global statements.
Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set
is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the
connected subsets of the line as the order-convex ones, is the topological content of the
intermediate value theorem proved in Chapter 4.
Mathlib has an extensive metric-space and compactness library, so much of this chapter exists
there in some form. What this mission adds is the explicit correspondence with Rudin's
formulations: his open-cover definition of compactness against the library's filter-based
`IsCompact` (a milestone in its own right), his $\varepsilon$-style limit points against
`closure`, and his $k$-cells against the library's boxes. The resulting dictionary is what the
remaining missions in the series use when they need a compactness argument.
## Difficulty
The mathematics is standard, and the difficulty is almost entirely in the translation layer.
Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the
statement is a $\Pi$-type over families of sets, while Mathlib's `IsCompact` is a statement
about filters; the equivalence is available in the library but only after the cover is
presented in the right indexed form. Second, "limit point" in Rudin's sense is *not*
`p ∈ closure E`: the point must be approached by points of $E$ *other than* $p$, so isolated
points of $E$ are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two
notions are conflated.
## Formalization scope
Conventions fixed by this mission:
* Metric spaces are Mathlib's `[MetricSpace X]`; `IsOpen`, `IsClosed`, `closure`, `Perfect`,
`IsCompact`, `Bornology.IsBounded` and `IsPreconnected` are used for Rudin's corresponding
notions.
* Rudin's limit points are `Rudin.IsLimitPoint p E`, defined with the explicit $\varepsilon$
and the condition $q \ne p$, and his open-cover compactness is `Rudin.IsCoverCompact`.
* $k$-cells are `Rudin.kCell k a b` inside `EuclideanSpace ℝ (Fin k)`; the case where some
$a_j > b_j$ gives the empty set, which is why the nested-cell milestone assumes each cell is
nonempty, exactly as Rudin's construction does.
* Connectedness is `IsPreconnected`, which admits the empty set, matching Rudin's convention
that a set is connected unless it splits into two *nonempty* separated pieces.
* The Heine–Borel goal is stated as a `TFAE` list in Rudin's order (a), (b), (c).
The equivalence is not vacuous: all three conditions are satisfied by any $k$-cell and all
three fail for $\mathbb{R}^k$ itself when $k \ge 1$.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 2 (pp. 24–55).
- The mathlib Community, *The Lean Mathematical Library*, CPP 2020.
https://doi.org/10.1145/3372885.3373824
15 thms2 active usersReviewed
Captain: Xinze-Li-Moqian
Formalization of the Poincaré ConjectureResearch Paper
**Our goal**
This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's [Notes on Perelman's Papers](https://arxiv.org/abs/math/0605667).
**Important references**
[Poincare-Conjecture](https://github.com/frenzymath/Poincare-Conjecture) and [DifferentialGeometry](https://github.com/qinz1yang/differential-geometry) are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.
**OpenGA's role**
[OpenGA](https://github.com/MathNetwork/OpenGA) focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.
The `PoincareConjecture` directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.
We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.