DSpace Kolekcja:

Formalization of Orthogonal Decomposition for Hilbert Spaces

2022-01-01T00:00:00Z

Tytuł: Formalization of Orthogonal Decomposition for Hilbert Spaces Autorzy: Okazaki, Hiroyuki Abstrakt: In this article, we formalize the theorems about orthogonal decomposition of Hilbert spaces, using the Mizar system [1], [2]. For any subspace S of a Hilbert space H, any vector can be represented by the sum of a vectorin S and a vector orthogonal to S. The formalization of orthogonal complements of Hilbert spaces has been stored in the Mizar Mathematical Library [4]. We referred to [5] and [6] in the formalization.

Existence and Uniqueness of Algebraic Closures

2022-01-01T00:00:00Z

Tytuł: Existence and Uniqueness of Algebraic Closures Autorzy: Schwarzweller, Christoph Abstrakt: This is the second part of a two-part article formalizing existence and uniqueness of algebraic closures, using the Mizar [2], [1] formalism. Our proof follows Artin’s classical one as presented by Lang in [3]. In the first part we proved that for a given field F there exists a field extension E such that every nonconstant polynomial p ∈ F[X] has a root in E. Artin’s proof applies Kronecker’s construction to each polynomial p ∈ F[X]\F simultaneously. To do so we needed the polynomial ring F[X₁, X₂, ...] with infinitely many variables, one for each polynomal p ∈ F[X]\F. The desired field extension E then is F[X₁, X₂, ...]\I, where I is a maximal ideal generated by all nonconstant polynomials p ∈ F[X]. Note, that to show that I is maximal Zorn’s lemma has tobe applied. In this second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension A of F, in which every non-constant polynomial p ∈ A[X] has a root. The field of algebraic elements of A then is an algebraic closure of F. To prove uniqueness of algebraic closures, e.g.that two algebraic closures of F are isomorphic over F, the technique of extending monomorphisms is applied: a monomorphism F−→A, where A is an algebraic closure of F can be extended to a monomorphism E−→A, where E is any algebraic extension of F. In case that E is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.

Prime Representing Polynomial with 10 Unknowns

2022-01-01T00:00:00Z

Tytuł: Prime Representing Polynomial with 10 Unknowns Autorzy: Pąk, Karol Abstrakt: In this article we formalize in Mizar [1], [2] the final step of ourattempt to formally construct a prime representing polynomial with 10 variablesproposed by Yuri Matiyasevich in [4].The first part of the article includes many auxiliary lemmas related to multivariate polynomials. We start from the properties of monomials, among them their evaluation as well as the power function on polynomials to define the substitution for multivariate polynomials. For simplicity, we assume that a polynomialand substituted ones as i-th variable have the same number of variables. Then we study the number of variables that are used in given multivariate polynomials. By the used variable we mean a variable that is raised at least once to a non-zeropower. We consider both adding unused variables and eliminating them. The second part of the paper deals with the construction of the polynomialproposed by Yuri Matiyasevich. First, we introduce a diophantine polynomialover 4 variables that has roots in integers if and only if indicated variable is thesquare of a natural number, and another two is the square of an odd naturalnumber. We modify the polynomial by adding two variables in such a way thatthe root additionally requires the divisibility of these added variables. Then wemodify again the polynomial by adding two variables to also guarantee the nonnegativity condition of one of these variables. Finally, we combine the prime diophantine representation proved in [7] with the obtained polynomial constructinga prime representing polynomial with 10 variables. This work has been partiallypresented in [8] with the obtained polynomial constructing a prime representingpolynomial with 10 variables in Theorem (85).

Prime Representing Polynomial with 10 Unknowns – Introduction. Part II

2022-01-01T00:00:00Z

Tytuł: Prime Representing Polynomial with 10 Unknowns – Introduction. Part II Autorzy: Pąk, Karol Abstrakt: In our previous work [7] we prove that the set of prime numbersis diophantine using the 26-variable polynomial proposed in [4]. In this paper,we focus on the reduction of the number of variables to 10 and it is the smal-lest variables number known today [5], [10]. Using the Mizar [3], [2] system, weformalize the first step in this direction by proving Theorem 1 [5] formulated asfollows: Let k ∈ N. Then k is prime if and only if there exists f, i, j, m, u ∈ N+,r, s, t ∈ N unknowns such that DFI is square ∧(M²−1)S²+1 is square ∧((M U)²−1)T²+1 is square ∧(4f²−1)(r−mST U)²+ 4u²S²T²<8f uST(r−mST U)F L|(H−C)Z+F(f+ 1)Q+F(k+ 1)((W²−1)Su−W²u²+ 1) (0.1) where auxiliary variables A−I, L, M, S−W, Q ∈ Z are simply abbreviations defined as follows W= 100f k(k+ 1),U= 100u³W³+ 1,M= 100mU W+ 1,S= (M−1)s+k+1,T= (M U−1)t+W−k+1,Q= 2M W−W²−1,L= (k+1)Q,A=M(U+ 1),B=W+ 1,C=r+W+ 1,D= (A²−1)C²+ 1,E= 2iC²LD,F= (A²−1)E²+1,G=A+F(F−A),H=B+2(j−1)C,I= (G²−1)H²+1. It is easily see that (0.1) uses 8 unknowns explicitly along with five implicit one foreach diophantine relationship: is square, inequality, and divisibility. Together with k this gives a total of 14 variables. This work has been partially presented in [8].