Registry · Theorem III.T77 tau-effective formalized

III.T77 — Squarefree Dominance

Squarefree dominance: c ≤ rad(abc) for all squarefree coprime pairs up to 100. Stronger than ABC (ε=0).

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D110

Depended on by (1)

III.P47

Lean Formalization

Module: TauLib.BookIII.Arithmetic.ABCDeep

Symbol: squarefree_dominance_100