VisualTrivialSegment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The visual tree has a segment with trivial pointwise stabilizer. This proves the segment step in CMMW (2026), Theorem 3.2, using the unconditional parabolic intersection theorem and rank descent.

lemma OAI.HarmonicArtin.ParabolicIntersections.visual_pair_isParabolic line 19
theorem OAI.HarmonicArtin.ParabolicIntersections.visual_exists_trivial_pair line 28
Source documentation
A finite segment of the genuine Bass--Serre tree has trivial stabilizer.
```
theorem visual_exists_trivial_pair (hIrred : IsIrreducible M) :
    ∃ u v : VisualVertex M Y Z, u≠v ∧ pairStabilizer (G := Artin M) u v=⊥ := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.VisualVertex, OAI.HarmonicArtin.Artin