Strict packed sketch ranks

The zero-bit branch of arbitrary-query correction requires a strict rank. Subtracting the number of sketches at least the query from the node occupancy handles equality and zero queries directly.

Main definitions

• LowerRankProgram.code: eight standard instructions for strict sketch rank.

Main results

• LowerRankProgram.exec: checked execution returning the number of sketches below the query.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.query : Fin 10

The input register layout agrees with RankProgram, except register seven is occupancy and register one contains the original sketches rather than their complements.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.node : Fin 10

Packed guarded sketches.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.copies : Fin 10

Replication multiplier.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.guards : Fin 10

Mask of field guards.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.bits : Fin 10

Payload width.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.middle : Fin 10

Middle digit divisor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.base : Fin 10

Field radix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.count : Fin 10

Number of stored sketches.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.temp : Fin 10

Scratch for the replicated query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.out : Fin 10

Final strict rank.

def Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.code : WordRAM.Code WordRAM.Basis.standard 10

Count guards for q ≤ sᵢ, then subtract the count from the occupancy.

def Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.result (x : WordRAM.Data 10) (b n : ℕ) (s : ℕ → ℕ) (q : ℕ) : WordRAM.Data 10

Exact state after all eight instructions.

theorem Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.countGuards_complement {b n q : ℕ} (s : ℕ → ℕ) (hn : 0 < n) (hb : n < 2 ^ (b + 1)) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) : n - countGuards b n s q = {i ∈ Finset.range n | s i < q}.card

theorem Cslib.Algorithms.WordRAM.FusionTree.LowerRankProgram.exec {w b n q : ℕ} (s : ℕ → ℕ) (x : WordRAM.Data 10) (hn : 0 < n) (hb : n < 2 ^ (b + 1)) (hs : ∀ i < n, s i < 2 ^ b) (hq : q < 2 ^ b) (hw : 2 * ((b + 1) * n) ≤ w) (hxq : x.regs query = q) (hxn : x.regs node = packedNode b n s) (hxc : x.regs copies = queryMultiplier b n) (hxg : x.regs guards = guardMask b n) (hxb : x.regs bits = b) (hxm : x.regs middle = 2 ^ ((b + 1) * (n - 1))) (hxr : x.regs base = 2 ^ (b + 1)) (hxn' : x.regs count = n) : WordRAM.Exec w code x (result x b n s q) 8 ∧ (result x b n s q).regs out = {i ∈ Finset.range n | s i < q}.card ∧ (result x b n s q).mem = x.mem

Eight checked instructions return the strict rank, including zero and equality queries. The node parameters and memory are preserved; query compression and constant loading are separate. The full guard-count product fits under the stated packed-width bound.