claimroutine

Descriptor bounds give A_ν=O(A)

Descriptor length

A

bounds all group integers, so

A_\nu=O(A)

uniform bit-length bound for group arithmetic

Claim·§A Packed additions on grouped rectangles·inside lemPacked selected-bit XOR on grouped streams

Statement (paper)

With

s=t-3

the number of spectator tags, one has

J(s+1)\le A

Jt\le 3A

J\le M

and

\log_2 M+\log_2 R=O(A)

. Every field length, partial suffix product, row count and group record count is at most

M

, and these integers as well as

V_\nu=M_\nu R

have

O(A)

bits. In particular

A_\nu:=\lceil\log_2(2V_\nu)\rceil=O(A)

with a constant independent of the number and shapes of the groups.

In plain English

With

s=t-3

spectator tags,

J(s+1)\le A

Jt\le 3A

J\le M

and

\log_2 M+\log_2 R=O(A)

. All field lengths, partial suffix products, row counts and group record counts are at most

M

and have

O(A)

bits, as does

V_\nu=M_\nu R

, so

A_\nu=\lceil\log_2(2V_\nu)\rceil=O(A)

with a constant independent of the number and shapes of the groups.

Why it's here

This claim turns the assumed bound

A

on the descriptor's total bit length into uniform

O(A)

bounds on every integer the procedure handles, including the per-group size parameter

A_\nu

. The later steps, which treat each group as a single rectangle and sum their costs, use it so that the per-group arithmetic costs are controlled by

A

and the

MA^3

and

A(R+A)

terms in the time bound hold.

Classified routine:

Direct bookkeeping from the assumed bound A on the descriptor's bit length. Every listed integer is a field of the descriptor or a product of such fields, so its bit length is at most a constant times A.

Uses

Nothing else in the paper

Used by

claimEach group collapses to a single rectangle

Sources

PaperOpen

Section: §A Packed additions on grouped rectangles
Page: —
Label: —
Line: sections/11-grouped-rectangles.tex:89

Leannot aligned

Phase 2 aligns this node to a Lean declaration.