Carryless Pairing: Additive Pairing in the Fibonacci Basis

Technische Samenvatting: Draagvrije Koppeling in de Fibonacci-basis

Probleemstelling
Het artikel behandelt de constructie van een koppelingsfunctie $\pi: \mathbb{N}^2 \to \mathbb{N}$ die strikt binnen de additieve beperkingen van de Zeckendorf (Fibonacci)-basis opereert. Traditionele koppelingsmethoden vertrouwen vaak op positionele cijferverweving (bijvoorbeeld Z-order/Morton-codes) of rekenkundige bewerkingen met vermenigvuldiging en priemontbinding (bijvoorbeeld Gödel-nrmering, Cantor-koppeling). De auteur zoekt een mechanisme waarbij het coderen en decoderen van een paar $(x, y)$ uitsluitend afhankelijk is van het extraheren van ondersteuning en additieve bewerkingen, waarbij vermenigvuldiging, exponentiatie en de noodzaak van "draag"-propagatie of normalisatiestappen tijdens de combinatie van data worden vermeden. Dit wordt gemotiveerd door de wens om onvolledigheidsargumenten en bewijstheoretische onderzoeken in zwakke rekenkundige substraten (zoals $I\Delta_0$) te ondersteunen, waar vermenigvuldiging niet wordt verondersteld of kostbaar is.

Methodologie
De voorgestelde oplossing, genaamd Draagvrije Koppeling ($\pi_{CL}$), codeert twee natuurlijke getallen in disjuncte "banden" van Fibonacci-indices gebaseerd op hun Zeckendorf-ondersteuning.

1. Zeckendorf-Representatie: Elk natuurlijk getal $n$ wordt uniek weergegeven als een som van niet-consecutieve Fibonacci-getallen $F_k$ (waarbij $k \ge 2$). De verzameling indices wordt aangeduid als $Z(n)$.
2. Delimitorconstructie: Voor een paar $(x, y)$ berekent het algoritme eerst de rang $r(x)$, gedefinieerd als de kleinste index zodat $F_{r(x)} > x$. Een delimitor $B(x)$ wordt ingesteld op $2r(x)$.
3. Bandenscheiding:
   • Even Band (voor $x$): De indices van $x$'s ondersteuning, $Z(x)$, worden via $e \mapsto 2e$ afgebeeld op even indices. Deze worden geplaatst in het bereik $[4, 2r(x))$.
   • Oneven Band (voor $y$): De indices van $y$'s ondersteuning, $Z(y)$, worden via $j \mapsto B(x) + (2j - 1)$ afgebeeld op oneven indices. Deze worden strikt boven de delimitor $B(x)$ geplaatst.
4. Draagvrije Invariant: Omdat $Z(x)$ geen opeenvolgende gehele getallen bevat, hebben de afgebeelde even indices gaten van minimaal 4. Evenzo hebben de afgebeelde oneven indices gaten van minimaal 4. Cruciaal zorgt de delimitor $B(x)$ ervoor dat de hoogste even index die door $x$ wordt gebruikt, strikt kleiner is dan de laagste oneven index die door $y$ wordt gebruikt. Bijgevolg bevat de vereniging van deze twee verzamelingen indices geen opeenvolgende gehele getallen.
5. Codering: De gecodeerde waarde is de som van Fibonacci-getallen die overeenkomen met de vereniging van deze indices. Omdat de ondersteuning geen opeenvolgende indices bevat, is het resultaat automatisch in Zeckendorf-normaalvorm; er is geen draagpropagatie vereist.

Belangrijkste Bijdragen

• Volledig Additief Apparaat: Het artikel definieert een koppelingsafbeelding $\pi_{CL}$ en een inversieafbeelding unpair die uitsluitend opereren op Zeckendorf-ondersteuningen met behulp van optelling en begrenste scans. Er wordt geen vermenigvuldiging of ontbinding gebruikt.
• Injectiviteit en Beslisbaarheid: De afbeelding is bewezen injectief. Hoewel niet surjectief, is lidmaatschap van het beeld beslisbaar via een "vaste-punttest": een getal $n$ behoort tot het beeld dan en slechts dan als $\pi_{CL}(\text{unpair}(n)) = n$.
• Een-staps Canonicalisatie: Het artikel introduceert een canonicalisatiefunctie $can(n) = \pi_{CL}(\text{unpair}(n))$. Deze functie beeldt elk natuurlijk getal in één stap af op zijn unieke vertegenwoordiger in het beeld van $\pi_{CL}$.
• Stabiliteitslemma: Het artikel stelt vast dat het wijzigen van de tweede coördinaat $y$ (het toevoegen of verwijderen van een index uit zijn ondersteuning) resulteert in een lokale verandering van de gecodeerde waarde (het toevoegen of aftrekken van een specifiek Fibonacci-getal), mits $x$ constant blijft.
• Mechanisatie: Alle kerncorrectheidstheorema's (inversie en injectiviteit) zijn gemechaniseerd in Rocq (voorheen Coq), met gebruik van de Gallina specificatietaal. De formalisatie omvat bewijzen van het bestaan en de uniciteit van Zeckendorf-ondersteuningen, zodat het koppelingsapparaat niet afhankelijk is van onbewezen axioma's met betrekking tot de ondersteuningsinterface.

Resultaten

• Correctheid: Theorema 6.0.1 bewijst dat unpair $\circ$ $\pi_{CL}$ de identiteitsfunctie is op $\mathbb{N}^2$.
• Niet-surjectiviteit: De afbeelding is niet surjectief; veel natuurlijke getallen (bijvoorbeeld 6) corresponderen niet met geldige paren onder dit schema omdat hun Zeckendorf-ondersteuningen niet aligneren met de specifieke pariteits- en delimitorbeperkingen.
• Complexiteit: De kosten van koppelen en ontkoppelen worden gedomineerd door de stap voor het extraheren van ondersteuning (typisch $O(r(n))$ voor een greedige scan). Het artikel merkt op dat dit informele observaties zijn en geen gecertificeerde complexiteitstheorema's.
• Vergelijking: In tegenstelling tot Gödel-nrmering (die ontbinding vereist) of Cantor-koppeling (die vermenigvuldiging en vierkantswortels vereist), opereert $\pi_{CL}$ puur additief. In tegenstelling tot Z-order (die vaste binaire posities verweeft), verschuift $\pi_{CL}$ de positie van de tweede operand op basis van de rang van de eerste, waardoor een dynamische delimitor ontstaat.

Betekenis en Claims
Het artikel positioneert deze constructie als een hulpmiddel voor reverse wiskunde en het onderzoek naar zwakke rekenkundige substraten. Door een koppelingsfunctie te bieden die vermenigvuldiging vermijdt, suggereert de auteur dat deze nuttig kan zijn voor het onderzoeken van consistentieargumenten en bewijsbaarheid in systemen waar vermenigvuldiging niet beschikbaar is of beperkt is (verwijzend naar Buss, 1997; Friedman, 1976).

De auteur verklaart expliciet bescheidenheid met betrekking tot bredere implicaties:

• Het artikel claimt niet de Zeckendorf-ondersteuningsinterface zelf af te leiden uit alleen-optelling principes, en conjectureert dat een dergelijke afleiding mogelijk niet bestaat.
• Het claimt geen eenvoudige gesloten-vorm karakterisering van het beeld van $\pi_{CL}$; de beslissingsprocedure is de op ondersteuning gebaseerde vaste-punttest.
• De primaire bijdrage is de expliciete constructie van een "draagvrij" apparaat en de verificatie van zijn eigenschappen, waardoor het beeld en zijn geometrische structuur direct inspecteerbaar zijn voor theoretische analyse.

Het werk wordt gepresenteerd als een fundamenteel rekenkundig apparaat in plaats van een praktische datastructuur voor algemeen rekenen, met nadruk op zijn theoretische bruikbaarheid in logica en bewijstheorie.