Registry · Definition III.D107 tau-effective formalized

III.D107 — CRT Twin Admissibility

Twin-admissible residues mod M_k: r with neither r nor r+2 ≡ 0 (mod p_i) for all i≤k. Always nonempty.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.T10

Depended on by (2)

III.P45 III.T75

Lean Formalization

Module: TauLib.BookIII.Spectral.TwinPrimeDeep

Symbol: crt_twin_admissible