EncodingIndex.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Indexing fixed-width concatenated codewords.

theorem OAI.TreeEdit.BinaryLower.getElem?_encode_block line 13
Source documentation
A block-coordinate lookup in the actual concatenation extension.
```
theorem getElem?_encode_block (c : α → Word β P) (x : List α)
    (i j : ℕ) (hi : i < x.length) (hj : j < P) :
    (encode c x)[i * P + j]? = (c x[i]).val[j]? := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode
theorem OAI.TreeEdit.BinaryLower.getElem?_encode_quotient line 36
Source documentation
Any encoded position is found by its quotient block and remainder offset.
```
theorem getElem?_encode_quotient (c : α → Word β P) (x : List α)
    (k : ℕ) (hP : 0 < P) (hk : k / P < x.length) :
    (encode c x)[k]? = (c x[k / P]).val[k % P]? := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode

theorem OAI.TreeEdit.BinaryLower.getElem_encode_block line 43

Source documentation

The total lookup counterpart of getElem?_encode_block.

theorem getElem_encode_block (c : α → Word β P) (x : List α)
    (i j : ℕ) (hi : i < x.length) (hj : j < P)
    (hbit : i * P + j < (encode c x).length) :
    (encode c x)[i * P + j] =
      (c x[i]).val[j]'(by rw [(c x[i]).property]; exact hj) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode

theorem OAI.TreeEdit.BinaryLower.getElem_encode_quotient line 53

Source documentation

Total lookup at an arbitrary encoded position.

theorem getElem_encode_quotient (c : α → Word β P) (x : List α)
    (k : ℕ) (hP : 0 < P) (hk : k / P < x.length)
    (hbit : k < (encode c x).length) :
    (encode c x)[k] =
      (c x[k / P]).val[k % P]'(by rw [(c x[k / P]).property]; exact Nat.mod_lt k hP) := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode

theorem OAI.TreeEdit.BinaryLower.encode_segment_eq line 65
Source documentation
A segment wholly contained in one encoded block is exactly the corresponding segment of that codeword.
```
theorem encode_segment_eq (c : α → Word β P) (x : List α)
    (i j a : ℕ) (hi : i < x.length) (hja : j + a ≤ P) :
    ((encode c x).drop (i * P + j)).take a =
      (((c x[i]).val).drop j).take a := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode

theorem OAI.TreeEdit.BinaryLower.encode_segment_quotient_eq line 78

Source documentation

The same segment identity with start specified as one global index.

theorem encode_segment_quotient_eq (c : α → Word β P) (x : List α)
    (k a : ℕ) (hk : k / P < x.length) (hka : k % P + a ≤ P) :
    ((encode c x).drop k).take a =
      (((c x[k / P]).val).drop (k % P)).take a := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.encode