claimroutineinferred_dep

One clock coefficient works throughout

One clock coefficient bb works for all primitives and nested stages
makes clock-gap terms telescope across stages
Claim·§10.6 The numerical interface·inside thmUniform numerical interface for arithmetic recipes

Statement (paper)

There is a single positive clock coefficient bb valid for all finite primitive and stage types, and constants a,ca,c, such that every requested operand digit jj at clock tt satisfies j≤t+cdj\leq t+cd and total suspended local binary record length ≤ad+b(t−j)\leq ad+b(t-j), which is Equation , with total overshoot O(d)O(d). Moreover, an internal arithmetic operation at current clock uu has intrinsic record of length at most C(d+u)C(d+u), and together with the outer saved portion of length at most Ad+b(t−u)Ad+b(t-u) the total is at most (A+C)d+bt(A+C)d+bt when b≥Cb\geq C, so the same bb is valid in all local bounds.

In plain English

A single positive clock coefficient bb works for every primitive and stage type, with constants a,ca,c, so each requested operand digit jj at clock tt has j≤t+cdj\leq t+cd and suspended local record length at most ad+b(t−j)ad+b(t-j). An internal operation at clock uu with intrinsic record at most C(d+u)C(d+u), added to an outer saved portion of length at most Ad+b(t−u)Ad+b(t-u), totals at most (A+C)d+bt(A+C)d+bt when b≥Cb\geq C, so the same bb persists.

Why it's here

The elementary, multiplication, reciprocal, rank and sum lemmas each give a bound of the form ad+b(t−j)ad+b(t-j) with their own constants. This claim takes a common bb (the maximum, at least every intrinsic constant CC) so the clock-gap terms telescope when stages are nested. Only the O(d)O(d) overshoot accumulates, which gives the interface bound (eq:arith-export) for whole recipes.
Classified routine:
Bookkeeping consequence of the elementary, multiplication, reciprocal, rank and sum lemmas: take b as the maximum of their finitely many constants (and at least each intrinsic C), so the clock-gap terms telescope under nesting and only the O(d) overshoots add up.

Uses

lemBalanced sums and scalings stay within local boundslemReciprocal with early-word storagelemElementary arithmetic operations have linear-space residue procedureslemMultiplication with linear clock-gap storagelemOrder statistics have linear-space residue procedures

Used by

Nothing in the paper

Sources

PaperOpen
Section
§10.6 The numerical interface
Page
—
Label
—
Line
sections/arithmetic.tex:798
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Common clock coefficient telescopes record bound" rests on lem:arith-elementary
  • info
    inferred_dep
    outline: "Common clock coefficient telescopes record bound" rests on lem:arith-multiplication
  • info
    inferred_dep
    outline: "Common clock coefficient telescopes record bound" rests on lem:arith-rank