Completeness Without Topology

ℤ_p^τ is complete in the τ sense: every tower-coherent sequence has unique limit. This is Global Hartogs (I.T31) restricted to the p-primary tower. No metric, no Cauchy sequences.

Completeness Without Topology

Summary

ℤ_p^τ is complete in the τ sense: every tower-coherent sequence has unique limit. This is Global Hartogs (I.T31) restricted to the p-primary tower. No metric, no Cauchy sequences.

Statement

%
\label{prop:completeness-without-topology}
Let $(b_n)_{n \geq 1}$ be a $k$-approximately coherent
sequence in the $p$-primary tower.
Then there exists a unique $a = (a_n)_{n \geq 1} \in \Z_p^\tau$
such that $a_n = b_n$ for all $n \geq k$.
In particular:
\begin{enumerate}
    \item[\textup{(i)}]
          Every tower-coherent sequence defines
          a unique $p$-adic $\tau$-integer.
    \item[\textup{(ii)}]
          Every $k$-approximately coherent sequence
          determines a unique $p$-adic $\tau$-integer
          by ``filling in'' the first $k-1$ levels.
    \item[\textup{(iii)}]
          No sequence that is coherent from some level onward
          escapes $\Z_p^\tau$:
          the ring is closed under eventual coherence.
\end{enumerate}

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 46
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part03/ch16-hensel-lifting-and-local-fields.tex lines 504-525

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Spectral.LocalFields
• Name: completeness_check

Dependencies

• Canonical: III.D21, I.T31

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.