OAI/NumberTheory/DukePrimeDegree/Geometry/RowLeafConstancy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic root leaves are constant in the other row coordinates

A diagonal flow can be neutral on one row root and contract all other row roots simultaneously, regardless of their index ordering. Neutral holonomy therefore identifies the selected intrinsic leaf at every pair of row-coordinate points with the same selected coordinate, off one null set. This supplies the geometric input for the abelian product step.

  1. theorem OAI.DukePrimeDegree.exists_neutral_row_contracting_weights line 24
  2. lemma OAI.DukePrimeDegree.rowRoot_neutral_root_limit line 33
  3. lemma OAI.DukePrimeDegree.rowRoot_neutral_limit line 66
  4. theorem OAI.DukePrimeDegree.exists_nullset_row_leaf_holonomy line 75
  5. theorem OAI.DukePrimeDegree.exists_nullset_row_leaf_constancy line 97