Constructive Encoding via ABCD

Constructive pairing and sequence encoding via prime powers, without importing set theory. Goedel numbering is a special case of the ABCD encoding (with C=1, D=1).

Constructive Encoding via ABCD

Summary

Constructive pairing and sequence encoding via prime powers, without importing set theory. Goedel numbering is a special case of the ABCD encoding (with C=1, D=1).

Statement

%
\label{cor:constructive-encoding}
The \textbf{constructive pairing} of two objects
$x, y \in \Obj(\tau)$ with indices
$\underline{m} = \mathrm{idx}(x)$
and $\underline{n} = \mathrm{idx}(y)$
is defined as:
\[
    \langle x, y \rangle_\tau
    \;:=\;
    \underline{p_1}^{\underline{m}} \cdot
    \underline{p_2}^{\underline{n}}
\]
where $\underline{p_1} < \underline{p_2}$ are the first two
primes of $\tau$-Idx
(i.e., $\underline{p_1} = \underline{2}$,
$\underline{p_2} = \underline{3}$).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 59
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part05/ch25-consequences.tex lines 49-67

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.Hyperfact
• Name: Tau.Coordinates.injectivity_check

Dependencies

• Canonical: I.T04

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.