ReducedDynamicsMain.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The remaining published geometric inputs

The Artin-specific edge-intersection argument of CMMW Theorem 3.2 is now proved locally. The following statements isolate the still-undischarged inputs: the general amalgam criterion (Minasyan--Osin, Acylindrical hyperbolicity of groups acting on trees, 2015, Corollary 2.2; stated as CMMW 2026, Theorem 3.1), and CMMW 2026, Proposition 4.2.

The first is stated for an arbitrary group explicitly isomorphic to a nontrivial amalgam. The second transfers weak malnormality from the edge group to all proper parabolics. Neither assumes the parabolic intersection theorem or its new argument. The local proofs supply the actual amalgam, injectivity, proper inclusions, exclusion of virtually cyclic groups, and weak malnormality of the edge group.

Sources: https://arxiv.org/abs/1310.6289 https://msp.org/agt/2026/26-4/agt-v26-n4-p08-p.pdf

structure OAI.HarmonicArtin.ParabolicIntersections.PublishedAmalgamCriterion line 29
Source documentation
Minasyan--Osin's general nontrivial-amalgam criterion, with the virtually cyclic alternative explicitly excluded.
```
structure PublishedAmalgamCriterion : Prop where
…
```
structure OAI.HarmonicArtin.ParabolicIntersections.PublishedProperParabolicCriterion line 40
Source documentation
CMMW (2026), Proposition 4.2, stated separately from its edge criterion.
```
structure PublishedProperParabolicCriterion : Prop where
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.visual_acylindricallyHyperbolic_of_amalgam line 47
Source documentation
Every hypothesis in the general amalgam criterion is supplied by unconditional theorems for the actual Artin visual splitting.
```
theorem visual_acylindricallyHyperbolic_of_amalgam (hMO : PublishedAmalgamCriterion)
    (hIrred : IsIrreducible M) (Y Z : Set S) (hsplit : IsVisualSplit M Y Z) :
    AcylindricallyHyperbolic (Artin M) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedAmalgamCriterion, OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.IsVisualSplit, OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic, OAI.HarmonicArtin.Artin
theorem OAI.HarmonicArtin.ParabolicIntersections.visualSplitting_of_amalgam_and_proper line 65
Source documentation
Reconstruction of the original published input after discharging its Artin-specific edge criterion.
```
theorem visualSplitting_of_amalgam_and_proper (hMO : PublishedAmalgamCriterion)
    (hProper : PublishedProperParabolicCriterion M) : PublishedVisualSplitting M where
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedAmalgamCriterion, OAI.HarmonicArtin.ParabolicIntersections.PublishedProperParabolicCriterion, OAI.HarmonicArtin.ParabolicIntersections.PublishedVisualSplitting
theorem OAI.HarmonicArtin.ParabolicIntersections.nonclique_dynamics_of_amalgam_and_proper line 75
Source documentation
Paper 082-03, Corollary 1.3, with all algebraic and Artin-specific edge arguments discharged. Only the two identified geometric inputs remain.
```
theorem nonclique_dynamics_of_amalgam_and_proper (hMO : PublishedAmalgamCriterion)
    (hProper : PublishedProperParabolicCriterion 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 :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedAmalgamCriterion, OAI.HarmonicArtin.ParabolicIntersections.PublishedProperParabolicCriterion, OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal