OAI/NumberTheory/DukePrimeDegree/Geometry/RootHolonomy.lean

Pointwise root holonomy under a neutral diagonal flow

This is the consequence of Einsiedler–Katok (2003), Proposition 5.1, needed by the high-entropy commutator argument. One null set works for all pairs and all relative matrices whose conjugates approach a root translation. Lusin compactness and strict neutral invariance identify both limiting root conditionals; pointwise rebasing supplies holonomy.