Manuscript Oai279-A@1 · Oai279-A.tex · section · a1abc73f

Complete prime-list encoding

Stage 0: freeze the mathematical claim and encoding › Complete prime-list encoding · lines 236–262

Oai279-A@1#eq:encoding, Oai279-A@1#eq:output-address

For $n = n (ℓ)$ , an output consists of $n$ entries of $n$ bits each. A correct output is

enc_{n} (N) = (p_{0}, \dots, p_{k - 1}, 0, \dots, 0),

where

2 \leq p_{0} \leq \dots \leq p_{k - 1}, p_{j} is prime, j = 0 \prod^{k - 1} p_{j} = N .

Multiplicities are retained. Since $N < 2^{n}$ and every prime factor is at least two, $k < n$ . Every entry fits in $n$ bits. Unique factorization makes $enc_{n} (N)$ unique.

The output wire for bit $j$ of entry $a$ is

ℓ + an + j, 0 \leq a, j < n .

This agrees with the inspected Comparator's convention LeanTarget279. Zero padding is not a prime entry.

Displayed formulas in this passage

Oai279-A@1#eq:encoding · line 240
$enc_{n} (N) = (p_{0}, \dots, p_{k - 1}, 0, \dots, 0),$
Oai279-A@1#eq:output-address · line 255
$ℓ + an + j, 0 \leq a, j < n .$
unlabeled · line 245
$2 \leq p_{0} \leq \dots \leq p_{k - 1}, p_{j} is prime, j = 0 \prod^{k - 1} p_{j} = N .$