Omega-Tail (Compatible Tower)

Compatible tower (x_k) on the primorial ladder M_k = prod of first k primes, with reduction maps. Pre-topological boundary data on bare-metal ontic elements. Polarity is a tail-stable predicate on omega-tails.

Omega-Tail (Compatible Tower)

Summary

Compatible tower (x_k) on the primorial ladder M_k = prod of first k primes, with reduction maps. Pre-topological boundary data on bare-metal ontic elements. Polarity is a tail-stable predicate on omega-tails.

Statement

%
\label{def:omega-tail}
An \textbf{omega-tail} (or \textbf{compatible tower})
is a family $(x_k)_{k \geq 1}$
with $x_k \in \mathbb{Z}/M_k\mathbb{Z}$ satisfying:
\[
    \pi_{\ell \to k}(x_\ell) \;=\; x_k
    \qquad \text{for all } k \leq \ell.
\]
The type of all omega-tails is denoted
$\mathrm{OmegaTail}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 64
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part07/ch28-omega-germs.tex lines 125-137

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Polarity.OmegaGerms
• Name: Tau.Polarity.OmegaTail

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.