OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockNoncentral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed root detects a transverse sequence

Every matrix outside the two-block preserving group fails to commute with a root in the selected nontrivial block. There are only finitely many such roots, so one root detects an entire subsequence. This chooses the shearing direction from the actual return matrices.

  1. theorem OAI.DukePrimeDegree.exists_noncentral_singleBlock_root line 22
  2. lemma OAI.DukePrimeDegree.exists_constant_subsequence_of_finite line 55
  3. theorem OAI.DukePrimeDegree.exists_fixed_noncentral_root_subsequence line 67