MainIntersection.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The main intersection theorems of paper 082-03

The hypotheses are exactly the published inputs documented in MeshNilpotence, FoldingGcdInput, AcyclicTwistInput, and RelativeInitialStabilizer. All relative-height, positive-height, stabilizer-containment and rank-induction arguments are proved in this local development; none of those new assertions is a hypothesis here.

structure OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalInputs line 24
Source documentation
Only the published general mesh-algebra, admissible-folding and acyclic-evaluation facts; see the individual definitions for exact sources.
```
structure PublishedSphericalInputs : Prop where
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_relative_stabilizers line 33
Source documentation
Theorem 8.2 on the actual pointed family with an unoperated frame.
```
theorem pointed_relative_stabilizers (hPub : PublishedSphericalInputs M)
    (f : S) (Y : Set S) (hf : f ∉ Y) (x : Artin M)
    (hx : x ∈ artinParabolic M {f}ᶜ) :
    ∃ (R : Set S) (c : Artin M), R ⊆ Y ∧ c ∈ artinParabolic M Y ∧
      relativeStabilizer M (pointedInitial M f) Y x = conjugate c⁻¹ (artinParabolic M R) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalInputs, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.relativeStabilizer, OAI.HarmonicArtin.ParabolicIntersections.pointedInitial
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_comap_standard line 53
lemma OAI.HarmonicArtin.ParabolicIntersections.relative_comap_conjugate line 59
theorem OAI.HarmonicArtin.ParabolicIntersections.inside_intersection_at line 67
Source documentation
The stronger inside-parabolic form, with its conjugator inside the acting parabolic. This is the result used by the arbitrary-family theorem.
```
theorem inside_intersection_at
    (hEmb : VanDerLekRelativeEmbedding M X) (hPub : PublishedSphericalInputs N)
    (Y : Set S) (g : Artin M) :
    ∃ (R : Set S) (c : Artin M), R ⊆ Y ∧ c ∈ artinParabolic M Y ∧
      artinParabolic M Y ⊓ conjugate g (artinParabolic M X) =
        conjugate c (artinParabolic M R) := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalInputs, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic
theorem OAI.HarmonicArtin.ParabolicIntersections.inside_intersection line 114
Source documentation
The entire inside-parabolic statement, conditional solely on published inputs.
```
theorem inside_intersection
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hPub : ∀ X : Set S, PublishedSphericalInputs (relativeMatrix M X)) :
    InsideIntersectionProperty M := fun X Y g => inside_intersection_at M X (hEmb X) (hPub X) Y g
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.VanDerLekRelativeEmbedding, OAI.HarmonicArtin.ParabolicIntersections.PublishedSphericalInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.ParabolicIntersections.InsideIntersectionProperty, OAI.HarmonicArtin.ParabolicIntersections.inside_intersection_at
theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_intersections line 120
Source documentation
Theorem 1.1, including arbitrary nonspherical types and infinite labels.
```
theorem parabolic_intersections
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hPub : ∀ X : Set S, PublishedSphericalInputs (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.PublishedSphericalInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.arbitrary_parabolic_intersections line 130

Source documentation

Corollary 1.2: arbitrary intersections and the sharp rank subfamily bound.

theorem arbitrary_parabolic_intersections
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hPub : ∀ X : Set S, PublishedSphericalInputs (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.PublishedSphericalInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic

theorem OAI.HarmonicArtin.ParabolicIntersections.parabolic_closure line 140
Source documentation
Corollary 1.2: every subset has a unique smallest parabolic closure.
```
theorem parabolic_closure
    (hEmb : ∀ X : Set S, VanDerLekRelativeEmbedding M X)
    (hPub : ∀ X : Set S, PublishedSphericalInputs (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.PublishedSphericalInputs, OAI.HarmonicArtin.ParabolicIntersections.relativeMatrix, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic