OAI/GroupTheory/PolycyclicRecognition/Analysis/MetricChainWords.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded words from the published large-scale chain metric

  1. theorem OAI.PolycyclicRecognition.LinearMetricChains.wordFactorization line 15

    Source documentation

    Consecutive group differences telescope to the original element. The published chain metric suffices; minimizing paths are unnecessary.

    theorem LinearMetricChains.wordFactorization
    {G : Type*} [Group G] [MetricSpace G] [IsIsometricSMul G G]
    (C : LinearMetricChains G) (g : G) :
    ∃ w : List G, (∀ q ∈ w, q ∈ closedBall 1 C.step) ∧ w.prod = g ∧
      (w.length : ℝ) ≤ C.slope * dist 1 g + C.error := by
…