lemmaroutine

Finite buffered comparison test for sums

Finite test accepts every

s>2u

and only

s>u

, with

O(d)

digits

fixed-precision comparison for the numerical interface

Lemma·lem:arith-buffered-test·§10.5 Indexed ranks, sums, scales, and structural leaves

Statement (paper)

Let

d\geq1

, let

s

and

u

have known magnitude bound

2^{\kappa d}

, and suppose

u\geq\rho\geq2^{-\kappa d}

. There is a deterministic finite test that accepts every

s>2u

and accepts only

s>u

. It uses

O(d)

-place digit queries after normalization, with intrinsic and suspended local lengths

O(d)

. Its result is independent of any subsequent numerical output clock.

In plain English

For

s

and

u

with known magnitude bound

2^{\kappa d}

and

u\geq\rho\geq2^{-\kappa d}

, there is a deterministic finite test that accepts every

s>2u

and accepts only

s>u

. It uses

O(d)

-place digit queries after normalization, has intrinsic and suspended local lengths

O(d)

, and its outcome does not depend on any later numerical output clock.

Why it's here

This gives a comparison with a factor-two buffer: inputs clearly above

2u

are accepted, inputs at or below

u

are rejected, and the gap in between may go either way. Because

u

is bounded below by

2^{-\kappa d}

, finitely many digits suffice to decide, so the test can be used inside the numerical interface at fixed precision without depending on output clocks. It supplies the buffered tests that the uniform numerical interface relies on.

Classified routine:

A standard approximate-comparison argument: since u is bounded below by 2^{-κd} and the factor-two gap is wide, truncating s and u to O(d) binary places and comparing the approximations decides the buffered comparison. The only new part is the bookkeeping of the paper's own length and clock accounting.

Uses

Nothing else in the paper

Used by

thmUniform numerical interface for arithmetic recipesclaimStructural leaves and buffered tests use fixed precision

Sources

PaperOpen

Section: §10.5 Indexed ranks, sums, scales, and structural leaves
Page: —
Label: lem:arith-buffered-test
Line: sections/arithmetic.tex:698

Leannot aligned

Phase 2 aligns this node to a Lean declaration.