DynamicsUnconditional.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Paper 082-03, Corollary 1.3, without published hypotheses

For a finite-rank irreducible Artin group whose defining graph is not a clique, the group is acylindrically hyperbolic and every proper parabolic subgroup is weakly malnormal. The acylindrical action is constructed from the genuine visual tree; the algebraic intersection theorem supplies a segment with trivial stabilizer. All metric, boundary, and malnormality arguments are proved in the imported development.

theorem OAI.HarmonicArtin.ParabolicIntersections.unconditional_nonclique_dynamics line 20
Source documentation
The full third main result of Parabolic intersections in Artin groups.
Distinct definitions of this name: ComparatorChallenges/ArtinParabolicIntersections.lean:121 (different declaration text). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.unconditional_nonclique_dynamics@path.
```
theorem unconditional_nonclique_dynamics
    (hIrred : IsIrreducible M) (hInf : ∃ s t : S,s≠t ∧ M s t=0) :
    AcylindricallyHyperbolic (Artin M) ∧
      ∀ P : Subgroup (Artin M),IsParabolic M P → P≠⊤ → WeaklyMalnormal P := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal