Why neighboring blocks cannot leak into a score

Getting the right answer is only half the battle

In Chapter 4, we showed that every intended product q_iv_j,i definitely reaches our target t_j = Dj+D−1. In math, we call that a completeness argument: everything we want is there. But we still need a soundness argument: we have to prove that absolutely no unintended garbage can sneak into that same target.

You can run a hundred successful examples, but they still won't prove your code is safe from contamination for every possible block and every valid input. Values can accidentally cancel each other out, and friendly test cases might never even touch a dangerous position. A real proof has to reason about all the positions that could possibly contribute, completely independently of what their current values happen to be.

Let's trace a target backward

Forward tracing asks, "where does this pair end up?" Proving we're safe from contamination is actually easier if we go backward: "which corpus positions could possibly even reach this target?" Any normal convolution term that manages to hit t_j must have a query position i and a corpus position t_j−i. Since our query support guarantees 0 ≤ i ≤ D−1, let's plug those limits in:

Look closely at those bounds! They are exactly the left and right edges of block j. Every possible contributor is safely locked inside that block, and every single position in that block neatly decodes back to one logical coordinate of vector j. These bounds don't just say the block is "near" the target; they perfectly cover exactly D positions and completely ignore the neighbors.

Now, let's recover the logical coordinate

A physical corpus position r inside block j represents logical coordinate i = t_j−r. When we pair it with query position i, we get q_iv_j,i. So, our proof just established both claims at once: all contributors come strictly from block j, and every single contributor matches up with the exact same logical coordinate.

def contributors(d, j):
    t = d*j + d - 1
    return [(i, t-i) for i in range(d)]
assert {k for _,k in contributors(4,2)} == {8,9,10,11}