ProperParabolicMalnormal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Weak malnormality of all proper parabolics

This proves the implication needed from Charney--Martin--Morris-Wright, Acylindrical hyperbolicity for Artin groups with a visual splitting, Algebraic & Geometric Topology 26 (2026), Proposition 4.2, for the present Artin groups. A proper parabolic preserves a proper convex subtree. Two translates can be placed at the ends of a segment with trivial stabilizer. Their common stabilizer fixes that segment, hence is trivial.

theorem OAI.HarmonicArtin.ParabolicIntersections.standard_parabolic_trivial_conjugates line 30
Source documentation
The two conjugates have trivial intersection; this is stronger than finiteness in the published weak-malnormality criterion.
```
theorem standard_parabolic_trivial_conjugates (hIrred : IsIrreducible M)
    (X : Set S) (hX : X≠Set.univ) :
    ∃ a b : Artin M,
      conjugate a (artinParabolic M X) ⊓ conjugate b (artinParabolic M X)=⊥ := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.proper_parabolic_weaklyMalnormal line 66
Source documentation
Every proper parabolic of an irreducible visually split Artin group is weakly malnormal, with no published hypotheses.
```
theorem proper_parabolic_weaklyMalnormal (hIrred : IsIrreducible M)
    (P : Subgroup (Artin M)) (hP : IsParabolic M P) (hne : P≠⊤) : WeaklyMalnormal P := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal