Finite convolution associativity — Exact Proof Explorer

Zero first or last factors and genuine nondivisor products give canonical zero without reading either zero-index input.

A real three-factor equation, three actual signed lookups and two actual products construct a retained grid cell.

Every actually omitted grid cell is zero; a retained factorization cannot coexist with its omitted guard.

Nonzero product cancellation identifies the supplied middle factor; canonical input lookups recover both actual signed products.

Each genuine first/last-factor cell has one canonical signed value, without identifying any table representation.

Constructively decide the factor guards, extract the actual middle factor, and construct three signed lookups and both products.

Interchanging the first and last factors preserves an actual cell, by proved signed scalar interchange and a real factor-equation permutation.

Actual division by S n decodes every flat index, then the genuinely constructed factor cell supplies its signed value.

Uniqueness of the actual quotient and strict remainder recovers the specified grid coordinates, rather than assuming a decoding oracle.

A genuinely constructed singleton supplies the first flat cell; no finite table or choice axiom is used.

Append one actual signed flat cell by real beta-stream extension and preserve all preceding represented values.

Ordinary induction constructs each actual inclusive flat prefix, with an independently witnessed quotient, remainder and signed value at every extension.

The actual flat prefix supplies every bounded grid cell; the old checked matrix index bound and unique division prove the row-major decoding.

Construct the entire real first/last-factor grid, including its harmless extra certified endpoint, from actual input tables.

Every actual bounded row-major lookup has precisely the independently defined factor-cell graph.

A positive first factor cancels from the actual nested factor equations, identifying the inner convolution quotient.

Multiplying an actual inner convolution summand gives the exact factor cell, including zero and omitted inner divisors.

Canonical factor-cell functionality identifies its value with the actual scalar multiple of any witnessed inner convolution summand.

A zero or nondivisor first factor forces every actual row cell to zero, independently of input values at zero.

A genuine factor row is the actual pointwise scalar product of a constructed padded convolution prefix, on the identical S n-entry window.

An actual row slice supplies the exact factor-row values; every affine coordinate is transported by a proved natural equality.

An actual column slice supplies the exact factor-row values; every affine coordinate is transported by a proved natural equality.

Construct the actual factor grid, both actual signed row/column tables and genuine prefix-sum traces with one common value, by the already proved finite Fubini theorem.

The actual signed sum of a zero or nondivisor factor row is zero; no value at either input zero index is used.

Construct the actual inner convolution sum, prove its positive quotient bound, remove its zero padding and identify the row total by actual signed scalar linearity.

Each actual factor-row total is precisely an outer convolution summand of the genuine inner output table, with all positive-index bounds proved.

The actual row sum table is the genuine nested-convolution summand prefix, including every omitted zero row and every proved positive quotient bound.

The actual column sum table is the genuine nested-convolution summand prefix, including every omitted zero row and every proved positive quotient bound.

Actual first/last-factor grid construction and finite Fubini prove F*(H*G)=H*(F*G) at every positive in-domain index; neither a pair permutation nor a rearrangement oracle is supplied.

Actual finite Dirichlet convolution is associative at each positive in-domain input, by genuine factor-grid Fubini and the checked divisor-complement commutativity.

Any genuine output tables for the two parenthesizations agree on precisely 0<n<=N; no equality of encodings or arbitrary zero values is asserted.

Construct all four actual intermediate/output beta tables and prove their positive-domain associativity, including the vacuous N=0 boundary.