Add three oriented-matroid conjectures (Roudneff, Las Vergnas simplex, two-colored triangle)

### What is the conjecture

This issue collects three famous conjectures about simplicial cells and mutations in arrangements of pseudolines and pseudohyperplanes, two of them from the standard textbook *Oriented Matroids* of Björner, Las Vergnas, Sturmfels, White and Ziegler. They are phrased through oriented matroids (chirotopes).

A chirotope of rank `r` on `n` elements assigns a sign in `{-1, 0, +1}` to every `r`-tuple, subject to the alternating axiom and the 3-term Grassmann–Plücker relations. A uniform chirotope is nonzero on all injective tuples (general position). A mutation is a flippable `r`-subset (a simplicial cell), and a complete cell is a tope bounded by all `n` pseudohyperplanes.

1. **Roudneff's conjecture**. Every arrangement of `n ≥ 2d+1 ≥ 5` pseudohyperplanes in projective `d`-space has at most `∑_{i=0}^{d-2} binom(n-1, i)` complete cells. The version stated here extends the original hyperplane conjecture to pseudohyperplanes (uniform oriented matroids).
2. **Las Vergnas simplex conjecture**. Every simple (uniform) oriented matroid has at least one simplicial tope. The conjecture is open in general and known in rank 3 (Levi and Shannon: a simple arrangement of `n` pseudolines has at least `n` triangles).
3. **Two-colored triangle conjecture** (Björner, Las Vergnas, Sturmfels, White and Ziegler). Every non-trivial 2-coloring of a simple pseudoline arrangement (at least one line of each color) has a bichromatic triangle, a triangular cell bounded by lines of both colors. The conjecture is known for realizable (straight-line) arrangements, with a proof outlined by Felsner, Pilz and Schnider, and open for pseudolines.

References:
- J.-P. Roudneff, *Cells with many facets in arrangements of hyperplanes*, Discrete Mathematics 98(3) (1991), 185–191.
- R. Hernández-Ortiz, K. Knauer, L. P. Montejano and M. Scheucher, [*Roudneff's conjecture in dimension 4*](https://doi.org/10.1080/10586458.2024.2334379), Experimental Mathematics (2024). Open-access version: [arXiv:2303.14212](https://arxiv.org/abs/2303.14212).
- A. Björner, M. Las Vergnas, B. Sturmfels, N. White and G. M. Ziegler, *Oriented Matroids*, Encyclopedia of Mathematics and its Applications 46, Cambridge University Press (1993). Source of the Las Vergnas conjecture and the two-colored triangle conjecture.
- Y. A. Radtke, B. Keszegh and R. Lauff, [*On triangles in colored pseudoline arrangements*](https://arxiv.org/abs/2601.20574), arXiv:2601.20574 (2026).
- S. Felsner, A. Pilz and P. Schnider, [*Arrangements of approaching pseudo-lines*](https://doi.org/10.1007/s00454-021-00361-w), Discrete & Computational Geometry 67(2) (2022), 380–402.

### Prerequisites needed

A chirotope layer: the chirotope axioms, uniform chirotopes, mutations, topes, and complete cells. Since Mathlib has no oriented matroids, the PR adds this from scratch to `FormalConjecturesForMathlib`. No open Mathlib dependency.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-52 Convex and discrete geometry
* ams-05 Combinatorics

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

No target files, tests, or entry points are named. Start by reading the required chirotope concepts and inspecting how existing conjectures are organized in the repository; done means adding the chirotope layer and formal statements for Roudneff's, Las Vergnas's simplex, and the two-colored triangle conjectures.

Written by the indexing model from the issue text.