OAI/NumberTheory/DukePrimeDegree/Arithmetic/ExceptionalSetExclusion.lean

Exclusion of exceptional neutral return sets

A measurable set on which all sufficiently small neutral return lifts centralize one root has measure zero. The recurrence strengthening makes these lifts centralize both roots on each quotient chart; the neutral ergodic decomposition then contradicts the arithmetic orbit obstruction. This combines the needed directions of EKL (2006), Lemma 4.2, Proposition 4.3, and Theorem 5.1, without assuming those results.