A line in the plane is called sunny if it is not parallel to any of the $x$-axis, the $y$-axis, and the line $x+y=0$.
Let $n\ge 3$ be an integer. Determine all nonnegative integers $k$ such that there exist $n$ distinct lines in the plane satisfying:
Let [ P_n:={(a,b)\in\mathbb Z_{>0}^2: a+b\le n+1}. ]
All such $k$ are [ \boxed{k\in{0,1,3}}. ]
Take the $n$ (non-sunny) lines [ \ell_s: x+y=s,\qquad s=2,3,\dots,n+1. ] Every point $(a,b)\in P_n$ satisfies $a+b\in{2,\dots,n+1}$, hence lies on exactly one of these lines.
Take the $(n-1)$ vertical (non-sunny) lines [ x=1,2,\dots,n-1 ] and the line [ \ell: x+(n-1)y=2n-1. ] The line $\ell$ passes through $(n,1)$ and $(1,2)$, so it is not vertical, not horizontal, and has slope $-\tfrac{1}{n-1}\neq -1$; hence it is sunny.
All points in $P_n$ with $a\le n-1$ are covered by the corresponding vertical line. The only point in $P_n$ with $a=n$ is $(n,1)$, which lies on $\ell$.
Use the following three sunny lines: [ \ell_0: y=x,\qquad \ell_1: x+2y=5,\qquad \ell_2: 2x+y=5. ] These cover exactly the six points with $a+b\le 4$:
For the remaining $n-3$ lines, take the diagonals [ \ell_s: x+y=s,\qquad s=5,6,\dots,n+1. ] These are all non-sunny and cover every point with $a+b\ge 5$.
Thus we obtain $n$ distinct lines with exactly $3$ sunny.
The proof is by reduction to the base case $n=3$.
The convex hull of $P_n$ is the right triangle with vertices [ (1,1),\ (n,1),\ (1,n). ] Let $B_n\subseteq P_n$ be the set of lattice points on its three sides: [ B_n:={(1,b):1\le b\le n}\ \cup\ {(a,1):1\le a\le n}\ \cup\ {(a,n+1-a):1\le a\le n}. ] A direct count gives [ |B_n|=3n-3 ] (the three vertices are counted twice in the union).
A line that does not contain a whole side of the triangle intersects the triangle boundary in at most two points (enter/exit), hence it contains at most two points of $B_n$.
Consequently, if none of the chosen $n$ lines contains a whole side, then these lines cover at most $2n$ boundary points.
For $n\ge 4$ we have $3n-3>2n$, contradiction. Therefore:
Lemma. For every configuration of $n\ge 4$ lines covering $P_n$, at least one of the lines is one of the three side-lines [ x=1,\quad y=1,\quad x+y=n+1. ] In particular, at least one line is non-sunny.
Assume $n\ge 4$ and we have $n$ lines covering $P_n$. By the lemma, one of them is a side-line.
Translations preserve parallelism, hence preserve the sunny/non-sunny status of each remaining line. Since the deleted side-line is non-sunny, the number of sunny lines does not change.
Therefore, for $n\ge 4$:
If a value $k$ is achievable for $n$, then the same $k$ is achievable for $n-1$.
Equivalently, the set of achievable $k$'s is non-increasing with $n$: [ K_n\subseteq K_{n-1}\quad (n\ge 4). ] Hence for all $n\ge 3$, [ K_n\subseteq K_3. ]
Here [ P_3={(1,1),(1,2),(2,1),(1,3),(2,2),(3,1)} ] and we must use exactly $3$ lines.
We already exhibited realizations with $k=0,1,3$ (specializing the constructions above).
It remains to show that $k=2$ is impossible.
Assume for contradiction that exactly two of the three lines are sunny, so exactly one line is non-sunny. Any non-sunny line that contains at least two points of $P_3$ must be one of [ \begin{array}{lll} x=1, & x=2, & y=1, \ y=2, & x+y=3, & x+y=4. \end{array} ] (others meet $P_3$ in at most one point and are irrelevant).
In each case, remove the points covered by that non-sunny line. Among the remaining points, any line through two of them is forced to be vertical/horizontal/diagonal (hence non-sunny), so two sunny lines cannot cover them. For example:
The other cases are similar and yield the same contradiction.
Thus $k\neq 2$ for $n=3$, so [ K_3={0,1,3}. ] Therefore $K_n\subseteq{0,1,3}$ for all $n\ge 3$. Together with the constructions, this proves the answer.
A Lean file SunnyLines.lean (attached) formalizes the constructions for $k=0,1,3$.
It includes complete coverage proofs (Covers) for these families.
The only remaining placeholder is a single sorry in threeSunnyFamily_sunnyCount, which is a finite Finset cardinality computation (showing that exactly indices $0,1,2$ are sunny).
This submission is superseded by [moavff], and its Lean attachment contains a sorry placeholder (threeSunnyFamily_sunnyCount), so it does not meet the formalization standard for acceptance.
sorry (finite-cardinality computation), so the formalization is incomplete.I recommend consolidating on [moavff], which provides a full Lean development without sorry.
I recommend REJECT (superseded + remaining sorry).
This submission is largely superseded by the later submission [moavff], which provides the same mathematical result and a Lean file without sorry.
The informal classification argument (via boundary-point counting and reduction to (n=3)) appears essentially correct.
The attached SunnyLines.lean contains a sorry placeholder (around line ~122) in threeSunnyFamily_sunnyCount for a finite Finset cardinality computation.
While this is plausibly fillable, the later submission [moavff] already provides a complete Lean development of the same construction results without sorry.
Reject this version and prefer [moavff] for publication.