ConditionalMain.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Main statements with the acyclic-evaluation input already discharged.

structure OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalAlgebraInputs line 12
Source documentation
The two remaining published finite-type algebra inputs.
```
structure PublishedSphericalAlgebraInputs : Prop where
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalAlgebraInputs.withAcyclic line 18
theorem OAI.HarmonicArtin.ParabolicIntersections.main_parabolic_intersections line 27
Source documentation
Paper 082-03, Theorem 1.1.
```
theorem main_parabolic_intersections
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hAlg : ∀ X : Set S, PublishedSphericalAlgebraInputs (relativeMatrix M X))
    (X Y : Set S) (g h : Artin M) :
    ∃ (Z : Set S) (k : Artin M),
      conjugate g (artinParabolic M X) ⊓ conjugate h (artinParabolic M Y) =
        conjugate k (artinParabolic M Z) :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalAlgebraInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.main_arbitrary_intersections line 37

Source documentation

Paper 082-03, Corollary 1.2, including the empty family.

theorem main_arbitrary_intersections
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hAlg : ∀ X : Set S, PublishedSphericalAlgebraInputs (relativeMatrix M X))
    (F : Set (Subgroup (Artin M))) (hF : ∀ P ∈ F, IsParabolic M P) :
    (∃ F₀ : Finset (Subgroup (Artin M)),
      (↑F₀ : Set (Subgroup (Artin M))) ⊆ F ∧ F₀.card ≤ Nat.card S ∧
        sInf F = sInf (↑F₀ : Set (Subgroup (Artin M)))) ∧ IsParabolic M (sInf F) :=
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalAlgebraInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.main_parabolic_closure line 47
Source documentation
Paper 082-03, Corollary 1.2, the closure assertion for every subset.
```
theorem main_parabolic_closure
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hAlg : ∀ X : Set S, PublishedSphericalAlgebraInputs (relativeMatrix M X))
    (E : Set (Artin M)) :
    ∃! P : Subgroup (Artin M), IsParabolic M P ∧ E ⊆ P ∧
      ∀ Q : Subgroup (Artin M), IsParabolic M Q → E ⊆ Q → P ≤ Q :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalAlgebraInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.main_nonclique_dynamics line 56
Source documentation
Paper 082-03, Corollary 1.3, both dynamical assertions.
```
theorem main_nonclique_dynamics
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hAlg : ∀ X : Set S, PublishedSphericalAlgebraInputs (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 :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalAlgebraInputs, 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