A rank-seven oriented matroid without a simplicial tope

Counterexample to Las Vergnas' simplex conjecture in the formulation for arbitrary simple oriented matroids, stated as Conjecture 1 of Knauer and Marc as "every OM has a simplicial tope" (simplicity assumed throughout that paper). The example is a simple oriented matroid of rank seven on 38 elements in which every tope has at least eight facets.

It is the oriented matroid 2-sum of two copies of Richter-Gebert's rank-four example with a mutation-free element. Each factor contributes at least four facets away from the common element, and those facets survive the 2-sum. The example is nonuniform, so the conjecture for uniform oriented matroids is unaffected.

Verification

The theorem is proved from the published existence and mutation-freeness of $R(20)$ and does not depend on a computation. Independently of that, r20-chirotope.tsv fixes a uniform rank-four oriented matroid with the property the argument needs, so the 2-sum of two of its copies is a directly reproducible counterexample. Run from the repository root:

python3 verify_static_certificate.py

The verifier uses only the Python standard library. It checks the file's SHA-256 digest, then the chirotope axioms through 190 rank-two contractions with explicit linear-order certificates, 35,969,280 tope/circuit orthogonality checks, and the neighbor count of all 2320 topes.

Two further checkers are included. verify_fixed_r20.py rebuilds the table from the construction in fixed_r20.py and checks all 581,400 uniform three-term Grassmann–Plücker relations. verify_fixed_two_sum.py builds all 2,572,864 topes of the 2-sum explicitly and checks the eight-neighbor bound on each one, rather than deducing it.

Contents

Path	Content
paper/COUNTEREXAMPLE.tex, paper/COUNTEREXAMPLE.pdf	the manuscript
r20-chirotope.tsv	the fixed chirotope, 4845 signed bases
verify_static_certificate.py	the verifier described in the manuscript
fixed_r20.py	the construction script, not imported by the verifier
verify_fixed_r20.py, verify_fixed_two_sum.py	the two additional checkers

Use of generative AI

GPT-6 Astra, through OpenAI Codex, developed the 2-sum argument, wrote the construction and verification code, and drafted the manuscript. A separate instance of the same model reviewed the argument and wrote the verifier that reads the fixed chirotope directly. Those checks were AI-assisted and computational; they are not human peer review.