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

Any index returned by xorSketchNeighbor is a sketch neighbor minimizing the exclusive-or distance to q.

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

xorSketchNeighbor returns none if and only if the key table is empty.

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.