WordMetricBridge.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite balls for the actual word metric

Mathlib constructs a normed group from a generating family. A finite family has only finitely many words of bounded length, so this metric supplies the finite-ball hypothesis used in the recognition and lattice comparison.

theorem OAI.PolycyclicRecognition.finite_bounded_length_lists line 22
Source documentation
There are finitely many words of bounded length over a finite alphabet.
```
theorem finite_bounded_length_lists (A : Type*) [Finite A] (n : ℕ) :
    {l : List A | l.length ≤ n}.Finite := by
…
```
theorem OAI.PolycyclicRecognition.finite_wordLength_ball line 41
Source documentation
The group elements of bounded word length form a finite set.
```
theorem finite_wordLength_ball [Finite ι] (P : Group.Generators G ι) (n : ℕ) :
    {g : G | P.wordLength g ≤ n}.Finite := by
…
```
theorem OAI.PolycyclicRecognition.finite_wordMetric_closedBall line 50
Source documentation
The normed group built from a finite generating family has finite closed balls.
```
theorem finite_wordMetric_closedBall [Finite ι] (P : Group.Generators G ι) :
    letI := P.normedGroup
…
```
theorem OAI.PolycyclicRecognition.exists_finite_wordMetric line 66
Source documentation
Finite generation supplies a finite generating family whose actual Mathlib word metric has finite closed balls.
```
theorem exists_finite_wordMetric [Group.FG G] :
    ∃ (n : ℕ) (P : Group.Generators G (Fin n)),
      letI := P.normedGroup
…
```
theorem OAI.PolycyclicRecognition.proper_wordMetric line 76
Source documentation
The actual word metric is proper because every translated closed ball is finite.
```
theorem proper_wordMetric [Finite ι] (P : Group.Generators G ι) :
    letI := P.normedGroup
…
```
theorem OAI.PolycyclicRecognition.discrete_wordMetric line 91
Source documentation
Distinct points have positive integral word distance, so every singleton is open in the word metric.
```
theorem discrete_wordMetric (P : Group.Generators G ι) :
    letI := P.normedGroup
…
```
def OAI.PolycyclicRecognition.wordMetric_linearChains line 107
Source documentation
Prefixes of a shortest representing word give unit-step chains of length exactly the word-metric distance.
```
def wordMetric_linearChains (P : Group.Generators G ι) :
    letI := P.normedGroup
…
```