NormalParabolic.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Normal parabolics in irreducible Artin groups

This proves the sufficient case of Charney--Martin--Morris-Wright (2026), Lemma 3.3, used in the visual-splitting argument. The obstruction is detected in the actual Coxeter geometric representation, without any assumption on positive-monoid embeddings.

lemma OAI.HarmonicArtin.ParabolicIntersections.artinCoxeter_mem_parabolic line 21
lemma OAI.HarmonicArtin.ParabolicIntersections.generator_mem_standard_iff line 34
Source documentation
The standard generators in a standard parabolic are exactly its type.
```
lemma generator_mem_standard_iff (X : Set S) (t : S) :
    generator M t ∈ artinParabolic M X ↔ t∈X := by
…
```
Mentions: OAI.HarmonicArtin.generator, OAI.HarmonicArtin.artinParabolic
lemma OAI.HarmonicArtin.ParabolicIntersections.standard_ne_top_of_ne_univ line 51
lemma OAI.HarmonicArtin.ParabolicIntersections.cartan_ne_zero_of_not_commuting line 62
theorem OAI.HarmonicArtin.ParabolicIntersections.generator_conjugate_not_mem line 77
Source documentation
A noncommuting generator outside a standard parabolic does not normalize it.
```
theorem generator_conjugate_not_mem {X : Set S} {s t : S}
    (hs : s∈X) (ht : t∉X) (hlabel : M s t≠2) :
    generator M t * generator M s * (generator M t)⁻¹ ∉ artinParabolic M X := by
…
```
Mentions: OAI.HarmonicArtin.generator, OAI.HarmonicArtin.artinParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.normal_standard_parabolic line 99
Source documentation
CMMW Lemma 3.3: in irreducible type a normal standard parabolic is trivial or the whole Artin group.
```
theorem normal_standard_parabolic (hIrred : IsIrreducible M) (X : Set S)
    (hn : (artinParabolic M X).Normal) : X=∅ ∨ X=Set.univ := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.artinParabolic