propositionnovelinferred_depunresolved_ref

Simultaneous Hadamard layer in near-linear time

Applies a Hadamard layer in

O(Vd^{\lambda'})

time with one final truncation

per-round black box for the synthetic transforms

Proposition·prop:simultaneous-layer·§5.4 An explicit guard-width bound

Statement (paper)

Fix

\tau=\sigma=1-2^{-50},\qquad \beta=\frac12,\qquad C_1=20.

Let

c,\epsilon,\lambda,\lambda'

be fixed positive rational numbers satisfying

\max\{\tau,\sigma\}<\lambda<1,\qquad \tau(1+c/\beta)<\lambda,\qquad \max\{\lambda,\sigma+\beta(1-\sigma)\}<\lambda'<1, \qquad \epsilon C_1<1.

Fix positive constants

a_d\le b_d

and

a_r\le b_r

, and fix positive constants

C_M,C_{\rm desc},C_w

with

C_w>1

. For these fixed choices there are a cutoff

p_0

, one fixed finite-alphabet multitape procedure, and an implicit time constant with the following guarantee. The cutoff and time constant may depend on the fixed rational parameters and these constants. For every choice of positive integers

p,d,r

with

p\ge p_0

and

a_dp^\epsilon\le d\le b_dp^\epsilon,\qquad 2^{a_rp/d}\le r\le 2^{b_rp/d},

put

K=\lfloor d^c\rfloor

, and let

1\le D\le d

P,S\ge1

, and

0\le\rho<K

be integers. Let

w\ge1

be an integer component width. The input supplies on a descriptor tape the self-delimiting header

\mathcal E= \Gamma(p)\Gamma(d)\Gamma(r)\Gamma(D)\Gamma(P)\Gamma(S) \Gamma(K)\Gamma(\rho+1)\Gamma(w),

using the integer code from . Assume that this header is valid with the stated values and that the accompanying array is in lexicographic order on the complete address set

[P]\times[2^K]^D\times[S], \qquad M=PS\,2^{KD},

with the following record format. For every address

x\in[P]\times[2^K]^D\times[S]

, write its record as

z(x)=\sum_{j=0}^{r-1}z_{x,j}y^j,

stored in coefficient order. For every

x

and

0\le j<r

, assume

\lvert z_{x,j}\rvert\le1

and

\Re z_{x,j},\Im z_{x,j}\in2^{-p}\mathbb Z

. Each component is

2^{-p}

times a signed

w

-bit two's-complement integer, written most significant bit first; the real component precedes the imaginary component. Require the pointwise bounds

\log_2(2M)\le C_Mp,\qquad |\mathcal E|\le C_{\rm desc}p,\qquad p+2\le w\le C_wp,

where

|\mathcal E|

is the header's bit length. The condition

w\ge p+2

allows every permitted disk-grid component, including

-1

and

1

. The logical bit volume is

V=2Mrw=\Theta(Mrp)

. On each of the

D

consecutive

K

-bit address chunks, select bit

\rho

, numbered from the least significant bit, and let

\mathcal H

be the tensor product of

H_0=\frac12\begin{pmatrix}1&1\\1&-1\end{pmatrix}

on those selected bits. It acts coefficientwise and fixes every unselected address bit and both spectator fields. Let

Q_p

truncate the real and imaginary parts of every coefficient toward zero to

2^{-p}\mathbb Z

. The procedure returns

Q_p(\mathcal H z)

in the same array, coefficient order, and component format in

O(Vd^{\lambda'})

time, uniformly over all these choices of

p,d,r,D,P,S,\rho,w

and

z

. Every returned coefficient belongs to the complex unit disk, and, in the maximum coefficient norm,

\|Q_p(\mathcal H z)-\mathcal H z\|_\infty <\sqrt2\,2^{-p}.

The procedure evaluates the entire layer exactly before this final truncation. Put

C_0=128m\bigl(s_{\rm c}+64(W_{\rm c}+m+1)^3\bigr)^2,

where

m,W_{\rm c},s_{\rm c}

are the fixed constants of Proposition . The procedure uses at most

p+\lceil C_0d^{C_1}\rceil

fractional bits and

\lceil C_0d^{C_1}\rceil+3

integer and sign bits per real component internally; these widths are

O(p)

. The time includes address changes, deterministic repair, row padding and its removal, and fixed-tape workspace cleanup. Its tape count is fixed, and its time constant is independent of the allowed array lengths and coefficient values.

In plain English

For the fixed parameters

\tau=\sigma=1-2^{-50}

\beta=1/2

C_1=20

and admissible

c,\epsilon,\lambda,\lambda'

, one fixed multitape procedure applies the Hadamard layer

\mathcal H

H_0

on bit

\rho

of each of

D

consecutive

K

-bit address chunks) to a complete lexicographic array of ring records in time

O(Vd^{\lambda'})

. The output is

Q_p(\mathcal H z)

in the same format, lies in the unit disk, and differs from

\mathcal H z

by less than

\sqrt2\,2^{-p}

in sup norm, since only one final truncation is done.

Why it's here

This is the main layer-level tool: it turns the complex network's translation-kernel factorization into a concrete

O(Vd^{\lambda'})

algorithm for a whole round of simultaneous Hadamard transforms, using packed selected-bit basis changes whose costs are summed by a recurrence. A guard width of order

d^{C_1}

, which is

o(p)

because

\epsilon C_1<1

, lets everything be computed exactly until a single final truncation, so the error bound and output format hold. Later transform-cost and ring-multiplication results call it as a black box for each round.

Classified novel:

This is the paper's main layer-level algorithm. It turns the complex-network translation-kernel factorization into an O(V d^{λ'}) multitape procedure for a whole round of simultaneous Hadamard transforms, with exact computation under a d^{C_1} guard width and a single final truncation. No prior integer-multiplication algorithm (e.g. Harvey–van der Hoeven's O(n log n)) provides a sub-n log n Hadamard-layer step of this kind.

Uses

lemPacked XOR of selected address bitspropComplex network edges factor into translation kernels

Used by

lemCost and accuracy of synthetic transformlemExact negacyclic product with one truncationclaimEach layout round meets layer hypothesesclaimFixed exponents satisfy all parameter conditionsclaimDisk margins and error propagation through transformsclaimCost table yields the final time bound

Inside the proof

claimUniform bound on packed-child width parameterclaimPacked basis changes cost uniformly near-linearclaimRecurrence total cost and conversion to HclaimGuarded evaluation with single final truncation

Sources

PaperOpen

Section: §5.4 An explicit guard-width bound
Page: —
Label: prop:simultaneous-layer
Line: sections/05-layers.tex:826

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The statement (sections/05-layers.tex:914-915) defines C_0 from "the fixed constants of Proposition ". The proof's "phase-frame construction reduces a group of e selected bits to s_c children" (line 929-930) is that proposition.
warn
unresolved_ref
The proof relies on unlabeled material preceding it in §5 (phase-frame recursion, row construction, recurrence unrolling, guard-width bound) rather than labeled statements.