math.CO — Combinatorics
A bigon-free dichotomy for pseudoline arrangements, after a note of Grothendieck
A pseudoline of an arrangement in the real projective plane is bigonal when it carries exactly two vertices of the arrangement. In an undated folder of working notes from the early 1980s, Grothendieck states that every arrangement without bigonal pseudolines is either four pseudolines in general position or contains one of three configurations: five pseudolines in general position, a pencil of three and a pencil of two without the line joining their centres, or the complete quadrangle. The notes derive this from a statement that is false as written, and they give no independent proof. We give a short proof, together with the ordering of the pseudolines that the notes ask for, and we deduce that for n ≥ 6 the near-pencils are the only arrangements of n pseudolines containing none of the three configurations. The dichotomy has been checked by an exhaustive enumeration of all arrangements of at most nine pseudolines, and it is formalised in the proof assistant Lean for a combinatorial model of arrangements, generalised maps of Euler characteristic one.