ModuleBlockIndex.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.RecursiveTotal.moduleBlocks line 9
Source documentation
Remove the zero input degree from the list of bar lengths.
```
def moduleBlocks : (r : ℕ) → {n : ℕ} → (t : Index (r+1) n) → Blocks r
  | 0, _, ⟨p,_⟩ => p.val.1
  | r+1, _, ⟨p,t⟩ => (p.val.1, moduleBlocks r t)
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index
theorem OAI.DerivedBar.RecursiveTotal.total_moduleBlocks line 13
theorem OAI.DerivedBar.RecursiveTotal.pattern_moduleBlocks line 23

def OAI.DerivedBar.RecursiveTotal.moduleIndex line 36

Source documentation

The recursive total index attached to a block tuple, with input degree zero.

def moduleIndex : (r : ℕ) → (b : Blocks r) → Index (r+1) (total r b)
  | 0, i => ⟨⟨⟨i,0⟩,by exact Nat.add_zero i⟩,()⟩
  | r+1, (i,b) => ⟨⟨⟨i,total r b⟩,rfl⟩,moduleIndex r b⟩

Mentions: OAI.DerivedBar.RecursiveTotal.Index

theorem OAI.DerivedBar.RecursiveTotal.inputDegree_moduleIndex line 40
theorem OAI.DerivedBar.RecursiveTotal.moduleBlocks_moduleIndex line 46
theorem OAI.DerivedBar.RecursiveTotal.inputDegree_castIndex line 52
theorem OAI.DerivedBar.RecursiveTotal.moduleBlocks_castIndex line 55
theorem OAI.DerivedBar.RecursiveTotal.moduleBlocks_injective line 60
Source documentation
All indices are recovered from the blocks and input degree; no quotient of block tensors or identification of distinct patterns is introduced.
```
theorem moduleBlocks_injective (r n : ℕ) (t s : Index (r+1) n)
    (ht : inputDegree (r+1) t=0) (hs : inputDegree (r+1) s=0)
    (h : moduleBlocks r t=moduleBlocks r s) : t=s := by
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.moduleBlocks
def OAI.DerivedBar.RecursiveTotal.moduleBlockEquiv line 87
Source documentation
Exact module-input indexing by the manuscript's tuples of r+1 block lengths.
```
def moduleBlockEquiv (r n : ℕ) :
    {t : Index (r+1) n // inputDegree (r+1) t=0} ≃
      {b : Blocks r // total r b=n} where
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree
def OAI.DerivedBar.RecursiveTotal.moduleShapeEquiv line 102
Source documentation
Exact full-degree shape index, including the shift by the number of X slots.
```
def moduleShapeEquiv (r n : ℕ) :
    {t : Index (r+1) n // inputDegree (r+1) t=0} ≃
      Multibar.Indexed.Shape (r+n) r :=
…
```
Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.Multibar.Indexed.Shape