Sum of four squares with square conditions

Any integer $n \geq 0$ can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers and $z \leq w$, such that both $x$ and $x + 24y$ are squares.

Zhi-Wei Sun has offered a $2,400 prize for the first proof.

References:

• OEIS A281976
• Z.-W. Sun, "Refining Lagrange's four-square theorem," J. Number Theory 175 (2017), 167-190. https://doi.org/10.1016/j.jnt.2016.11.008
• Z.-W. Sun, "Restricted sums of four squares," arXiv:1701.05868 [math.NT], 2017. https://arxiv.org/abs/1701.05868

def OeisA281976.IsSumOfFourSquaresWithSquareConditions (n : ℕ) : Prop

The predicate that n can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers, $z \leq w$, such that both $x$ and $x + 24y$ are squares.

Equations

• OeisA281976.IsSumOfFourSquaresWithSquareConditions n = ∃ (x : ℕ) (y : ℕ) (z : ℕ) (w : ℕ), n = x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2 ∧ z ≤ w ∧ IsSquare x ∧ IsSquare (x + 24 * y)

theorem OeisA281976.isSumOfFourSquaresWithSquareConditions_0 : IsSumOfFourSquaresWithSquareConditions 0

theorem OeisA281976.isSumOfFourSquaresWithSquareConditions_8 : IsSumOfFourSquaresWithSquareConditions 8

theorem OeisA281976.isSumOfFourSquaresWithSquareConditions_12 : IsSumOfFourSquaresWithSquareConditions 12

theorem OeisA281976.isSumOfFourSquaresWithSquareConditions_23 : IsSumOfFourSquaresWithSquareConditions 23

theorem OeisA281976.isSumOfFourSquaresWithSquareConditions_24 : IsSumOfFourSquaresWithSquareConditions 24

theorem OeisA281976.conjecture (n : ℕ) : IsSumOfFourSquaresWithSquareConditions n

Zhi-Wei Sun's Conjecture (A281976): Any integer $n \geq 0$ can be written as $x^2 + y^2 + z^2 + w^2$ with $x, y, z, w$ nonnegative integers and $z \leq w$, such that both $x$ and $x + 24y$ are squares.