SelectedCountExtinction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.SelectedCountExtinction.tail_zero line 13
Source documentation
After actual tensor extinction, all later original count summands vanish.
```
theorem tail_zero (Y : FiniteSelectionFamily.S.{0}) (t r : ℕ) (htr : t ≤ r)
    (h : IsZero (object Y t)) : IsZero (count Y r) :=
…
```
theorem OAI.LittleFinitistic.SelectedCountExtinction.uniform_bounded line 20
Source documentation
A zero iterate gives one finite cohomological window for the entire original count family, including the infinitely many counts that have already vanished.
```
theorem uniform_bounded (Y : FiniteSelectionFamily.S.{0}) (t : ℕ)
    (h : IsZero (object Y t)) (r : ℕ) :
    (count Y r).IsGE (-((t * (3 * length + 5) : ℕ) : ℤ)) ∧ (count Y r).IsLE 0 := by
…
```

theorem OAI.LittleFinitistic.SelectedCountExtinction.uniform_homology_zero line 37

Source documentation

Every original count has zero cohomology outside that single finite window.

theorem uniform_homology_zero (Y : FiniteSelectionFamily.S.{0}) (t : ℕ)
    (h : IsZero (object Y t)) (r : ℕ) (i : ℤ)
    (hi : i < -((t * (3 * length + 5) : ℕ) : ℤ) ∨ 0 < i) :
    IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) i).obj (count Y r)) := by
…