BlockExtraction.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact contiguous-window extraction from fixed-width block concatenations.

theorem OAI.TreeEdit.BinaryLower.BlockExtraction.length_flatten_fixed line 12

Source documentation

A list of fixed-width blocks has the expected total length.

theorem length_flatten_fixed {α : Type*} (blocks : List (List α)) (B : ℕ)
    (hB : ∀ z ∈ blocks, z.length = B) : blocks.flatten.length = blocks.length * B := by
…

theorem OAI.TreeEdit.BinaryLower.BlockExtraction.extract_flatten_fixed line 24

Source documentation

The i-th fixed-width block is exactly the corresponding window of the flattened list. This includes width zero.

theorem extract_flatten_fixed {α : Type*} (blocks : List (List α)) (B : ℕ)
    (hB : ∀ z ∈ blocks, z.length = B) (i : ℕ) (hi : i < blocks.length) :
    (blocks.flatten.drop (i * B)).take B = blocks[i] := by
…

theorem OAI.TreeEdit.BinaryLower.BlockExtraction.length_flatten_ofFn line 44
Source documentation
The expected length for a finite indexed family of fixed-width blocks.
```
theorem length_flatten_ofFn {α : Type*} {n B : ℕ} (blocks : Fin n → Word α B) :
    (List.ofFn (fun i => (blocks i).val)).flatten.length = n * B := by
…
```
Mentions: OAI.TreeEdit.Word

theorem OAI.TreeEdit.BinaryLower.BlockExtraction.extract_flatten_ofFn line 53

Source documentation

Window extraction for an indexed family of fixed-width words.

theorem extract_flatten_ofFn {α : Type*} {n B : ℕ}
    (blocks : Fin n → Word α B) (i : Fin n) :
    ((List.ofFn (fun j => (blocks j).val)).flatten.drop (i.val * B)).take B =
      (blocks i).val := by
…

Mentions: OAI.TreeEdit.Word

def OAI.TreeEdit.BinaryLower.BlockExtraction.concatenate line 65
Source documentation
The finite-range flatMap presentation used for rows in the manuscript.
```
def concatenate {α : Type*} {n B : ℕ} (blocks : Fin n → Word α B) : List α :=
…
```
Mentions: OAI.TreeEdit.Word
theorem OAI.TreeEdit.BinaryLower.BlockExtraction.length_concatenate line 68
theorem OAI.TreeEdit.BinaryLower.BlockExtraction.extract_concatenate line 74
Source documentation
Exact extraction from the finite-range flatMap presentation.
```
theorem extract_concatenate {α : Type*} {n B : ℕ}
    (blocks : Fin n → Word α B) (i : Fin n) :
    ((concatenate blocks).drop (i.val * B)).take B = (blocks i).val := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.BlockExtraction.concatenate
def OAI.TreeEdit.BinaryLower.BlockExtraction.rowWord line 81
Source documentation
A row is itself a word of width mB.
```
def rowWord {α : Type*} {m B : ℕ} (blocks : Fin m → Word α B) : Word α (m * B) :=
…
```
Mentions: OAI.TreeEdit.Word
def OAI.TreeEdit.BinaryLower.BlockExtraction.concatenateRows line 85
Source documentation
Concatenation of a finite ordered array of fixed-width blocks.
```
def concatenateRows {α : Type*} {T m B : ℕ}
    (blocks : Fin T → Fin m → Word α B) : List α :=
…
```
Mentions: OAI.TreeEdit.Word
theorem OAI.TreeEdit.BinaryLower.BlockExtraction.length_concatenateRows line 90
theorem OAI.TreeEdit.BinaryLower.BlockExtraction.extract_row line 96
Source documentation
Taking the a-th row of the nested concatenation recovers that precise row.
```
theorem extract_row {α : Type*} {T m B : ℕ}
    (blocks : Fin T → Fin m → Word α B) (a : Fin T) :
    ((concatenateRows blocks).drop (a.val * (m * B))).take (m * B) =
      concatenate (blocks a) := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.BlockExtraction.concatenateRows, OAI.TreeEdit.BinaryLower.BlockExtraction.concatenate

theorem OAI.TreeEdit.BinaryLower.BlockExtraction.extract_cell_in_row line 103

Source documentation

Extracting a cell after its row recovers the original source block.

theorem extract_cell_in_row {α : Type*} {T m B : ℕ}
    (blocks : Fin T → Fin m → Word α B) (a : Fin T) (i : Fin m) :
    ((((concatenateRows blocks).drop (a.val * (m * B))).take (m * B)).drop
      (i.val * B)).take B = (blocks a i).val := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.BlockExtraction.concatenateRows

theorem OAI.TreeEdit.BinaryLower.BlockExtraction.nested_window line 112
Source documentation
Nested windows agree with direct extraction whenever the inner window fits in the outer one.
```
theorem nested_window {α : Type*} (x : List α) (A L a b : ℕ)
    (hfit : a + b ≤ L) :
    ((((x.drop A).take L).drop a).take b) = (x.drop (A + a)).take b := by
…
```
theorem OAI.TreeEdit.BinaryLower.BlockExtraction.extract_cell line 119
Source documentation
Direct extraction of any cell at its absolute position in the array.
```
theorem extract_cell {α : Type*} {T m B : ℕ}
    (blocks : Fin T → Fin m → Word α B) (a : Fin T) (i : Fin m) :
    ((concatenateRows blocks).drop ((a.val * m + i.val) * B)).take B =
      (blocks a i).val := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.BlockExtraction.concatenateRows