OAI/GroupTheory/PolycyclicRecognition/Geometry/SequenceRootSwitch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sublinear root switches with subexponential coordinate bounds

At a contact facet the exponential root amplitude cancels its scalar contraction. The remaining polynomial correction contributes only a sublinear distance, uniformly in the translated sheet and position.

  1. theorem OAI.PolycyclicRecognition.sublinear_root_switch_sequence line 23