CoarseSeed.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded-shift coarse tree

Section 3's deterministic shift representation uses a complete finite branching tree with empty/singleton source leaves. Bounded integer shifts are encoded by Fin (2k+1); code k is shift zero. Virtual target positions are represented by fresh none symbols in a finite surrounding frame.

def OAI.EditApproximation.coarseTreeValue line 44
Source documentation
The zero root shift is the middle integer code.
```
def coarseTreeValue {B D : ℕ} {α : Type u} [DecidableEq α]
    (tree : CoarseSourceTree B α D) (target : List α) (k : ℕ) : ℕ :=
…
```
Mentions: OAI.EditApproximation.CoarseSourceTree
theorem OAI.EditApproximation.substring_split line 48
theorem OAI.EditApproximation.substring_one line 59

theorem OAI.EditApproximation.coarse_leaf_edit_le line 65

Source documentation

Leaf editing costs are at most the literal mismatch/virtual-position value, including positions outside the finite frame.

theorem coarse_leaf_edit_le {B : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (frame : List (Option α)) (letter : Option α) (start : ℕ)
    (shift : Fin (2 * k + 1)) :
    edit ((CoarseSourceTree.leaf (B := B) letter).word.map some)
…

theorem OAI.EditApproximation.coarse_child_shift_edit_le line 94

Source documentation

Moving both endpoints by a shift change costs at most twice the absolute difference of their bounded integer codes.

theorem coarse_child_shift_edit_le {α : Type u} (frame : List α) (source : List α)
    (start shift next : ℕ) :
    edit source (substring frame (start + shift) (start + shift + source.length)) ≤
      edit source (substring frame (start + next) (start + next + source.length)) +
        2 * Nat.dist shift next := by
…

Mentions: OAI.EditApproximation.substring

theorem OAI.EditApproximation.coarseChildrenCost_edit_lower line 118

Source documentation

Actual child editing and endpoint movement give the recurrence's lower invariant, proved directly on concatenated source strings.

theorem coarseChildrenCost_edit_lower {B D : ℕ} {α : Type u}
    (k : ℕ) (frame : List (Option α))
    (value : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (children : List (CoarseSourceTree B α D))
    (hchild : ∀ child ∈ children, ∀ start shift,
      edit (child.word.map some)
        (substring frame (start + shift.val) (start + shift.val + child.word.length)) ≤
          value child start shift) (start : ℕ) (shift : Fin (2 * k + 1)) :
    edit ((children.map CoarseSourceTree.word).flatten.map some)
      (substring frame (start + shift.val)
        (start + shift.val + (children.map CoarseSourceTree.word).flatten.length)) ≤
      coarseChildrenCost k value children start shift := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.substring, OAI.EditApproximation.CoarseSourceTree.word, OAI.EditApproximation.coarseChildrenCost

theorem OAI.EditApproximation.coarseShiftCost_edit_lower line 170

Source documentation

The literal bounded-shift tree always dominates edit distance to its corresponding shifted equal-width target interval.

theorem coarseShiftCost_edit_lower {B D : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (frame : List (Option α)) (tree : CoarseSourceTree B α D)
    (start : ℕ) (shift : Fin (2 * k + 1)) :
    edit (tree.word.map some)
      (substring frame (start + shift.val) (start + shift.val + tree.word.length)) ≤
      coarseShiftCost k frame tree start shift := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.substring, OAI.EditApproximation.coarseShiftCost

theorem OAI.EditApproximation.coarseTargetFrame_center line 191
Source documentation
The central equal-width target interval excludes all virtual symbols.
```
theorem coarseTargetFrame_center {α : Type u} (k : ℕ) (target : List α) :
    substring (coarseTargetFrame k target) k (k + target.length) = target.map some := by
…
```
Mentions: OAI.EditApproximation.substring, OAI.EditApproximation.coarseTargetFrame
theorem OAI.EditApproximation.coarseTreeValue_edit_lower line 200
Source documentation
First deterministic shift-tree distortion inequality, for the actual unrestricted unit-cost edit distance and actual finite recurrence.
```
theorem coarseTreeValue_edit_lower {B D : ℕ} {α : Type u} [DecidableEq α] [Inhabited α]
    (tree : CoarseSourceTree B α D) (target : List α) (k : ℕ)
    (hlength : tree.word.length = target.length) :
    edit tree.word target ≤ coarseTreeValue tree target k := by
…
```
Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseTreeValue
theorem OAI.EditApproximation.coarseChildrenCost_le_width line 212

theorem OAI.EditApproximation.coarseShiftCost_le_width line 231

Source documentation

Constant shifts give the exact node-width bound used by pruning.

theorem coarseShiftCost_le_width {B D : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (frame : List (Option α)) (tree : CoarseSourceTree B α D)
    (start : ℕ) (shift : Fin (2 * k + 1)) :
    coarseShiftCost k frame tree start shift ≤ tree.word.length := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseShiftCost

theorem OAI.EditApproximation.coarse_capacity_chunks line 256

Source documentation

The literal consecutive capacity chunks cover exactly the permitted before; zero capacity and empty trailing chunks are included.

theorem coarse_capacity_chunks {α : Type u} (source : List α) (B capacity : ℕ) :
    (List.ofFn fun i : Fin B => (source.drop (i.val * capacity)).take capacity).flatten =
      source.take (B * capacity) := by
…

theorem OAI.EditApproximation.coarseSourceTreeOfList_word line 277
Source documentation
A concrete complete source tree with empty/singleton leaves. Its recursive child chunks have the capacity prescribed by the remaining depth.
```
theorem coarseSourceTreeOfList_word {α : Type u} (B D : ℕ) (source : List α) :
    (coarseSourceTreeOfList B D source).word = source.take (B ^ D) := by
…
```
Mentions: OAI.EditApproximation.coarseSourceTreeOfList
theorem OAI.EditApproximation.coarseSourceTreeOfList_word_eq line 285

theorem OAI.EditApproximation.coarseTargetFrame_prefix_get line 291

Source documentation

A real target character is present at its framed before index.

theorem coarseTargetFrame_prefix_get {α : Type u} (k : ℕ)
    (before suffix : List α) (letter : α) :
    (coarseTargetFrame k (before ++ letter :: suffix))[k + before.length]?.getD none = some letter := by
…

Mentions: OAI.EditApproximation.coarseTargetFrame

theorem OAI.EditApproximation.coarse_anchor_advance line 302

Source documentation

Advancing an actual alignment cut gives a legal bounded shift. The only budget is its preceding displacement plus its remaining edit cost.

theorem coarse_anchor_advance (k start before : ℕ) (shift : Fin (2 * k + 1))
    (sourceWidth targetWidth cutCost remaining : ℕ)
    (hanchor : start + shift.val = k + before)
    (hbudget : Nat.dist start before + (cutCost + remaining) ≤ k)
    (hsource : sourceWidth ≤ targetWidth + cutCost)
    (htarget : targetWidth ≤ sourceWidth + cutCost) :
    ∃ next : Fin (2 * k + 1),
      start + sourceWidth + next.val = k + (before + targetWidth) ∧
      Nat.dist shift.val next.val ≤ cutCost ∧
      Nat.dist (start + sourceWidth) (before + targetWidth) + remaining ≤ k := by
…

theorem OAI.EditApproximation.coarse_leaf_edit_upper line 324

Source documentation

Exact first-child alignment cost controls every actual shift-tree leaf; no leaf correspondence oracle is assumed.

theorem coarse_leaf_edit_upper {B : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (target before piece suffix : List α) (letter : Option α)
    (start : ℕ) (shift : Fin (2 * k + 1))
    (htarget : target = before ++ piece ++ suffix)
    (hanchor : start + shift.val = k + before.length) :
    coarseShiftCost k (coarseTargetFrame k target) (.leaf (B := B) letter) start shift ≤
…

Mentions: OAI.EditApproximation.coarseShiftCost, OAI.EditApproximation.coarseTargetFrame

theorem OAI.EditApproximation.coarseChildrenCost_edit_upper line 347

Source documentation

Recursive actual optimal cuts bound child minima. The explicit before allowance accounts for the displacement from the parent's shift.

theorem coarseChildrenCost_edit_upper {B D : ℕ} {α : Type u}
    (k : ℕ) (target : List α) (C : ℕ)
    (value : CoarseSourceTree B α D → ℕ → Fin (2 * k + 1) → ℕ)
    (children : List (CoarseSourceTree B α D))
    (hchild : ∀ child ∈ children, ∀ (before piece suffix : List α) start shift,
      target = before ++ piece ++ suffix →
      start + shift.val = k + before.length →
      Nat.dist start before.length + edit child.word piece ≤ k →
      value child start shift ≤ C * edit child.word piece)
    (before piece suffix : List α) (start : ℕ)
    (parent anchor : Fin (2 * k + 1)) (allowance : ℕ)
    (htarget : target = before ++ piece ++ suffix)
…

Mentions: OAI.EditApproximation.CoarseSourceTree

theorem OAI.EditApproximation.coarseShiftCost_edit_upper line 405

Source documentation

The actual bounded-shift recurrence is at most the manuscript's linear-in-depth distortion, using optimal unrestricted edit scripts.

theorem coarseShiftCost_edit_upper {B D : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (target : List α) (tree : CoarseSourceTree B α D)
    (before piece suffix : List α) (start : ℕ) (shift : Fin (2 * k + 1))
    (htarget : target = before ++ piece ++ suffix)
    (hanchor : start + shift.val = k + before.length)
    (hbudget : Nat.dist start before.length + edit tree.word piece ≤ k) :
    coarseShiftCost k (coarseTargetFrame k target) tree start shift ≤
      (1 + 2 * B * D) * edit tree.word piece := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseShiftCost, OAI.EditApproximation.coarseTargetFrame

theorem OAI.EditApproximation.coarseTreeValue_edit_upper line 435
Source documentation
Section 3's second deterministic distortion inequality for the executable finite coarse tree, conditional only on the guessed distance.
```
theorem coarseTreeValue_edit_upper {B D : ℕ} {α : Type u} [DecidableEq α]
    (tree : CoarseSourceTree B α D) (target : List α) (k : ℕ)
    (hguess : edit tree.word target ≤ k) :
    coarseTreeValue tree target k ≤ (1 + 2 * B * D) * edit tree.word target := by
…
```
Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.coarseTreeValue