The induced action on the commutator layer has infinite Reidemeister number (Section 3.2)
ProvedRInf.layer_reid_infiniteEvery automorphism of the pure Artin braid group acts on the commutator layer with infinite Reidemeister number. By the eigenvalue-one theorem the induced action of the automorphism on the layer has the eigenvalue one; transported along the standard coordinates of the layer, the lattice criterion yields infinitely many pairwise non-twisted-conjugate elements of the layer. This is the statement of Section 3.2 from which the main theorem follows by the transfer of Remark 1.
import Mathlib import Definitions.Def_RInf_alg import Definitions.Def_RInf_braid
namespace RInf
/-! Milestone 6: the induced action on the commutator layer has infinite
Reidemeister number. By milestone 5 the induced action of α on the layer has
the eigenvalue one; transporting along the standard coordinates of the layer
and applying the eigenvalue-one criterion of milestone 3, the Reidemeister
number of the induced automorphism of the layer is infinite. This is the
statement R of the second induced action is infinite of Section 3.2, from
which the main theorem follows by the transfer of Remark 1. -/
theorem layer_reid_infinite {n : Nat} {P Q : Type*} [Group P] [AddCommGroup Q]
(W : BraidWorld n P Q) (α : P ≃* P) : ReidInfAdd (W.act α) := by sorry
end RInf
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every automorphism of the pure braid group of the world, the induced automorphism of the commutator layer has infinite Reidemeister number: there is an infinite sequence of pairwise non-twisted-conjugate elements of the layer. Hypotheses: the braid world is given; no further hypotheses appear.