PC0001 polynomial_zero_extended_entry_existsEvery 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 StableActual antidiagonal sums · canonical residues · nonzero leading terms
Construct highest-degree-first coefficient convolution, prove its finite support, and establish degree addition for genuinely nonzero-leading prime-field representations.
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.
PC0001 polynomial_zero_extended_entry_existsEvery 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 StablePC0002 polynomial_zero_extended_entry_functionalZero extension is value-functional; the inside and outside cases cannot overlap.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0003 polynomial_zero_extended_entry_insideInside 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 StablePC0004 polynomial_zero_extended_entry_transportArbitrary 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 StablePC0005 polynomial_zero_extended_zero_valueThe 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 StablePC0006 polynomial_diagonal_term_existsFor 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 StablePC0007 polynomial_diagonal_term_functionalThe 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 StablePC0008 polynomial_diagonal_term_transportReencoding either input preserves every actual antidiagonal multiplication term.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0009 polynomial_diagonal_term_leadingFor 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 StablePC000A polynomial_diagonal_term_zero_leftAn actually all-zero left coefficient prefix makes every antidiagonal product zero.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC000B polynomial_diagonal_term_zero_rightAn actually all-zero right coefficient prefix makes every antidiagonal product zero.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC000C polynomial_diagonal_term_past_supportBeyond 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 StablePC000D polynomial_diagonal_prefix_entryEvery 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 StablePC000E polynomial_diagonal_prefix_recodingAn 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 StablePC000F polynomial_diagonal_prefix_from_pointwiseOrdinary 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 StablePC0010 polynomial_diagonal_prefix_functionalThe 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 StablePC0011 polynomial_diagonal_prefix_existsConstruct 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 StablePC0012 polynomial_diagonal_prefix_input_transportRecoding 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 StablePC0013 prime_field_convolution_coefficient_existsEvery output index has an actual finite antidiagonal product sum and its actual canonical residue.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0014 prime_field_convolution_coefficient_functionalDifferent real beta sum histories and diagonal encodings yield exactly the same canonical convolution coefficient.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0015 prime_field_convolution_coefficient_boundedEvery actual convolution coefficient is a canonical representative strictly below the modulus.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0016 prime_field_convolution_coefficient_transportInput coefficient reencoding preserves each actual convolution sum and its canonical output.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0017 prime_field_convolution_coefficient_leadingThe 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 StablePC0018 prime_field_convolution_coefficient_zero_leftAn actual zero left input prefix gives zero at every canonical convolution coefficient.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0019 prime_field_convolution_coefficient_zero_rightAn actual zero right input prefix gives zero at every canonical convolution coefficient.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC001A prime_field_convolution_coefficient_zero_past_supportEvery coefficient past the genuine finite convolution support is zero.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC001B prime_field_convolution_prefix_entryEvery 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 StablePC001C prime_field_convolution_prefix_recodingAn 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 StablePC001D prime_field_convolution_prefix_from_pointwiseOrdinary 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 StablePC001E prime_field_convolution_prefix_functionalThe 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 StablePC001F prime_field_convolution_prefix_existsConstruct 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 StablePC0020 prime_field_convolution_prefix_boundedThe constructed convolution coefficient table is actually canonical at every encoded position.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0021 prime_field_convolution_prefix_input_transportReencoding both finite inputs preserves the same actual canonical convolution output prefix.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0022 polynomial_product_length_existsConstruct 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 StablePC0023 polynomial_product_length_functionalThe 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 StablePC0024 prime_field_polynomial_convolution_boundedEvery coefficient of the actual proper-length product is a canonical field representative.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0025 prime_field_polynomial_convolution_entryEvery 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 StablePC0026 prime_field_polynomial_convolution_transportIndependent 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 StablePC0027 prime_field_polynomial_convolution_functionalThe 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 StablePC0028 prime_field_polynomial_convolution_at_length_existsConstruct an actual canonical product at its proved proper length, using genuine finite antidiagonal computations.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0029 prime_field_polynomial_convolution_exists_uniqueFor 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 StablePC002A prime_field_polynomial_convolution_emptyEither 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 StablePC002B prime_field_polynomial_convolution_zero_leftAn 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 StablePC002C prime_field_polynomial_convolution_zero_rightAn 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 StablePC002D prime_field_polynomial_convolution_outside_zeroEvery 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 StablePC002E polynomial_product_length_positive_inputsTwo nonempty representation lengths S d and S e have the unique proper product length S(d+e).
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC002F prime_field_polynomial_represented_degree_leading_nonzeroEvery decoding of the leading coefficient of this nonzero-leading representation is actually nonzero.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0030 prime_field_polynomial_represented_degree_transportReencoding an actual coefficient prefix preserves its annotated length, canonical bounds and nonzero leading coefficient.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0031 prime_field_polynomial_represented_degree_excludes_zeroAn actual zero polynomial prefix cannot satisfy represented nonzero degree, including degree zero.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0032 prime_field_polynomial_monic_degree_examplesFor 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 StablePC0033 prime_field_polynomial_convolution_leading_coefficientThe leading coefficient of the actual proper-length convolution is the actual canonical product of the input leading coefficients.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePC0034 prime_field_polynomial_convolution_represented_degreeOver 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 StablePC0035 prime_field_polynomial_convolution_represented_degree_existsConstruct the genuine product and its exact sum-of-degrees certificate for arbitrary nonzero-leading input representations, including constants and characteristic two.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not StablePD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1ND0263 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 1PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
Conservative definition · notation layer 0ND0023 CanonicalModularResidue(m,a,r)A strictly bounded canonical natural residue r<m together with exact balanced congruence to a modulo m.
Conservative definition · notation layer 1ND0230 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 2ND0291 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 1ND0292 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 2ND0293 PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l)A real beta table contains the actual antidiagonal products for j<l. The full window l=S i is constructed, so every complementary index is natural.
Conservative definition · notation layer 3ND0294 FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r)Build the S i antidiagonal terms, take their actual natural Sum, then take its canonical residue r modulo p. No evaluation-product identity or degree assertion is assumed.
Conservative definition · notation layer 4ND0295 FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,l)Every output coefficient at i<l is the independently defined actual antidiagonal sum residue. The finite output beta table is constructed rather than postulated.
Conservative definition · notation layer 5ND0296 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 0ND0262 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 1ND0297 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 6ND0298 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 2Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.