Exercise SP-120

An exact-real-interval binary search returns the true tail/bridge cutoff index for every width and scale, with endpoint and single-cell boundary cases, using 2n field operations and n+1 comparisons.

1. The interval invariant start <= cutIndex <= start+2^remaining with the base-case single comparison returns start or start+1, covering endpoint cases.
2. The inductive step compares the exact midpoint gridPoint(start+2^remaining) and recurses into the correct half, preserving the invariant, so compute returns cutIndex.
3. The search costs 2n field operations and n+1 comparisons (2n+2 field ops including the pi*L / subtraction initialisation).

Model the search by an interval invariant: at a node with 'remaining' halvings left, 'start' already-decided low-order index, and current interval first point gridPoint(start) and width span = step * 2^remaining, assume the true cutoff c = cutIndex satisfies start <= c <= start + 2^remaining (it lies in the current interval). We prove the returned value equals c by induction on 'remaining'. Base case (remaining = 0, one cell): the interval has a single cell starting at 'start'. The search compares the grid point at 'start' against -1. If gridPoint(start) < -1, then 'start' is still below the threshold, so the crossing is at start+1 and the hypotheses force c = start+1; the search returns start+1. Otherwise 'start' is at or past the threshold, so c = start and the search returns start. In both branches the returned value equals c; this also covers the endpoint boundary cases (crossing at the first or last point) because the invariant pins c to one of the two interval ends when the cell is minimal. Inductive step (remaining+1): the search forms the midpoint, which equals gridPoint(start + 2^remaining) (the first point of the upper half), and compares it to -1. If it is below -1, the crossing lies in the upper half, so recurse with start' = start + 2^remaining and the same remaining; the lower bound updates to start' <= c (since the midpoint is still below threshold, c >= start + 2^remaining) and the width halves, preserving the invariant, so by induction the recursion returns c. If it is at or past -1, the crossing lies in the lower half; recurse with the same start and halved width, and the invariant's upper bound tightens to c <= start + 2^remaining, again returning c. The key geometric identities are span/2 = step * 2^remaining and gridPoint(start) + step*2^remaining = gridPoint(start+2^remaining), which make the carried real endpoints exact — no ceiling evaluation or grid enumeration occurs. Starting the top-level search with the full interval [-pi L, 0] and remaining = n satisfies the initial invariant (the cutoff lies between index 0 and the midpoint index 2^n), so the top-level call returns cutIndex exactly. Cost: each of the n internal halvings performs 2 real field operations (one division to halve the span, one addition to form the midpoint) and 1 real comparison; the base level performs 1 comparison. The top-level producer additionally does one multiplication (pi*L) and one subtraction (0 - width) to initialise the interval. Hence the search proper uses exactly 2n field operations and n+1 comparisons; including initialisation the producer uses 2n+2 field operations and n+1 comparisons. Natural-index arithmetic, powers of two, and counter bookkeeping are outside this real-arithmetic cost model; finite-bit comparison of arbitrary real inputs is not claimed.

1. Formulates the interval invariant start <= cutIndex <= start + 2^remaining and proves the base case returns start or start+1 by the single comparison, covering endpoint boundary cases. (1 weight)
2. Proves the inductive step: the midpoint equals gridPoint(start+2^remaining), and each comparison recurses into the correct half while preserving the invariant. (1 weight)
3. Uses the exact real identities span/2 = step*2^remaining and gridPoint(start)+step*2^remaining = gridPoint(start+2^remaining) so endpoints stay exact (no ceiling/enumeration). (1 weight)
4. States the exact cost: 2n field operations and n+1 comparisons for the search (2n+2 field ops with the pi*L and subtraction initialisation), noting the real-arithmetic cost model's scope. (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• QuantumBlockEncoding/HermiteBinaryCutoff.lean

  lines 22-128: search (remaining start lower span) recursion; search_value (hlo : start <= cutIndex) (hhi : cutIndex <= start + 2^remaining) : (search ...).value = cutIndex via half_span and middle_point; compute n L = do width<-mul pi L; lower<-sub 0 width; search n 0 lower width; compute_value : = cutIndex; search_cost : cost op = 2*remaining*tick field op + (remaining+1)*tick compare op; compute_comparisons = n+1; compute_field_operations = 2n+2

  Source SHA-256: 3e236d6572ceba6d0418cb75da49512152bf03586cebc03b4d9cd8132029d098 · MIT (repository LICENSE)

Contract: 7169ee40ac139b5a42ff3dbfd1f4914c6cabd5f296812d2414de82854c81ed5b

Item digest: 345c21e4f78ee80ed2cbaa7372d069aacbfb19d8c3c2f046e5b8df13c107196a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 3. This is not measured graph distance or model difficulty.