Registry · Proposition III.P48 established formalized

III.P48 — ABC Gap Characterization

ABC gap = structural. Primorial tower is squarefree → avoids the hard case. Genuine difficulty in perfect-power parts. exponential_quantification (K4).

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

III.P47 III.D69

Depended on by (1)

III.D112

Lean Formalization

Module: TauLib.BookIII.Bridge.ConjectureGaps

Symbol: abc_gap_structural