Prueba inductiva de codificación de Fibonacci

Demostrar por inducción sobre$n$, que todo entero positivo tiene una representación de Fibonacci, como en la representación del código de Fibonacci .

Entonces, aunque entiendo la premisa detrás de la codificación de Fibonacci, y puedo ver que cada número entero positivo tendrá su propia representación única al tener en cuenta el hecho de que la longitud del código aumenta para cada número de Fibonacci que$n$pasa, permitiendo más combinaciones de 1 en la cadena resultante, de alguna manera tengo que relacionar esto con la diferencia entre dos números de Fibonacci consecutivos, y realmente estoy luchando para formalizar todo esto. Me parece bastante extraño en comparación con una prueba de inducción algebraica típica.

Como referencia, aquí hay un código de Python que genera la representación de Fibonacci de$n$.

def FibEncode(n):
  Fib = [0, 1]
  while Fib[-1] <= n:
    Fib += [Fib[-1] + Fib[-2]]
  Fib = Fib[:-1]
  rep = '1'
  for i in range(len(Fib) - 1, 1, -1):
    if Fib[i] <= n:
      rep = '1' + rep
      n = n - Fib[i]
    else:
      rep = '0' + rep
  return rep

for i in range(1, 15):
  print("i:", i, "\t|FibEncode(i):", FibEncode(i))

¿Cómo formalizarías todos los diferentes aspectos a los que tendrías que referirte para probar esto por inducción?

Editar:

Así que estoy un poco más cerca, pero todavía no estoy seguro de cómo proceder.

Denotar$F_a$como el$a^{th}$número de Fibonacci, y$G_n$como el número de números de Fibonacci menor o igual que$n$(contando$1$dos veces). Deseamos mostrar que$\forall n\in\mathbb{Z}^+\exists$una secuencia de$x_i$,$x_i\in\{0, 1\}, 2\le i\le G_n$tal que$n=\sum_{j=1}^{G_n-1}x_jF_{j+2}$.

Para$n=1,2,3$esos son solo números de Fibonacci, por lo que esos casos base son bastante simples.

Para$n=4$, entonces$x_1=1,x_2=0,x_3=1$lo que implica que$4=1*1+0*2+1*3$lo cual es cierto.

Así que ahora solo tengo que dar el paso inductivo, pero realmente no estoy seguro de cómo lo escribiría dada la forma en que lo he configurado hasta ahora.