Finite convolution associativity

Witness-defined non-strict order on natural numbers.

Witness-defined strict order on natural numbers.

The natural number d divides n.

q and r are a quotient and a strict remainder for n by d.

One canonical injective doubled-Cantor code for all four signed-minor beta-code parameters.

x is the bounded beta-decoded value at index i.

The original canonical integer code: even 2p denotes p, and odd 2k+1 denotes −(k+1). The decoded positive and negative parts are normalized.

The original canonical code z represents the integer difference p−n; these supplied components need not be normalized.

An actual packed signed table with canonical signed entries through index N, including index zero. It contains no divisor transform or inversion hypothesis.

Two genuine beta entries of the packed table represent the unique canonical signed value z. Distinct component representations need not be equal.

Actual multiplication of original canonical signed codes; opposite-sign products remain on the negative side of the balance.

At a positive divisor d, witness n=d*q, read the actual signed values F(d) and G(q), and multiply them. Zero and nondivisors contribute canonical zero without reading either input at zero. Source-table validity is separate.

An actual signed table M records the independently defined convolution entry at every inclusive index 0<=d<=l. The endpoint l is included and can differ from n; no sum or convolution identity is assumed.

z is the sum of a beta-coded prefix of length l.

The signed balance of two actual natural finite sums, at exactly the indices 0<=i<l. Existence, uniqueness and representation independence are proved separately.

Require n>0, construct a real convolution-summand prefix through n, and take its actual signed fold over exactly S n entries. Zero is outside this sum's input domain; no value is assigned by a unit or inversion formula.

Three actual finite signed tables whose output H(n), at every 0<n<=N, is the independently defined convolution sum of F and G. All zero entries are unrestricted; only represented positive values, not table codes, are subsequently proved unique.

Every actual signed lookup on the half-open interval k<=i<l has value zero. Table validity, existence of folds, and equality after padding are separate hypotheses or theorems, not part of this graph.

Actual signed tables with witnessed values G(i)=F(o+s*i) for i<l. The output is constructed by real beta-stream recoding; its separately certified endpoint is unused.

An actually constructed affine slice followed by its genuine signed prefix sum. Both zero length and zero stride are meaningful; no sum oracle is part of the graph.

An actual row table R contains, at i<m, the signed sum of the n entries F((o+s*i)+t*j). Source and row-table packings are explicit, including empty dimensions.

Construct an actual row-sum table and take its actual m-entry signed sum. Equality after swapping strides and dimensions is the independently proved finite Fubini theorem.

Actual source and output tables with witnessed multiplication of every represented entry below l by the signed scalar a. Sum distributivity is a separate theorem.

Equality of represented values at precisely 0<d<=N. Values at zero are unrestricted, and raw codes or positive/negative representatives are not asserted equal.

A retained cell has a!=0, e!=0, an actual middle factor n=(a*e)*c, and the two signed products F(a)*(H(e)*G(c)). Cells with a=0, e=0 or a*e not dividing n are zero. Positivity of n and source-table validity are separate guards.

Witness genuine row-major quotient/remainder coordinates i=(S n)*a+e with e<S n, then require the corresponding actual factor-grid entry. This graph does not itself bound a by n or assume a rearrangement law.

An actual signed table stores each independently defined flat grid entry at every inclusive index i<=l. Its construction uses finite division and beta recoding; no supplied grid, sum, or Fubini conclusion is built into the graph.

The actual row-major (S n)-by-(S n) factor grid specifies cells a,e<=n at index (S n)*a+e. The underlying table separately certifies its unused endpoint (S n)*(S n). Construction from a flat prefix is a proof dependency, not an extra definition condition.

An actual signed row V records the factor cells for fixed a at every e<=n. Its separately valid endpoint S n is unused. No bound a<=n, scalar-sum identity, or associativity law is included as an assumption.