Carryless Pairing: Additive Pairing in the Fibonacci Basis

Sintesi Tecnica: Accoppiamento Senza Riporto nella Base di Fibonacci

Enunciato del Problema
Il lavoro affronta la costruzione di una funzione di accoppiamento $\pi: \mathbb{N}^2 \to \mathbb{N}$ che operi strettamente all'interno dei vincoli additivi della base di Zeckendorf (Fibonacci). I tradizionali schemi di accoppiamento spesso si basano sull'interleaving posizionale delle cifre (ad esempio, codici Z-order/Morton) o su operazioni aritmetiche che coinvolgono moltiplicazione e fattorizzazione in primi (ad esempio, numerazione di Gödel, accoppiamento di Cantor). L'autore cerca un meccanismo in cui la codifica e la decodifica di una coppia $(x, y)$ dipendano esclusivamente dall'estrazione del supporto e da operazioni additive, evitando moltiplicazione, esponenziazione e la necessità di propagazione del "riporto" o di passaggi di normalizzazione durante la combinazione dei dati. Ciò è motivato dal desiderio di supportare argomenti di incompletezza e indagini proof-theoretic in substrati aritmetici deboli (come $I\Delta_0$) in cui la moltiplicazione non è assunta o è costosa.

Metodologia
La soluzione proposta, denominata Accoppiamento Senza Riporto ($\pi_{CL}$), codifica due numeri naturali in "bande" disgiunte di indici di Fibonacci basate sui loro supporti di Zeckendorf.

1. Rappresentazione di Zeckendorf: Ogni numero naturale $n$ è rappresentato in modo unico come somma di numeri di Fibonacci non consecutivi $F_k$ (dove $k \ge 2$). L'insieme degli indici è denotato $Z(n)$.
2. Costruzione del Delimitatore: Per una coppia $(x, y)$, l'algoritmo calcola prima il rango $r(x)$, definito come il più piccolo indice tale che $F_{r(x)} > x$. Un delimitatore $B(x)$ è impostato a $2r(x)$.
3. Separazione delle Bande:
   • Banda Pari (per $x$): Gli indici del supporto di $x$, $Z(x)$, sono mappati su indici pari tramite $e \mapsto 2e$. Questi sono collocati nell'intervallo $[4, 2r(x))$.
   • Banda Dispari (per $y$): Gli indici del supporto di $y$, $Z(y)$, sono mappati su indici dispari tramite $j \mapsto B(x) + (2j - 1)$. Questi sono collocati strettamente al di sopra del delimitatore $B(x)$.
4. Invariante Senza Riporto: Poiché $Z(x)$ non contiene interi consecutivi, gli indici pari mappati presentano spazi vuoti di almeno 4. Analogamente, gli indici dispari mappati presentano spazi vuoti di almeno 4. Crucialmente, il delimitatore $B(x)$ assicura che il più alto indice pari utilizzato da $x$ sia strettamente inferiore al più basso indice dispari utilizzato da $y$. Di conseguenza, l'unione di questi due insiemi di indici non contiene interi consecutivi.
5. Codifica: Il valore codificato è la somma dei numeri di Fibonacci corrispondenti all'unione di questi indici. Poiché il supporto non contiene indici consecutivi, il risultato è automaticamente in forma normale di Zeckendorf; non è richiesta alcuna propagazione del riporto.

Contributi Chiave

• Dispositivo Puramente Additivo: Il lavoro definisce una mappa di accoppiamento $\pi_{CL}$ e una mappa di inversione unpair che operano esclusivamente sui supporti di Zeckendorf utilizzando addizione e scansioni limitate. Non viene utilizzata alcuna moltiplicazione o fattorizzazione.
• Iniettività e Decidibilità: La mappa è dimostrata essere iniettiva. Sebbene non sia suriettiva, l'appartenenza all'immagine è decidibile tramite un "test del punto fisso": un numero $n$ è nell'immagine se e solo se $\pi_{CL}(\text{unpair}(n)) = n$.
• Canonicalizzazione in un Passo: Il lavoro introduce una funzione di canonicalizzazione $can(n) = \pi_{CL}(\text{unpair}(n))$. Questa funzione mappa qualsiasi numero naturale al suo unico rappresentante nell'immagine di $\pi_{CL}$ in un singolo passo.
• Lemma di Stabilità: Il lavoro stabilisce che modificare la seconda coordinata $y$ (aggiungendo o rimuovendo un indice dal suo supporto) comporta un cambiamento locale nel valore codificato (aggiungendo o sottraendo un specifico numero di Fibonacci), purché $x$ rimanga fisso.
• Meccanizzazione: Tutti i teoremi fondamentali di correttezza (inversione e iniettività) sono meccanizzati in Rocq (precedentemente Coq), utilizzando il linguaggio di specifica Gallina. La formalizzazione include dimostrazioni dell'esistenza e unicità dei supporti di Zeckendorf, garantendo che il dispositivo di accoppiamento non si basi su assiomi non dimostrati riguardanti l'interfaccia del supporto.

Risultati

• Correttezza: Il Teorema 6.0.1 dimostra che unpair $\circ$ $\pi_{CL}$ è la funzione identità su $\mathbb{N}^2$.
• Non-Suriettività: La mappa non è suriettiva; molti numeri naturali (ad esempio, 6) non corrispondono a coppie valide secondo questo schema perché i loro supporti di Zeckendorf non si allineano con i vincoli specifici di parità e delimitatore.
• Complessità: Il costo dell'accoppiamento e dell'acoppiamento inverso è dominato dal passo di estrazione del supporto (tipicamente $O(r(n))$ per una scansione greedy). Il lavoro nota che queste sono osservazioni informali piuttosto che teoremi di complessità certificati.
• Confronto: A differenza della numerazione di Gödel (che richiede fattorizzazione) o dell'accoppiamento di Cantor (che richiede moltiplicazione e radici quadrate), $\pi_{CL}$ opera puramente in modo additivo. A differenza dell'ordine Z (che interleava posizioni binarie fisse), $\pi_{CL}$ sposta la posizione del secondo operando in base al rango del primo, creando un delimitatore dinamico.

Significato e Affermazioni
Il lavoro posiziona questa costruzione come uno strumento per la matematica inversa e lo studio dei substrati aritmetici deboli. Fornendo una funzione di accoppiamento che evita la moltiplicazione, l'autore suggerisce che potrebbe essere utile per investigare argomenti di consistenza e dimostrabilità in sistemi in cui la moltiplicazione non è disponibile o è limitata (riferendosi a Buss, 1997; Friedman, 1976).

L'autore dichiara esplicitamente modestia riguardo alle implicazioni più ampie:

• Il lavoro non afferma di derivare l'interfaccia del supporto di Zeckendorf stessa da principi basati solo sull'addizione, ipotizzando che una tale derivazione potrebbe non esistere.
• Non afferma una caratterizzazione in forma chiusa semplice dell'immagine di $\pi_{CL}$; la procedura decisionale è il test del punto fisso basato sul supporto.
• Il contributo principale è la costruzione esplicita di un dispositivo "senza riporto" e la verifica delle sue proprietà, rendendo l'immagine e la sua struttura geometrica direttamente ispezionabili per l'analisi teorica.

Il lavoro è presentato come un dispositivo aritmetico fondazionale piuttosto che come una struttura dati pratica per l'informatica generale, sottolineando la sua utilità teorica nella logica e nella proof theory.