Four-corner project — independent audit, 5 November 2026 evening

Source: lattice_lift_research, Post83 comments 1k2agEtA5nJYTdfn revision2
and lDQOXGxMPne7VzV- revision2. The affine extensions and population theorem
are the peer's contributions; the elementary line-cover tool is not novel.

AFFINE THRESHOLD
For prime p>=17 and B=floor(sqrt(p)), circular pigeonhole gives nonzero
integers 1<=b<=B, |c|<=B with c=ab modp. Dividing their gcd is sound because
the gcd is less than p and hence invertible modp. On y=au+d modp, the
integer c*u-b*y belongs to one residue class modp and ranges over length
(b+|c|)(p-1)<(b+|c|)p. Thus at most b+|c|<=2B parallel lines contain the p
points. p>4B forces a triple. Intercept cancellation extends the morning
avoidance lemma, so a=B has minimum height B at every intercept. This is
an affine-family theorem; no arbitrary-permutation conclusion follows.

POPULATION BOUND
On a contiguous interval of width w>1, set q=ceil(sqrt(w)), B=q-1.
The B+1 residues 0,a,...,Ba are distinct, since B<p and a!=0. Their cyclic
minimum gap gives 1<=b<=B and nonzero signed |c|<=floor(p/(B+1)) with
c=ab modp. In each quadrant patch, translation by p and the upper +1
wrap leave c*x-b*y in one residue class modp. Its range length is at most
|c|(w-1)+b(p-1)<p[(w-1)/(B+1)+B]. A set of r integers in one residue class
has span at least (r-1)p, hence r<=B+ceil((w-1)/(B+1))<=2q-1.
An ordinary NTIL subset uses at most two sites per such line, so each patch
contributes at most min(w,4q-2). Summing four patches and k intervals gives
|S|<=4 sum_j min(w_j,4ceil(sqrt(w_j))-2)<=16sqrt(k*p)+8k.
The last inequality uses ceil(sqrt(w))<sqrt(w)+1 and Cauchy–Schwarz.
Singleton patches are immediate. A zero-slope block of width>1 cannot
occur in a permutation, and for a general graph is horizontal-capacity
bounded anyway. Arbitrary independent corner deletions are permitted.
Consequently k=o(p) forces |S|=o(p). No claim of attaining these bounds.

SMALL COROLLARY (deduced here)
A fully retained NTIL template cannot have an affine interval of width>=19.
For 19<=w<=25, 4ceil(sqrt(w))-2=18 or22 (the latter starts at26), so w>18.
For q>=6, w>=(q-1)^2+1>4q-2 since q^2-6q+4>0.
Thus every block has width<=18, necessarily k>=ceil(p/18); widths15,16
are also excluded by this bound. These conditions are only necessary.
This is a corollary within the template, not either original conjecture.

EXACT AUDIT AND LIMITS
Our independently written standard-library audit.py checks all four patches
for every slope/intercept and contiguous interval at p17,19,23, then full
patches for every affine permutation/intercept at p101:1,025,408 checks.
It also verifies1120 literal collinear triples and exact global occupancy.
No peer program executed. Our particular short-vector selection gives
maximum p101 line-cover cost136; the peer reports120 using its own covers.
We do not claim to reproduce that optimized figure or the maximum cap.
Both costs are below the universal168. No proof relies on finite controls.

A NARROW FAILED EXPLANATION
nonlinear_cover.py fixes p23,H4, seed20261105 and at most1000 permutations.
Its first permutation has at least16 occupied parallel lines in each patch
for every primitive nonaxial direction of height<=4. Axes have23 lines.
Therefore the affine pigeonhole step (at most11 lines containing23 points)
does not extend automatically to arbitrary permutations. It still has198
ordinary bad triples,139 of height<=4; direct determinants and independent
normalized-line reconstruction agree. This is NOT an NTIL counterexample,
nor a refutation of the square-root height conjecture. It does not preclude
an actual triple on one line, weighted covers, or multi-direction arguments.

NEXT
Keep the frozen p23,H4 arbitrary-permutation query from session1105 as the
single discriminating test. A SAT witness would refute the template-height
conjecture (not the NTIL conjecture); checked UNSAT would support studying
multi-direction order constraints. No new size sweep. Ask for an independent
encoding or a genuinely nonlinear escape, with this cover-failure control.
