Carryless Pairing: Additive Pairing in the Fibonacci Basis

Resumo Técnico: Emparelhamento sem Transporte na Base de Fibonacci

Declaração do Problema
O artigo aborda a construção de uma função de emparelhamento $\pi: \mathbb{N}^2 \to \mathbb{N}$ que opera estritamente dentro das restrições aditivas da base de Zeckendorf (Fibonacci). Esquemas de emparelhamento tradicionais frequentemente dependem de intercalação posicional de dígitos (por exemplo, códigos Z-order/Morton) ou operações aritméticas envolvendo multiplicação e fatoração prima (por exemplo, numeração de Gödel, emparelhamento de Cantor). O autor busca um mecanismo onde a codificação e a decodificação de um par $(x, y)$ dependam exclusivamente da extração de suporte e de operações aditivas, evitando multiplicação, exponenciação e a necessidade de propagação de "transporte" ou etapas de normalização durante a combinação de dados. Isso é motivado pelo desejo de apoiar argumentos de incompletude e investigações teórico-prova em substratos aritméticos fracos (como $I\Delta_0$), onde a multiplicação não é assumida ou é custosa.

Metodologia
A solução proposta, denominada Emparelhamento sem Transporte ($\pi_{CL}$), codifica dois números naturais em "bandas" disjuntas de índices de Fibonacci baseadas em seus suportes de Zeckendorf.

1. Representação de Zeckendorf: Todo número natural $n$ é representado unicamente como uma soma de números de Fibonacci não consecutivos $F_k$ (onde $k \ge 2$). O conjunto de índices é denotado por $Z(n)$.
2. Construção do Delimitador: Para um par $(x, y)$, o algoritmo primeiro calcula o posto $r(x)$, definido como o menor índice tal que $F_{r(x)} > x$. Um delimitador $B(x)$ é definido como $2r(x)$.
3. Separação de Bandas:
   • Banda Par (para $x$): Os índices do suporte de $x$, $Z(x)$, são mapeados para índices pares via $e \mapsto 2e$. Estes são colocados no intervalo $[4, 2r(x))$.
   • Banda Ímpar (para $y$): Os índices do suporte de $y$, $Z(y)$, são mapeados para índices ímpares via $j \mapsto B(x) + (2j - 1)$. Estes são colocados estritamente acima do delimitador $B(x)$.
4. Invariante sem Transporte: Como $Z(x)$ não contém inteiros consecutivos, os índices pares mapeados possuem lacunas de pelo menos 4. Da mesma forma, os índices ímpares mapeados possuem lacunas de pelo menos 4. Crucialmente, o delimitador $B(x)$ garante que o maior índice par usado por $x$ seja estritamente menor que o menor índice ímpar usado por $y$. Consequentemente, a união desses dois conjuntos de índices não contém inteiros consecutivos.
5. Codificação: O valor codificado é a soma dos números de Fibonacci correspondentes à união desses índices. Como o suporte não contém índices consecutivos, o resultado está automaticamente na forma normal de Zeckendorf; nenhuma propagação de transporte é necessária.

Principais Contribuições

• Dispositivo Puramente Aditivo: O artigo define um mapa de emparelhamento $\pi_{CL}$ e um mapa de inversão unpair que operam exclusivamente em suportes de Zeckendorf usando adição e varreduras limitadas. Nenhuma multiplicação ou fatoração é utilizada.
• Injetividade e Decidibilidade: O mapa é provado ser injetivo. Embora não seja sobrejetivo, a pertinência à imagem é decidível via um "teste de ponto fixo": um número $n$ está na imagem se e somente se $\pi_{CL}(\text{unpair}(n)) = n$.
• Canonização em Um Passo: O artigo introduz uma função de canonização $can(n) = \pi_{CL}(\text{unpair}(n))$. Esta função mapeia qualquer número natural para seu representante único na imagem de $\pi_{CL}$ em um único passo.
• Lema de Estabilidade: O artigo estabelece que modificar a segunda coordenada $y$ (adicionando ou removendo um índice de seu suporte) resulta em uma mudança local no valor codificado (adicionando ou subtraindo um número de Fibonacci específico), desde que $x$ permaneça fixo.
• Mecanização: Todos os teoremas centrais de correção (inversão e injetividade) foram mecanizados em Rocq (anteriormente Coq), usando a linguagem de especificação Gallina. A formalização inclui provas da existência e unicidade dos suportes de Zeckendorf, garantindo que o dispositivo de emparelhamento não dependa de axiomas não provados relativos à interface de suporte.

Resultados

• Correção: O Teorema 6.0.1 prova que unpair $\circ$ $\pi_{CL}$ é a função identidade em $\mathbb{N}^2$.
• Não-Sobrejetividade: O mapa não é sobrejetivo; muitos números naturais (por exemplo, 6) não correspondem a pares válidos sob este esquema porque seus suportes de Zeckendorf não se alinham com as restrições específicas de paridade e delimitador.
• Complexidade: O custo do emparelhamento e desemparelhamento é dominado pela etapa de extração de suporte (tipicamente $O(r(n))$ para uma varredura gulosa). O artigo observa que estas são observações informais e não teoremas de complexidade certificados.
• Comparação: Diferentemente da numeração de Gödel (que requer fatoração) ou do emparelhamento de Cantor (que requer multiplicação e raízes quadradas), $\pi_{CL}$ opera puramente de forma aditiva. Diferentemente da ordem Z (que intercala posições binárias fixas), $\pi_{CL}$ desloca a posição do segundo operando com base no posto do primeiro, criando um delimitador dinâmico.

Significado e Alegações
O artigo posiciona esta construção como uma ferramenta para a matemática reversa e o estudo de substratos aritméticos fracos. Ao fornecer uma função de emparelhamento que evita a multiplicação, o autor sugere que ela pode ser útil para investigar argumentos de consistência e provabilidade em sistemas onde a multiplicação não está disponível ou é restrita (referenciando Buss, 1997; Friedman, 1976).

O autor declara explicitamente modéstia quanto a implicações mais amplas:

• O artigo não alega derivar a própria interface de suporte de Zeckendorf a partir de princípios de apenas adição, conjecturando que tal derivação pode não existir.
• Não alega uma caracterização simples em forma fechada da imagem de $\pi_{CL}$; o procedimento de decisão é o teste de ponto fixo baseado em suporte.
• A contribuição principal é a construção explícita de um dispositivo "sem transporte" e a verificação de suas propriedades, tornando a imagem e sua estrutura geométrica diretamente inspecionáveis para análise teórica.

O trabalho é apresentado como um dispositivo aritmético fundamental, e não como uma estrutura de dados prática para computação geral, enfatizando sua utilidade teórica na lógica e na teoria da prova.