Proof of the Arad–Herzog conjecture

We prove the Arad–Herzog conjecture, posed in 1985: the product of two nonidentity conjugacy classes in a nonabelian finite simple group contains at least two conjugacy classes. Building on published cases, we complete the remaining classical and exceptional families using finite-field invariants, orbit-difference arguments and genuine character identities, with exact arithmetic certificates for small-field exceptional groups.This record includes the manuscript and supporting source and verification archive. Lean formalisation is partial and literature-relative. The archive is not a complete universal Lean proof or a complete offline reconstruction of every external source pipeline. Rights differ by file.5.