Polynomial Structure of No-Three-In-Line Sets: Degree Optimality, Bounded Intersection, and CRT Obstructions

The No-Three-In-Line (NTIL) problem asks for the maximum number f (n) ofpoints on an n × n integer grid with no three collinear. The classical parabolic con-struction gives f (p) ≥ p for primes p via {(t, t2 mod p) : 0 ≤ t < p}.We present three novel contributions that clarify the algebraic structure underlyingNTIL constructions. Our main result is a Degree Characterization Theorem showingthat degree two is the unique polynomial degree producing a cap modulo p: linearpolynomials and polynomials of degree d ≥ 3 are never caps modulo p, while everyquadratic with p ∤ leading coefficient is. Since cap modulo p implies NTIL (and theconverse holds for degree-2 sets), this gives a complete algebraic characterization. Theproof is unified by a single principle: the second divided difference of a polynomial ofdegree d has degree d − 2, which is zero (and hence nonvanishing) precisely when d = 2.As further consequences we prove a Bounded Intersection Theorem showing thatany two distinct generalized quadratic NTIL sets share at most two points, and developa Modular Lifting Framework that identifies a precise obstruction to extending theparabolic construction to composite grids via the Chinese Remainder Theorem.All core results are formalized in Lean 4 with zero sorry tactics in a single self-contained file of 935 lines. The formalization covers the classical bounds, the general-ized quadratic construction, balanced structure theorems, the modular lifting frame-work, CRT obstruction analysis, and the degree characterization for quadratics, lin-ears, and the specific cubic t3. The general cubic and higher degree failure theoremsare established by mathematical proof in this paper. The formalization is available athttps://github.com/alejandrozu/NTIL.