OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanGeneratorSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite generator chains along the geometric scale sequence

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cartan_generator_sequence line 28

    Source documentation

    All endpoints in one rescaled box admit chains of the same finite length. One vanishing error envelope bounds every prefix, uniformly over all endpoint choices. No measurable choice of the chains is asserted or needed for deterministic subsequence arguments.

    theorem exists_cartan_generator_sequence
    [Nonempty (Fin M.letterCount)]
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput