Finite Zeckendorf Euler Identity

Abstract

Bounded Zeckendorf names enumerate an initial Fibonacci interval and its finite Euler sum.

Theorem 1.1 (Finite Zeckendorf names give the complete Fibonacci interval).

$$\begin{array}{c}\forall Q:\mathbb{N},\\ \text{let }{E}_Q:\mathrm{GoldenName}\left(Q\right)\to \mathrm{Fin}\left(\mathrm{Fib}\left(Q+2\right)\right):=(eta:\mathrm{GoldenName}\left(Q\right)\mapsto \sum _{k\in eta}\mathrm{Fib}\left(k\right));\\ \mathrm{Bijective}\left(E_Q\right)\wedge \\ \forall x:\mathbb{R},|x|<1\Rightarrow \\ \sum _{eta\in \mathrm{GoldenName}\left(Q\right)}{x}^{(E_Q(eta):\mathbb{N})}=\sum _{e\in \mathrm{Fin}\left(\mathrm{Fib}\left(Q+2\right)\right)}{x}^e\wedge \\ \sum _{e\in \mathrm{Fin}\left(\mathrm{Fib}\left(Q+2\right)\right)}{x}^e=\frac{1-x^{\mathrm{Fib}\left(Q+2\right)}}{1-x}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenCoding/FiniteZeckendorfEulerIdentity.finite_zeckendorf_interval_and_euler (✓ std3). ∎

Source. Repository-derived.

Commentary.

GoldenName(Q) is the canonical carrier of admissible occupied indices from two through Q+1. Thus Q=N-1 relative to the source notation, and the source endpoint Fib(N+1) is Fib(Q+2).

The displayed exponent is constructed directly by summing the occupied Fibonacci weights. The proof identifies this source-defined map with the inverse of the existing canonical golden-name equivalence.

Reindexing the finite sum through that equivalence gives the initial-interval sum. The source-wide bound |x|<1 supplies x != 1 for the quotient form of the finite geometric series.

References

• Truth anchor: D5/S3/Observer/GoldenCoding/FiniteZeckendorfEulerIdentity.finite_zeckendorf_interval_and_euler
• Dependency: D5/S0/Tower/GoldenNames