PointedSphericalNoChain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The bounded-positive-height obstruction for the actual pointed family.

lemma OAI.HarmonicArtin.ParabolicIntersections.pointed_endomorphism_dimension_le_one line 19
Source documentation
Every member is the transport of one indecomposable projective.
```
lemma pointed_endomorphism_dimension_le_one (z : Artin M)
    (hz : z ∈ artinParabolic M {f}ᶜ) (L : PointedLabel M) :
    classHomDimension Q 0 0 (pointedFamily M f z L) (pointedFamily M f z L) ≤ 1 := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.PointedLabel, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily
lemma OAI.HarmonicArtin.ParabolicIntersections.pointed_exterior_generator line 29
Source documentation
An unoperated frame supplies a nonzero exterior generator in each member, including when its cochain position is not explicitly chosen.
```
lemma pointed_exterior_generator (Y : Set S) (hf : f ∉ Y) (z : Artin M)
    (hz : z ∈ artinParabolic M {f}ᶜ) (L : PointedLabel M) :
    ∃ p : GeneratorPlacement (FusionVertex (V := S⊕Unit) m),
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.PointedLabel, OAI.HarmonicArtin.GeneratorPlacement, OAI.HarmonicArtin.FusionVertex

theorem OAI.HarmonicArtin.ParabolicIntersections.pointed_no_bounded_complete_positive_chain line 52

Source documentation

Proposition 7.4, with the actual Artin action and complete passes through the original colors. The mesh hypothesis is the abstract published finite-Dynkin path input; no categorical obstruction is assumed.

theorem pointed_no_bounded_complete_positive_chain (Y : Set S) (hf : f ∉ Y)
    (hmesh : MeshNilpotent Q (fusionColorRegion m (Sum.inl '' Y)))
    (z : ℕ → Artin M) (u : ℕ → List S)
    (hz : z 0 ∈ artinParabolic M {f}ᶜ)
    (hstep : ∀ n, z (n+1) = wordArtin M (u n) * z n)
    (hu : ∀ n s, s ∈ u n ↔ s ∈ Y)
    (L : PointedLabel M)
    (hnonzero : ¬ ∀ α ∈ fusionColorRegion m (Sum.inl '' Y), ∀ l c,
      ClassTestExact Q α l c (pointedFamily M f (z 0) L))
    (t : ℤ) (ht : ∀ n, ClassTestUpper Q (pointedFamily M f (z n) L)
      (fusionColorRegion m (Sum.inl '' Y)) t) : False := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent, OAI.HarmonicArtin.fusionColorRegion, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.wordArtin, OAI.HarmonicArtin.ParabolicIntersections.PointedLabel, OAI.HarmonicArtin.ParabolicIntersections.pointedFamily