VisualInfiniteBranching.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Infinite branching for the genuine visual tree.

lemma OAI.HarmonicArtin.ParabolicIntersections.injective_zpow_orbit line 10
theorem OAI.HarmonicArtin.ParabolicIntersections.visual_infinite_branching line 28
Source documentation
Every oriented edge belongs to an infinite orbit under the stabilizer of its initial vertex. In particular, the visual tree is not a line.
```
theorem visual_infinite_branching {u v : VisualVertex M Y Z}
    (h : (visualGraph M Y Z).Adj u v) :
    ∃ a : Artin M, a∈MulAction.stabilizer (Artin M) u ∧
      Function.Injective (fun n : ℤ => a^n • v) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.VisualVertex, OAI.HarmonicArtin.ParabolicIntersections.visualGraph, OAI.HarmonicArtin.Artin