Actual antidiagonal sums · canonical residues · nonzero leading terms

Canonical polynomial products and represented degree

Construct highest-degree-first coefficient convolution, prove its finite support, and establish degree addition for genuinely nonzero-leading prime-field representations.

53 kernel- and Lean-verified Alpha-closed theorems · 19 conservative definitions · 30 notation dependencies

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

72 items
PC0001 polynomial_zero_extended_entry_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0003 polynomial_zero_extended_entry_inside

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0004 polynomial_zero_extended_entry_transport

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0005 polynomial_zero_extended_zero_value

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0006 polynomial_diagonal_term_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0007 polynomial_diagonal_term_functional

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0008 polynomial_diagonal_term_transport

Reencoding either input preserves every actual antidiagonal multiplication term.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0009 polynomial_diagonal_term_leading

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC000A polynomial_diagonal_term_zero_left

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC000B polynomial_diagonal_term_zero_right

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC000C polynomial_diagonal_term_past_support

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC000D polynomial_diagonal_prefix_entry

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC000E polynomial_diagonal_prefix_recoding

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC000F polynomial_diagonal_prefix_from_pointwise

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0010 polynomial_diagonal_prefix_functional

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0011 polynomial_diagonal_prefix_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0012 polynomial_diagonal_prefix_input_transport

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0017 prime_field_convolution_coefficient_leading

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC001B prime_field_convolution_prefix_entry

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC001C prime_field_convolution_prefix_recoding

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC001D prime_field_convolution_prefix_from_pointwise

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC001E prime_field_convolution_prefix_functional

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC001F prime_field_convolution_prefix_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0020 prime_field_convolution_prefix_bounded

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0022 polynomial_product_length_exists

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0023 polynomial_product_length_functional

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0025 prime_field_polynomial_convolution_entry

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0026 prime_field_polynomial_convolution_transport

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0027 prime_field_polynomial_convolution_functional

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0029 prime_field_polynomial_convolution_exists_unique

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC002A prime_field_polynomial_convolution_empty

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC002B prime_field_polynomial_convolution_zero_left

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC002C prime_field_polynomial_convolution_zero_right

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC002D prime_field_polynomial_convolution_outside_zero

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.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0032 prime_field_polynomial_monic_degree_examples

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.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PC0034 prime_field_polynomial_convolution_represented_degree

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

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0004 Prime(p)

p is nonunit and every factorization of p has a unit factor.

Conservative definition · notation layer 0
PD0013 BetaAt(b,c,i,x)

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

Conservative definition · notation layer 0
PD0015 Sum(b,c,l,z)

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

Conservative definition · notation layer 1
PD0019 Repeat(b,c,a,l)

The decoded prefix repeats a for l positions.

Conservative definition · notation layer 1
ND0263 BetaPrefixEqual(b,c,d,e,l)

Every decoded source entry at i<l also decodes in the target. Actual beta totality and functionality make this extensional prefix equality, not equality of the two code parameters.

Conservative definition · notation layer 1
PD0008 ModEq(m,a,b)

Balanced-natural congruence modulo m.

Conservative definition · notation layer 0
ND0230 FpMul(p,a,b,c)

Bounded operands and the actual canonical residue of their natural product; no multiplication law is assumed.

Conservative definition · notation layer 2
ND0291 BetaZeroExtend(b,c,L,i,a)

Decode the genuine beta entry when i<L and return zero when L<=i. This explicitly length-annotated zero extension imposes no false condition on raw beta values beyond the represented prefix.

Conservative definition · notation layer 1
ND0292 PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)

Witness k with j+k=i and multiply the two actual zero-extended coefficients. These are natural products in a highest-degree-first antidiagonal, before reduction modulo the field prime.

Conservative definition · notation layer 2
ND0296 PolynomialProductLength(L,M,N)

The proper product representation is empty if either input is empty; otherwise L+M=S N. This is a representation-length relation, not a claim that a possibly zero-leading polynomial has that degree.

Conservative definition · notation layer 0
ND0262 BetaPrefixInto(b,c,l,B)

Every actual beta entry below the strict length l has a witnessed value below B. The same generic graph describes canonical polynomial coefficients when B is the modulus; empty prefixes are allowed.

Conservative definition · notation layer 1
ND0297 FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)

Canonical input prefixes, the proper product length, and a genuine convolution output prefix. Terms beyond this length vanish by a separate support theorem, not by assuming the discarded tail is zero.

Conservative definition · notation layer 6
ND0298 FpRepresentedDegree(p,b,c,L,d)

A length-annotated canonical coefficient prefix has L=S d and an actually decoded nonzero leading coefficient. This does not assign degree to zero or normalize arbitrary leading-zero representations.

Conservative definition · notation layer 2

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.