OAI/GroupTheory/PolycyclicRecognition/Geometry/RootIntervalSlack.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Interior slack for the actual bounded root intervals

  1. theorem OAI.PolycyclicRecognition.root_interval_conjugation_mem_box line 26

    Source documentation

    Every bounded interval in an interior root direction remains in the unit normalized box after conjugation by the enlarged suffix. The actual finite-word envelope is constructed from the root and suffix coordinates.

    theorem root_interval_conjugation_mem_box
    [Nonempty (Fin (finrank ℝ L))]
    (X : I → L) {k₀ c₀ : ℕ} (hk : lowerCentralSeries ℝ L L k₀ = ⊥)
    (hletters : ∀ i, FreeMagma.of i ∈ boundedBracketWords (I := I) k₀)
…

    Mentions: OAI.PolycyclicRecognition.boundedBracketWords