NonCliqueDynamics.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Corollary 1.3 of paper 082-03

The published inputs are Charney--Martin--Morris-Wright, Acylindrical hyperbolicity for Artin groups with a visual splitting, Algebraic & Geometric Topology 26 (2026), 1507--1528, Theorem 3.2 and Proposition 4.2; also arXiv:2404.11393, pp. 9, 14. https://msp.org/agt/2026/26-4/agt-v26-n4-p08-p.pdf https://arxiv.org/pdf/2404.11393

Their hypotheses concern the edge group of an actual visual splitting. The required parabolic-intersection premise is proved by parabolic_intersections, rather than postulated as part of these published inputs.

structure OAI.HarmonicArtin.ParabolicIntersections.PublishedVisualSplitting line 24
Source documentation
The exact two published implications used by the target corollary.
```
structure PublishedVisualSplitting : Prop where
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.nonclique_dynamics line 37
Source documentation
Corollary 1.3 in full: acylindrical hyperbolicity and weak malnormality of every proper parabolic for every irreducible non-clique Artin matrix.
```
theorem nonclique_dynamics
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hPub : ∀ X : Set S, PublishedSphericalInputs (relativeMatrix M X))
    (hVisual : PublishedVisualSplitting M)
    (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.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.ParabolicIntersections.PublishedVisualSplitting, OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal