OAI/GroupTheory/PolycyclicRecognition/Algebra/CharacterHemisphereEndgame.lean

The character hemisphere criterion reaches the nilpotent endgame

Finite module generation over the quotient ring comes from the group itself. The hemisphere condition supplies an actual ascending base for conjugation. The still separate FP-infinity implication must supply that condition and the nilpotent-by-abelian structure; neither is introduced as a new main input.