Arbitrary-query sketch correction

Correct the rank of an arbitrary query using the actual significant-bit sketch and the two stored keys neighboring its inclusive sketch rank. Exact hits return that rank directly; other queries use a second sketch rank at a prefix boundary. No word-RAM running-time bound is asserted.

Main definitions

• upperRank, lowerRank: inclusive and strict ranks in a finite sequence.
• IsSketchNeighbor: predicate for the indices t - 1 and t around inclusive sketch rank t.
• boundaryRank: inclusive sketch rank at the highest-differing-bit prefix boundary.
• sketchRank: inclusive rank in the stored compressed sketches.
• sketchPredecessor, sketchSuccessor: neighboring stored indices around sketchRank.
• chooseByScore, divergenceScore: longest-common-prefix tie-breaking between sketch neighbors.
• bestSketchNeighbor: select between indices t-1 and t at inclusive sketch rank t.
• correctedRank: the resulting arbitrary-query correction.

Main results

• highestDiff_mem_relevantBits_of_lt: every stored pair's highest differing bit is selected.
• exists_sketchNeighbor_prefix: every nonempty query-prefix block contains a sketch neighbor.
• exists_sketchNeighbor_min_highestDiff: a sketch neighbor attains a globally longest prefix.
• correctedRank_eq_upperRank: correction gives the true inclusive rank for every bounded query.

References

See [FW93] and [MIT 6.851, Spring 2021, Lecture 12, handwritten page 4] (https://courses.csail.mit.edu/6.851/spring21/lectures/L12.pdf).

theorem Cslib.Algorithms.Lean.FusionTree.highestDiff_mem_relevantBits_of_lt {n w : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) {i j : Fin n} (hij : i < j) : BitString.highestDiff w (keys i) (keys j) ∈ relevantBits w keys

Every pair of distinct stored keys has its highest differing bit among the adjacent-pair bits, even when the keys are not adjacent.

def Cslib.Algorithms.Lean.FusionTree.upperRank {n : ℕ} (values : Fin n → ℕ) (q : ℕ) : ℕ

The inclusive rank is the number of stored values at most the query.

def Cslib.Algorithms.Lean.FusionTree.lowerRank {n : ℕ} (values : Fin n → ℕ) (q : ℕ) : ℕ

The strict rank is the number of stored values strictly below the query.

theorem Cslib.Algorithms.Lean.FusionTree.upperRank_le {n : ℕ} (values : Fin n → ℕ) (q : ℕ) : upperRank values q ≤ n

An inclusive rank is a cut between zero and the number of stored values.

theorem Cslib.Algorithms.Lean.FusionTree.lt_upperRank_iff {n q : ℕ} {values : Fin n → ℕ} (hsorted : StrictMono values) (i : Fin n) : ↑i < upperRank values q ↔ values i ≤ q

In a sorted sequence, inclusive rank exactly characterizes the indices below its cut.

def Cslib.Algorithms.Lean.FusionTree.IsSketchNeighbor {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) (i : Fin n) : Prop

The immediate sketch neighbors of the inclusive query cut. At the endpoints there is only one neighbor; in an empty sequence there are none.

theorem Cslib.Algorithms.Lean.FusionTree.exists_sketchNeighbor_prefix {n w q cut : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hprefix : ∃ (i : Fin n), keys i >>> cut = q >>> cut) : ∃ (j : Fin n), IsSketchNeighbor w keys q j ∧ keys j >>> cut = q >>> cut

Every nonempty full-prefix block contains an immediate sketch neighbor of the query. The query is arbitrary: it need not be a stored key or have a faithful sketch rank.

theorem Cslib.Algorithms.Lean.FusionTree.exists_sketchNeighbor_min_highestDiff {n w q : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hq : q < 2 ^ w) (hn : 0 < n) (hmiss : ∀ (i : Fin n), keys i ≠ q) : ∃ (j : Fin n), IsSketchNeighbor w keys q j ∧ ∀ (i : Fin n), BitString.highestDiff w (keys j) q ≤ BitString.highestDiff w (keys i) q

For a query unequal to every stored key, an immediate sketch neighbor attains the longest full common prefix, expressed as the minimum highest differing position.

def Cslib.Algorithms.Lean.FusionTree.boundaryRank {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) (j : Fin n) : ℕ

The second sketch query, with the comparison convention determined by the divergence bit.

theorem Cslib.Algorithms.Lean.FusionTree.boundaryRank_eq_upperRank {n w q : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hq : q < 2 ^ w) (hmiss : ∀ (i : Fin n), keys i ≠ q) (j : Fin n) (hbest : ∀ (i : Fin n), IsSketchNeighbor w keys q i → BitString.highestDiff w (keys j) q ≤ BitString.highestDiff w (keys i) q) : boundaryRank w keys q j = upperRank keys q

The corrected sketch rank equals the true inclusive rank when j minimizes divergence among the immediate sketch neighbors. This hypothesis is a comparison of at most two keys.

theorem Cslib.Algorithms.Lean.FusionTree.upperRank_apply {n : ℕ} {values : Fin n → ℕ} (hsorted : StrictMono values) (i : Fin n) : upperRank values (values i) = ↑i + 1

The inclusive rank of a stored key is its index plus one.

theorem Cslib.Algorithms.Lean.FusionTree.upperRank_sketch_apply {n w : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (i : Fin n) : upperRank (fun (j : Fin n) => BitString.sketch (relevantBits w keys) (keys j)) (BitString.sketch (relevantBits w keys) (keys i)) = upperRank keys (keys i)

An exact hit has its true inclusive rank already, before correction.

def Cslib.Algorithms.Lean.FusionTree.sketchRank {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) : ℕ

Initial inclusive rank of the uncorrected query sketch.

def Cslib.Algorithms.Lean.FusionTree.sketchPredecessor {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) : Option (Fin n)

The predecessor of the inclusive sketch cut, when present.

def Cslib.Algorithms.Lean.FusionTree.sketchSuccessor {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) : Option (Fin n)

The successor of the inclusive sketch cut, when present.

theorem Cslib.Algorithms.Lean.FusionTree.sketchPredecessor_eq_some_iff {n w q : ℕ} {keys : Fin n → ℕ} (i : Fin n) : sketchPredecessor w keys q = some i ↔ ↑i + 1 = sketchRank w keys q

The predecessor is precisely index t-1, using the inclusive convention.

theorem Cslib.Algorithms.Lean.FusionTree.sketchSuccessor_eq_some_iff {n w q : ℕ} {keys : Fin n → ℕ} (i : Fin n) : sketchSuccessor w keys q = some i ↔ ↑i = sketchRank w keys q

The successor is precisely index t, using the inclusive convention.

theorem Cslib.Algorithms.Lean.FusionTree.isSketchNeighbor_iff {n w q : ℕ} {keys : Fin n → ℕ} (i : Fin n) : IsSketchNeighbor w keys q i ↔ sketchPredecessor w keys q = some i ∨ sketchSuccessor w keys q = some i

The two optional candidates are exactly the immediate sketch neighbors.

def Cslib.Algorithms.Lean.FusionTree.chooseByScore {α : Type u_1} (score : α → ℕ) : Option α → Option α → Option α

Compare at most two optional candidates by a natural-number score.

theorem Cslib.Algorithms.Lean.FusionTree.chooseByScore_spec {α : Type u_1} (score : α → ℕ) {a b : Option α} {j : α} (h : chooseByScore score a b = some j) : (a = some j ∨ b = some j) ∧ ∀ (i : α), a = some i ∨ b = some i → score j ≤ score i

A chosen candidate belongs to the input pair and has minimum score among that pair.

theorem Cslib.Algorithms.Lean.FusionTree.chooseByScore_eq_none_iff {α : Type u_1} (score : α → ℕ) (a b : Option α) : chooseByScore score a b = none ↔ a = none ∧ b = none

No candidate is selected exactly when both inputs are absent.

def Cslib.Algorithms.Lean.FusionTree.divergenceScore (w x q : ℕ) : ℕ

Exact hits score zero; other keys are scored by their highest differing bit plus one.

def Cslib.Algorithms.Lean.FusionTree.bestSketchNeighbor {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) : Option (Fin n)

Select a longest-prefix candidate from the two sketch neighbors, preferring exact hits.

theorem Cslib.Algorithms.Lean.FusionTree.bestSketchNeighbor_spec {n w q : ℕ} {keys : Fin n → ℕ} {j : Fin n} (h : bestSketchNeighbor w keys q = some j) : IsSketchNeighbor w keys q j ∧ ∀ (i : Fin n), IsSketchNeighbor w keys q i → divergenceScore w (keys j) q ≤ divergenceScore w (keys i) q

The selected neighbor minimizes the divergence score among the two candidates.

theorem Cslib.Algorithms.Lean.FusionTree.bestSketchNeighbor_eq_none_iff {n w q : ℕ} {keys : Fin n → ℕ} : bestSketchNeighbor w keys q = none ↔ n = 0

A nonempty node always has at least one of the two sketch neighbors.

theorem Cslib.Algorithms.Lean.FusionTree.isSketchNeighbor_of_eq {n w q : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (i : Fin n) (hi : keys i = q) : IsSketchNeighbor w keys q i

An exact stored hit is the predecessor of the inclusive sketch cut.

def Cslib.Algorithms.Lean.FusionTree.correctedRank {n : ℕ} (w : ℕ) (keys : Fin n → ℕ) (q : ℕ) : ℕ

Arbitrary-query correction using two sketch neighbors. Exact hits return the initial inclusive sketch rank directly. Otherwise a second sketch rank uses the appropriate boundary. After taking sketch ranks, candidate selection and correction use at most two full-key values. The sketches and rank primitives here are mathematical specifications, without a RAM-time bound.

theorem Cslib.Algorithms.Lean.FusionTree.correctedRank_eq_upperRank {n w q : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hq : q < 2 ^ w) : correctedRank w keys q = upperRank keys q

For every bounded query, correction of the actual significant-bit sketch gives the true inclusive rank among the stored keys. This includes empty nodes, boundary cuts, and exact hits.