Positive Pythagorean triples and 16-parameter variant

This file contains the positive-triple remark and the unrestricted 16-parameter substitution obtained from the four-square theorem.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.aPosParam : RatPoly 4

a_pos = y + (1+w)·z

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.bPosParam : RatPoly 4

b_pos = y

Equations

• LeanPool.PythagoreanPolynomialParametrization.bPosParam = LeanPool.PythagoreanPolynomialParametrization.yVar

noncomputable def LeanPool.PythagoreanPolynomialParametrization.cPosParam : RatPoly 4

c_pos = x + (1-w)²·x

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.fPosParam : RatPoly 4

f_pos = c_pos·(a_pos² - b_pos²)/2

In the paper: ((x+(1-w)²x)((y+(1+w)z)²-y²))/2

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.gPosParam : RatPoly 4

g_pos = c_pos·a_pos·b_pos

In the paper: (x+(1-w)²x)(y+(1+w)z)y

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.hPosParam : RatPoly 4

h_pos = c_pos·(a_pos² + b_pos²)/2

In the paper: ((x+(1-w)²x)((y+(1+w)z)²+y²))/2

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PythagoreanPolynomialParametrization.f_pos_param_intValued : IsIntValued fPosParam

The first coordinate polynomial in the positive parametrization is integer-valued.

theorem LeanPool.PythagoreanPolynomialParametrization.g_pos_param_intValued : IsIntValued gPosParam

The second coordinate polynomial in the positive parametrization is integer-valued.

theorem LeanPool.PythagoreanPolynomialParametrization.h_pos_param_intValued : IsIntValued hPosParam

The third coordinate polynomial in the positive parametrization is integer-valued.

def LeanPool.PythagoreanPolynomialParametrization.mkRatPolyInput4 (x' y' z' w' : ℤ) : Fin 4 → ℤ

Construct a 4-tuple input for polynomial evaluation from individual components.

Equations

• LeanPool.PythagoreanPolynomialParametrization.mkRatPolyInput4 x' y' z' w' i = if i = 0 then x' else if i = 1 then y' else if i = 2 then z' else w'

theorem LeanPool.PythagoreanPolynomialParametrization.positive_triples_parametrization : IsIntValued fPosParam ∧ IsIntValued gPosParam ∧ IsIntValued hPosParam ∧ positivePythagoreanTriples = {(x, y, z) : ℤ × ℤ × ℤ | ∃ (x' : ℤ) (y' : ℤ) (z' : ℤ) (w' : ℤ), 0 < x' ∧ 0 < y' ∧ 0 < z' ∧ 0 ≤ w' ∧ ratPolyEval fPosParam (mkRatPolyInput4 x' y' z' w') = ↑x ∧ ratPolyEval gPosParam (mkRatPolyInput4 x' y' z' w') = ↑y ∧ ratPolyEval hPosParam (mkRatPolyInput4 x' y' z' w') = ↑z}

Frisch--Vaserstein's positive Pythagorean-triple parametrization, with positive parameters x, y, z and nonnegative parameter w.

16-parameter parametrization via four-square theorem

noncomputable def LeanPool.PythagoreanPolynomialParametrization.xSub : RatPoly 16

xSub = x₁² + x₂² + x₃² + x₄² + 1

Equations

• LeanPool.PythagoreanPolynomialParametrization.xSub = MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 2 + MvPolynomial.X 2 ^ 2 + MvPolynomial.X 3 ^ 2 + MvPolynomial.C 1

noncomputable def LeanPool.PythagoreanPolynomialParametrization.ySub : RatPoly 16

ySub = y₁² + y₂² + y₃² + y₄² + 1

Equations

• LeanPool.PythagoreanPolynomialParametrization.ySub = MvPolynomial.X 4 ^ 2 + MvPolynomial.X 5 ^ 2 + MvPolynomial.X 6 ^ 2 + MvPolynomial.X 7 ^ 2 + MvPolynomial.C 1

noncomputable def LeanPool.PythagoreanPolynomialParametrization.zSub : RatPoly 16

zSub = z₁² + z₂² + z₃² + z₄² + 1

Equations

• LeanPool.PythagoreanPolynomialParametrization.zSub = MvPolynomial.X 8 ^ 2 + MvPolynomial.X 9 ^ 2 + MvPolynomial.X 10 ^ 2 + MvPolynomial.X 11 ^ 2 + MvPolynomial.C 1

noncomputable def LeanPool.PythagoreanPolynomialParametrization.wSub : RatPoly 16

wSub = w₁² + w₂² + w₃² + w₄²

Equations

• LeanPool.PythagoreanPolynomialParametrization.wSub = MvPolynomial.X 12 ^ 2 + MvPolynomial.X 13 ^ 2 + MvPolynomial.X 14 ^ 2 + MvPolynomial.X 15 ^ 2

noncomputable def LeanPool.PythagoreanPolynomialParametrization.a16Param : RatPoly 16

a_16 = ySub + (1 + wSub) * zSub

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.b16Param : RatPoly 16

b_16 = ySub

Equations

• LeanPool.PythagoreanPolynomialParametrization.b16Param = LeanPool.PythagoreanPolynomialParametrization.ySub

noncomputable def LeanPool.PythagoreanPolynomialParametrization.c16Param : RatPoly 16

c_16 = xSub + (1 - wSub)² * xSub

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.f16Param : RatPoly 16

f_16 = c_16·(a_16² - b_16²)/2

In the paper: ((xSub+(1-wSub)²xSub)((ySub+(1+wSub)zSub)²-ySub²))/2

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.g16Param : RatPoly 16

g_16 = c_16·a_16·b_16

In the paper: (xSub+(1-wSub)²xSub)(ySub+(1+wSub)zSub)ySub

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PythagoreanPolynomialParametrization.h16Param : RatPoly 16

h_16 = c_16·(a_16² + b_16²)/2

In the paper: ((xSub+(1-wSub)²xSub)((ySub+(1+wSub)zSub)²+ySub²))/2

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PythagoreanPolynomialParametrization.exists_16_param_parametrization : IsIntValued f16Param ∧ IsIntValued g16Param ∧ IsIntValued h16Param ∧ positivePythagoreanTriples = {(x, y, z) : ℤ × ℤ × ℤ | ∃ (a : Fin 16 → ℤ), ratPolyEval f16Param a = ↑x ∧ ratPolyEval g16Param a = ↑y ∧ ratPolyEval h16Param a = ↑z}

The positive-triple parametrization with unrestricted integer parameters, obtained from the four-variable positive parametrization by replacing the positive/nonnegative parameters with four-square expressions.