OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingWindowControl.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform control during the logarithmic recurrence window

The shearing scale remains small throughout the chosen diagonal window. The growing matrix entries are bounded by that scale; all other off-diagonal entries contract. Thus moving to the selected recurrence time preserves convergence of the relative return matrices to identity.

  1. theorem OAI.DukePrimeDegree.rootShearingKappa_window_bound line 22
  2. theorem OAI.DukePrimeDegree.rootPairConjugate_entry_difference_bound line 51