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 notation; not a theorem, primitive, or axiom.

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

Definition in prerequisite notation

(L = 0 ∨ M = 0) ∧ N = 0 ∨ ¬L = 0 ∧ (¬M = 0 ∧ L + M = S N)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
(((((L))=0 \/ ((M))=0) /\ ((((N))=0)))) \/ (((~(((L))=0)) /\ (((~(((M))=0)) /\ ((((L))+((M))=S ((N))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)

Checked theorems using this definition

PX003C · polynomial_quotient_length_productPX0050 · prime_field_polynomial_left_distributive_products_existsPX0051 · prime_field_polynomial_right_distributive_products_existsPX006A · polynomial_product_length_left_padding_leftPX006B · polynomial_product_length_left_padding_rightPX0070 · prime_field_polynomial_convolution_both_left_paddings_equivalentPX0071 · prime_field_polynomial_convolution_both_left_paddings_existsPX0079 · prime_field_polynomial_convolution_equivalent_congruent