SphericalProperSupport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One proper support controls every bounded-height positive continuation.

theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_proper_positive_support line 19

Source documentation

Lemma 7.6 for the actual pointed family. Both conditional inputs concern published positive-monoid or mesh-algebra results.

theorem spherical_proper_positive_support (Y : Set S) (hY : IsSpherical M Y)
    (hf : f ∉ Y) (hGcd : PublishedFoldingGcd M Y hY)
    (hmesh : MeshNilpotent Q (fusionColorRegion m (Sum.inl '' Y)))
    (x : Artin M) (hx : x ∈ artinParabolic M {f}ᶜ) (t : ℤ)
    (ht : ∀ L, ClassTestUpper Q (pointedFamily M f x L)
      (Set.range (unfoldedInclusion M Y)) t)
    (hnonzero : ∃ L, ¬ ∀ α ∈ Set.range (unfoldedInclusion M Y), ∀ l c,
      ClassTestExact Q α l c (pointedFamily M f x L)) :
    ∃ p : PositiveArtin (restrictedMatrix M Y),
      (∀ L, ClassTestUpper Q (restrictedPointedFamily M f Y x (positiveToArtin _ p) L)
        (Set.range (unfoldedInclusion M Y)) t) ∧
      ∃ J : Set Y, J ⊂ Set.univ ∧ ∀ b : PositiveArtin (restrictedMatrix M Y),
…

Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.ParabolicIntersections.PublishedFoldingGcd, OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent, OAI.HarmonicArtin.fusionColorRegion, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily, OAI.HarmonicArtin.unfoldedInclusion, OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.ParabolicIntersections.restrictedPointedFamily, OAI.HarmonicArtin.positiveToArtin