FiberedGraph.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual finite graph with congruence fibers

The inter-fiber edge relation is written at the common shallower level. This uniformly describes the equal-depth, parent and child cases. The generating set is symmetrized and contains the identity to record pure base moves in a common list of left/right operations.

theorem OAI.CoarseAssembly.one_mem_symmetricMoves line 22
theorem OAI.CoarseAssembly.inv_mem_symmetricMoves line 25
abbrev OAI.CoarseAssembly.fiberLevel line 33
theorem OAI.CoarseAssembly.liftStep_of_common line 36
theorem OAI.CoarseAssembly.liftStep_reverse line 54
theorem OAI.CoarseAssembly.fiberedGraph_projects line 66

theorem OAI.CoarseAssembly.liftStep_reduce line 73

Source documentation

An edge has the same left/right description at every lower common level.

theorem liftStep_reduce {S : Finset ArithmeticGroup} {t : ℤ_[2]ˣ} {j l : ℕ}
    {x y : FiberVertex j} (h : LiftStep S t x y)
    (hx : l ≤ discDepth j x.1) (hy : l ≤ discDepth j y.1) :
    ∃ s ∈ symmetricMoves S,
      fiberCoordinate y hy = reduce l s * fiberCoordinate x hx *
        holonomy t l ^ fiberCharge x y := by
…

Mentions: OAI.CoarseAssembly.FiberVertex, OAI.CoarseAssembly.LiftStep, OAI.CoarseAssembly.discDepth, OAI.CoarseAssembly.symmetricMoves, OAI.CoarseAssembly.fiberCoordinate, OAI.CoarseAssembly.fiberCharge

theorem OAI.CoarseAssembly.walk_reduced_lift line 84

Source documentation

Record every edge of a walk as an integral left move and a ray charge, after reducing all its coordinates to one common level.

theorem walk_reduced_lift {S : Finset ArithmeticGroup} {t : ℤ_[2]ˣ} {j : ℕ}
    {u v : FiberVertex j} (p : (fiberedGraph S t j).Walk u v) (l : ℕ)
    (hp : ∀ w ∈ p.support, l ≤ discDepth j w.1) :
    ∃ steps : List (ArithmeticGroup × ℤ),
      steps.length = p.length ∧
      holonomyCharge steps = walkCharge fiberCharge p ∧
      (∀ s ∈ steps, s.1 ∈ symmetricMoves S ∧ s.2.natAbs ≤ 1) ∧
      holonomyEndpoint (holonomy t l) (reduceSteps l steps)
          (fiberCoordinate u (hp u p.start_mem_support)) =
        fiberCoordinate v (hp v p.end_mem_support) := by
…

Mentions: OAI.CoarseAssembly.FiberVertex, OAI.CoarseAssembly.fiberedGraph, OAI.CoarseAssembly.discDepth, OAI.CoarseAssembly.holonomyCharge, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.fiberCharge, OAI.CoarseAssembly.symmetricMoves, OAI.CoarseAssembly.holonomyEndpoint, OAI.CoarseAssembly.fiberCoordinate

theorem OAI.CoarseAssembly.fiberedGraph_short_loops line 116
Source documentation
The manuscript's small-loop assertion for the actual finite fibered graphs. The radius estimate supplies a common deep quotient; arithmetic trace separation then forces the ray charge to vanish.
```
theorem fiberedGraph_short_loops (S : Finset ArithmeticGroup) (A : ℕ) :
    ∃ J : ℕ, ∀ j, J ≤ j → ∀ u : FiberVertex j,
      ∀ p : (fiberedGraph S chosenHolonomyUnit j).Walk u u,
        p.length ≤ A → walkCharge fiberCharge p = 0 := by
…
```
Mentions: OAI.CoarseAssembly.FiberVertex, OAI.CoarseAssembly.fiberedGraph, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.fiberCharge