CocyclePathLifting.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Integer lifts and winding along graph walks

The real lift of the constructed circle map along an actual graph walk ends at the sum of its edge charges. This is the topological degree calculation used before applying the published circle index formula.

structure OAI.CoarseAssembly.IntegerPathLift line 25
Source documentation
A real path lift normalized to start at zero, with integral endpoint.
```
structure IntegerPathLift (p : Path x y) (n : ℤ) where
…
```
def OAI.CoarseAssembly.shiftedRealPath line 29
def OAI.CoarseAssembly.IntegerPathLift.refl line 36
def OAI.CoarseAssembly.IntegerPathLift.trans line 41

def OAI.CoarseAssembly.Rips.walkPath line 62

Source documentation

Follow the barycentric unit edges of a graph walk.

def walkPath {G : SimpleGraph X} (hr : 0 ≤ r)
    (hE : ∀ x y, G.Adj x y → dist x y ≤ r) :
    {x y : X} → G.Walk x y → Path (vertex x hr) (vertex y hr)
  | _, _, .nil => Path.refl _
  | _, _, .cons h p => (edgePath (hE _ _ h)).trans (walkPath hr hE p)

variable [Fintype X]

Mentions: OAI.CoarseAssembly.Rips.vertex, OAI.CoarseAssembly.Rips.edgePath

def OAI.CoarseAssembly.Rips.IntegralCocycle.edgeLift line 70
def OAI.CoarseAssembly.Rips.IntegralCocycle.walkLift line 79
theorem OAI.CoarseAssembly.Rips.IntegralCocycle.closed_walk_lift line 89
Source documentation
A closed graph walk yields a circle-valued loop with a real lift whose endpoint is exactly its integral cocycle evaluation.
```
theorem IntegralCocycle.closed_walk_lift (c : IntegralCocycle X r) {G : SimpleGraph X}
    (hr : 0 ≤ r) (hE : ∀ x y, G.Adj x y → dist x y ≤ r)
    {x : X} (p : G.Walk x x) :
    ∃ L : Path (0 : ℝ) (walkCharge c.charge p : ℝ),
      ∀ t, c.circleMap (walkPath hr hE p t) = (L t : AddCircle (1 : ℝ)) :=
…
```
Mentions: OAI.CoarseAssembly.Rips.IntegralCocycle, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.Rips.walkPath