OAI/Algebra/Finitistic/Iteration/BinomialEvenIteration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExternalTensor.Binomial.evenIteration line 15

   Source documentation

   Section 6's even-iterate formula, for an actual endofunctor and an objectwise two-step split.

   def evenIteration
       (split : ∀ Y, F.obj (F.obj (M Y)) ≅ (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+3⟧)
       (j : ℕ) (Y : S) :
       (F.obj^[2*j]) (M Y) ≅
         ⨁ fun q : Fin (j+1) => ⨁ fun _ : Fin (Nat.choose j q.val) =>
           (M ((H^[j]) Y))⟦(j : ℤ)*b + 3*(q.val : ℤ)⟧ := by
   …

2. theorem OAI.ExternalTensor.Binomial.evenIteration_isZero_iff line 27

   Source documentation

   The precise vanishing equivalence behind the main proof's extinction step.

   theorem evenIteration_isZero_iff
       (split : ∀ Y, F.obj (F.obj (M Y)) ≅ (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+3⟧)
       (j : ℕ) (Y : S) :
       IsZero ((F.obj^[2*j]) (M Y)) ↔ IsZero (M ((H^[j]) Y)) :=
   …

3. theorem OAI.ExternalTensor.Binomial.even_extinction_pair line 35

   Source documentation

   Transfer a concrete zero/nonzero pair without assuming M preserves or reflects zero.

   theorem even_extinction_pair
       (split : ∀ Y, F.obj (F.obj (M Y)) ≅ (M (H Y))⟦b⟧ ⊞ (M (H Y))⟦b+3⟧)
       (m : ℕ) (Y : S)
       (vanishes : IsZero (M ((H^[m+1]) Y)))
       (survives : ¬ IsZero (M ((H^[m]) Y))) :
       IsZero ((F.obj^[2*(m+1)]) (M Y)) ∧ ¬ IsZero ((F.obj^[2*m]) (M Y)) :=
   …