OAI.HarmonicArtin.ParabolicIntersections.unconditional_nonclique_dynamics
OpenThe theorem states that, for a Coxeter matrix M on a finite, linearly ordered generating set S, if M is irreducible and some pair of distinct generators s and t has M s t = 0 (the Coxeter-matrix entry meaning no braid relation between them, so the pair generates a free-product-type factor with no relation), then the Artin group Artin(M), presented by the braid relations alternating(s,t) of length M s t equal to alternating(t,s) of length M s t, has two properties. First, it is acylindrically hyperbolic, meaning it acts by isometries on some geodesic Gromov-hyperbolic metric space, with an acylindrical action (for each ε>0 there are R and N such that any two points at distance at least R are moved by at most N group elements, a finite set, by at most ε each) that is non-elementary in the sense that three orbit sequences exist with Gromov-sequence limit behavior and pairwise bounded Gromov products. Second, every parabolic subgroup P, meaning a conjugate of the subgroup generated by the standard generators in some subset X of S, that is not the whole group is weakly malnormal: there is some g in Artin(M) for which P intersected with gPg⁻¹ is finite. Irreducibility means that no nontrivial partition of S has all cross labels equal to 2. The proof is admitted in the source.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ArtinParabolicIntersections.lean; bytes 4812..5222
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
import Definitions.Def_ArtinParabolicIntersections
namespace OAI
namespace HarmonicArtin.ParabolicIntersections
variable {S : Type} [Fintype S] [LinearOrder S] (M : CoxeterMatrix S)
/-- An irreducible non-clique Artin group has an acylindrical non-elementary
hyperbolic action and all its proper parabolics are weakly malnormal. -/
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
sorry
end HarmonicArtin.ParabolicIntersections
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.