OAI/NumberTheory/DukePrimeDegree/Dynamics/NoCentralizerOrbit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Excluding a probability measure on a root centralizer orbit

This is the consequence of EKL Theorem 5.1 and Proposition 5.2 needed in the low-entropy argument. The neutral direction is explicit: its double weight is negative and its complementary weights are distinct.

  1. theorem OAI.DukePrimeDegree.no_invariant_rootPair_orbit_of_weights line 20