CodeAdditive.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The longest encoded matching is partitioned by equality of its original block labels. Segment separation and the span loss budget bound the number of unequal-label matches.

def OAI.TreeEdit.BinaryLower.Code.originalLetterAtBit line 17
Source documentation
The original letter whose block contains a specified encoded position.
```
def originalLetterAtBit {α : Type u} {M P : ℕ} (x : List α)
    (hx : x.length = M) (hP : 0 < P) (q : Fin (M*P)) : α :=
…
```
def OAI.TreeEdit.BinaryLower.Code.encodedBit line 22
Source documentation
A bit of the actual concatenation, with its prescribed-length indexing.
```
def encodedBit {α : Type u} {β : Type v} {M P : ℕ}
    (c : α → Word β P) (x : List α) (hx : x.length = M)
    (q : Fin (M*P)) : β :=
…
```
Mentions: OAI.TreeEdit.Word
theorem OAI.TreeEdit.BinaryLower.Code.ofFn_encodedBit line 28
Source documentation
Reading all encoded positions reconstructs the concrete concatenation.
```
@[simp] theorem ofFn_encodedBit {α : Type u} {β : Type v} {M P : ℕ}
    (c : α → Word β P) (x : List α) (hx : x.length = M) :
    List.ofFn (encodedBit c x hx) = encode c x := by
…
```
Mentions: OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.Code.encodedBit, OAI.TreeEdit.encode
theorem OAI.TreeEdit.BinaryLower.Code.getElem?_blockLetter line 38
Source documentation
Optional lookup at an encoded position's block always succeeds and returns exactly its original letter. This avoids partial-label conventions.
```
theorem getElem?_blockLetter {α : Type u} {M P : ℕ} (x : List α)
    (hx : x.length = M) (hP : 0 < P) (q : Fin (M*P)) :
    x[q.val/P]? = some (originalLetterAtBit x hx hP q) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.Code.originalLetterAtBit

def OAI.TreeEdit.BinaryLower.Code.unequalEdges line 47

Source documentation

Precisely the selected unequal-original-label edges of a matching.

noncomputable def unequalEdges {α : Type u} {M P r : ℕ}
    (x y : List α) (hx : x.length = M) (hy : y.length = M) (hP : 0 < P)
    (f g : Fin r → Fin (M*P)) : Finset (Fin r) := by
…

theorem OAI.TreeEdit.BinaryLower.Code.unequalEdges_eq_filter_getElem? line 56

Source documentation

Unequal-edge selection can equivalently be expressed by a total predicate on the two natural-number block indices using optional original-word lookup.

theorem unequalEdges_eq_filter_getElem? {α : Type u} [DecidableEq α] {M P r : ℕ}
    (x y : List α) (hx : x.length = M) (hy : y.length = M) (hP : 0 < P)
    (f g : Fin r → Fin (M*P)) :
    unequalEdges x y hx hy hP f g =
      Finset.univ.filter (fun t => x[(f t).val/P]? ≠ y[(g t).val/P]?) := by
…

Mentions: OAI.TreeEdit.BinaryLower.Code.unequalEdges

theorem OAI.TreeEdit.BinaryLower.Code.additive_of_longest_unequal_bound line 68

Source documentation

Equal-label coloring and the unequal-label estimate, for actual encoded words and a matching of their longest-common-subsequence length.

theorem additive_of_longest_unequal_bound {α : Type u} {β : Type v}
    {M P a₀ : ℕ} (c : α → Word β P) (x y : List α)
    (hx : x.length = M) (hy : y.length = M) (hP : 0 < P)
    (f g : Fin (lcs (encode c x) (encode c y)) → Fin (M*P))
    (hf : StrictMono f) (hg : StrictMono g)
    (hunequal : (unequalEdges x y hx hy hP f g).card ≤
      200*(M*P-lcs (encode c x) (encode c y))+2*M*a₀) :
    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.encode, OAI.TreeEdit.BinaryLower.Code.unequalEdges, OAI.TreeEdit.BinaryLower.deficit

theorem OAI.TreeEdit.BinaryLower.Code.additive_of_unequal_matching_bound line 112

Source documentation

An unequal count proved for every actual encoded matching yields the source additive estimate by choosing a longest encoded matching.

theorem additive_of_unequal_matching_bound {α : Type u} {β : Type v}
    {M P a₀ : ℕ} (c : α → Word β P) (x y : List α)
    (hx : x.length = M) (hy : y.length = M) (hP : 0 < P)
    (hunequal : ∀ (r : ℕ) (f g : Fin r → Fin (M*P)),
      StrictMono f → StrictMono g →
      (∀ t, encodedBit c x hx (f t) = encodedBit c y hy (g t)) →
      (unequalEdges x y hx hy hP f g).card ≤ 200*(M*P-r)+2*M*a₀) :
    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.BinaryLower.Code.encodedBit, OAI.TreeEdit.BinaryLower.Code.unequalEdges, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.encode