claimroutineinferred_dep

Early-word payment at early input places

Early-word queries at j≤kj\le k pay for the long word via t−jt-j
gives the early-word clause of the reciprocal bound
Claim·§10.4 Reciprocals and the early-word convention·inside lemReciprocal with early-word storage

Statement (paper)

Every original-input query made during the formation of the coefficient word has input place j≤k≤t/2+O(1)j\leq k\leq t/2+O(1). Hence there are fixed constants C2,C3C_2,C_3 such that t+1≤C2+C3(t−j)t+1\leq C_2+C_3(t-j) at all such queries, and since the enclosing gate path has length O(t+1)O(t+1), the complete suspended local record satisfies the required bound there.

In plain English

Every query to the original input while forming the coefficient word is at a place j≤k≤t/2+O(1)j\leq k\leq t/2+O(1). So t+1≤C2+C3(t−j)t+1\leq C_2+C_3(t-j) holds at those queries for fixed constants C2,C3C_2,C_3, and the whole suspended local record meets the required bound there.

Why it's here

Since the previous claim shows all input queries occur at places up to kk, and kk is about t/2t/2, the O(t+1)O(t+1)-bit coefficient word is only held while t−jt-j is linearly large, so its size is paid for by the t−jt-j term. Adding the O(t+1)O(t+1) gate-path length keeps the same bound, which gives the early-word clause of the reciprocal lemma and lets the suffix-branch claim treat j>kj>k separately.
Classified routine:
Direct bookkeeping consequence of the preceding claim (queries only at places up to k ≈ t/2), so t−j is linearly large and absorbs the O(t+1)-bit word and gate-path length; this is a simple inequality calculation.

Uses

claimCoefficient digits via integer arithmetic

Used by

claimSuffix branch holds no coefficient word

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Early-word payment at early input places" rests on claim-lem-arith-reciprocal-3