DynamicsMain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Corollary 1.3 with only the general amalgam criterion remaining

The Artin-specific statements of Charney--Martin--Morris-Wright, Theorem 3.2 and Proposition 4.2, are proved in this development. The only remaining published input is Minasyan--Osin (2015), Corollary 2.2, for arbitrary amalgamated products. In particular the weak-malnormality half of the corollary has no published hypotheses.

theorem OAI.HarmonicArtin.ParabolicIntersections.proper_parabolic_criterion line 19
Source documentation
The sufficient case of CMMW Proposition 4.2, now proved locally.
```
theorem proper_parabolic_criterion : PublishedProperParabolicCriterion M where
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedProperParabolicCriterion
theorem OAI.HarmonicArtin.ParabolicIntersections.unconditional_nonclique_weaklyMalnormal line 26
Source documentation
The weak-malnormality assertion of paper 082-03, Corollary 1.3, without any published input.
```
theorem unconditional_nonclique_weaklyMalnormal
    (hIrred : IsIrreducible M) (hInf : ∃ s t : S,s≠t ∧ M s t=0)
    (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
theorem OAI.HarmonicArtin.ParabolicIntersections.nonclique_dynamics_of_amalgam line 35
Source documentation
Paper 082-03, Corollary 1.3, conditional only on the general published amalgam theorem of Minasyan--Osin, with every Artin-specific input discharged.
```
theorem nonclique_dynamics_of_amalgam
    (hMO : PublishedAmalgamCriterion)
    (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 :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedAmalgamCriterion, OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal