Garg’s Fibonacci Prefix Antipower

Abstract

The first F_n−1 blocks of length F_n/2+F_{n−1} in the Fibonacci word are distinct whenever F_n is even.

Definition 1.1 (Binary letters).

$$\forall b\in \mathrm{Bool}\left(\right),\mathrm{digit}\left(b\right)=\mathrm{if}b\mathrm{then}0\mathrm{else}1$$

Formalization. D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.digit (✓ std3).

Source. Repository-derived.

Acknowledgement. Swapnil Garg (2021). Antipowers in Uniform Morphic Words and the Fibonacci Word. DOI: 10.46298/dmtcs.7134. URL: https://arxiv.org/abs/1907.10816v4.

Commentary.

Boolean true in goldenWord denotes the source’s letter 0; false denotes 1. The binary alphabet is Fin 2.

Definition 1.2 (Finite Fibonacci prefixes).

$$\begin{array}{r}S\left(0\right)=[0]\\ S\left(1\right)=[0,1]\\ \forall n\in \mathbb{N},S\left(n+2\right)=S\left(n+1\right)++S\left(n\right)\end{array}$$

Formalization. D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.S (✓ std3).

Citation. Swapnil Garg (2021). Antipowers in Uniform Morphic Words and the Fibonacci Word. DOI: 10.46298/dmtcs.7134. URL: https://arxiv.org/abs/1907.10816v4.

Commentary.

Source definition (§3, printed page 5), verbatim: “We prove that the Fibonacci word $\mathbf{f}$, which is equal to ${\phi }^{\omega }(0)$ for $\phi (0)=01$, $\phi (1)=0$ and thus pure morphic but not generated by a uniform morphism, also satisfies Conjecture 3.”

The Fibonacci word begins with 0 and is fixed by the morphism 0 ↦ 01, 1 ↦ 0. The recursive prefixes begin [0] and [0,1], followed by concatenation of the previous two prefixes in that order. The plus-plus symbol is List append.

Definition 1.3 (Infinite Fibonacci word).

$$\forall i\in \mathbb{N},\mathrm{fibW}\left(i\right)=(S\left(i\right))[i]$$

Formalization. D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.fibW (✓ std3).

Citation. Swapnil Garg (2021). Antipowers in Uniform Morphic Words and the Fibonacci Word. DOI: 10.46298/dmtcs.7134. URL: https://arxiv.org/abs/1907.10816v4.

Commentary.

Source definition (§3, printed page 5), verbatim: “We prove that the Fibonacci word $\mathbf{f}$, which is equal to ${\phi }^{\omega }(0)$ for $\phi (0)=01$, $\phi (1)=0$ and thus pure morphic but not generated by a uniform morphism, also satisfies Conjecture 3.”

The ith letter is read from prefix S(i). These prefixes are compatible, and their lengths exceed i. List indexing includes the proved bound. The proof identifies this limit with digit(goldenWord(i)), so the source’s initial letter and letter correspondence are preserved.

Definition 1.4 (The specified block length).

$$\forall n\in \mathbb{N},\mathrm{blockLength}\left(n\right)=\mathrm{Nat}.\mathrm{div}\left(\mathrm{Nat}.\mathrm{fib}\left(n\right),2\right)+\mathrm{Nat}.\mathrm{fib}\left(n-1\right)$$

Formalization. D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.blockLength (✓ std3).

Citation. Swapnil Garg (2021). Antipowers in Uniform Morphic Words and the Fibonacci Word. DOI: 10.46298/dmtcs.7134. URL: https://arxiv.org/abs/1907.10816v4.

Commentary.

Conjecture 18 (printed page 8), verbatim: “Let $F_n$ be an even Fibonacci number. Then, there is an $(F_n-1)$-antipower with block length $\frac{F_n}{2}+F_{n-1}$ that is a prefix of $\mathbf{f}$.”

Nat.fib has F_0=0 and F_1=F_2=1. Nat.div denotes floor division on naturals; it is exact division by 2 for the even Fibonacci numbers in the claim. Natural subtraction is truncated subtraction.

Definition 1.5 (Conjecture 18).

$$(\mathrm{claim}\left(\right))\iff (\forall n\in \mathbb{N},\forall i\in \mathbb{N},\forall j\in \mathbb{N},((1\le n)\wedge \left((\mathrm{Even}\left(\mathrm{Nat}.\mathrm{fib}\left(n\right)\right))\wedge \left((i<\mathrm{Nat}.\mathrm{fib}\left(n\right)-1)\wedge \left((j<\mathrm{Nat}.\mathrm{fib}\left(n\right)-1)\wedge (i\ne j)\right)\right)\right))\Rightarrow ((\mathrm{fun}(t:\mathrm{Fin}\left(\mathrm{blockLength}\left(n\right)\right))\mapsto \mathrm{fibW}\left(i\cdot \mathrm{blockLength}\left(n\right)+\mathrm{val}\left(t\right)\right))\ne (\mathrm{fun}(t:\mathrm{Fin}\left(\mathrm{blockLength}\left(n\right)\right))\mapsto \mathrm{fibW}\left(j\cdot \mathrm{blockLength}\left(n\right)+\mathrm{val}\left(t\right)\right))))$$

Formalization. D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.claim (✓ std3).

Citation. Swapnil Garg (2021). Antipowers in Uniform Morphic Words and the Fibonacci Word. DOI: 10.46298/dmtcs.7134. URL: https://arxiv.org/abs/1907.10816v4.

Commentary.

Conjecture 18 (printed page 8), verbatim: “Let $F_n$ be an even Fibonacci number. Then, there is an $(F_n-1)$-antipower with block length $\frac{F_n}{2}+F_{n-1}$ that is a prefix of $\mathbf{f}$.”

Source definition (printed page 1), verbatim: “Fici, Restivo, Silva, and Zamboni define a $k$-antipower to be a word composed of $k$ pairwise distinct, concatenated words of equal length.”

For every n ≥ 1 with Nat.fib(n) even, the indices i and j range over the first Nat.fib(n)−1 blocks. Each block is a function Fin(blockLength(n)) → Fin 2, starting at index i·blockLength(n) or j·blockLength(n). Distinct indices give distinct functions. Thus the concatenation is a prefix antipower.

Theorem 1.6 (The prefix antipower exists).

$$\mathrm{claim}\left(\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.result (✓ std3). ∎

Resolves. Problems/garg-2019-fibonacci-prefix-antipowers (proved) by D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.result.

Source. Repository-derived.

Acknowledgement. Swapnil Garg (2021). Antipowers in Uniform Morphic Words and the Fibonacci Word. DOI: 10.46298/dmtcs.7134. URL: https://arxiv.org/abs/1907.10816v4.

Commentary.

Binet’s identities put the sampled phases in a perturbed half-integer grid. The two parity classes occupy distinct golden cylinder cells. Equality of length-L blocks would imply equality of their length-(F_n−1) prefixes, contradicting the cylinder ranks. The n=3 case has one block; n=6 is checked directly within the proof. The remaining even Fibonacci numbers satisfy the strict residual bounds of the general sample-grid theorem.

References

• Truth anchor: D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.S
• Truth anchor: D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.blockLength
• Truth anchor: D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.claim
• Truth anchor: D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.digit
• Truth anchor: D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.fibW
• Truth anchor: D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.result
• Dependency: D5/S1/Words/Antipowers/PerturbedGoldenSampleGrid