Improved Upper Bounds on the Size of Condorcet Domains

We prove f(n) ≤ 32n f(n − 1)/(11n + 8) for the maximum size of a Condorcet domain, giving exponential base 32/11 < 3. An exact deletion count, a decomposition into adjacent-swap components and a local counting inequality give the bound; the same local inequality gives base 8/3 for peak-pit domains. Small examples illustrate the structural counts. The mathematical argument is presented here; the exact finite calculations, reproducible programs and complete Lean formalisation are supplied as accompanying computational material.