Registry · Definition III.D108 tau-effective formalized

III.D108 — Sieve-Accelerated ABC

ABC quality check pushed to bound 100. Weak ABC (c < rad(abc)²) for all coprime pairs.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Arithmetic.ABCDeep

Symbol: abc_sieve_check