Correction with one exclusive-or comparison

Compare the two neighboring full keys by their exclusive or with the query, then compute the highest differing bit only for the chosen key. This avoids two highest-bit computations. The rank primitives remain mathematical specifications in this module.

Main definitions

• xorSketchNeighbor: select a neighboring key by exclusive-or value.
• xorCorrectedRank: arbitrary-query correction with this selection rule.

Main results

• xorCorrectedRank_eq_upperRank: exact inclusive rank for every bounded query.

References

• Fredman and Willard, Surpassing the information theoretic bound with fusion trees.

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

Compare only the two sketch neighbors, using a single full-word exclusive or per key.

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

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

theorem Cslib.Algorithms.Lean.FusionTree.miss_of_xorSketchNeighbor {n w q : ℕ} {keys : Fin n → ℕ} (hsorted : StrictMono keys) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) {j : Fin n} (hj : xorSketchNeighbor w keys q = some j) (hmiss : keys j ≠ q) (i : Fin n) : keys i ≠ q

theorem Cslib.Algorithms.Lean.FusionTree.xorSketchNeighbor_highestDiff_le {n w q : ℕ} {keys : Fin n → ℕ} (hq : q < 2 ^ w) (hbound : ∀ (i : Fin n), keys i < 2 ^ w) (hmiss : ∀ (i : Fin n), keys i ≠ q) {j : Fin n} (hj : xorSketchNeighbor w keys q = some j) (i : Fin n) (hi : IsSketchNeighbor w keys q i) : BitString.highestDiff w (keys j) q ≤ BitString.highestDiff w (keys i) q

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

Correction using an exclusive-or comparison to select the longest-prefix neighbor. Exact hits return the initial inclusive rank; misses use the sibling-boundary correction.

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

Exclusive-or selection gives the true inclusive rank for all bounded queries. This establishes the selection rule's semantics; RAM execution is proved separately.