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

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookI.Polarity.TeichmuellerLift

Symbol: Tau.Polarity.teich_lift