Divisor-Bucketed Quadruple Sum

Abstract

A divisor condition sorts the summands into classes rather than restricting them, leaving a square-sum identity.

Indices run over the interval from one to n, which includes both endpoints. The summand is an integer and may be zero or negative; the divisor is taken of its absolute value. Sums are over finite index sets, so no convergence question arises.

Definition 1.1 (The summand).

$$f\left(x,y,z\right)=x^2+y^2-z^2$$

Formalization. D5/S3/Factorization/A373561.f (✓ std3).

Citation. OEIS Foundation Inc. (2024). OEIS A373561. URL: https://oeis.org/A373561.

Commentary.

Two positive squares against one negative square. The value is an integer rather than a natural number precisely so that the negative case is not silently truncated.

Theorem 1.2 (The condition sorts rather than restricts).

$$\forall n\in \mathbb{N},\sum _{k\in \mathrm{Icc}\left(1,n\right)}\sum _{z\in \mathrm{Icc}\left(1,n\right)}\sum _{y\in \mathrm{Icc}\left(1,n\right)}\sum _{x\in \mathrm{Icc}\left(1,n\right)}[\gcd \left(|f\left(x,y,z\right)|,n\right)=k]f\left(x,y,z\right)=\sum _{z\in \mathrm{Icc}\left(1,n\right)}\sum _{y\in \mathrm{Icc}\left(1,n\right)}\sum _{x\in \mathrm{Icc}\left(1,n\right)}f\left(x,y,z\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A373561.gcd_buckets_eq_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a positive n the divisor of any summand with n lies between one and n, so each triple falls into exactly one class of the outer index. Summing over all classes therefore returns the threefold sum unchanged. A vanishing summand is not an exception: the divisor of zero with n is n, which is still a legitimate class. At n equal to zero every index set is empty and both sides vanish.

Theorem 1.3 (The threefold sum).

$$\forall n\in \mathbb{N},\sum _{z\in \mathrm{Icc}\left(1,n\right)}\sum _{y\in \mathrm{Icc}\left(1,n\right)}\sum _{x\in \mathrm{Icc}\left(1,n\right)}f\left(x,y,z\right)=n^2\cdot \sum _{x\in \mathrm{Icc}\left(1,n\right)}{x}^2$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A373561.triple_sum_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each of the two positive squares contributes a full square sum scaled by the square of the interval length, and the negative square cancels one of them, leaving that square times a single square sum.

Lemma 1.4 (The two layers composed).

$$\forall n\in \mathbb{N},\sum _{k\in \mathrm{Icc}\left(1,n\right)}\sum _{z\in \mathrm{Icc}\left(1,n\right)}\sum _{y\in \mathrm{Icc}\left(1,n\right)}\sum _{x\in \mathrm{Icc}\left(1,n\right)}[\gcd \left(|f\left(x,y,z\right)|,n\right)=k]f\left(x,y,z\right)=n^2\cdot \sum _{x\in \mathrm{Icc}\left(1,n\right)}{x}^2$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A373561.a373561_core (✓ std3). ∎

Source. Repository-derived.

Commentary.

Nothing new is proved here; it records the composition that the closed form is then read off from.

Theorem 1.5 (The conjecture).

$$\forall n\in \mathbb{N},\sum _{k\in \mathrm{Icc}\left(1,n\right)}\sum _{z\in \mathrm{Icc}\left(1,n\right)}\sum _{y\in \mathrm{Icc}\left(1,n\right)}\sum _{x\in \mathrm{Icc}\left(1,n\right)}[\gcd \left(|f\left(x,y,z\right)|,n\right)=k]f\left(x,y,z\right)=\frac{n^3\cdot n+1\cdot 2\cdot n+1}{6}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A373561.a373561 (✓ std3). ∎

Resolves. Problems/oeis-a373561-gcd-bucketed-quadruple-sum (proved) by D5/S3/Factorization/A373561.a373561.

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2024). OEIS A373561. URL: https://oeis.org/A373561.

Commentary.

The printed form divides by six, and division on the integers truncates, so the final step multiplies through by six instead and appeals to the standard square-sum formula. The statement holds for every natural n, the empty case included.

References

• Truth anchor: D5/S3/Factorization/A373561.a373561
• Truth anchor: D5/S3/Factorization/A373561.a373561_core
• Truth anchor: D5/S3/Factorization/A373561.f
• Truth anchor: D5/S3/Factorization/A373561.gcd_buckets_eq_sum
• Truth anchor: D5/S3/Factorization/A373561.triple_sum_eq