OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockCorrectedPairs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalized generic pairs from null block orbits

The small return matrices, their within-block normalizations and the common compact corrections are selected in this proof. The correction group is the closure of the single root block, so it preserves the same component measure. The conclusion does not assume genericity of the normalized points or a transverse limiting element.

  1. def OAI.DukePrimeDegree.singleBlockClosureGroup line 25
  2. theorem OAI.DukePrimeDegree.exists_singleBlock_corrected_generic_pairs line 30