<abstract xmlns="http://www.w3.org/1999/xhtml">

The main purpose of the article is to construct a sophisticated polynomial proposed by Matiyasevich and Robinson [5] that is often used to reduce the number of unknowns in diophantine representations, using the Mizar [1], [2] formalism. The polynomial <disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0013_eq_001.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><msub><mrow><mi>J</mi></mrow><mi>k</mi></msub><mrow><mo>(</mo><mrow><msub><mrow><mi>a</mi></mrow><mn>1</mn></msub><mo>,</mo><mo>…</mo><mo>,</mo><msub><mrow><mi>a</mi></mrow><mi>k</mi></msub><mo>,</mo><mi>x</mi></mrow><mo>)</mo></mrow><mo>=</mo><munder><mo>∏</mo><mrow><msub><mrow><mi>ɛ</mi></mrow><mn>1</mn></msub><mo>,</mo><mo>…</mo><mo>,</mo><msub><mrow><mi>ɛ</mi></mrow><mi>k</mi></msub><mo>∈</mo><mrow><mo>{</mo> <mrow><mo>±</mo><mn>1</mn></mrow> <mo>}</mo></mrow></mrow></munder><mrow><mrow><mo>(</mo><mrow><mi>x</mi><mo>+</mo><msub><mrow><mi>ɛ</mi></mrow><mn>1</mn></msub><msqrt><mrow><msub><mrow><mi>a</mi></mrow><mn>1</mn></msub></mrow></msqrt><mo>+</mo><msub><mrow><mi>ɛ</mi></mrow><mn>2</mn></msub><msqrt><mrow><msub><mrow><mi>a</mi></mrow><mn>2</mn></msub></mrow></msqrt><mi>W</mi></mrow><mo>)</mo></mrow><mo>+</mo><mo>…</mo><mo>+</mo><msub><mrow><mi>ɛ</mi></mrow><mi>k</mi></msub><msqrt><mrow><msub><mrow><mi>a</mi></mrow><mi>k</mi></msub></mrow></msqrt><msup><mrow><mi>W</mi></mrow><mrow><mi>k</mi><mo>-</mo><mn>1</mn></mrow></msup></mrow></mrow></math>
<tex-math>{J_k}\left( {{a_1}, \ldots ,{a_k},x} \right) = \prod\limits_{{\varepsilon _1}, \ldots ,{\varepsilon _k} \in \left\{ { \pm 1} \right\}} {\left( {x + {\varepsilon _1}\sqrt {{a_1}} + {\varepsilon _2}\sqrt {{a_2}} W} \right) + \ldots + {\varepsilon _k}\sqrt {{a_k}} {W^{k - 1}}}</tex-math>
</alternatives>
</disp-formula> with <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0013_eq_002.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>W</mi><mo>=</mo><msubsup><mo>∑</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>k</mi></msubsup><mrow><msubsup><mrow><mi>x</mi></mrow> <mi>i</mi><mn>2</mn></msubsup></mrow></mrow></math>
<tex-math>W = \sum\nolimits_{i = 1}^k {x_i^2} </tex-math>
</alternatives>
</inline-formula> has integer coefficients and <italic>Jk</italic>(<italic>a</italic>1, . . ., <italic>ak, x</italic>) = 0 for some <italic>a</italic>1, . . ., <italic>ak, x</italic> ∈ ℤ if and only if <italic>a</italic>1, . . ., <italic>ak </italic>are all squares. However although it is nontrivial to observe that this expression is a polynomial, i.e., eliminating similar elements in the product of all combinations of signs we obtain an expression where every square root will occur with an even power. This work has been partially presented in [7].
</abstract>

The main purpose of the article is to construct a sophisticated polynomial proposed by Matiyasevich and Robinson [5] that is often used to reduce the number of unknowns in diophantine representations, using the Mizar [1], [2] formalism. The polynomial 


Jk(a1,…,ak,x)=∏ɛ1,…,ɛk∈{ ±1 }(x+ɛ1a1+ɛ2a2W)+…+ɛkakWk-1
{J_k}\left( {{a_1}, \ldots ,{a_k},x} \right) = \prod\limits_{{\varepsilon _1}, \ldots ,{\varepsilon _k} \in \left\{ { \pm 1} \right\}} {\left( {x + {\varepsilon _1}\sqrt {{a_1}}  + {\varepsilon _2}\sqrt {{a_2}} W} \right) +  \ldots  + {\varepsilon _k}\sqrt {{a_k}} {W^{k - 1}}}

 with 


W=∑i=1kx i2
W = \sum\nolimits_{i = 1}^k {x_i^2} 

 has integer coefficients and Jk(a1, . . ., ak, x) = 0 for some a1, . . ., ak, x ∈ ℤ if and only if a1, . . ., ak are all squares. However although it is nontrivial to observe that this expression is a polynomial, i.e., eliminating similar elements in the product of all combinations of signs we obtain an expression where every square root will occur with an even power. This work has been partially presented in [7].

Prime Representing Polynomial with 10 Unknowns – Introduction

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Prime Representing Polynomial with 10 Unknowns \u2013 Introduction"}

The main purpose of the article is to construct a sophisticated polynomial proposed by Matiyasevich and Robinson [5] that is often used to reduce the number of...

Prime Representing Polynomial with 10 Unknowns – Introduction

Publicado en línea: 30 dic 2022

Páginas: 169 - 198

Aceptado: 30 sept 2022

DOI: https://doi.org/10.2478/forma-2022-0013

Palabras clave
polynomial reduction, diophantine equation

© 2022 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Prime Representing Polynomial with 10 Unknowns – Introduction

Publicado en línea: 30 dic 2022

Páginas: 169 - 198

Aceptado: 30 sept 2022

DOI: https://doi.org/10.2478/forma-2022-0013

Palabras clavepolynomial reduction, diophantine equation

© 2022 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Palabras clave
polynomial reduction, diophantine equation