Skip to section
Foundationsfor rotation-free search
Section 24 of 5246% of course
Contents
Chapter 4 Section 4.5 75 min

Part III · Construction and proof

Laboratory: make the score appear

Edit inputs and observe the exact output coefficient with JointJS.

Get your hands dirty before we prove anything

This lab uses N=16 and D=4 so you can see every single coefficient clearly. Try editing the query and your selected corpus vector. Toggle between the natural and reversed packing. The JointJS contribution graph will actually trace every single term that reaches your selected coefficient!

Hands-on derivation

Make the score appear

This deliberately small ring uses N = 16 and D = 4 so every coefficient stays visible. Production uses the same index rule at N = 4096.

Query q
Selected corpus vector v1
Direct dot product8
Product coefficient c78
aligned

A(x) = 2 - x + 3x^2 + x^3

B(x) = 2 - 2x + 4x^2 + x^3 - x^4 + x^5 + 3x^7 + x^8 + 2x^9 + 2x^10 - 2x^11 + 3x^12 - x^14 + x^15

A(x)B(x) mod (x^16 + 1) = 8 - 8x + 15x^2 - 6x^3 + 7x^4 + 10x^5 - 3x^6 + 8x^7 + 12x^9 + 8x^10 + x^11 + 16x^12 - 7x^13 + 5x^14 + 6x^15

Query coefficients A

02
1-1
23
31
40
50
60
70
80
90
100
110
120
130
140
150

Reversed corpus coefficients B

02
1-2
24
31
4-1
51
60
73
81
92
102
11-2
123
130
14-1
151

Negacyclic product C

08
1-8
215
3-6
47
510
6-3
78
80
912
108
111
1216
13-7
145
156
Coefficient microscope: c73 nonzero contributions in this example
The indices are forced to meet. For every element i, query coefficient i pairs with corpus coefficient 4j + 3 − i. Their degrees sum to the same target: 4j + 3.

Worked example

Picking a good diagnostic input

Using all-ones vectors is actually a terrible first test, because a lot of incorrect pairings will still accidentally add up to 4! Try using q=[1,2,4,8] and v=[3,5,7,11] instead. Having distinct contributions makes it really obvious if a coordinate gets swapped. Designing good tests is a real part of mathematical reasoning: your examples should be able to tell the difference between your intended invariant and a plausible bug.

Check your understanding

When natural order fails but reversed order succeeds for a bunch of values you edited, what has the lab actually established?

Lab summary

  • Natural order forces us along the anti-diagonals.
  • Reversed blocks perfectly align matching logical coordinates.
  • Our target coefficient perfectly equals the direct dot product.
  • JointJS lets us expose and see the contributing terms, rather than hiding the math.

Repository layer · second pass

What should an experiment establish before we attempt a proof?

The laboratory lets you edit coordinates, switch between natural and reversed packing, and inspect which product nodes feed a chosen coefficient. Experiments reveal the invariant and catch index mistakes; they do not prove correctness for every value or dimension.

Use adversarial values rather than symmetric friendly ones. Distinct primes, negative signs, zeros, and one-hot vectors make it possible to identify which logical product reached a coefficient. If every value is one, many incorrect pairings produce the same total.

Reasoning chain

  1. 1

    Predict the target before running.

  2. 2

    Choose distinguishable coordinate values.

  3. 3

    Trace one matching and one nonmatching product.

  4. 4

    Switch layout while holding values constant.

  5. 5

    Record what evidence supports the invariant.

  6. 6

    State what remains for symbolic proof.

Worked trace

One-hot probes identify routing

  1. Set q coordinate 2 to one and all others zero.
  2. Set v coordinate 2 to seven and all others distinct.
  3. Reversed packing places their product at the target.
  4. Natural packing places it at destination 4 instead.

Result. The probe tests routing independently of accumulation complexity.

Executable lens · Python

Make the hidden state visible

def one_hot(size, index, value=1):
    out = [0] * size
    out[index] = value
    return out
q, v = one_hot(4,2), one_hot(4,2,7)
assert sum(a*b for a,b in zip(q,v)) == 7

Retype this example, predict each intermediate value, and then change one input that touches a boundary.

Misconception clinic

Tempting mistakes

  • Calling many passing random tests a proof.
  • Using values that allow wrong terms to cancel invisibly.

Retrieval and transfer

Close the book first

  1. Design a probe for every coordinate of D=5.
  2. Find a natural-order case that accidentally passes.
  3. Write a property-based test over several D values.