claimroutineinferred_dep

Suffix branch holds no coefficient word

Suffix branch (j>kj>k) holds no coefficient word, record O(1)+c(t−j)O(1)+c(t-j)
covers the late-place case of the reciprocal bound
Claim·§10.4 Reciprocals and the early-word convention·inside lemReciprocal with early-word storage

Statement (paper)

On a suffix branch with j>kj>k, the local record holds no coefficient word: the coefficient digit is obtained at a separate leaf and only its bounded code bits are returned, while any pending data for a late suffix digit consists only of bounded pending bits and gate choices. Consequently the suspended record on this branch satisfies the bound O(1)+c(t−j)O(1)+c(t-j), and all intrinsic records have O(t+1)O(t+1) bits.

In plain English

On a suffix branch of the reciprocal procedure, where the queried place jj exceeds kk, the local record never contains a coefficient word. The suspended record there is at most O(1)+c(t−j)O(1)+c(t-j), and every intrinsic record has O(t+1)O(t+1) bits.

Why it's here

This is the complement of the early-word claim: the long O(t+1)O(t+1)-bit word is held only at places j≤kj\le k, and for j>kj>k the coefficient digit comes from a separate leaf that returns only bounded code bits, so nothing large is stored. Together the two cases give the reciprocal lemma's suspended-record and intrinsic-space bounds, with the early-word exception confined to places j≤⌊t/2⌋+O(1)j\le\lfloor t/2\rfloor+O(1).
Classified routine:
A case-analysis bookkeeping step inside the reciprocal lemma: it complements the early-word claim (claim-lem-arith-reciprocal-4) and bounds the suspended and intrinsic records using the storage bounds of the elementary-arithmetic and multiplication lemmas.

Uses

lemElementary arithmetic operations have linear-space residue procedureslemMultiplication with linear clock-gap storageclaimEarly-word payment at early input places

Used by

Nothing in the paper

Sources

PaperOpen
Section
§10.4 Reciprocals and the early-word convention
Page
—
Label
—
Line
sections/arithmetic.tex:518
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Suffix branch holds no coefficient word" rests on lem:arith-elementary
  • info
    inferred_dep
    outline: "Suffix branch holds no coefficient word" rests on lem:arith-multiplication
  • info
    inferred_dep
    outline: "Suffix branch holds no coefficient word" rests on claim-lem-arith-reciprocal-4