pith. sign in

arxiv: 2509.10382 · v5 · submitted 2025-09-12 · 🧮 math.LO · cs.LO

Carryless Pairing: Additive Pairing in the Fibonacci Basis

Milan Rosko This is my paper

Pith reviewed 2026-05-18 17:29 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords carryless pairingZeckendorf representationFibonacci basispairing functioninjective mapsupport operationsRocq mechanization
0
0 comments X

The pith

A carryless pairing map encodes pairs of natural numbers into one by placing their Zeckendorf supports into two disjoint Fibonacci index bands separated by a delimiter from the first number.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper defines a pairing map π_CL from pairs of natural numbers to natural numbers by computing a delimiter from x and placing the Zeckendorf support of y in one band and of x in another, with the bands kept disjoint. The construction ensures the combined support has no consecutive indices, so the output is already in Zeckendorf normal form. Encoding and decoding use only additive operations on index supports, without multiplication, factorization, or digit interleaving. The map is injective but not surjective, and membership in its image is decidable by the same support checks used for inversion. Core correctness results on injectivity and decoding are formally mechanized in Rocq.

Core claim

The map π_CL is defined by computing a delimiter from x to separate two bands of indices; the Zeckendorf support of y is placed in the first band and the support of x in the second, producing a code whose index set has no consecutive elements and is therefore already Zeckendorf normal. The map is injective, and both evaluation and partial inversion are performed by support operations alone.

What carries the argument

The delimiter computed from x that separates the two bands of Zeckendorf indices, ensuring the combined support remains free of consecutive indices.

If this is right

  • Different input pairs always produce different outputs because the map is injective.
  • Decoding recovers x and y by locating the delimiter and reading the two separated supports.
  • Image membership can be decided by checking the band structure and delimiter without full inversion.
  • All steps remain within additive support manipulations on the Fibonacci indices.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The band-separation technique might extend to representations in other linear recurrence bases.
  • The additive-only operations could reduce computational cost in contexts where multiplication is restricted.
  • Formal mechanization in Rocq opens a path to verified pairing primitives inside proof assistants.

Load-bearing premise

The delimiter computed from x always produces two bands whose supports remain disjoint and free of consecutive indices after placement of y's Zeckendorf support.

What would settle it

An explicit pair x and y such that the index set of π_CL(x, y) contains at least one pair of consecutive Fibonacci numbers.

Figures

Figures reproduced from arXiv: 2509.10382 by Milan Rosko.

Figure 1
Figure 1. Figure 1: Additive Zeckendorf Composition avoids positional carries and is invertible in O(log n ) time by separating even and odd Fibonacci indices. Observation . The Incompleteness Theorems of Gödel [1931] are tradi￾tionally formalized using multiplicative encodings: sequences are represented by products of prime powers, substitution is implemented through exponent manipulation, and syntactic structure is recovere… view at source ↗
Figure 2
Figure 2. Figure 2: Gödel Numbering encodes syntactic structures into arithmetic form, while the inverse mapping exhibits superpolynomial complexity, reflecting the intrinsic compression of the encoding. Observation. The classical Gödel Numbering represents finite sequences by products of prime powers and recovers structure through divisibility and factorization, [PITH_FULL_IMAGE:figures/full_fig_p019_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Bit-Interleaving generates the characteristic Z-Order, providing a semantic ordering of multidimensional data for efficient indexing. Although computationally succinct, Morton Interleaving depends 19 [PITH_FULL_IMAGE:figures/full_fig_p019_3.png] view at source ↗
read the original abstract

We define a pairing map $\pi_{\mathsf{CL}} : \mathbb{N}^2\to\mathbb{N}$ that encodes $x$ and $y$ into two disjoint bands of Zeckendorf indices separated by a delimiter computed from $x$. The construction is "carryless" by design: the combined support has no consecutive indices, so each produced code is already in Zeckendorf-normal form, and both evaluation and inversion proceed by additive support operations alone, without multiplication, factorization, or positional digit interleaving. The map is injective not surjective, image membership is decidable by the same support machinery used for decoding. The core correctness theorems are mechanized in Rocq.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper defines a pairing map π_CL : ℕ² → ℕ that encodes x and y into two disjoint bands of Zeckendorf indices separated by a delimiter computed from x. The construction is carryless: the combined support has no consecutive indices, so each code is already in Zeckendorf form, and both evaluation and inversion use only additive support operations. The map is injective (not surjective), image membership is decidable via support operations, and the core correctness theorems are mechanized in Rocq.

Significance. If the mechanized results hold, the construction supplies a parameter-free, additive pairing function in the Fibonacci basis that avoids multiplication, factorization, and positional interleaving. The Rocq mechanization of injectivity and decoding provides independent, machine-checked evidence for the delimiter construction and the preservation of Zeckendorf normality, which strengthens the contribution for constructive mathematics and formal verification.

minor comments (2)
  1. [Abstract] Abstract: the description of the delimiter is high-level; a brief formula or pseudocode for its computation from x would improve immediate readability.
  2. The manuscript would benefit from a short worked example (e.g., π_CL(3,5)) showing the Zeckendorf supports, delimiter placement, and resulting code before the formal definitions.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the carryless pairing construction, the recognition of its significance for constructive mathematics and formal verification, and the recommendation for minor revision. No specific major comments were raised.

Circularity Check

0 steps flagged

No significant circularity: direct definition with mechanized Rocq proofs

full rationale

The paper defines π_CL directly via Zeckendorf supports, bands, and a delimiter computed from x, then states that injectivity, decoding correctness, and image-membership decidability are mechanized in Rocq. Mechanized proofs constitute independent evidence under the review criteria. No equation reduces the claimed properties to a fitted parameter, self-citation chain, or ansatz; the construction is self-contained and the central claims rest on the formal verification rather than on any internal renaming or load-bearing self-reference.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The construction rests on standard properties of the Zeckendorf representation and the existence of a delimiter that separates supports without creating consecutives; no free parameters or invented entities are introduced.

axioms (2)
  • standard math Every natural number has a unique Zeckendorf representation as a sum of non-consecutive Fibonacci numbers.
    Invoked to guarantee that supports can be manipulated additively while preserving normality.
  • domain assumption A delimiter position derived from x can always be chosen so that the supports of x and y remain disjoint and non-adjacent.
    This is the load-bearing premise that makes the carryless property hold for arbitrary x and y.

pith-pipeline@v0.9.0 · 5632 in / 1275 out tokens · 27855 ms · 2026-05-18T17:29:30.597188+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith/Constants.lean phi_golden_ratio echoes
    ?
    echoes

    ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

    every natural number admits a unique decomposition as a sum of non-consecutive Fibonacci numbers... Z(n) is finite and has no adjacent elements (Theorem 2.3, Definition 2.4)

  • IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel echoes
    ?
    echoes

    ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

    the combined support has no consecutive indices, so each produced code is already in Zeckendorf-normal form... π_CL is injective (Lemma 3.6, Theorem 3.7)

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

12 extracted references · 12 canonical work pages

  1. [1]

    Samuel R. Buss. Bounded Arithmetic. Bibliopolis, Naples, 1986. ISBN 88-7088-149-0. Ph.D. thesis published as a book; foundational for bounded arithmetic and _0 -definability

    work page 1986

  2. [2]

    Friedman

    Harvey M. Friedman. Some systems of second order arithmetic and their use. In Proceedings of the International Congress of Mathematicians, volume 1, pages 235--242, Vancouver, B.C., 1975. Canadian Mathematical Congress

    work page 1975

  3. [3]

    o del. \

    Kurt G \"o del. \"U ber formal unentscheidbare s \"a tze der principia mathematica und verwandter systeme i. Monatshefte f \"u r Mathematik und Physik , 38 0 (1): 0 173--198, 1931. doi:10.1007/BF01700692. Gödel's original incompleteness paper introducing Gödel numbering

    work page doi:10.1007/bf01700692 1931

  4. [4]

    On formally undecidable propositions of Principia Mathematica and related systems i

    Kurt G \"o del. On formally undecidable propositions of Principia Mathematica and related systems i. In Martin Davis, editor, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, pages 5--38. Raven Press, New York, 1965. English translation of Gödel's 1931 paper

    work page 1965

  5. [5]

    James P. Jones. Universal Diophantine equation. The Journal of Symbolic Logic, 47 0 (3): 0 549--571, 1982. doi:10.2307/2273588. Constructs a universal Diophantine equation of degree 4

    work page doi:10.2307/2273588 1982

  6. [6]

    C. G. Lekkerkerker. Voorstelling van natuurlijke getallen door een som van getallen van fibonacci. Zuivere Wiskunde, 1951

    work page 1951

  7. [7]

    Matiyasevich

    Yuri V. Matiyasevich. Enumerable sets are diophantine. Soviet Mathematics Doklady, 11: 0 354--358, 1970

    work page 1970

  8. [8]

    Characterizing integers among rational numbers with a universal-existential formula

    Bjorn Poonen. Characterizing integers among rational numbers with a universal-existential formula. American Journal of Mathematics, 131 0 (3): 0 675--682, 2009. doi:10.1353/ajm.0.0055. Discusses undecidability in number theory and Diophantine equations; relevant to degree bounds

    work page doi:10.1353/ajm.0.0055 2009

  9. [9]

    Robinson

    Raphael M. Robinson. An essentially undecidable axiom system. In Proceedings of the International Congress of Mathematicians, pages 729--730, Cambridge, Massachusetts, 1950. American Mathematical Society

    work page 1950

  10. [10]

    Barkley Rosser

    J. Barkley Rosser. Extensions of some theorems of G \"o del and Church . Journal of Symbolic Logic, 1 0 (3): 0 87--91, 1936

    work page 1936

  11. [11]

    Solomonoff

    Ray J. Solomonoff. A formal theory of inductive inference. part i. Information and Control, 7 0 (1): 0 1--22, 1964. doi:10.1016/S0019-9958(64)90223-2

    work page doi:10.1016/s0019-9958(64)90223-2 1964

  12. [12]

    Repr \'e sentation des nombres naturels par une somme de nombres de Fibonacci ou de nombres de Lucas

    Edouard Zeckendorf. Repr \'e sentation des nombres naturels par une somme de nombres de Fibonacci ou de nombres de Lucas . Bulletin de la Soci \'e t \'e Royale des Sciences de Li \`e ge , 41 0 (4-6): 0 179--182, 1972. Often cited for Zeckendorf's theorem on unique Fibonacci representations

    work page 1972