RecursiveSuffixInduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_generator_positive line 26
theorem OAI.DerivedBar.ParityBridge.innerSummand_positive_input_zero line 82
Source documentation
A zero final input term cannot contribute an element, at any recursive depth.
```
theorem innerSummand_positive_input_zero (r n : ℕ) (t : RecursiveTotal.Index r n)
    (h : RecursiveTotal.inputDegree r t ≠ 0) (v : RecursiveTotal.summand B Z r n t) : v=0 := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.summand

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_generator_bottom line 91

Source documentation

The only remaining generator case has suffix total degree zero. Its tail face vanishes by the already proved augmented bottom identity.

theorem innerEmbedding_generator_bottom (r n i : ℕ) (h : i+0=n+1)
    (t : RecursiveTotal.Index r 0)
    (v : RecursiveTotal.summand B Z (r+1) (n+1) ⟨⟨⟨i,0⟩,h⟩,t⟩) :
    SquareZero.multibarAugmentedDifferential k D X N ((r+1)+n)
      (innerEmbedding k D X N (r+1) (n+1)
        ((RecursiveTotal.lof B Z (r+1) (n+1) ⟨⟨⟨i,0⟩,h⟩,t⟩).hom v)) =
    -innerEmbedding k D X N (r+1) n
      ((RecursiveTotal.differential B Z (r+1) n).hom
        ((RecursiveTotal.lof B Z (r+1) (n+1) ⟨⟨⟨i,0⟩,h⟩,t⟩).hom v)) := by
…

Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.lof, OAI.DerivedBar.RecursiveTotal.differential

theorem OAI.DerivedBar.ParityBridge.innerEmbedding_differential line 140
Source documentation
The canonical inner finite-sum embedding compares the actual independently recursive differential with minus augmented slot parity, at every depth and degree.
```
theorem innerEmbedding_differential (r n : ℕ) (v : RecursiveTotal.flat B Z r (n+1)) :
    SquareZero.multibarAugmentedDifferential k D X N (r+n)
      (innerEmbedding k D X N r (n+1) v) =
    -innerEmbedding k D X N r n ((RecursiveTotal.differential B Z r n).hom v) := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.flat, OAI.DerivedBar.SquareZero.multibarAugmentedDifferential, OAI.DerivedBar.ParityBridge.innerEmbedding, OAI.DerivedBar.RecursiveTotal.differential