SelectedCountCohomology.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.SelectedCountCohomology.count line 14
Source documentation
The original summand with exactly r square-zero factors in the actual bar complex.
```
abbrev count (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :=
…
```
def OAI.LittleFinitistic.SelectedCountCohomology.comparison line 18
Source documentation
Its exact standard integer-shift identification with the genuine derived iterate.
```
def comparison (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :
    (object Y r)⟦(r : ℤ)⟧ ≅ count Y r :=
…
```
Mentions: OAI.LittleFinitistic.SelectedCountCohomology.count
theorem OAI.LittleFinitistic.SelectedCountCohomology.isZero_iff line 22
theorem OAI.LittleFinitistic.SelectedCountCohomology.bounded line 27
theorem OAI.LittleFinitistic.SelectedCountCohomology.nonzero_degree line 45
Source documentation
Every surviving iterate contributes a nonzero original count class in a homological degree at least r, with an explicit finite upper bound.
```
theorem nonzero_degree (Y : FiniteSelectionFamily.S.{0}) (r : ℕ)
    (h : ¬ IsZero (object Y r)) :
    ∃ n : ℕ, r ≤ n ∧ n ≤ r * (3 * length + 5) ∧
      ¬ IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj (count Y r)) := by
…
```
Mentions: OAI.LittleFinitistic.SelectedCountCohomology.count