Arithmetic ranks and full-key correction

The arithmetic ranks use natural-number arrays; the correction theorems use Fin-indexed keys. These bridges identify the two counts and justify correction for the concrete exclusive-or neighbor selection, including exact hits.

Main results

• NodeSemantics.upperRank_eq: the arithmetic count is the inclusive perfect-sketch rank.
• NodeSemantics.correct: a minimum-exclusive-or sketch neighbor suffices for full-key rank.

References

• [FW93]

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeSemantics.upperRank_eq {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (q : ℕ) : upperRankExpr p.b n p.sketches (p.compressed q) = Lean.FusionTree.sketchRank w keys q

The arithmetic inclusive count agrees with the perfect-sketch rank on every input.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeSemantics.lowerRank_eq {w n : ℕ} {keys : Fin n → ℕ} (p : NodeParameters w keys) (hn : 0 < n) (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (q : ℕ) : n - countGuards p.b n p.sketches (p.compressed q) = Lean.FusionTree.lowerRank (fun (i : Fin n) => BitString.sketch (Lean.FusionTree.relevantBits w keys) (keys i)) (BitString.sketch (Lean.FusionTree.relevantBits w keys) q)

The arithmetic strict count agrees with the strict perfect-sketch rank.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeSemantics.miss {w n q : ℕ} {keys : Fin n → ℕ} (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (j : Fin n) (hbest : ∀ (i : Fin n), Lean.FusionTree.IsSketchNeighbor w keys q i → keys j ^^^ q ≤ keys i ^^^ q) (hj : keys j ≠ q) (i : Fin n) : keys i ≠ q

A minimum-exclusive-or neighbor is an exact hit whenever any stored key is a hit.

theorem Cslib.Algorithms.WordRAM.FusionTree.NodeSemantics.correct {w n q : ℕ} {keys : Fin n → ℕ} (hs : StrictMono keys) (hk : ∀ (i : Fin n), keys i < 2 ^ w) (hq : WordRAM.Fits w q) (j : Fin n) (hbest : ∀ (i : Fin n), Lean.FusionTree.IsSketchNeighbor w keys q i → keys j ^^^ q ≤ keys i ^^^ q) : (if keys j = q then Lean.FusionTree.sketchRank w keys q else Lean.FusionTree.boundaryRank w keys q j) = Lean.FusionTree.upperRank keys q

Concrete exclusive-or selection supports the full correction theorem. This statement does not require identifying an Option-valued selection implementation.