ChosenHolonomy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The choice in §3 is made once. The separation level can then depend on the length bound, without changing the chosen 2-adic unit.

theorem OAI.CoarseAssembly.Congruence.chosenHolonomyUnit_transcendental line 16
theorem OAI.CoarseAssembly.Congruence.chosenHolonomyUnit_principal line 20
theorem OAI.CoarseAssembly.Congruence.chosenHolonomy_short_lifts line 27
Source documentation
The fixed principal holonomy excludes short charged closed lifts at every finite length bound. This is an arithmetic statement, not a coarse assembly or K-homology theorem.
```
theorem chosenHolonomy_short_lifts (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 chosenHolonomyUnit k) (reduceSteps k steps) z = z →
        holonomyCharge steps = 0 :=
…
```
Mentions: OAI.CoarseAssembly.Congruence.ArithmeticGroup, OAI.CoarseAssembly.Congruence.Quotient, OAI.CoarseAssembly.holonomyEndpoint, OAI.CoarseAssembly.Congruence.holonomy, OAI.CoarseAssembly.Congruence.chosenHolonomyUnit, OAI.CoarseAssembly.Congruence.reduceSteps, OAI.CoarseAssembly.holonomyCharge