MeshMain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Main results after discharging standard embeddings, acyclic twists, and folding. Only mesh nilpotence and the dynamical criteria remain.

theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_intersections_of_mesh line 14
Source documentation
Paper 082-03, Theorem 1.1, with all inputs except mesh nilpotence discharged.
```
theorem parabolic_intersections_of_mesh
    (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.PublishedMeshInput, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.arbitrary_intersections_of_mesh line 23

Source documentation

Paper 082-03, Corollary 1.2, arbitrary intersections.

theorem arbitrary_intersections_of_mesh
    (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.PublishedMeshInput, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_closure_of_mesh line 32
Source documentation
Paper 082-03, Corollary 1.2, parabolic closure.
```
theorem parabolic_closure_of_mesh
    (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.PublishedMeshInput, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.nonclique_dynamics_of_mesh line 40
Source documentation
Paper 082-03, Corollary 1.3, with only the mesh and dynamics inputs.
```
theorem nonclique_dynamics_of_mesh
    (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.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