Polarity Pairing

Pairing function Pair: P_tau^+ x P_tau^- -> Z measuring rank distance between B-dominant and C-dominant primes. Consecutive polarity pairs exist infinitely often.

Polarity Pairing

Summary

Pairing function Pair: P_tau^+ x P_tau^- -> Z measuring rank distance between B-dominant and C-dominant primes. Consecutive polarity pairs exist infinitely often.

Statement

%
\label{def:polarity-pairing}
The \textbf{polarity pairing function}
\[
    \mathrm{Pair} : \mathbb{P}_\tau^+ \times \mathbb{P}_\tau^-
    \;\to\; \mathbb{Z}
\]
is defined by
\[
    \mathrm{Pair}(\underline{p}, \underline{q})
    \;:=\;
    \mathrm{rank}(\underline{p}) - \mathrm{rank}(\underline{q}),
\]
where $\mathrm{rank}(\underline{p})$ is the ordinal position
of $\underline{p}$ in the enumeration of $\mathbb{P}_\tau$
(i.e., $\mathrm{rank}(\underline{2}) = 1$,
$\mathrm{rank}(\underline{3}) = 2$, etc.).
The \textbf{polarity gap} of the pair
is $|\mathrm{Pair}(\underline{p}, \underline{q})|$:
the distance between their positions
in the prime enumeration.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 244
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part06/ch27-prime-polarity.tex lines 445-466

Lean / Formalization Notes

• Formalization: planned
• Module: None
• Name: None

Dependencies

• Canonical: I.T05

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.