Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: mbirika-spilker-gibonacci-power-gcd-normalization
bibkey: mbirikaspilker2022gibonaccipowers
doi: 10.1080/00150517.2022.12427444
url: https://arxiv.org/abs/2204.12626v2
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/GibonacciPowerGcdNormalization.result

Gibonacci power-window gcd normalization

Problem

Section 6.1, Question 6.2, PDF p. 14 of arXiv:2204.12626v2 asks:

Fix and set . Consider the two Gibonacci sequences and , where is generated by the relatively prime initial conditions and . Then the following identities holds:

; .

The first formula holds from Guyer-Mbirika [4, Theorem 19], while the second formula holds from Theorem 3.6 in this current paper. Will it be the case that for all ?

For every signed integer seed pair , every natural and every natural , let , and . Define the nonnegative gcd of the entire shift family by

With , the target is

The quotients are exact integers. Both gcds satisfy their divisibility iff for every integer divisor, including zero and negative divisors. Individual zero seeds, zero windows and odd exponents remain in scope.

Motivation

The paper gives the corresponding seed-content scaling for first and second powers and asks whether it persists for every higher power.

Gap

The printed question concerns the entire infinite shift family. A finite prefix, an exponent-three instance or a conditional gcd-existence premise would not discharge it.

Route

Linearity of Mathlib’s seeded recurrence gives termwise scaling by . Distributing powers and the finite window sum gives scaling by for every shift. The set-gcd universal property, cancellation by a positive scalar and nonnegative divisibility antisymmetry give scaling of the whole-family gcd. Exact integer quotients and normalized-seed gcd one are proved from the seed gcd.

Falsifier

A nonzero signed integer seed pair, a positive window length and a natural exponent at least three for which the two fully specified nonnegative infinite-family gcds violate the equality.

Evidence

The result declaration is D5/S1/Recurrence/GibonacciPowerGcdNormalization.result. Its conclusion includes , both exact seed reconstructions, coprime normalized seeds, both recurrences, both gcd nonnegativity assertions, both universal integer-divisor iff specifications and the whole scaling equality. The definitions use Mathlib’s Nat.setGcd on the full range of natural absolute window values. The axiom closure of every public declaration is contained in {Classical.choice, Quot.sound, propext}.

Triage

Proved: the whole assertion holds in the stated nonzero-pair domain. The mechanism is homogeneous scaling of the recurrence and the gcd universal property, with no parity restriction on the exponent or positivity restriction on individual terms. Proved: the private window-scaling identity also permits any natural exponent and length; the public result retains exactly the source exponent and length hypotheses. Proved: the generic gcd step applies to any integer family and any positive scalar. No new public generalization is asserted. This result supplies the normalization requested in Question 6.2; it does not supply a closed formula for the coprime-seed gcd or settle the separate Question 6.1. Open: further closed forms for the coprime-seed gcd and the separate Question 6.1 remain unresolved here.

ASSUMED-UNVERIFIED

The source correspondence and literature coverage are bounded readings, not a global openness or priority certificate. The later papers arXiv:2301.05758v3 and arXiv:2408.14632v2 and the targeted source and author searches did not yield a whole-question answer in the inspected passages. Spilker’s 2016 chapter was not inspected. The four-slot registration is unfinished, with the missing intervention, sensitivity, dependence and binding evidence described in issue #23012. That issue is not a validated registration or a mathematical premise.