HEXAGONbeta

A bigon-free dichotomy for pseudoline arrangements, after a note of Grothendieck

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.HO — History and Overviewmath.MG — Metric Geometrycs.LO — Logic in Computer Science

Contributed by Michel Hua ↗

Version 1 / Nov 07, 2026 / CC BY 4.0

Abstract

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.

Provenance statement

Drafted with Claude (Claude Code, Anthropic; Opus 5 and Opus 5.5) from the transcription of folder 80 of Grothendieck’s working notes (University of Montpellier), itself made with language models. The search for a proof, the exhaustive enumeration of arrangements of at most nine pseudolines (program in computations/bigon of the repository Commutator-IO/grothendieck-project) and the Lean 4 formalisation were done with the same models, under the author’s direction. The main theorem is checked by Lean with mathlib, for generalised maps of Euler characteristic one. The author checked the proofs, the computations and the references.

Formalizations

Tools used

Lean
LeanVersion 4
Anthropic
Claude OpusVersion 5.5

References

  1. A. Björner, M. Las Vergnas, B. Sturmfels, N. White, G. M. Ziegler, Oriented Matroids , 2nd ed., Encyclopedia of Mathematics and its Applications 46, Cambridge University Press, 1999, doi:10.1017/CBO9780511586507 (https://doi.org/10.1017/CBO9780511586507).DOI
  2. J. Bokowski, P. Pokora, On the Sylvester--Gallai and the orchard problem for pseudoline arrangements, Period.\ Math.\ Hungar. 77 (2018), 164--174, doi:10.1007/s10998-017-0224-x (https://doi.org/10.1007/s10998-017-0224-x).DOI
  3. S. Felsner, J. E. Goodman, Pseudoline arrangements, in J. E. Goodman, J. O'Rourke, C. D. Tóth (eds.), Handbook of Discrete and Computational Geometry , 3rd ed., CRC Press, Boca Raton, FL, 2017, ch. 5.
  4. L. Finschi, K. Fukuda, Combinatorial generation of small point configurations and hyperplane arrangements, in B. Aronov et al.\ (eds.), Discrete and Computational Geometry: The Goodman--Pollack Festschrift , Algorithms and Combinatorics 25, Springer, 2003, 425--440, doi:10.1007/978-3-642-55566-4_19 (https://doi.org/10.1007/978-3-642-55566-4_19).DOI
  5. B. Grünbaum, Arrangements and Spreads , CBMS Regional Conference Series in Mathematics 10, American Mathematical Society, 1972.
  6. M. Hua, Grothendieck Montpellier. Énoncés des lectures modernisées démontrés, Hexagon preprint hexagon:2611.00125v1 (https://hexagonmath.org/2611.00125v1), 2026.hexagon
  7. L. M. Kelly, R. Rottenberg, Simple points in pseudoline arrangements, Pacific J.\ Math. 40 (1972), 617--622, doi:10.2140/pjm.1972.40.617 (https://doi.org/10.2140/pjm.1972.40.617).DOI
  8. P. Lienhardt, NN-dimensional generalized combinatorial maps and cellular quasi-manifolds, Internat.\ J.\ Comput.\ Geom.\ Appl. 4 (1994), 275--324, doi:10.1142/S0218195994000173 (https://doi.org/10.1142/S0218195994000173).DOI
  9. E. Melchior, Über Vielseite der projektiven Ebene, Deutsche Math. 5 (1941), 461--475, Zbl 0025.09105.

Version history

  1. v1 · 7 pagesSubmitted by Michel HuaInitial depositCurrentNov 07, 2026