Registry · Definition
I.D30
established
formalized
I.D30 — 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.
Book I
Part 7
Ch. 30