OAI/NumberTheory/DukePrimeDegree/Dynamics/RootOrbitSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Root-orbit separation outside one null set

Countably many long root boxes cover every finite segment of every free root orbit. Removing their exceptional sets turns the chartwise separation theorem into separation for all root translations at once. This proves the one-dimensional part of EKL Lemma 4.4(2), without a pointwise rebasing assumption.

  1. theorem OAI.DukePrimeDegree.exists_nullset_root_orbit_leaf_separation line 22