claimroutine

Public coefficients via shared-scratch division

Public rational coefficients get digits by long division in

O(B+r)

scratch

covers coefficient leaves with no operand queries

Claim·§10.6 The numerical interface·inside thmUniform numerical interface for arithmetic recipes

Statement (paper)

Let

P/Q

be a public rational coefficient with

Q>0

and

O(B)

-bit numerator and denominator that can be generated in

O(B)

scratch. Then a place-

r

approximation of

P/Q

, and hence its queried digits in the clock range with

r=O(B)

, can be produced by integer division of

2^rP

Q

(with signed floors when needed) using only shared scratch of size

O(B+r)

, which is

O(B)

for

r=O(B)

, and with no operand or recursive graph call.

In plain English

A public rational coefficient

P/Q

with

Q>0

and

O(B)

-bit numerator and denominator, generable in

O(B)

scratch, has its place-

r

approximation computed by integer division of

2^rP

Q

(signed floors if needed). This uses only

O(B+r)

shared scratch, so

O(B)

when

r=O(B)

, and makes no operand or recursive graph calls.

Why it's here

This step shows that public coefficient leaves satisfy the hypothesis of the arithmetic interface theorem, which requires exact normalized digit procedures in

O(B+d+t)

shared scratch with no operand or graph queries. Plain long division of the scaled numerator by the denominator gives the queried digits directly, so such leaves add no suspended operand records.

Classified routine:

Direct application of schoolbook integer long division: computing floor(2^r P / Q) for O(B)-bit integers in O(B+r) space is a standard space-bounded arithmetic fact. Here it is only bookkeeping to check that public coefficient leaves meet the interface hypothesis.

Uses

Nothing else in the paper

Used by

Nothing in the paper

Sources

PaperOpen

Section: §10.6 The numerical interface
Page: —
Label: —
Line: sections/arithmetic.tex:842

Leannot aligned

Phase 2 aligns this node to a Lean declaration.