Chapter 11: formalize Theorem 1 (the Sylvester–Gallai theorem)

[Solarys431]

Formalizes Theorem 1 of Chapter 11, the Sylvester–Gallai theorem. Theorems 2–4 and the appendix are left as they are.

theorem sylvester_gallai (S : Set P) (hfin : S.Finite) (hncol : ¬ Collinear ℝ S) :
    ∃ a ∈ S, ∃ b ∈ S, IsOrdinaryLine S a b

IsOrdinaryLine S a b: a ≠ b are points of S, and every point of S on the line through them is a or b.

The proof

Kelly's, as in the book: over all triples of non-collinear points, take the one minimizing the distance from a point to the line through the other two; that line carries a third point of S, two of the three fall on the same side of the foot of the perpendicular, and that yields a strictly closer triple.

Two points worth flagging:

• Purely vectorial — no areas, no angles, no similar triangles, only the inner product. Everything turns on perp w z, the component of z orthogonal to w: it is linear in z, and the strict inequality is ⟪A, w⟫ = ‖A‖ ^ 2 > 0 (the minimizing point is not the foot of the perpendicular).
• The pigeonhole step is isolated over the reals (Pigeonhole.three). That is where the order of ℝ is used, and it must be used somewhere: the theorem is false over ℂ.

The distance to a line is defined from perp rather than Metric.infDist, and the minimum is over triples of points rather than point/line pairs — as the book phrases Kelly's minimization. The final statement mentions no distances.

Generality

Proved in an arbitrary real inner product space with its affine torsor, with no dimension hypothesis — Kelly's proof never needs one. The classical plane is EuclideanSpace ℝ (Fin 2); I can add it as a corollary if the chapter prefers.

Checks

• lake build passes on the whole project (v4.27.0-rc1); both lint.yml style checks pass.
• No sorry. #print axioms chapter11.SylvesterGallai.sylvester_gallai → [propext, Classical.choice, Quot.sound].
• The hypotheses are satisfiable (a concrete non-collinear triple is machine-checked), so the statement is not vacuously true.

Prior art

Not in mathlib. In Lean 4, YaelDillies/misc-yd proves Sylvester–Chvátal (Chen's metric generalization); its Euclidean corollary — the statement here — is left there in a commented-out block with a sorry. A Lean 3 development also exists (Happyves/Master_Thesis).

Methodological note

I built a pipeline for validating proofs and formalizations of mathematical theorems, driven by AI (Claude, by Anthropic); this file is its output. I am not a mathematician, but a software developer, so I would be very glad of the community's help in making sure the work is rigorous and correct by the standards I have set for it.

On naming, structure and level of generality I will follow your conventions.

Companion issue: #139.