Thin Checkerboard of Side Seventeen

Abstract

The odd-parity class of the 17 by 17 integer grid has no-three-in-line optimum 26.

Definition 1.1 (Integer lattice points).

$$\mathrm{Point}=\mathbb{Z}\times \mathbb{Z}$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.Point (✓ std3).

Source. Repository-derived.

Commentary.

Point abbreviates Prod Int Int; its two coordinates are integers.

Definition 1.2 (Integer line equations).

$$\mathrm{LineKey}=\mathbb{Z}\times (\mathbb{Z}\times \mathbb{Z})$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.LineKey (✓ std3).

Source. Repository-derived.

Commentary.

LineKey abbreviates Prod Int (Prod Int Int). The nested pair (a,(b,c)) represents ax+by=c; properness is proved privately for every certificate line.

Definition 1.3 (Displacement determinant).

$$\forall p,q,r:\mathrm{Point},\det \left(p,q,r\right)=(q_1-p_1)\cdot (r_2-p_2)-(q_2-p_2)\cdot (r_1-p_1)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.det (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression is the integer determinant of q-p and r-p, exactly as in GICT Theorem 3.4.16. Subscripts denote the first and second integer coordinates.

Definition 1.4 (Odd-parity grid membership).

$$\forall p:\mathrm{Point},\mathrm{Thin}\left(p\right)⟺(0\le p_1\wedge p_1\le 16\wedge 0\le p_2\wedge p_2\le 16\wedge \mathrm{intMod}\left(p_1+p_2,2\right)=1)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.Thin (✓ std3).

Source. Repository-derived.

Commentary.

Both coordinates lie between zero and sixteen. intMod denotes Lean integer remainder, so the last equality expresses odd coordinate sum.

Definition 1.5 (All-slopes no-three-in-line).

$$\forall S:\mathrm{Finset}\left(\mathrm{Point}\right),\mathrm{NTIL}\left(S\right)⟺(\forall p\in S,\forall q\in S,\forall r\in S,p\ne q\Rightarrow p\ne r\Rightarrow q\ne r\Rightarrow \det \left(p,q,r\right)\ne 0)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.NTIL (✓ std3).

Source. Repository-derived.

Commentary.

This predicate ranges over every ordered triple of members and requires nonzero integer determinant whenever the three points are pairwise distinct. It imposes no restriction on slopes.

Definition 1.6 (Integer line incidence).

$$\forall p:\mathrm{Point},\forall l:\mathrm{LineKey},\mathrm{onLine}\left(p,l\right)⟺\mathrm{fst}\left(l\right)\cdot p_1+\mathrm{fst}\left(\mathrm{snd}\left(l\right)\right)\cdot p_2=\mathrm{snd}\left(\mathrm{snd}\left(l\right)\right)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.onLine (✓ std3).

Source. Repository-derived.

Commentary.

fst and snd are product projections. Incidence is the displayed integer equation, with no geometric Collinear predicate involved.

Definition 1.7 (The explicit point certificate).

$$\mathrm{witness}:\mathrm{Finset}\left(\mathrm{Point}\right)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness (✓ std3).

Source. Repository-derived.

Commentary.

The defining finite set is the fixed list of 26 integer points in the Lean source, copied unchanged from the preregistered certificate. It is kernel-decided finite data; the three following theorems check cardinality, thin membership, and all distinct triples. The entries are not duplicated in this mirror.

Definition 1.8 (The weighted line certificate).

$$\mathrm{weightedLines}:\mathrm{List}\left(\mathrm{LineKey}\times \mathbb{N}\right)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.weightedLines (✓ std3).

Source. Repository-derived.

Commentary.

The defining list contains the fixed 40 pairs of integer line coefficients and natural weights from the preregistered certificate, unchanged. These are kernel-decided finite data, not an assumed optimizer output. The entries are not duplicated here; the weights sum to 320 and the required coverage scale is 24.

Theorem 1.9 (The witness has 26 points).

$$\mathrm{card}\left(\mathrm{witness}\right)=26$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

Kernel reduction counts 26 distinct points.

Theorem 1.10 (Every witness point is thin).

$$\forall p\in \mathrm{witness},\mathrm{Thin}\left(p\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness_thin (✓ std3). ∎

Source. Repository-derived.

Commentary.

Kernel reduction checks the coordinate bounds and odd parity for all 26 entries.

Theorem 1.11 (Every distinct witness triple is noncollinear).

$$\mathrm{NTIL}\left(\mathrm{witness}\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness_ntil (✓ std3). ∎

Source. Repository-derived.

Commentary.

Kernel reduction verifies every distinct ordered triple; equivalently all 2600 unordered triples have nonzero determinant. No native_decide is used.

Definition 1.12 (Line at a certificate index).

$$\forall i:\mathrm{Fin}\left(40\right),\mathrm{line}\left(i\right)=\mathrm{fst}\left(\mathrm{get}\left(\mathrm{weightedLines},\mathrm{val}\left(i\right)\right)\right)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.line (✓ std3).

Source. Repository-derived.

Commentary.

get is zero-based list lookup at val(i). Lean transports i from Fin 40 to Fin weightedLines.length using the kernel-checked length equality before taking the first projection.

Definition 1.13 (Weight at a certificate index).

$$\forall i:\mathrm{Fin}\left(40\right),\mathrm{weight}\left(i\right)=\mathrm{snd}\left(\mathrm{get}\left(\mathrm{weightedLines},\mathrm{val}\left(i\right)\right)\right)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.weight (✓ std3).

Source. Repository-derived.

Commentary.

The same zero-based lookup and length transport is followed by the second projection, yielding a natural number.

Definition 1.14 (Total incident line weight).

$$\forall p:\mathrm{Point},\mathrm{cover}\left(p\right)=\sum _{i:\mathrm{Fin}\left(40\right)}\mathrm{ite}\left(\mathrm{onLine}\left(p,\mathrm{line}\left(i\right)\right),\mathrm{weight}\left(i\right),0\right)$$

Formalization. D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.cover (✓ std3).

Source. Repository-derived.

Commentary.

The sum is over all forty indices and takes natural values. ite(P,a,b) equals a when P holds and b otherwise.

Theorem 1.15 (Total certificate weight).

$$\sum _{i:\mathrm{Fin}\left(40\right)}\mathrm{weight}\left(i\right)=320$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.weight_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Lean kernel checks the sum of the forty natural weights.

Theorem 1.16 (Every thin grid point has coverage at least 24).

$$\forall x,y:\mathrm{Fin}\left(17\right),\mathrm{natMod}\left(\mathrm{val}\left(x\right)+\mathrm{val}\left(y\right),2\right)=1\Rightarrow 24\le \mathrm{cover}\left((\mathrm{ofNat}\left(\mathrm{val}\left(x\right)\right),\mathrm{ofNat}\left(\mathrm{val}\left(y\right)\right))\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.cover_grid (✓ std3). ∎

Source. Repository-derived.

Commentary.

val maps Fin 17 to the naturals, natMod denotes natural remainder, and ofNat explicitly embeds each coordinate into the integers before cover is applied. Kernel enumeration checks the whole 17 by 17 grid under its parity premise.

Theorem 1.17 (Every admissible set has at most 26 points).

$$\forall S:\mathrm{Finset}\left(\mathrm{Point}\right),(\forall p\in S,\mathrm{Thin}\left(p\right))\Rightarrow \mathrm{NTIL}\left(S\right)\Rightarrow \mathrm{card}\left(S\right)\le 26$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.upper_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

A proper integer line carries at most two points of an NTIL set. Double counting weighted incidences therefore gives 24card(S) <= 2320 = 640, and natural arithmetic yields card(S) <= 26.

Theorem 1.18 (Exact optimum: attainment and universal bound).

$$(\exists S:\mathrm{Finset}\left(\mathrm{Point}\right),(\forall p\in S,\mathrm{Thin}\left(p\right))\wedge \mathrm{card}\left(S\right)=26\wedge \mathrm{NTIL}\left(S\right))\wedge (\forall T:\mathrm{Finset}\left(\mathrm{Point}\right),(\forall p\in T,\mathrm{Thin}\left(p\right))\Rightarrow \mathrm{NTIL}\left(T\right)\Rightarrow \mathrm{card}\left(T\right)\le 26)$$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.thinCheckerboard17_ntil_max_eq_26 (✓ std3). ∎

Source. Repository-derived.

Commentary.

GICT Theorem 3.4.16 is mirrored as one conjunction: an admissible 26-point set exists and every admissible set has at most 26 points. Both preregistered escape certificates from Remark 3.4.17 are live in the proof; the remark is not claimed as covered. This exact finite result is derived in this repository. Prellberg, arXiv:2605.09215, Definition 2, Table 1, and Section 4 supply the problem context: Table 1 gives exact thin-checkerboard maxima through n=16, ending at 24. The present claim is only for n=17 and its odd-parity class. It asserts neither a result for other n nor a bridge to Mathlib Collinear, and makes no global novelty claim.

References

• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.LineKey
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.NTIL
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.Point
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.Thin
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.cover
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.cover_grid
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.det
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.line
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.onLine
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.thinCheckerboard17_ntil_max_eq_26
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.upper_bound
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.weight
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.weight_sum
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.weightedLines
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness_card
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness_ntil
• Truth anchor: D5/S3/Arith/Lattices/ThinCheckerboardNoThreeInLineSeventeen.witness_thin