ReducedInputsMain.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Main results after discharging the acyclic-twist and folding inputs.

def OAI.HarmonicArtin.ParabolicIntersections.PublishedMeshInput line 12
Source documentation
The remaining finite-type input is positive-degree mesh nilpotence.
```
def PublishedMeshInput : Prop :=
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.PublishedMeshInput.withAlgebra line 17
theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_parabolic_intersections line 25
Source documentation
Theorem 1.1 with both the acyclic and folding inputs discharged.
```
theorem mesh_parabolic_intersections
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hMesh : ∀ X : Set S, PublishedMeshInput (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.PublishedMeshInput, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_arbitrary_intersections line 36
Source documentation
Corollary 1.2: every intersection is parabolic and is already a finite intersection of at most the rank many members.
```
theorem mesh_arbitrary_intersections
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hMesh : ∀ X : Set S, PublishedMeshInput (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.PublishedMeshInput, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_parabolic_closure line 46
Source documentation
Corollary 1.2: every subset has a unique smallest containing parabolic.
```
theorem mesh_parabolic_closure
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hMesh : ∀ X : Set S, PublishedMeshInput (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.PublishedMeshInput, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_nonclique_dynamics line 55
Source documentation
Corollary 1.3 with both categorical inputs discharged.
```
theorem mesh_nonclique_dynamics
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hMesh : ∀ X : Set S, PublishedMeshInput (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.PublishedMeshInput, 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