FiniteWords.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform exclusion of short charged closed words

This is the algebraic part of the small-loop lemma in §3, specialized to SL₃(ℤ) and its actual congruence quotients. The finite family of possible word traces is constructed, rather than postulated as an extra input.

def OAI.CoarseAssembly.Congruence.wordBall line 16
Source documentation
Words of length at most n in a finite set of left moves.
```
def wordBall (S : Finset ArithmeticGroup) : ℕ → Finset ArithmeticGroup
  | 0 => {1}
  | n + 1 => wordBall S n ∪ (wordBall S n).biUnion (fun w => S.image (w * ·))
```
Mentions: OAI.CoarseAssembly.Congruence.ArithmeticGroup
theorem OAI.CoarseAssembly.Congruence.wordBall_mono line 20
theorem OAI.CoarseAssembly.Congruence.holonomyWord_mem line 26
theorem OAI.CoarseAssembly.Congruence.holonomyCharge_natAbs_le line 37
def OAI.CoarseAssembly.Congruence.reduceSteps line 48
Source documentation
Reduction of each left move, preserving its signed base charge.
```
def reduceSteps (k : ℕ) (steps : List (ArithmeticGroup × ℤ)) : List (Quotient k × ℤ) :=
…
```
Mentions: OAI.CoarseAssembly.Congruence.ArithmeticGroup, OAI.CoarseAssembly.Congruence.Quotient
theorem OAI.CoarseAssembly.Congruence.holonomyCharge_reduceSteps line 51
theorem OAI.CoarseAssembly.Congruence.holonomyWord_reduceSteps line 57
theorem OAI.CoarseAssembly.Congruence.bounded_closed_lifts_have_zero_charge line 68
Source documentation
At a sufficiently deep quotient, no bounded list of allowed Cayley/base moves can close with nonzero charge. This conclusion does not assume a spectral gap, a property-(T) theorem, or an analytic K-homology fact.
```
theorem bounded_closed_lifts_have_zero_charge (t : ℤ_[2]ˣ)
    (ht : Transcendental ℤ (t : ℤ_[2])) (S : Finset ArithmeticGroup) (A : ℕ) :
    ∃ N : ℕ, 1 ≤ N ∧ ∀ k, N ≤ k → ∀ z : Quotient k,
      ∀ steps : List (ArithmeticGroup × ℤ), steps.length ≤ A →
        (∀ s ∈ steps, s.1 ∈ S ∧ s.2.natAbs ≤ 1) →
        holonomyEndpoint (holonomy t k) (reduceSteps k steps) z = z →
        holonomyCharge steps = 0 := by
…
```
Mentions: OAI.CoarseAssembly.Congruence.ArithmeticGroup, OAI.CoarseAssembly.Congruence.Quotient, OAI.CoarseAssembly.holonomyEndpoint, OAI.CoarseAssembly.Congruence.holonomy, OAI.CoarseAssembly.Congruence.reduceSteps, OAI.CoarseAssembly.holonomyCharge