UnconditionalMain.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Unconditional parabolic intersections and closure

The spherical mesh input is proved by weighted path contractions and finite Jones--Wenzl projections. Together with the proved standard embeddings, folding, and acyclic evaluation, this discharges every input to Theorem 1.1 and Corollary 1.2 of paper 082-03. The dynamical corollary below still names its separate published geometric input explicitly.

theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_mesh_input line 20
Source documentation
The full spherical mesh input, without hypotheses from the literature.
```
theorem spherical_mesh_input : PublishedMeshInput M :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedMeshInput
theorem OAI.HarmonicArtin.ParabolicIntersections.unconditional_inside_intersection line 26
Source documentation
The stronger inside-parabolic form used in the rank arguments.
```
theorem unconditional_inside_intersection : InsideIntersectionProperty M :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty
theorem OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections line 31
Source documentation
Paper 082-03, Theorem 1.1, with every published input discharged.
Distinct definitions of this name: ComparatorChallenges/ArtinParabolicIntersections.lean:98 (same statement text; different proof or body). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections@path.
```
theorem unconditional_parabolic_intersections
    (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.Artin, OAI.HarmonicArtin.artinParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.unconditional_arbitrary_intersections line 39
Source documentation
Paper 082-03, Corollary 1.2: arbitrary intersections and the rank bound.
Distinct definitions of this name: ComparatorChallenges/ArtinParabolicIntersections.lean:106 (same statement text; different proof or body). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.unconditional_arbitrary_intersections@path.
```
theorem unconditional_arbitrary_intersections
    (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.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_closure line 47
Source documentation
Paper 082-03, Corollary 1.2: the unique smallest containing parabolic.
Distinct definitions of this name: ComparatorChallenges/ArtinParabolicIntersections.lean:114 (same statement text; different proof or body). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_closure@path.
```
theorem unconditional_parabolic_closure (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.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.nonclique_dynamics_of_visual_splitting line 54
Source documentation
Paper 082-03, Corollary 1.3, conditional only on the geometric criteria of Charney--Martin--Morris-Wright, Theorem 3.2 and Proposition 4.2.
```
theorem nonclique_dynamics_of_visual_splitting
    (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.PublishedVisualSplitting, OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible, OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic, OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal