A counterexample to the cocircuit diameter conjecture

A rationally realizable uniform rank-41 oriented matroid on 80 elements has cocircuit-graph diameter at least $42>41=n-r+2$, refuting the general cocircuit diameter conjecture. We build on the rank-21 example of Adler, De Loera, Klee and Zhang, the non-Hirsch polytope of Matschke, Santos and Weibel, Santos's product construction, and the source certification of Allamigeon, Canu and Strub. A count of negative coordinates confines every potentially shorter walk to two affine sections; projection to the product factors then gives the lower bound. Two rational perturbations make the resulting oriented matroid uniform. Lean 4 separately verifies the matrix existence and walk lower bound for a different realizing matrix; the printed perturbations are proved here, not checked in Lean. This work has not yet been reviewed by experts. The proofs, the Lean formalization, the certificate checkers and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.