Canonical polynomial products and represented degree — Exact Proof Explorer

Every index has an actual beta value inside the prefix and the actual zero value outside it.

Zero extension is value-functional; the inside and outside cases cannot overlap.

Inside the finite input domain the padded lookup is exactly the original beta entry.

Arbitrary beta reencoding of the finite input preserves every zero-extended value, including all outside indices.

The zero extension of a genuinely all-zero coefficient prefix is zero at every natural index.

For every j<=i construct its genuine complementary index and the actual product of the two padded coefficients.

The complementary index and both padded values determine a unique actual antidiagonal product.

Reencoding either input preserves every actual antidiagonal multiplication term.

For two nonempty highest-degree-first inputs the first antidiagonal contains exactly their leading-coefficient product.

An actually all-zero left coefficient prefix makes every antidiagonal product zero.

An actually all-zero right coefficient prefix makes every antidiagonal product zero.

Beyond the true antidiagonal support, at least one factor is genuinely padded zero; no nonzero term is discarded by the product-length convention.

Every decoded entry of the actual finite coding satisfies its precise value relation, independently of chosen witnesses.

An independently encoded but extensionally equal target prefix preserves the actual finite value graph.

Ordinary induction and genuine beta-prefix extension construct this concrete finite value table from pointwise witnesses; later roots discharge those witnesses.

The actual finite output is unique coefficientwise, without identifying different beta-code pairs.

Construct all I+1 genuine antidiagonal products, including boundary padding, without supplying any product table.

Recoding either input preserves the same concrete antidiagonal product table at every requested prefix length.

Every output index has an actual finite antidiagonal product sum and its actual canonical residue.

Different real beta sum histories and diagonal encodings yield exactly the same canonical convolution coefficient.

Every actual convolution coefficient is a canonical representative strictly below the modulus.

Input coefficient reencoding preserves each actual convolution sum and its canonical output.

The leading convolution coefficient of two nonempty canonical prefixes is their actual canonical field product, proved from its one-term natural sum.

An actual zero left input prefix gives zero at every canonical convolution coefficient.

An actual zero right input prefix gives zero at every canonical convolution coefficient.

Every coefficient past the genuine finite convolution support is zero.

Every decoded entry of the actual finite coding satisfies its precise value relation, independently of chosen witnesses.

An independently encoded but extensionally equal target prefix preserves the actual finite value graph.

Ordinary induction and genuine beta-prefix extension construct this concrete finite value table from pointwise witnesses; later roots discharge those witnesses.

The actual finite output is unique coefficientwise, without identifying different beta-code pairs.

Construct an actual beta-coded prefix of canonical convolution coefficients of every requested finite length.

The constructed convolution coefficient table is actually canonical at every encoded position.

Reencoding both finite inputs preserves the same actual canonical convolution output prefix.

Construct the exact product representation length: zero for an empty input, and L+M-1 for two nonempty inputs.

The proper finite convolution length is unique, with both-empty and one-empty cases handled explicitly.

Every coefficient of the actual proper-length product is a canonical field representative.

Every actual decoded product coefficient has precisely the genuine antidiagonal-sum-and-residue certificate.

Independent beta reencoding of both inputs and the output preserves the whole actual polynomial convolution.

The proper output length and every encoded convolution coefficient are unique; beta code numbers themselves are not.

Construct an actual canonical product at its proved proper length, using genuine finite antidiagonal computations.

For every pair of canonical finite prefixes construct a genuine proper-length convolution, including empty inputs, and prove its exact length and coefficientwise uniqueness.

Either empty input has the actual empty product; arbitrary empty output codes are equivalent and no spurious length-one coefficient is introduced.

An actual zero left polynomial yields an actually all-zero output prefix at the correct representation length.

An actual zero right polynomial yields an actually all-zero output prefix at the correct representation length.

Every genuine antidiagonal coefficient outside the proper product length is zero; this makes no assertion about arbitrary raw beta entries beyond the encoded output prefix.

Two nonempty representation lengths S d and S e have the unique proper product length S(d+e).

Every decoding of the leading coefficient of this nonzero-leading representation is actually nonzero.

Reencoding an actual coefficient prefix preserves its annotated length, canonical bounds and nonzero leading coefficient.

An actual zero polynomial prefix cannot satisfy represented nonzero degree, including degree zero.

For every prime and every degree construct an actual all-one coefficient prefix, proving that the nonzero-leading degree interface is inhabited, also in characteristic two.

The leading coefficient of the actual proper-length convolution is the actual canonical product of the input leading coefficients.

Over an actual prime field the convolution of two nonzero-leading representations has nonzero leading coefficient and represented degree exactly d+e.

Construct the genuine product and its exact sum-of-degrees certificate for arbitrary nonzero-leading input representations, including constants and characteristic two.