Gibonacci Power-Window GCD Normalization

Abstract

Integer seed content scales the gcd of all shifted power windows by its exponent.

Mbirika and Spilker’s Question 6.2 concerns the gcd of infinitely many finite power sums. The seeds are arbitrary signed integers except for the pair (0,0); either individual seed may vanish. The window length is any positive natural number, and every natural exponent at least three is included.

Definition 1.1 (The seeded integer recurrence).

$$\forall a:\mathbb{Z},\forall b:\mathbb{Z},\left(\mathrm{gibonacci}\left(a,b\right):\left(\mathbb{N}\to \mathbb{Z}\right)\right)=\mathrm{mkSol}\left(fibRecZ,[a,b]\right)$$

Formalization. D5/S1/Recurrence/GibonacciPowerGcdNormalization.gibonacci (✓ std3).

Source. Repository-derived.

Acknowledgement. aBa Mbirika; Jürgen Spilker (2022). GCD of sums of k consecutive squares of generalized Fibonacci numbers. DOI: 10.1080/00150517.2022.12427444. URL: https://arxiv.org/abs/2204.12626v2.

Commentary.

Here fibRecZ is Mathlib’s order-two linear recurrence over the integers with coefficients (1,1), and mkSol assigns its unique solution to the initial vector (a,b). Thus the sequence starts at indices zero and one, with the recurrence G(n+2)=G(n+1)+G(n).

Definition 1.2 (The exact source window).

$$\forall a:\mathbb{Z},\forall b:\mathbb{Z},\forall k:\mathbb{N},\forall e:\mathbb{N},\forall t:\mathbb{N},\mathrm{windowSum}\left(a,b,k,e,t\right)=\sum _{i=1}^k\mathrm{gibonacci}{\left(a,b,t+i\right)}^e$$

Formalization. D5/S1/Recurrence/GibonacciPowerGcdNormalization.windowSum (✓ std3).

Source. Repository-derived.

Acknowledgement. aBa Mbirika; Jürgen Spilker (2022). GCD of sums of k consecutive squares of generalized Fibonacci numbers. DOI: 10.1080/00150517.2022.12427444. URL: https://arxiv.org/abs/2204.12626v2.

Commentary.

The endpoints are inclusive: the terms have indices t+1 through t+k. The definition also permits k=0 and any natural exponent; the theorem uses the positive lengths and exponents at least three of the source question.

Definition 1.3 (The nonnegative gcd of a whole integer family).

$$\forall f:\mathbb{N}\to \mathbb{Z},\mathrm{familyGcd}\left(f\right)=\mathrm{IntCast}\left(\mathrm{NatSetGcd}\left(\{\mathrm{natAbs}\left(f\left(t\right)\right)\mid t\in \mathbb{N}\}\right)\right)$$

Formalization. D5/S1/Recurrence/GibonacciPowerGcdNormalization.familyGcd (✓ std3).

Source. Repository-derived.

Acknowledgement. aBa Mbirika; Jürgen Spilker (2022). GCD of sums of k consecutive squares of generalized Fibonacci numbers. DOI: 10.1080/00150517.2022.12427444. URL: https://arxiv.org/abs/2204.12626v2.

Commentary.

NatSetGcd denotes Mathlib’s Nat.setGcd. It is applied to the full range of natural absolute values and cast to the integers. Its universal divisibility property includes every integer divisor, including zero and negative divisors. No finite prefix or nonzero-family assumption enters this definition.

Definition 1.4 (The infinite power-window gcd).

$$\forall a:\mathbb{Z},\forall b:\mathbb{Z},\forall k:\mathbb{N},\forall e:\mathbb{N},\mathrm{powerGcd}\left(a,b,k,e\right)=\mathrm{familyGcd}\left((t:\mathbb{N})\mapsto \mathrm{windowSum}\left(a,b,k,e,t\right)\right)$$

Formalization. D5/S1/Recurrence/GibonacciPowerGcdNormalization.powerGcd (✓ std3).

Source. Repository-derived.

Acknowledgement. aBa Mbirika; Jürgen Spilker (2022). GCD of sums of k consecutive squares of generalized Fibonacci numbers. DOI: 10.1080/00150517.2022.12427444. URL: https://arxiv.org/abs/2204.12626v2.

Commentary.

This family ranges over every natural shift, starting at zero. In particular, zero-valued windows and windows of odd powers of signed terms are included.

Theorem 1.5 (Normalization by the gcd of the seeds).

$$\forall a:\mathbb{Z},\forall b:\mathbb{Z},\left(\left(a\ne 0\right)\vee \left(b\ne 0\right)\right)\Rightarrow \left(\forall k:\mathbb{N},\left(1\le k\right)\Rightarrow \left(\forall e:\mathbb{N},\left(3\le e\right)\Rightarrow \left(\forall d:\mathbb{Z},\left(d=\mathrm{IntCast}\left(\gcd \left(a,b\right)\right)\right)\Rightarrow \left(\left(0<d\right)\wedge \left(d\cdot \mathrm{ediv}\left(a,d\right)=a\right)\wedge \left(d\cdot \mathrm{ediv}\left(b,d\right)=b\right)\wedge \left(\gcd \left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right)\right)=1\right)\wedge \left(\left(\mathrm{gibonacci}\left(a,b,0\right)=a\right)\wedge \left(\mathrm{gibonacci}\left(a,b,1\right)=b\right)\wedge \left(\forall n:\mathbb{N},\mathrm{gibonacci}\left(a,b,n+2\right)=\mathrm{gibonacci}\left(a,b,n+1\right)+\mathrm{gibonacci}\left(a,b,n\right)\right)\right)\wedge \left(\left(\mathrm{gibonacci}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),0\right)=\mathrm{ediv}\left(a,d\right)\right)\wedge \left(\mathrm{gibonacci}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),1\right)=\mathrm{ediv}\left(b,d\right)\right)\wedge \left(\forall n:\mathbb{N},\mathrm{gibonacci}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),n+2\right)=\mathrm{gibonacci}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),n+1\right)+\mathrm{gibonacci}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),n\right)\right)\right)\wedge \left(0\le \mathrm{powerGcd}\left(a,b,k,e\right)\right)\wedge \left(0\le \mathrm{powerGcd}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),k,e\right)\right)\wedge \left(\forall r:\mathbb{Z},\left(r\mid \mathrm{powerGcd}\left(a,b,k,e\right)\right)⟺\left(\forall t:\mathbb{N},r\mid \mathrm{windowSum}\left(a,b,k,e,t\right)\right)\right)\wedge \left(\forall r:\mathbb{Z},\left(r\mid \mathrm{powerGcd}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),k,e\right)\right)⟺\left(\forall t:\mathbb{N},r\mid \mathrm{windowSum}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),k,e,t\right)\right)\right)\wedge \left(\mathrm{powerGcd}\left(a,b,k,e\right)=d^e\cdot \mathrm{powerGcd}\left(\mathrm{ediv}\left(a,d\right),\mathrm{ediv}\left(b,d\right),k,e\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/GibonacciPowerGcdNormalization.result (✓ std3). ∎

Resolves. Problems/mbirika-spilker-gibonacci-power-gcd-normalization (proved) by D5/S1/Recurrence/GibonacciPowerGcdNormalization.result.

Source. Repository-derived.

Acknowledgement. aBa Mbirika; Jürgen Spilker (2022). GCD of sums of k consecutive squares of generalized Fibonacci numbers. DOI: 10.1080/00150517.2022.12427444. URL: https://arxiv.org/abs/2204.12626v2.

Commentary.

The symbol ediv is integer division, and d is the integer cast of the natural gcd of the seeds. The reconstruction equalities prove that both quotients are exact; their gcd is one. Both recurrences, both nonnegativity assertions and both all-integer-divisor specifications are part of the conclusion. The proof uses LinearRecurrence.toInit to scale the entire seeded solution, then mul_pow and Finset.mul_sum to scale each window. Nat.dvd_setGcd_iff and Int.natAbs_dvd_natAbs characterize the infinite gcd. Divisibility antisymmetry and cancellation by the positive scalar d raised to e give the displayed equality. These are applications of general Mathlib algebra to the source question; no assertion of literature priority is made.

References

• Truth anchor: D5/S1/Recurrence/GibonacciPowerGcdNormalization.familyGcd
• Truth anchor: D5/S1/Recurrence/GibonacciPowerGcdNormalization.gibonacci
• Truth anchor: D5/S1/Recurrence/GibonacciPowerGcdNormalization.powerGcd
• Truth anchor: D5/S1/Recurrence/GibonacciPowerGcdNormalization.result
• Truth anchor: D5/S1/Recurrence/GibonacciPowerGcdNormalization.windowSum