Registry · Theorem I.T18 tau-effective formalized

I.T18 — CRT Coherence Constraint

Tower-coherent functions that are well-defined on Z/M_kZ depend only on the CRT residue at stage k. Proved concretely for chi_plus and chi_minus; the general case requires residue-respect as hypothesis.

Book I Part 13 Ch. 50

Dependency Graph

Depends on (2)

I.D46 I.D29

Depended on by (29)

I.T21 I.T40 II.D09 II.D10 II.D12 II.D25 II.D36 II.D37 II.D39 II.D42 II.D45 II.D46 II.L01 II.L02 II.L05 II.L06 II.L13 II.P07 II.P08 II.T01 II.T02 II.T04 II.T07 II.T20 II.T26 II.T27 II.T30 II.T31 II.T32

Lean Formalization

Module: TauLib.BookI.Holomorphy.TauHolomorphic

Symbol: Tau.Holomorphy.chi_plus_crt