The Alternating Binomial Sum of OEIS A385590

Abstract

The Fibonacci triangle satisfies the alternating binomial sum in OEIS A385590.

Werner Schulte’s OEIS entry, dated July 3, 2025, states the sum as a conjecture. The statement and triangle are from that entry; the proof below is derived in this repository. The other conjecture in the entry, that the triangle permutes the natural numbers, is a separate question.

All indices are natural numbers, F is the Fibonacci sequence with F(0)=0 and F(1)=1, and g(n) denotes Nat.greatestFib(n). Subtraction inside an index of F or a binomial coefficient is natural subtraction. The triangle values, their differences, products, and sums are integers. The remainder in A is the natural remainder modulo two.

Definition 1.1 (The triangle and its row constants).

$$\begin{array}{r}\forall n,k:\mathbb{N},T\left(n,k\right)=A\left(n,g\left(n\right)\right)+\left(k-1\right)\cdot B\left(g\left(n\right)\right)\\ \forall n,i:\mathbb{N},A\left(n,i\right)=F{\left(i-1\right)}^2+1-\left(i-1\right)\mathrm{mod}2+\left(n-F\left(i\right)\right)\cdot F\left(i-2\right)\\ \forall i:\mathbb{N},B\left(i\right)=F\left(i-1\right)\end{array}$$

Formalization. D5/S1/Recurrence/Parity/A385590.T (✓ std3).

Citation. Werner Schulte (2025). OEIS A385590, a triangle based on Fibonacci numbers. URL: https://oeis.org/A385590.

Commentary.

The lower Fibonacci inverse g chooses the row’s interval. Its constant term A and slope B depend on n and i, and neither depends on k.

Lemma 1.2 (The unique Fibonacci interval).

$$\begin{array}{r}\forall n:\mathbb{N},1\le n⟹\\ 1<g\left(n\right)\wedge F\left(g\left(n\right)\right)\le n\wedge n<F\left(g\left(n\right)+1\right)\wedge \\ (\forall i:\mathbb{N},1<i⟹F\left(i\right)\le n⟹n<F\left(i+1\right)⟹i=g\left(n\right))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/A385590.row_index_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s greatestFib inequalities give the two interval bounds. Any other index satisfying them is both at most g(n) and greater than g(n)-1, so it equals g(n). For n at least one, g(n) is at least two.

Lemma 1.3 (Each row is affine).

$$\forall n,k,i:\mathbb{N},i=g\left(n\right)⟹T\left(n,k\right)=A\left(n,i\right)+\left(k-1\right)\cdot B\left(i\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/A385590.row_affine (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Werner Schulte (2025). OEIS A385590, a triangle based on Fibonacci numbers. URL: https://oeis.org/A385590.

Commentary.

Substitution of the fixed row index gives the displayed affine expression with the explicit A and B above.

Theorem 1.4 (The full conjectured sum).

$$\begin{array}{r}\forall n:\mathbb{N},1\le n⟹\\ \sum _{k\in \mathrm{Icc}\left(1,n\right)}((-1{)}^k\cdot \mathrm{choose}\left(n-1,k-1\right)\cdot T\left(n,k\right))=\\ \mathrm{if}n<3\mathrm{then}(-1{)}^n\mathrm{else}0\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/A385590.alternating_binomial_sum (✓ std3). ∎

Resolves. Problems/oeis-a385590-alternating-binomial (proved) by D5/S1/Recurrence/Parity/A385590.alternating_binomial_sum.

Source. Repository-derived.

Acknowledgement. Werner Schulte (2025). OEIS A385590, a triangle based on Fibonacci numbers. URL: https://oeis.org/A385590.

Commentary.

Put m=n-1 and j=k-1. The sum becomes the negative of the alternating binomial transform of A+jB. For m at least two, the constant moment is zero by Mathlib’s alternating_sum_range_choose_of_ne. The identity (j+1) choose(m,j+1) = m choose(m-1,j) reduces the linear moment to another such zero sum. The first row is [1] and the second is [2,3], giving -1 and 1 respectively. This proves the assertion for every positive n.

References

• Truth anchor: D5/S1/Recurrence/Parity/A385590.T
• Truth anchor: D5/S1/Recurrence/Parity/A385590.alternating_binomial_sum
• Truth anchor: D5/S1/Recurrence/Parity/A385590.row_affine
• Truth anchor: D5/S1/Recurrence/Parity/A385590.row_index_spec