SelectedCountPDConsumer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.SelectedPDDetection.lower_bound_of_surviving_count line 16
Source documentation
A supplied inclusion/retraction of the original count summand into the actual full bar converts native iterate survival directly into the pd bound. Native supplies the proved nonzero degree; no shift/amplitude proof is duplicated.
```
theorem lower_bound_of_surviving_count (Y : FiniteSelectionFamily.S.{0}) (r : ℕ)
    (h : ¬ IsZero (SelectedBaseIterates.object Y r))
    (i : SelectedCountCohomology.count Y r ⟶ PDBarQuotient.baseDerived augmentation (Inflated Y))
    (p : PDBarQuotient.baseDerived augmentation (Inflated Y) ⟶ SelectedCountCohomology.count Y r)
    (hip : i ≫ p = 𝟙 (SelectedCountCohomology.count Y r)) :
    r ≤ projectiveDimension (module Y) := by
…
```
Mentions: OAI.LittleFinitistic.SelectedBaseIterates.object, OAI.LittleFinitistic.SelectedCountCohomology.count, OAI.LittleFinitistic.PDBarQuotient.baseDerived