Boundary Local Ring

Ring structure on omega-tails from primorial inverse limit. CRT factors Z/M_k into B-prime and C-prime contributions. Earned ring operations on boundary data.

Boundary Local Ring

Summary

Ring structure on omega-tails from primorial inverse limit. CRT factors Z/M_k into B-prime and C-prime contributions. Earned ring operations on boundary data.

Statement

%
\label{def:boundary-local-ring}
The \textbf{boundary local ring} $\hat{\mathbb{Z}}_\tau$
is the inverse limit
\[
    \hat{\mathbb{Z}}_\tau
    \;:=\;
    \varprojlim_k \mathbb{Z}/M_k\mathbb{Z}
\]
equipped with componentwise addition and multiplication.
An element of $\hat{\mathbb{Z}}_\tau$
is an omega-tail $(x_k)_{k \geq 1}$
(Definition~\ref{def:omega-tail})
that is additionally compatible with ring operations:
if $(x_k)$ and $(y_k)$ are compatible towers,
so are $(x_k + y_k)$ and $(x_k \cdot y_k)$
(Section~\ref{subsec:ch30-ring-ops}).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 68
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part07/ch30-bipolar-algebra.tex lines 246-264

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Polarity.BipolarAlgebra
• Name: Tau.Polarity.bdry_add

Dependencies

• Canonical: I.D25

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.