The pure Artin braid groups on at least five strings have the R-infinity property (Theorem 12)
ProvedRInf.pure_braid_r_infinityThe pure Artin braid group on n strings has the R-infinity property for every n of at least five: every automorphism of the braid group has infinite Reidemeister number. The automorphism acts on the commutator layer with the eigenvalue one, hence with infinite Reidemeister number on the layer, and the transfer carries the infinitude to the Reidemeister number of the automorphism itself. The cases of three and four strings are treated separately in the paper and are pruned from this mission.
import Mathlib import Definitions.Def_RInf_alg import Definitions.Def_RInf_braid
namespace RInf
/-! The goal (Theorem 12): every pure Artin braid group on at least five
strings has the R-infinity property. Every automorphism α of the braid group
acts on the commutator layer with the eigenvalue one by milestone 5, hence
with infinite Reidemeister number on the layer by milestone 6, and the
transfer of the world carries the infinitude to the Reidemeister number of α
itself, by the reductions of milestones 1 and 7. The cases of three and four
strings are treated separately in the paper and are pruned from this
mission. -/
theorem pure_braid_r_infinity {n : Nat} {P Q : Type*} [Group P] [AddCommGroup Q]
(W : BraidWorld n P Q) (hn : 5 ≤ n) : RInfinity P := by sorry
end RInf
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in the braid world on n strings, if n is at least five, then every automorphism of the pure braid group has infinite Reidemeister number: the group has the R-infinity property. Hypotheses: the braid world is given and five is at most n.