Registry · Proposition III.P45 established formalized

III.P45 — Twin Admissibility Fraction

At each odd prime p≥3, exactly (p-2)/p fraction of residues are twin-admissible. Only r≡0 and r≡p-2 excluded.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D107

Depended on by (1)

III.P46

Lean Formalization

Module: TauLib.BookIII.Spectral.TwinPrimeDeep

Symbol: twin_admissibility_fraction_5