Proof: checkerboard monochromatic no-three-in-line bound for all n ≥ 6

[DomTheDeveloper]

Theorem

For every n ≥ 6, every subset of either checkerboard color class in the n × n lattice with no three Euclidean-collinear points has cardinality at most 2n - 4.

The public Lean theorem is:

theorem Checkerboard.checkerboard_upper_all_n {n parity : ℕ}
    (hn : 6 ≤ n) (hp : parity = 0 ∨ parity = 1)
    (s : Finset (Checkerboard.Point n))
    (hcolor : Checkerboard.Monochromatic parity s)
    (hntil : Checkerboard.NoThreeInLine s) :
    s.card ≤ 2 * n - 4

Semantic audit

• NoThreeInLine uses the exact determinant criterion for every triple of pairwise distinct lattice points, so arbitrary Euclidean slopes are covered.
• Monochromatic is exactly the parity condition (row + column) % 2 = parity % 2.
• Rows, columns, and slopes ±1 are used only as necessary line-capacity constraints inside valid upper-bound certificates; they do not weaken the theorem statement.

Proof architecture

• n = 6: explicit 18-variable Boolean/Presburger certificates for both parity classes, transported from the geometric no-three-in-line condition through closed row, column, and diagonal fiber certificates.
• odd n ≥ 7: exact nonnegative quadratic line-cover weights with constant point coverage and closed objective formulas.
• even n ≥ 8: the analogous exact quadratic cover and objective calculation.
• exceptional thin color on 7 × 7: a separate explicit rational line cover.

Verification

Final verified source commit: 11391b32292ca39da502522a733486b580916439

Final pinned audit: GitHub Actions run 30035472008

The audit:

• built the complete Checkerboard Lean library under repository-pinned Lean/Mathlib v4.32.0;
• rejected sorry, admit, native_decide, bv_decide, project-defined axioms, opaque proof shortcuts, and compiler-trust escape hatches;
• compiled the exact public theorem;
• ran #print axioms Checkerboard.checkerboard_upper_all_n;
• reported only standard Lean axioms [propext, Quot.sound].

The exact 6 × 6 public base cases also passed their separate focused build and axiom audit.

Proof developed by Dominic Dabish. ProofOrchestrator, using OpenAI GPT-5.6 Thinking, assisted with the mathematical argument, Lean formalization, compatibility repair, and submission preparation. Every formal claim is checked by the pinned Lean kernel.