EncodedSegmentSeparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.Code.encoded_block_segment_separation line 15
Source documentation
Simultaneous separation of the actual codeword segments implies the concrete within-block separation predicate used by unequal matching counts. Optional lookup makes the bad-pair predicate total on natural block indices; the predicate is only used at the explicitly valid indices in this theorem.
```
theorem encoded_block_segment_separation {α : Type u} {β : Type v}
    {M P a₀ : ℕ} (c : α → Word β P)
    (hsep : ∀ k l : α, k ≠ l → ∀ a i j : ℕ, a₀ ≤ a →
      i + a ≤ P → j + a ≤ P →
      100 * lcs (((c k).val.drop i).take a) (((c l).val.drop j).take a) ≤ 99 * a)
    (x y : List α) (hx : x.length = M) (hy : y.length = M) :
    BlockSegmentSeparation (encodedBit c x hx) (encodedBit c y hy)
      (fun b => x[b.1]? ≠ y[b.2]?) a₀ := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.Code.BlockSegmentSeparation, OAI.TreeEdit.BinaryLower.Code.encodedBit

theorem OAI.TreeEdit.BinaryLower.Code.additive_of_codeword_separation line 50

Source documentation

The actual codebook's segment property gives the full additive deficit bound, with no remaining local charge or matching-count hypothesis.

theorem additive_of_codeword_separation {α : Type u} {β : Type v}
    {M P a₀ : ℕ} (hP : 0 < P) (c : α → Word β P)
    (hsep : ∀ k l : α, k ≠ l → ∀ a i j : ℕ, a₀ ≤ a →
      i + a ≤ P → j + a ≤ P →
      100 * lcs (((c k).val.drop i).take a) (((c l).val.drop j).take a) ≤ 99 * a)
    (x y : List α) (hx : x.length = M) (hy : y.length = M) :
    P * deficit M x y ≤
      201 * deficit (M * P) (encode c x) (encode c y) + 2 * M * a₀ := by
…

Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.lcs, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.encode