SelectedFiniteAmplitude.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.SelectedFiniteAmplitude.bounded line 14
Source documentation
Every genuine X-derived iterate of each actual test input has finite amplitude. The extra two degrees per iteration are harmless for the finite-dimension argument.
```
theorem bounded (Y : FiniteSelectionFamily.S.{0}) (r : ℕ) :
    (object Y r).IsGE (-((r * (3 * length + 4) : ℕ) : ℤ)) ∧
    (object Y r).IsLE 0 := by
…
```

theorem OAI.LittleFinitistic.SelectedFiniteAmplitude.nonzero_in_window line 22

Source documentation

A nonzero actual iterate is detected in a finite, explicit cohomological window.

theorem nonzero_in_window (Y : FiniteSelectionFamily.S.{0}) (r : ℕ)
    (h : ¬ Limits.IsZero (object Y r)) :
    ∃ n : ℕ, n ≤ r * (3 * length + 4) ∧
      ¬ Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat D) (-(n : ℤ))).obj
        (object Y r)) := by
…

theorem OAI.LittleFinitistic.SelectedFiniteAmplitude.terminal_exact line 33

Source documentation

Any additive terminal tensor applied to a resolved actual iterate has a uniform finite homological bound. This supplies the later residue/simple tests.

theorem terminal_exact {E : Type*} [Category E] [Abelian E]
    (F : ModuleCat.{0} D ⥤ E) [F.Additive]
    (Y : FiniteSelectionFamily.S.{0}) (r n : ℕ)
    (hn : (r+1) * (3 * length + 4) < n) :
    ((F.mapHomologicalComplex (.down ℕ)).obj
      (DerivedBar.barTotal ℂ D (DerivedBar.IterateSupport.resolvedModel ℂ D X (input Y) r))).ExactAt n := by
…

Mentions: OAI.DerivedBar.barTotal, OAI.DerivedBar.IterateSupport.resolvedModel