OAI/NumberTheory/DukePrimeDegree/Dynamics/EqualLeafReturns.lean

Noncentral return pairs with equal actual leaves

The strictly invariant version removes a single null set. Every neutral pair outside it has equal intrinsic leaves, even when the neutral parameter is chosen after the points. Applying the exceptional-set exclusion to the remaining positive-measure set gives noncentral return matrices tending to identity with the required equal-leaf pairs.