Registry · Definition I.D29 established formalized

I.D29 — CRT Decomposition

CRT decomposition and reconstruction on the primorial ladder: forward map x -> (x mod p_i), inverse map via coprime idempotents e_i, round-trip verified exhaustively by native_decide. Basis elements are idempotent, orthogonal, sum to unity. CRT coherence with primorial reduction verified.

Book I Part 7 Ch. 30

Dependency Graph

Depends on (2)

Depended on by (6)

Lean Formalization

Module: TauLib.BookI.Polarity.ChineseRemainder

Symbol: Tau.Polarity.crt_decompose