OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockShearingContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed-window contradiction for a normalized transverse pair

All quantifiers retain the order needed by the argument: the compact shell and its separating tests are fixed first, then the terminal fraction and the generic set, and only then the nearby pair and its root-dependent stopping times. The limit is proved to lie in the shell by its normalized matrix entries.

  1. theorem OAI.DukePrimeDegree.singleBlock_fixed_window_contradiction line 23