Teichmueller Lift

Canonical lift of single-prime residue r in Z/p_iZ to omega-tail via CRT reconstruction at each stage. Satisfies retraction (Lift_i(r) mod p_i = r), orthogonality (Lift_i(r) mod p_j = 0 for j != i), compatibility (compatible tower), multiplicativity, and decomposition (nat_to_tail = sum of lifts). All properties verified by native_decide.

Teichmueller Lift

Summary

Canonical lift of single-prime residue r in Z/p_iZ to omega-tail via CRT reconstruction at each stage. Satisfies retraction (Lift_i(r) mod p_i = r), orthogonality (Lift_i(r) mod p_j = 0 for j != i), compatibility (compatible tower), multiplicativity, and decomposition (nat_to_tail = sum of lifts). All properties verified by native_decide.

Statement

%
\label{def:teichmueller-lift}
For $r \in \mathbb{Z}/\underline{p}_i\mathbb{Z}$,
the \textbf{Teichmüller lift}
$\mathrm{Lift}_i(r) \in \hat{\mathbb{Z}}_\tau$
is the omega-tail whose $k$-th component
(for $k \geq i$) is
\[
    \mathrm{Lift}_i(r)_k
    \;:=\;
    \varphi_k^{-1}\bigl(0, \ldots, 0, \underbrace{r}_{i}, 0, \ldots, 0\bigr)
    \;=\; r \cdot e_i^{(k)} \;\bmod\; M_k,
\]
where $e_i^{(k)}$ is the CRT basis element at depth $k$.
For $k < i$, the component is $0$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Polarity.TeichmuellerLift
• Name: Tau.Polarity.teich_lift

Dependencies

• Canonical: I.D29, I.D25

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.