Congruent Tails Agree

n = m (mod M_k) implies canonical tails agree at level k. Agreement at each primorial level is a finite modular check. Underlies Cauchy-compactness of the profinite completion.

Congruent Tails Agree

Summary

n = m (mod M_k) implies canonical tails agree at level k. Agreement at each primorial level is a finite modular check. Underlies Cauchy-compactness of the profinite completion.

Statement

%
\label{prop:congruent-tails-agree}
% Depends: def:omega-tail, def:primorial-ladder
If $n \equiv m \pmod{M_k}$,
then the canonical omega-tails
$\hat{n}$ and $\hat{m}$
agree at level $k$:
\[
    n \equiv m \pmod{M_k}
    \quad\Longrightarrow\quad
    \hat{n}_k = \hat{m}_k.
\]

Proof / Justification

The $k$-th component of the canonical embedding is
$\hat{n}_k = n \bmod M_k$.
If $n \equiv m \pmod{M_k}$,
then $n \bmod M_k = m \bmod M_k$,
hence $\hat{n}_k = \hat{m}_k$.

Source Context

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

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Structural
• Name: Tau.Denotation.congruent_tails_agree

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.