Skip to section
Foundationsfor rotation-free search
Section 31 of 5260% of course
Contents
Chapter 5 Section 5.6 75 min

Part III · Construction and proof

Chapter studio: attack the proof

Search for counterexamples and distinguish essential assumptions.

Let's attack the construction

You only truly understand a construction when you can deliberately break it, immediately identify which assumption failed, and precisely predict the symptom. Try to answer each prompt in your head before revealing the explanation.

1. A query accidentally has a nonzero coefficient at position D. Which block is now going to contaminate tⱼ?

tⱼ − D = Dj−1, which is exactly the last position of block j−1. For j=0, that exact same extra degree also suddenly makes our earliest wrapped source reachable.

2. Why is it that negative coefficient values don't affect our block isolation proof at all?

Because support is only about positions that *may* be nonzero. The actual signs and magnitudes just affect the final totals, they don't change reachability.

3. Quickly derive the maximum ordinary product degree.

max degree A plus max degree B = (D−1) + (N−1) = N+D−2.

4. State the absolute narrowest, most honest performance claim for this design.

The reversed coefficient layout eliminates encrypted rotations and explicit coordinate-reduction stages strictly from the scoring path, while completely retaining the polynomial product and all downstream work.

5. Why are completeness and soundness two totally separate proof obligations?

Completeness proves that every desired matching product successfully reaches the target. Soundness goes a step further and proves that NO product from any other block or wrapped source manages to reach it.

6. Give a test that can cleanly distinguish a layout error from CKKS approximation noise.

Run the coefficient packing and ordinary integer convolution with small, exact integer values. If it fails there, your error is purely structural. You should only start measuring encrypted output error after the integer reference passes flawlessly.

Proof gate

What two completely independent contamination paths did we manage to rule out?

Chapter 5 complete

The coefficient has truly earned its meaning

Our support bounds isolate a single block. Our degree bounds exclude all wrapped sources. We turn those assumptions into hard validations. The glorious payoff is zero score rotations, beautifully qualified by full transform work, our N/D packing density, a bunch of incidental coefficients, and the response cost. Next up: Chapter 6.

Reactive Python laboratory · marimo + PyodideDerive and attack the score-tap layout

Solve the index equation, inspect contributor bounds, and probe the proof with small exact examples.

Open full-screen lab ↗

Runs entirely in this browser. Python executes in Pyodide WebAssembly with no remote kernel. The construction code stays visible while reactive dependents recompute whenever you change an input.

Repository layer · second pass

Can you break a claim without breaking its stated assumptions?

Proof review searches for a legal counterexample. Random values are secondary; start by attacking index ranges, boundary degrees, partial blocks, zero padding, and parameter mismatch. If a counterexample violates an explicit premise, it tests validation rather than the theorem.

A strong proof studio records attempted attacks and why each fails. This is more valuable than rereading the successful derivation because it reveals which assumptions are essential and which are merely convenient.

Reasoning chain

  1. 1

    Negate the conclusion.

  2. 2

    Keep every premise fixed.

  3. 3

    Search smallest dimensions first.

  4. 4

    Probe boundary indices.

  5. 5

    Separate theorem failure from validator failure.

  6. 6

    Convert discovered edge cases into permanent tests.

Worked trace

An invalid “counterexample”

  1. Choose N=10,D=4.
  2. Packing leaves a partial block.
  3. A target formula appears inconsistent.
  4. But the theorem assumed D divides N.

Result. This attacks missing validation, not the proof under its domain.

Executable lens · Python

Make the hidden state visible

def exhaustive_small(reference, packed_score):
    values = (-1,0,1)
    # enumerate tiny inputs in the accompanying notebook
    # and compare every target with the reference dot product
    return values

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

Misconception clinic

Tempting mistakes

  • Changing two assumptions at once.
  • Accepting floating-point closeness in an integer identity test.

Retrieval and transfer

Close the book first

  1. Attempt attacks on support, divisibility, reversal, and wrap.
  2. Write the smallest valid N,D test matrix.
  3. Explain why exhaustive tiny tests complement but do not replace proof.