definitionroutine

Grouped packed stream format

Defines grouped packed streams: records in rectangles with tagged chunks

input format for packed addition on grouped data

Definition·def:grouped-packed-stream·§A Packed additions on grouped rectangles

Statement (paper)

Let

M,R\ge1

K\ge6

f\ge1

L=fK

, and

0\le\rho<K

. Fix an ordered template of

t\ge3

two-bit tags:

\mathtt{00}

denotes a spectator field, and

\mathtt{01},\mathtt{10},\mathtt{11}

denote

x,y,z

, respectively. Each chunk tag occurs exactly once. The template is common to all

J\ge1

groups of this input, but its length may vary between inputs. Group

\nu

has a positive row count

n_\nu

and a positive length

a_{\nu,h}

at each spectator tag

h

; at a chunk tag put

a_{\nu,h}=2^L

. Define

Q_\nu=\prod_{h=1}^t a_{\nu,h},\qquad M_\nu=n_\nu Q_\nu,\qquad C_\nu=\sum_{\mu<\nu}M_\mu,\qquad V_\nu=M_\nu R,

and require

M=\sum_{\nu=1}^J M_\nu

. The stream consists of

M

records of

R

bits. In group order, their addresses form the consecutive lexicographic rectangles

[n_\nu]\times\prod_{h=1}^t[a_{\nu,h}].

The first coordinate is a row ordinal. Every row contains the full Cartesian suffix displayed above: no suffix length depends on a coordinate within that row. The suffix lengths may differ between groups. Every finite sequence of per-row spectator length vectors in the fixed template is representable, using groups of count one when necessary. Use the integer code

\Gamma

from . The supplied descriptor is exactly

\begin{split} \mathcal D={}& \Gamma(M)\Gamma(R)\Gamma(K)\Gamma(f)\Gamma(\rho+1)\Gamma(t)\, T_1\cdots T_t\,\Gamma(J)\\ &{}\cdot\prod_{\nu=1}^{J} \left(\Gamma(n_\nu) \prod_{h:T_h=\mathtt{00}}\Gamma(a_{\nu,h})\right), \end{split}

where

T_h

is the tag at position

h

, and juxtaposition and products mean bitstring concatenation in increasing index order. The header, tag count, and group count delimit the entire list. A grouped packed stream is valid when this descriptor and its accompanying records have exactly the parameters, shapes, and orders just specified.

In plain English

Defines a valid grouped packed stream:

M

records of

R

bits laid out as consecutive lexicographic rectangles

[n_\nu]\times\prod_h[a_{\nu,h}]

for groups

\nu=1,\dots,J

, over a common template of

t\ge3

two-bit tags (spectator

\mathtt{00}

, and

x,y,z

once each) with spectator lengths

a_{\nu,h}

and chunk length

2^L

L=fK

. It also fixes the exact

\Gamma

-coded descriptor that lists

M,R,K,f,\rho+1,t

, the tags,

J

, and each group's

n_\nu

and spectator lengths.

Why it's here

This fixes the data layout and its self-delimiting description so that packed-addition procedures on grouped rectangles have a precisely specified input. Later results, beginning with the packed selected-bit addition lemma, take a valid grouped packed stream as input and rely on these shapes, orders and descriptor contents, including that every row has a full Cartesian suffix and that the suffix lengths may vary between groups.

Classified routine:

A bookkeeping definition of a data layout and self-delimiting descriptor for Turing-machine implementation. It adapts standard multitape data-layout conventions, as in Harvey–van der Hoeven 2021, to grouped lexicographic rectangles, and is not a conceptual novelty.

Uses

Nothing else in the paper

Used by

lemPacked selected-bit XOR on grouped streams

Sources

PaperOpen

Section: §A Packed additions on grouped rectangles
Page: —
Label: def:grouped-packed-stream
Line: sections/11-grouped-rectangles.tex:12

Leannot aligned

Phase 2 aligns this node to a Lean declaration.