OAI/NumberTheory/DukePrimeDegree/Dynamics/StrongStableConjugates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fine recurrent lifts eliminate the neutral diagonal

Bounded future conjugates are upper triangular. If these same conjugates enter arbitrarily small identity neighborhoods, their unchanged diagonal entries are one, so the displacement is a genuine upper-root word.

  1. theorem OAI.DukePrimeDegree.upperRootWord_of_bounded_fine_conjugates line 18