FiniteWindingIndex.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The analytic winding test on a finite Rips component

This derives the finite-component index evaluation from the explicit published scalar-circle pairing. The cocycle, continuous map, parametrized loop and its degree are explicit.

theorem OAI.CoarseAssembly.graphEdgeBound line 22
def OAI.CoarseAssembly.graphLoopClass line 32
Source documentation
The analytic class of the parametrized boundary loop at this scale.
```
def graphLoopClass (input : PublishedCircleInput) (hG : G.Connected)
    (r : ℕ) (hr : 1 ≤ r) {x : X} (p : G.Walk x x) :
    letI := graphMetric G hG
…
```
Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.graphMetric

theorem OAI.CoarseAssembly.graph_loop_index line 41

Source documentation

The finite-component analytic index is the original graph winding.

theorem graph_loop_index (input : PublishedCircleInput) (hG : G.Connected)
    (a : X → X → ℤ) (ha : ∀ x y, G.Adj x y → a y x = -a x y)
    (r : ℕ) (hr : 1 ≤ r)
    (hloop : ∀ x (p : G.Walk x x), p.length ≤ 3 * r → walkCharge a p = 0)
    {x : X} (p : G.Walk x x) :
    letI := graphMetric G hG
…

Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.graphMetric

theorem OAI.CoarseAssembly.graph_loop_infinite_order line 60

Source documentation

A charge-one boundary class has infinite order at the specified Rips scale. Only the cited published circle-index input is conditional.

theorem graph_loop_infinite_order (input : PublishedCircleInput) (hG : G.Connected)
    (a : X → X → ℤ) (ha : ∀ x y, G.Adj x y → a y x = -a x y)
    (r : ℕ) (hr : 1 ≤ r)
    (hloop : ∀ x (p : G.Walk x x), p.length ≤ 3 * r → walkCharge a p = 0)
    {x : X} (p : G.Walk x x) (hp : walkCharge a p = 1)
    (n : ℤ) (hn : n ≠ 0) :
    letI := graphMetric G hG
…

Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.graphMetric