Eigenvalue one or minus one on a lattice yields two Reidemeister classes (Lemma 4)
ProvedRInf.reid_two_classesIf the automorphism of the standard integer lattice of rank k has the eigenvalue one or the eigenvalue minus one - some nonzero lattice vector is fixed or negated - then there are two lattice elements that are not twisted conjugate under the automorphism: its Reidemeister number is at least two. The proof follows the lattice analysis of Lemma 4: for the eigenvalue one the classes are infinite in number, and for the eigenvalue minus one the fixed sublattice splits the Reidemeister counting at least in two.
import Mathlib import Definitions.Def_RInf_alg import Definitions.Def_RInf_braid
namespace RInf
/-! Milestone 2 (Lemma 4): an automorphism of a standard integer lattice
whose matrix has the eigenvalue one or minus one has at least two Reidemeister
classes. If some nonzero lattice vector is fixed or negated by m, then there
are two elements of the lattice that are not twisted conjugate under m. The
proof follows the lattice analysis of Lemma 4: for the eigenvalue one the
classes are infinite in number, and for the eigenvalue minus one the fixed
sublattice splits the Reidemeister counting at least in two. -/
theorem reid_two_classes {k : Nat} (m : (Fin k → Int) ≃+ (Fin k → Int))
(h : ∃ v : Fin k → Int, v ≠ 0 ∧ (m v = v ∨ m v = -v)) :
∃ x y : Fin k → Int, ¬ TwistedConjAdd m x y := by sorry
end RInf
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: if the automorphism m of the integer lattice of rank k fixes or negates some nonzero lattice vector, then there are two lattice elements that no lattice element makes twisted conjugate under m. Hypotheses: the existence of a nonzero vector with m v = v or m v = -v.