Winding Arithmetic II: Conserved Phase BasesResearch Paper
## Motivation
Winding number is a topological integer: continuous deformation preserves it, while crossing a branch cut or registering a reset can change it by an integer amount. Transcendence theory gives a different kind of rigidity. For a nonzero algebraic coupling $\alpha$, the phases $e^{i\alpha n}$ attached to distinct integers $n$ are linearly independent over the field $\overline{\mathbb Q}$ of algebraic complex numbers. This mission joins those statements at their exact formal interfaces.
The result is useful wherever a model first produces an integer winding label and then represents that label by a complex phase. Topology supplies the discrete coordinate, dynamics determines when it is conserved or reset, and Lindemann–Weierstrass supplies arithmetic distinguishability. None of those layers is asked to manufacture the others.
The foundation comes from three completed private missions: *Winding Dynamics I: Homotopy Conservation and Reset Balance*, *Integer Winding Transcendence I: Exponential Phase Independence*, and *Lindemann–Weierstrass I: Exponential Independence*. The transcendence proof is an attributed Lean 4.30-compatible port of Yuyang Zhao's [mathlib PR #28013](https://github.com/leanprover-community/mathlib4/pull/28013).
## Setting
Let $S^1$ be the complex unit circle. A **based Circle loop** is a continuous path in $S^1$ that starts and ends at $1$. Its canonical real lift through the exponential covering starts at $0$; the lift endpoint determines an integer $\operatorname{wind}(\gamma)$.
For $\beta\in\mathbb C$ and $n\in\mathbb Z$, define the **integer exponential character**
$$
\chi_\beta(n)=\exp(n\beta).
$$
The arithmetic consumer uses $\beta=i\alpha$, where $\alpha$ is nonzero and algebraic over $\mathbb Q$. Thus a loop $\gamma$ carries the phase $\chi_{i\alpha}(\operatorname{wind}(\gamma))$.
A **closed Circle field** is a jointly continuous map on the time/spatial square $I\times I$ whose two spatial endpoints agree at every time. Each spatial slice is normalized by its moving basepoint, producing a based loop. A **carrier/readout segment** generalizes this: an ambient trajectory remains in a registered carrier subspace and is observed through a continuous map from that carrier to $S^1$.
The discontinuous branch is represented separately by a finite **reset ledger**. It stores successive integer edge-turn cochains. Pairing those cochains with a certified closed edge cycle produces integer winding values and reset periods.
## Formalization targets
### Circle winding separates algebraic phases
For a family of loops $(\gamma_j)_{j\in J}$ with pairwise-distinct windings,
$$
\left(e^{i\alpha\operatorname{wind}(\gamma_j)}\right)_{j\in J}
\text{ is linearly independent over }\overline{\mathbb Q}.
$$
### Continuous evolution preserves the phase basis
If the initial windings of a family of closed Circle fields are distinct, then the initial phase family is linearly independent, every phase is unchanged between endpoint times, and the final phase family remains linearly independent. The same conclusion is exposed through the carrier/readout interface.
### Reset balance becomes phase factorization
If a reset ledger has endpoint winding change $W_{\mathrm f}-W_{\mathrm i}$ and registered reset periods $\Delta W_j$, then
$$
\chi_\beta(W_{\mathrm f}-W_{\mathrm i})
=\prod_j\chi_\beta(\Delta W_j).
$$
This is the multiplicative image of the exact additive ledger balance.
### The phase readout is faithful
For nonzero algebraic $\alpha$, the character $\chi_{i\alpha}$ is injective on
$\mathbb Z$. Consequently, two actual Circle loops have equal algebraic phase
readouts exactly when they have equal canonical winding. On the reset branch,
$$
\prod_j\chi_{i\alpha}(\Delta W_j)=1
\quad\Longleftrightarrow\quad W_{\mathrm f}=W_{\mathrm i}.
$$
Thus the multiplicative reset record detects zero net winding change without
losing integer information.
## Significance
The main theorem upgrades conservation of a single integer to conservation of an arithmetic basis. Distinct homotopy classes do not merely retain distinct integer labels: after the algebraic exponential readout, the corresponding phases admit no nontrivial finite linear relation with algebraic coefficients. This lets downstream consumers treat a family of winding sectors as a linearly independent family over $\overline{\mathbb Q}$.
The reset theorem provides the matching event law. Continuous evolution preserves the basis, whereas a registered reset multiplies phases according to the reset periods. The two branches share one character but retain different hypotheses, so a discontinuous ledger event is not misrepresented as a continuous homotopy.
The algebraic readout is also faithful: despite taking values on the complex
exponential curve, it neither aliases two winding sectors nor hides a nonzero
net reset behind total phase $1$ under the stated algebraic hypothesis.
This does not establish a particle–wave duality or a quantum-mechanical interpretation. It establishes a precise mathematical analogy: an integer topological label has a complex character representation whose distinct values enjoy a strong arithmetic independence theorem under an algebraic nonresonance condition.
## Difficulty
The individual deductions are short only because three difficult interfaces have already been proved. Replacing an arbitrary integer map by actual Circle winding requires using the canonical covering lift rather than postulating labels. Preserving the phase basis requires transporting injectivity and linear independence through a jointly continuous moving-basepoint normalization. The reset branch requires respecting the sign convention and mapping a finite sum to a finite product, including the empty ledger.
Several tempting statements would be false. Duplicate winding labels cannot give a linearly independent family. The exponent $\alpha=0$ collapses every phase to $1$. Continuity of finitely many vertex phases does not by itself define a continuous spatial Circle field, and crossing the principal cut can change a discrete principal-turn winding. A global readout from a simply connected carrier such as all of $SU(2)$ cannot support nonzero loop winding without a separately registered non-simply-connected subcarrier or channel.
For a general complex coupling, exponential resonance can destroy injectivity.
The nonzero algebraic hypothesis excludes that resonance here through the
proved Lindemann--Weierstrass theorem; it is not merely a convenient side
condition.
## Formalization scope
All artifacts use Lean 4.30 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`. The Circle winding is the floor of the canonical zero-based lift endpoint divided by $2\pi$. Closed fields live on $I\times I$ and are normalized at spatial coordinate zero. The coupling $\alpha$ is an arbitrary complex algebraic number, not necessarily real, and must be nonzero.
The main carrier/readout theorem is conditional on an explicit continuous carrier-valued trajectory, closed spatial slices, and continuous Circle readout. It does not prove existence of a Kuramoto, XY, or Lohe solution, nor preservation of a particular carrier by such an ODE. Those are model-specific successors.
The reset factorization consumes the registered coherent ledger and certified closed cycle. It is an exact algebraic event law, not an energy estimate and not a claim that every physical trajectory realizes such a ledger. Its vertex and edge types retain the universe-zero scope of the existing reset interface.
## Selected references
- Yuyang Zhao, *The Lindemann–Weierstrass theorem*, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
- Nathan Jacobson, *Basic Algebra I*, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
- Allen Hatcher, *Algebraic Topology*, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
13 thms1 active userReviewed
🏆Completed
Captain: lisamegawatts
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
🏆Completed
Captain: dbenbenn
Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroupTextbook
## Motivation
This mission formalizes §4 of Cannon, Floyd and Parry's *Introductory notes on Richard
Thompson's groups*, together with the definition of **Thompson's group $F$** from their §1.
The goal is their Theorem 4.5: the commutator subgroup $[F,F]$ is simple.
In the 1960s Richard Thompson defined three groups, now written $F$, $T$ and $V$, whose
properties have kept them in use ever since as a source of examples at the edge of what
groups can do. $F$ is the smallest of the three and the least understood. It is finitely
presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and
whether it is **amenable** — whether it carries a finitely additive left-invariant probability
measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that
Geoghegan raised the question and conjectured in 1979 both that $F$ contains no non-Abelian
free subgroup and that $F$ is not amenable.
That question is what makes $F$ worth pinning down precisely. Write $AG$ for the class of
amenable discrete groups, $EG$ for the elementary amenable ones, and $NF$ for the groups with
no free subgroup of rank two. That $AG \subset NF$ was noted by
[Day](https://doi.org/10.1215/ijm/1255380675) and follows from
[von Neumann](https://doi.org/10.4064/fm-13-1-73-116); whether it is strict is the **von
Neumann–Day problem**. It is: Olshanskii proved $AG \neq NF$ in a 1984 ICM address and
[Gromov](https://doi.org/10.1007/978-1-4613-9586-7_3) gave an independent proof — but by
examples that are not finitely presented. Brin and Squier proved in 1985 that $F \in NF$, and
$F$ is known not to be elementary amenable (Theorem 4.10 of the source, out of scope here). So
$F$ is a finitely presented group in $AG \setminus EG$ if it is amenable and in
$NF \setminus AG$ if it is not — a question with no other finitely presented candidate.
## Setting
Call a real number **dyadic** if it has the form $m/2^{k}$ with $m \in \mathbb{Z}$ and
$k \in \mathbb{N}$.
**Thompson's group $F$**, as §1 of the source defines it, is the set of piecewise linear
homeomorphisms of the closed unit interval $[0,1]$ onto itself that are differentiable except
at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of $2$.
Since those derivatives are positive, every element preserves orientation, so the elements of
$F$ are increasing. Composition of two such maps is again one, and so is the inverse of one,
so $F$ is a group.
The formalization calls such a map **piecewise linear over the dyadics**, and defines $F$ as
the subgroup *generated by* those maps — so that closure under composition and inverses is a
theorem rather than part of the construction, as the source has it. What the model fixes rather
than derives is under **Formalization scope** below.
Two particular elements generate it. Write
$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\ 2x-1 & \tfrac34 \le x \le 1\end{cases}
\qquad
B(x) = \begin{cases} x & 0 \le x \le \tfrac12 \\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34 \\ x - \tfrac18 & \tfrac34 \le x \le \tfrac78 \\ 2x-1 & \tfrac78 \le x \le 1.\end{cases}$$
An element of $F$ is **trivial near $0$** if it fixes every point of some interval
$[0,\varepsilon)$, and **trivial near $1$** if it fixes every point of some
$(1-\varepsilon, 1]$. The **support** of $f$ is the set of points of $[0,1]$ that $f$ moves.
The commutator convention throughout is $[x,y] = xyx^{-1}y^{-1}$, and $[F,F]$ denotes the
commutator subgroup.
## Formalization targets
### Goal
$$[F,F] \ \text{is a simple group.}$$
This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than
itself and the trivial one. It is the goal because the rest of the section feeds it — both
halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its
proof.
### Theorem 4.1, which has two parts
$$[F,F] \;=\; \{\, f \in F : f \text{ is trivial near } 0 \text{ and near } 1 \,\}$$
$$F/[F,F] \;\cong\; \mathbb{Z} \oplus \mathbb{Z}$$
### Theorem 4.3
$$N \trianglelefteq F,\ N \neq 1 \;\Longrightarrow\; F/N \text{ is Abelian}$$
So $F$ has no interesting proper quotients at all. With the first part of Theorem 4.1 this
forces every nontrivial normal subgroup of $F$ to contain $[F,F]$.
### Supporting results
That the piecewise-linear maps are already closed under composition and inverses, so that $F$
consists of exactly those maps; a transitivity lemma on dyadic partitions of $[0,1]$; the fact
that the subgroup of elements supported in a dyadic interval $[a,b]$ of dyadic length is
isomorphic to $F$ itself; triviality of the center; that $F$ contains no non-Abelian free group;
and that $F$ admits a total order invariant under multiplication on both sides.
## Significance
**What the results give.** Theorem 4.1 identifies $[F,F]$ concretely — a subgroup defined by a
global algebraic condition turns out to be cut out by local behavior at the two endpoints —
and computes the abelianization, making the pair of endpoint slopes a complete invariant of $F$
modulo commutators. Theorem 4.3 and the simplicity of $[F,F]$ together determine the whole
normal subgroup lattice: every normal subgroup of $F$ is trivial or contains $[F,F]$. That
lattice is the input to the elementary-amenability argument.
**What formalizing adds.** All of these are proved in the source; none is in Mathlib, which
has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are
proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements
of $F$ permute the dyadic rationals, that $F$ embeds in the group Brin and Squier work with, and
the absence of a free subgroup of rank two, which follows from the already-formalized
Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness,
dyadic-breakpoint bookkeeping, extension by the identity — is reusable for $T$, for $V$, and
for the wider family of piecewise-linear homeomorphism groups.
## Difficulty
The obvious approach to the goal is to argue that a normal subgroup of $[F,F]$ containing a
nontrivial element must be everything, by conjugating that element around. It fails on its own:
an element of $[F,F]$ is pinned down only by being trivial near the two endpoints, and one still
has to manufacture — inside $[F,F]$, not merely inside $F$ — an element carrying a prescribed
pair of neighborhoods into those. That construction is what the dyadic-partition transitivity
lemma supplies, and it is where the combinatorics of dyadic subdivision enters.
The second difficulty was that the source proves §4 using the tree-diagram normal form of §2.
That section is now formalized in its own mission, *Cannon–Floyd–Parry §2: tree diagrams and the
normal form* (mission `ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8`), all of whose milestones are proved.
Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem
2.5 (`represents_word_exponents`) and the normal form (`existsUnique_normalForm`) are available to
a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file
imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions
are public and written to be reused that way. The piecewise-linear route — dyadic-partition
transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own
argument uses.
## Formalization scope
The unit interval is $[0,1] \subseteq \mathbb{R}$ as a subtype, and an element of $F$ is an
order isomorphism of it, so orientation preservation is built into the representation rather
than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise
linearity is stated as: there is a finite set $B$ of dyadic reals such that the map is affine,
with slope a power of two, on every closed interval whose interior misses $B$. Intercepts are
**not** required to be dyadic — that is derived by induction along the breakpoints, not part of
the definition.
The definition is not vacuous: $A$ and $B$ of Example 1.1 are constructed explicitly, and that
$F$ is not the trivial group is one of the milestones below — so no statement here is satisfied
by the trivial group. In particular the goal, which asserts simplicity and therefore
nontriviality, is not trivially false.
A companion definition places the same data on the real line, each element extended by the
identity outside $[0,1]$; that line realisation is what the bridge statement connects to Brin
and Squier's group. Corollaries 4.6, 4.7 and 4.10 of the source are out of scope: they need free
products of monoids, growth of finitely generated groups, and the transfinite class of
elementary amenable groups respectively, none of which Mathlib has.
## Selected references
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Mathématique (2) **42** (1996), 215–256.
[doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877)
- M. G. Brin, C. C. Squier, *Groups of piecewise linear homeomorphisms of the real line*,
Inventiones Mathematicae **79** (1985), 485–498.
[doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519)
- C. Chou, *Elementary amenable groups*, Illinois Journal of Mathematics **24** (1980), 396–407.
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)
- M. M. Day, *Amenable semigroups*, Illinois Journal of Mathematics **1** (1957), 509–544.
[doi:10.1215/ijm/1255380675](https://doi.org/10.1215/ijm/1255380675)
- J. von Neumann, *Zur allgemeinen Theorie des Maßes*, Fundamenta Mathematicae **13** (1929),
73–116. [doi:10.4064/fm-13-1-73-116](https://doi.org/10.4064/fm-13-1-73-116)
- A. Yu. Olshanskii, *On a geometric method in the combinatorial group theory*, Proceedings of
the International Congress of Mathematicians (Warsaw, 1983), vol. 1, 1984, pp. 415–424.
[IMU archive](https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1983.1/ICM1983.1.ocr.pdf)
- M. Gromov, *Hyperbolic groups*, in *Essays in Group Theory* (S. M. Gersten, ed.), MSRI
Publications **8**, Springer, 1987, pp. 75–263.
[doi:10.1007/978-1-4613-9586-7_3](https://doi.org/10.1007/978-1-4613-9586-7_3)
34 thms3 active usersReviewed
🏆Completed
Captain: Lucas
An Introduction to Chaotic Dynamical Systems II: Sarkovskii's TheoremTextbook
## Motivation
In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is
remarkable both for how little it assumes — continuity, nothing more — and for how much it
concludes: the set of periods of the periodic orbits of such a map is completely constrained
by a single linear ordering of the positive integers. Its best-known corollary, rediscovered
by Li and Yorke in 1975 under the slogan *period three implies chaos*, says that a continuous
map of $\mathbb{R}$ with an orbit of period three has orbits of every period.
Devaney presents the theorem in §1.10 of *An Introduction to Chaotic Dynamical Systems* (2nd
edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the
elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering
relations. This mission is the second in a series formalizing the book; it is independent of
the first, sharing only the book-wide namespace.
Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely
unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave
the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave
the short interval-covering proofs, the latter being the one Devaney reproduces.
## Setting
Let $f : \mathbb{R} \to \mathbb{R}$ be continuous. A point $x$ has **prime period** $n \ge 1$
if $f^{n}(x) = x$ and $f^{m}(x) \ne x$ for every $0 < m < n$.
The **Sarkovskii ordering** of the positive integers is
$$3 \,\triangleright\, 5 \,\triangleright\, 7 \,\triangleright\, \cdots \,\triangleright\,
2\cdot 3 \,\triangleright\, 2\cdot 5 \,\triangleright\, \cdots \,\triangleright\,
2^2\cdot 3 \,\triangleright\, 2^2 \cdot 5 \,\triangleright\, \cdots \,\triangleright\,
2^3 \,\triangleright\, 2^2 \,\triangleright\, 2 \,\triangleright\, 1 :$$
first the odd numbers greater than one in increasing order, then $2$ times the odds, then
$2^2$ times the odds, and so on; the powers of two come last, in decreasing order. Writing
$k = 2^{a}p$ and $\ell = 2^{b}q$ with $p, q$ odd, $k \triangleright \ell$ holds exactly when
either $p, q > 1$ and $(a,p)$ precedes $(b,q)$ lexicographically, or $p > 1$ and $q = 1$, or
$p = q = 1$ and $b < a$.
Two elementary facts drive the proof. If $I$ is a closed interval with $f(I) \supseteq I$,
then $f$ has a fixed point in $I$; and if closed intervals satisfy
$f(A_i) \supseteq A_{i+1}$ for $i < n$, then some point of $A_0$ has $f^{i}(x) \in A_i$ for all
$i \le n$. One writes $I \to J$, "$f(I)$ covers $J$", for $J \subseteq f(I)$.
## Target
The goal is Devaney's Theorem 10.2: for continuous $f : \mathbb{R} \to \mathbb{R}$,
$$\text{if } f \text{ has a point of prime period } k \text{ and } k \triangleright \ell,
\text{ then } f \text{ has a point of prime period } \ell .$$
The milestones are the steps of the book's proof: the two covering observations, the
period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed
case $p \cdot 2^m$ into which the general theorem is decomposed, the remark that a period which
is not a power of two forces infinitely many periodic points, and the converse direction,
witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.
## Significance
Sarkovskii's theorem is the sharpest general statement known about the period structure of
one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no
stronger implication holds. Its first consequence — only powers of two can occur as the set of
periods of a map with finitely many periodic points — is what makes the period-doubling
cascade the canonical route to chaos, a theme the book returns to in §1.17.
The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by
$120^\circ$ has every point of period three and no other period.
Formalizing it contributes a reusable Lean treatment of interval covering relations and of the
Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and
the covering machinery is exactly what §1.13 and §1.16 of the book reuse.
## Difficulty
The period-three case is a short argument once the covering observations are available, and it
is a reasonable first milestone. The general theorem is not: the odd case requires choosing the
right interval $I_1 = [x_i, x_{i+1}]$ on the orbit, building the increasing family of unions
$O_\ell$ of covered intervals, and showing that the shortest return loop has length exactly
$n-1$ — a combinatorial argument on the cyclic order of the orbit that is easy to draw and
tedious to formalize. Attempts to shortcut the ordering with a naive induction on $n$ fail:
the statement for $n$ genuinely depends on the geometric arrangement of the orbit points.
## Formalization scope
1. Periodicity is *prime* period throughout: $f^n(x) = x$ together with minimality of $n$. The
statements would be false or trivial with "period" read as "fixed by $f^n$".
2. The Sarkovskii relation is defined arithmetically, in terms of the $2$-adic valuation and
the odd part of an integer, rather than as a listed order; it is a strict relation, so
$k \triangleright k$ is false and the goal theorem says nothing about $\ell = k$ (which
holds by hypothesis anyway).
3. $0$ is outside the ordering: the relation is false whenever either argument is $0$.
4. Intervals in the covering lemmas are closed intervals $[a,b]$ with $a \le b$, given by their
endpoints; "covers" means containment of the interval in the *image*, $J \subseteq f(I)$.
5. The converse milestone asserts the existence of a continuous map with a period-five point
and no period-three point; the book's witness is piecewise linear on $[1,5]$, but the
statement does not prescribe it.
## Selected references
- Robert L. Devaney, *An Introduction to Chaotic Dynamical Systems*, 2nd edition, Westview
Press, 2003 (ISBN 0-8133-4085-3) — §1.10, pp. 60–68. The mission's primary source.
- T. Y. Li and J. A. Yorke, *Period three implies chaos*, American Mathematical Monthly 82
(1975), 985–992, DOI:
[10.1080/00029890.1975.11994008](https://doi.org/10.1080/00029890.1975.11994008).
- L. Block, J. Guckenheimer, M. Misiurewicz, L. S. Young, *Periodic points and topological
entropy of one-dimensional maps*, in Global Theory of Dynamical Systems, Lecture Notes in
Mathematics 819, Springer, 1980, 18–34, DOI:
[10.1007/BFb0086977](https://doi.org/10.1007/BFb0086977) — the proof Devaney follows.
## Audit note (provenance of the read-backs)
**The read-backs attached to every draft item in this proposal are not independent.** They were
written by the same agent that drafted the Lean statements, not by a separate auditor working
blind from the code alone. They are included because they are still useful as a line-by-line
rendering of each statement, but they are **not** independent testimony: any misreading baked
into a formalization is likely repeated in its read-back, and agreement between the two should
not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own
first paragraph. Reviewers who want independent testimony should commission fresh, blind
read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`): all files
elaborate with no errors, the only warnings being the expected `sorry` placeholders in the
theorem bodies.
12 thms2 active usersReviewed
🏆Completed
Captain: Lucas
An Introduction to Chaotic Dynamical Systems I: Chaos in the Quadratic FamilyTextbook
## Motivation
The word *chaos* entered mathematics with a precise meaning, and Robert L. Devaney's
*An Introduction to Chaotic Dynamical Systems* (2nd edition, Westview Press, 2003) is the
text that fixed the meaning now used in most of the literature: a map is chaotic when it is
unpredictable (sensitive dependence on initial conditions), indecomposable (topological
transitivity), and nevertheless regular (dense periodic points). The book develops this
definition on the simplest possible object — the real quadratic family
$F_\mu(x) = \mu x(1-x)$ on the unit interval — and shows that for large $\mu$ the map is
chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.
This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8:
the invariant set of the quadratic family, symbolic dynamics on the sequence space
$\Sigma_2$, topological conjugacy, and Devaney's definition of chaos. Everything later in
the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets —
is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the
vocabulary of the whole series.
## Setting
Write $I = [0,1]$ and let $F_\mu(x) = \mu x(1-x)$ for a real parameter $\mu$. Iterates are
written $F_\mu^n$, with $F_\mu^0$ the identity.
For $\mu > 4$ the maximum value $\mu/4$ of $F_\mu$ exceeds $1$, so some points of $I$ leave
$I$ after one iteration. Let
$$A_0 = \{x \in I : F_\mu(x) > 1\}, \qquad A_n = \{x \in I : F_\mu^{\,n}(x) \in A_0\},$$
so that $A_n$ is the set of points escaping from $I$ at the $(n+1)$-st iteration. The set of
points that never escape is
$$\Lambda = I \setminus \bigcup_{n \ge 0} A_n = \{x : F_\mu^{\,n}(x) \in I \text{ for all } n \ge 0\}.$$
The complement $I \setminus A_0$ consists of two closed intervals, $I_0$ to the left of the
midpoint $1/2$ and $I_1$ to its right.
On the symbolic side, $\Sigma_2$ is the set of one-sided infinite sequences
$s = (s_0 s_1 s_2 \dots)$ with $s_i \in \{0,1\}$, metrized by
$$d[s,t] = \sum_{i=0}^{\infty} \frac{|s_i - t_i|}{2^i},$$
and $\sigma : \Sigma_2 \to \Sigma_2$ is the shift map $\sigma(s_0 s_1 s_2 \dots) = (s_1 s_2 s_3 \dots)$.
The *itinerary* of $x \in \Lambda$ is the sequence $S(x) = (s_0 s_1 s_2 \dots)$ with $s_j = 0$
when $F_\mu^{\,j}(x) \in I_0$ and $s_j = 1$ when $F_\mu^{\,j}(x) \in I_1$.
Following Devaney, $f : J \to J$ is **topologically transitive** if for every pair of open
sets $U, V$ meeting $J$ there is $k > 0$ with $f^k(U \cap J) \cap V \neq \emptyset$; it has
**sensitive dependence on initial conditions** if there is $\delta > 0$ such that every point
of $J$ has points of $J$ arbitrarily near it whose orbit eventually separates from its own by
more than $\delta$; and it is **chaotic on $J$** when it has sensitive dependence, is
topologically transitive, and has a dense set of periodic points in $J$.
## Target
The goal is Devaney's Example 8.8: for $\mu > 2 + \sqrt 5$,
$$F_\mu \text{ is chaotic on } \Lambda .$$
The milestones are the results the book uses to get there, in the book's own order:
the escape of orbits outside $I$ (Proposition 5.2), the tame regime $1 < \mu < 3$
(Proposition 5.3), the Cantor structure of $\Lambda$ (Theorem 5.6), the metric and dynamics of
the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its
dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of
$F_4$ on all of $I$ (Example 8.9).
## Significance
The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the
horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic
by producing a conjugacy with a shift. The conjugacy also gives quantitative information that
is otherwise inaccessible — for example, that $F_\mu$ has exactly $2^n$ points fixed by
$F_\mu^{\,n}$, which no direct computation with the degree-$2^n$ polynomial delivers.
Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's
three chaos conditions, the sequence space $\Sigma_2$ with its metric and shift, topological
conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the
foundation the rest of the book's series will import.
## Difficulty
The obvious route to the goal — analyze $F_\mu$ on $\Lambda$ directly — fails, because
$\Lambda$ has no explicit description: it is a nested intersection of $2^{n+1}$ intervals
whose endpoints are not available in closed form. The whole argument therefore goes through
the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which
needs the nested-interval construction $I_{s_0 \dots s_n} = I_{s_0} \cap F_\mu^{-1}(I_{s_1}) \cap
\dots \cap F_\mu^{-n}(I_{s_n})$ together with the fact that these intervals are nonempty and
nested; and (ii) injectivity, which needs the hyperbolicity estimate $|F_\mu'| > \lambda > 1$
on $I_0 \cup I_1$, valid exactly because $\mu > 2 + \sqrt 5$, and the mean value theorem. The
hypothesis $\mu > 2 + \sqrt 5$ is not cosmetic: Devaney notes the results hold for $\mu > 4$,
but only with a more delicate argument.
## Formalization scope
The Lean development fixes the following conventions.
1. $\Lambda$ is defined as $\{x : \forall n,\ F_\mu^{\,n}(x) \in [0,1]\}$ — the points whose
whole forward orbit stays in $I$ — rather than as a complement of the sets $A_n$; the two
descriptions agree, and the definitional form makes invariance immediate. The sets
$A_0, A_n, I_0, I_1$ are nonetheless defined, since the book's arguments refer to them.
2. The itinerary is defined as a total function of a real argument, taking entry $0$ at step
$n$ when $F_\mu^{\,n}(x) \le 1/2$ and $1$ otherwise. On $\Lambda$ this agrees with Devaney's
$I_0/I_1$ test, since the midpoint $1/2$ lies in the gap $A_0$ when $\mu > 4$.
3. $\Sigma_2$ carries Devaney's metric $d$ literally, as a summable series, not merely a
topology; the metric space instance is part of the definitional layer, so Proposition 6.2
is not a separate milestone.
4. Sensitive dependence, transitivity, chaos and periodicity are stated for a map
$f : X \to X$ of a metric space together with an invariant subset $J$, using open sets of
the ambient space intersected with $J$; this avoids subtype bookkeeping while keeping the
relative formulation of the book.
5. Cardinality claims ("$\operatorname{Per}_n$ has $2^n$ elements") are stated with
`Set.ncard` and are restricted to $n > 0$; for $n = 0$ every point is fixed by $F^0$ and the
claim would be false.
6. Nothing here is vacuous: the hypothesis $\mu > 2+\sqrt 5$ is satisfiable, $\Lambda$ is
nonempty (it contains $0$), and the chaos predicate is a conjunction of three nontrivial
conditions rather than a definitional abbreviation.
Contributions of any kind are welcome: full proofs, reductions splitting a milestone into
lemmas, and reusable lemmas about $\Sigma_2$ or about conjugacy that later missions in the
series can import.
## Selected references
- Robert L. Devaney, *An Introduction to Chaotic Dynamical Systems*, 2nd edition, Westview
Press, 2003 (ISBN 0-8133-4085-3) — §1.5 (pp. 31–38), §1.6 (pp. 39–43), §1.7 (pp. 44–47),
§1.8 (pp. 49–52). The mission's primary and authoritative source.
- J. Banks, J. Brooks, G. Cairns, G. Davis, P. Stacey, *On Devaney's definition of chaos*,
American Mathematical Monthly 99 (1992), 332–334, DOI:
[10.1080/00029890.1992.11995856](https://doi.org/10.1080/00029890.1992.11995856) — proves
that transitivity plus dense periodic points already imply sensitive dependence.
## Audit note (provenance of the read-backs)
**The read-backs attached to every draft item in this proposal are not independent.** They were
written by the same agent that drafted the Lean statements, not by a separate auditor working
blind from the code alone. They are included because they are still useful as a line-by-line
rendering of each statement, but they are **not** independent testimony: any misreading baked
into a formalization is likely repeated in its read-back, and agreement between the two should
not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own
first paragraph. Reviewers who want independent testimony should commission fresh, blind
read-backs.
Every definition and statement in this proposal was compiled locally against this mission's
environment (Lean 4.33.1, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`): all files
elaborate with no errors, the only warnings being the expected `sorry` placeholders in the
theorem bodies.
21 thms2 active usersReviewed
🏆Completed
Captain: Lucas
Kawahira: The Riemann Hypothesis and Holomorphic Index in Complex DynamicsResearch Paper
## Motivation
The **Riemann hypothesis** asserts that every non-trivial zero of the Riemann zeta function $\zeta$ lies on the line $\operatorname{Re} s = 1/2$; the **simplicity hypothesis** asserts in addition that every such zero is a simple zero of $\zeta$. Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.
Kawahira (2016) gives a reformulation of a different kind. He attaches to $\zeta$ an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is *equivalent* to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the **holomorphic index** (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.
## Setting
For a non-constant meromorphic $g : \mathbb{C} \to \widehat{\mathbb{C}}$, define the **nu function**
$$\nu_g(z) \;=\; z - \frac{g(z)}{z\,g'(z)}.$$
If $\alpha \neq 0$ is a zero of $g$ of order $m \ge 1$, then $\alpha$ is a fixed point of $\nu_g$ with **multiplier**
$$\lambda \;=\; \nu_g'(\alpha) \;=\; 1 - \frac{1}{m\alpha},$$
and if $\alpha$ is a pole of order $m$ the multiplier is $1 + \frac{1}{m\alpha}$. A fixed point $\alpha$ of a holomorphic map $f$ is **attracting** if $|f'(\alpha)| < 1$, **indifferent** if $|f'(\alpha)| = 1$, and **repelling** if $|f'(\alpha)| > 1$.
The **holomorphic index** of $f$ at a fixed point $\alpha$ is
$$\iota(f,\alpha) \;=\; \frac{1}{2\pi i}\oint_{C} \frac{dz}{z - f(z)},$$
the integral being over a small positively oriented circle around $\alpha$. When the multiplier $\lambda$ is not $1$ one has $\iota = \frac{1}{1-\lambda}$, and the Möbius map $\lambda \mapsto \frac{1}{1-\lambda}$ carries the unit disk onto the half-plane $\operatorname{Re}\iota > 1/2$. So a fixed point is attracting, indifferent or repelling exactly according to whether $\operatorname{Re}\iota$ is $> 1/2$, $= 1/2$ or $< 1/2$: the critical line reappears, in the index plane.
The point of the construction is that $\nu_g$ is engineered so that the index of $\nu_g$ at a simple zero $\alpha$ of $g$ is $\alpha$ itself (and $m\alpha$ at a zero of order $m$). Writing $\nu_\zeta = \nu_g$ for $g = \zeta$: a non-trivial zero $\alpha$ of order $m$ has index $m\alpha$, so $\operatorname{Re}\iota = m\operatorname{Re}\alpha$, and asking that this equal $1/2$ is asking for $m = 1$ and $\operatorname{Re}\alpha = 1/2$.
## Formalization targets
### Goal — Theorem 1 of the paper, conditions (a), (b), (c)
$$\Big(\text{RH} \wedge \text{simplicity}\Big) \iff \Big(\text{every non-trivial zero is an indifferent fixed point of } \nu_\zeta\Big) \iff \Big(\nu_\zeta \text{ has no attracting fixed point}\Big).$$
### Supporting targets
The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function $\xi$), and Proposition 13 of the appendix (the Newton map $N_g(z) = z - g(z)/g'(z)$, for which every zero of $g$ becomes an *attracting* fixed point — the contrast that explains why $\nu_g$, and not $N_g$, sees the critical line).
## Significance
The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry $\alpha \mapsto 1 - \alpha$ of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.
Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.
## Difficulty
The obvious route to the goal — compute $\nu_\zeta'$ at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets $\operatorname{Re}(m\alpha) \le 1/2$ for each non-trivial zero $\alpha$ of order $m$, which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair $\alpha$ with $1-\alpha$, whose index is $m(1-\alpha)$; only the two inequalities together force $m = 1$ and $\operatorname{Re}\alpha = 1/2$. A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip $0 < \operatorname{Re} s < 1$, that $\alpha$ and $1-\alpha$ are zeros of the same order, and that the trivial zeros and the pole at $s = 1$ give repelling fixed points.
The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that $z - f(z)$ has exactly one zero inside; the other genuinely analytic milestone is the order-$m$ computation of $\nu_g'$, where $g'$ vanishes at the fixed point when $m \ge 2$ and the singularity is removable rather than absent.
## Formalization scope
The development is over $\mathbb{C}$ with Mathlib's `riemannZeta`. Conventions the Lean statements commit to:
1. **Non-trivial zero** means: a zero of $\zeta$ that is not one of $-2, -4, -6, \dots$. Nothing about the critical strip is built into the definition; that the non-trivial zeros lie in $0 < \operatorname{Re} s < 1$ is part of the work.
2. **Simplicity** of a zero $\alpha$ is expressed as $\zeta'(\alpha) \neq 0$.
3. $\nu_g$ is a total function $\mathbb{C} \to \mathbb{C}$, using Lean's convention that division by zero returns zero. At a zero of $g$ this total function agrees with the genuine holomorphic extension of $\nu_g$, so multipliers there are the true ones. At a point where $g$ is non-zero and $g'$ vanishes, and at a pole of $g$, the total function takes an artefactual value; the statements about $\nu_\zeta$ therefore carry the explicit guard $\zeta(\alpha) = 0 \vee \zeta'(\alpha) \neq 0$ together with $\alpha \neq 0, 1$. The excluded points are exactly the pole of $\zeta$ (a repelling fixed point, by Proposition 7 of the paper) and the poles of $\nu_\zeta$, so the guarded statements are equivalent to the paper's, but they are guarded, and a reader should check that they consider the guards faithful.
4. The **xi function** is taken in Kawahira's normalization $\xi(z) = \frac{1}{2}z(1-z)\pi^{-z/2}\Gamma(z/2)\zeta(z)$, written in Lean through Mathlib's entire function $\Lambda_0$ so that the Lean $\xi$ is entire and has the correct values at $z = 0, 1$ rather than removable-singularity artefacts; the definition file carries a proved lemma identifying it with $\frac{1}{2}z(1-z)\Lambda(z)$ off $\{0,1\}$.
5. Conditions **(d)** and **(e)** of the paper's Theorems 1 and 10 — the purely topological reformulations in terms of a topological disk $D$ with $\nu_\zeta(D) \subset D$, and their homeomorphic deformations — are **not** part of this mission. They rest on the topological characterization of attracting fixed points (the paper's Proposition 2), whose proof uses the Riemann mapping theorem and the Schwarz–Pick lemma; the Riemann mapping theorem is not available in Mathlib, and the intended strength of the inclusion $\nu_\zeta(D) \subset D$ (compact containment) needs to be fixed before the statement can be formalized faithfully. Theorem 14 of the appendix, which is of the same topological kind, is likewise out of scope. A contribution supplying Proposition 2 in a defensible form would be welcome, as a separate mission.
Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of $\nu_\zeta$ is known not to model the meromorphic map.
Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order $m$ — all stated for an arbitrary function analytic at the point, not for $\zeta$.
## Selected references
- T. Kawahira, *The Riemann Hypothesis and Holomorphic Index in Complex Dynamics*, Experimental Mathematics (2016). https://doi.org/10.1080/10586458.2016.1217443
- J. Milnor, *Dynamics in One Complex Variable*, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. (Holomorphic index: Lemma 12.2; topological characterization of fixed points: Section 8.)
- E. C. Titchmarsh, *The Theory of the Riemann Zeta Function*, 2nd ed., Oxford University Press, 1986. (Functional equation; trivial zeros; the xi function.)
- D. Schleicher, *Newton's Method as a Dynamical System: Efficient Root Finding of Polynomials and the Riemann $\zeta$ Function*, Fields Inst. Commun. 53 (2008), 213–224.
22 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).