OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootContraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Contracting diagonal dynamics on full upper-root leaves

The explicit root coordinates identify the contracting unipotent foliation. Uniform root-weight gaps give an exponential bound on its Euclidean size; strict gaps give convergence to the identity.

  1. lemma OAI.DukePrimeDegree.EliminationChain.timeVectorHomeomorph_zero line 22
  2. lemma OAI.DukePrimeDegree.upperRootEuclideanCoordinates_zero line 35
  3. def OAI.DukePrimeDegree.upperRootSize line 43
  4. lemma OAI.DukePrimeDegree.upperRootSize_dilation_le line 46
  5. lemma OAI.DukePrimeDegree.upperRootDilation_tendsto_zero line 64
  6. lemma OAI.DukePrimeDegree.upperRoot_conjugate_tendsto_one line 85