slug: garg-2019-fibonacci-prefix-antipowers bibkey: garg2021antipowers doi: 10.46298/dmtcs.7134 url: https://arxiv.org/abs/1907.10816v4 triage: theorem motivation_gids:

D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.result

Garg’s Fibonacci prefix antipower conjecture

Problem

Swapnil Garg, Antipowers in Uniform Morphic Words and the Fibonacci Word, arXiv:1907.10816v4, DMTCS 23(3), article 14, Conjecture 18, printed page 8:

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 $f$ .

The Fibonacci word is the fixed point starting with $0$ of $0 \mapsto 01$ , $1 \mapsto 0$ ; $F_{1} = F_{2} = 1$ . A $k$ -antipower consists of $k$ consecutive, pairwise distinct blocks of equal length. The source note quotes the definitions from §3 and the conjecture. Issue #14479 fixes the universal statement GARG-1: every $n \geq 1$ with $F_{n}$ even, $K = F_{n} - 1$ , $L = F_{n} /2 + F_{n - 1}$ , and the first $K$ blocks starting at $j L$ .

Motivation

D5/S1/Words/Antipowers/GargFibonacciPrefixAntipower.result : claim proves GARG-1. The literal finite-prefix convention is $S_{0} = [0]$ , $S_{1} = [0, 1]$ , $S_{k + 2} = S_{k + 1} S_{k}$ , with fibW their compatible diagonal limit. The proved fibW_bridge identifies this limit with the existing golden word, with Boolean true corresponding to letter $0$ . Blocks are functions Fin (blockLength n) → Fin 2; no extra hypothesis is imposed.

Gap

The preregistration records the source and literature checks: arXiv v4; MathDB’s Fibonacci prefix antipower conjecture entry with no solutions; Berger–Defant and Postic do not settle this exact prefix length. This is not-found-in-searched-scope, not a proof of absence of other literature. The source’s longest-gap estimate does not establish the proposed length: the sampled even-parity displacement is $5 δ$ , smaller than the coarse longest-gap scale $φ^{2} δ$ .

Route

The paper argument below gives the proof outline from the supplied proof, with $α = φ^{- 1}$ , $φ = (1 + 5) /2$ , $q = F_{n}$ , $p = F_{n - 1}$ , $δ = φ^{- n}$ , $s = (- 1)^{n}$ , $H = q /2$ , and $L = H + p$ .

Cylinder coding. Fact 14 gives $f (t) = 1 - (⌊(t + 2) α ⌋ - ⌊(t + 1) α ⌋)$ . For a length- $m$ factor beginning at $a$ , put $x = {(a + 1) α}$ . Telescoping gives $k - \sum_{t < k} f (a + t) = ⌊ x + k α ⌋$ . Successive differences recover the letters. Since $α$ is irrational, $⌊ x + k α ⌋ = ⌊ k α ⌋ + 1_{x \geq {- k α}}$ . Thus factor equality is equality of the cells cut by ${- k α}$ , $1 \leq k \leq m$ , with cuts assigned to their right cell. The proof uses the frozen golden_factor_eq_iff_cylinder_rank_eq.
Binet sampling. The Lean helpers residual, binet_residual, sampling_identity and sampling_phase establish $q α = p - sδ$ , $q 5 δ = 1 - s δ^{2}$ and $Lα = M + 1/2 + s 5 δ /2$ , where $M = F_{n - 2} + (p - 1) /2$ is an integer. The scaled sampled phase is congruent modulo $q$ to $X_{j} = p + j H + s j /2 + e_{j}$ , $e_{j} = - sδ - j δ^{2} /2$ .
Bounds. For $n \geq 9$ , large_bounds proves $0 < δ < 1/50$ , $B = q δ < 9/20$ , $A = δ + q δ^{2} /2 < 49/2000$ ; hence $A + B < 1/2$ . These follow from $φ > 8/5$ , $5 > 223/100$ and Binet.
Actual cuts. Coprimality lets $k_{r} \in {0, \dots, q - 1}$ solve $- k_{r} p \equiv r (mod q)$ . Set $C_{r} = r + s k_{r} δ$ . Then $C_{r + q} = C_{r} + q$ , $C_{0} = 0$ , $C_{q} = q$ , and the cuts strictly increase. C_endpoint proves $C_{r} / q \in$ goldenCylinderEndpointSet (q-1) for $0 < r < q$ . This is the new cut construction on the active proof path.
Parity cells. For $s = 1$ , the labels are $R_{2 h} = p + h - 1$ , $R_{2 h + 1} = p + H + h$ ; for $s = - 1$ , $R_{2 h} = p - h$ , $R_{2 h + 1} = p + H - h - 1$ . sample_in_lifted_cell places each reduced phase strictly between $C_{R_{j}}$ and $C_{R_{j} + 1}$ . The bounds in step 3 separate both parity classes. labels_injective_mod proves that distinct $j < q - 1$ have distinct labels modulo $q$ . Together these give golden_sample_grid_rank_injective.
Block distinction. large_distinct supplies distinct length- $(q - 1)$ factors. Since $L \geq q - 1$ , equality of the full blocks would imply equality of these prefixes. For $n < 9$ , the even Fibonacci cases are $n = 3, 6$ : one block at $n = 3$ ; the seven length- $9$ blocks at $n = 6$ are checked locally inside result by Lean. This covers every admissible $n$ .

The seven length- $9$ blocks at $n = 6$ are $010010100$ , $100101001$ , $010010010$ , $100100101$ , $001010010$ , $010100101$ , $001001010$ .

Falsifier

A collision between two distinct indices $i, j < F_{n} - 1$ at the prescribed length, with $n \geq 1$ and $F_{n}$ even, would refute GARG-1. The Lean theorem excludes such a collision under the literal word convention. A failure of the stronger $F_{n}$ -block statement is a sharpness observation, not a counterexample to GARG-1.

Evidence

The two modules provide the general sample-grid construction and the universal settling theorem. The axiom closure of every public declaration is contained in ${propext, Classical.choice, Quot.sound}$ . The Scribe attaches OpenProblemResolutionClaim with resolution Proved to the settling result. No digestion atom or coverage assertion is involved. The finite computations below corroborate the proof in their stated scope; they are not its universal proof.

Triage

What the settlement shows

Target item	Status	Evidence and boundary
Mechanism	proved in Lean	`C_endpoint`, `golden_sample_grid_rank_injective`, `sampling_identity`, `sampling_phase`, `large_distinct` and `result`: Binet sampling and disjoint parity cells, rather than a longest-gap estimate.
Consequence	proved by paper argument	The following subsequence argument proves $lim inf_{k} γ_{0} (k) / k \leq 5 /2$ . It is not an additional Lean theorem.
Sharpness	computed through $n \leq 21$ ; uniform extension open	The script below finds $F_{n}$ blocks distinct at $n = 3$ , and the collision $(0, F_{n} - 1)$ at $n = 6, 9, 12, 15, 18, 21$ .
Generalisation	open for other Sturmian slopes	The supporting Lean theorem permits arbitrary coprime $p, q$ , positive even $q$ , and its explicit signed golden-slope residual bounds. It retains the golden slope; changing the slope requires a new coding and cut bridge.

Consequence, paper argument. Write $γ_{0} (k)$ for the least block length of a prefix $k$ -antipower. For $n = 3 r$ , Fibonacci parity gives even $F_{n}$ , and $K_{r} = F_{3 r} - 1 \to \infty$ . The theorem gives $γ_{0} (K_{r}) \leq L_{r}$ . Binet yields $F_{n - 1} / F_{n} \to φ^{- 1}$ , so $L_{r} / K_{r} \to 1/2 + φ^{- 1} = 5 /2$ . Taking the liminf along this unbounded subsequence proves the stated upper bound. The source’s Sturmian complexity argument gives the lower bound $1$ . The source’s other propositions remain applicable under their original hypotheses; the conditional prefix liminf remark following Conjecture 18 therefore has its premise discharged. The general all-start bounds are not strengthened by this prefix-only settlement.

Scope and sharpness. For $n \geq 9$ , large_distinct proves the stronger fact that the first $F_{n} - 1$ letters already distinguish the sampled blocks. The collision at the next block is a computation for the listed indices; no uniform collision theorem is claimed. Other Sturmian slopes and optimal prefix block lengths remain open follow-up questions.

Prefix computation

The orchestrator’s check is reproduced verbatim below. Command python3 /tmp/op-garg/check.py, exit $0$ , SHA-256 7e48fc0d01b338691ccddb2633e42c85965acba18ed018879b052275bc363172. A reader can save the block as check.py and run python3 check.py. It tests exactly the even Fibonacci indices $n = 3, 6, 9, 12, 15, 18, 21$ ; all $F_{n} - 1$ prescribed blocks are distinct. The $(F_{n}, K, L)$ values are $(2, 1, 2)$ , $(8, 7, 9)$ , $(34, 33, 38)$ , $(144, 143, 161)$ , $(610, 609, 682)$ , $(2584, 2583, 2889)$ , $(10946, 10945, 12238)$ .

import sys
# Fibonacci word f = phi^omega(0), phi(0)=01, phi(1)=0
a,b=b'0',b'01'
while len(b)<160_000_000: a,b=b,b+a
f=b
F=[0,1,1]
while len(F)<30: F.append(F[-1]+F[-2])
res={}
for n in range(3,22):
    if F[n]%2: continue
    K=F[n]-1; L=F[n]//2+F[n-1]
    assert K*L<=len(f)
    blocks=set(f[j*L:(j+1)*L] for j in range(K))
    res[n]=(F[n],K,L,len(blocks)==K)
    print(n,res[n],flush=True)

Sharpness computation

Command python3 /tmp/op-garg/stage-b/sharpness.py, exit $0$ , SHA-256 ff7d35868595a80ecb17bc73383a977ef4a68787103063ea83891b46a9116a99. Save the following source as sharpness.py to rerun with python3 sharpness.py. It compares all $F_{n}$ prefix blocks in the same index range and reports the first collision. The resulting scope and status are exactly those in the Triage table.

import json
from pathlib import Path
F=[0,1]
for n in range(2,22):F.append(F[-1]+F[-2])
need=max(F[n]*(F[n]//2+F[n-1]) for n in range(1,22) if F[n]%2==0)
a,b=b'0',b'01'
while len(b)<need:a,b=b,b+a
rows=[]
for n in range(1,22):
 if F[n]%2:continue
 q=F[n];L=q//2+F[n-1];seen={};collision=None
 for j in range(q):
  block=b[j*L:(j+1)*L]
  if block in seen:
   collision=[seen[block],j];break
  seen[block]=j
 row=dict(n=n,F=q,L=L,F_blocks_distinct=collision is None,first_collision=collision)
 rows.append(row);print(json.dumps(row),flush=True)

ASSUMED-UNVERIFIED

The external literature gap is bounded by the searches recorded in #14479; absence of a result outside that scope is unverified. The liminf consequence has a paper argument here, with no separate kernel-checked limit theorem. Uniform $F_{n}$ -block sharpness and extensions to other Sturmian slopes are open.

Keyboard shortcuts

trureturing — Discovering truth