When a polynomial differential equation forces a straight line
One short identity says that a polynomial whose derivative is balanced against a second polynomial in a particular way can only be linear, and that rigidity is what closes a block in the strip reduction.
Take two polynomials in one variable, and , and form the combination
where is a positive integer. Suppose the result is a nonzero constant. What does that force?
For the combination is the Wronskian , the classical test for whether two functions are linearly independent. Asking for it to be a nonzero constant is a strong demand. The answer, for every , is surprisingly rigid: has to be linear or constant. No polynomial of degree two or more can appear.
A first look at the top terms
Write and , with leading coefficients and . The two products have the same degree:
Their leading coefficients are and . So the coefficient of in the combination is
If , this is nonzero, so the combination has degree exactly . A nonzero constant has degree zero, which forces . The only options are with , or with . Either way , which is the conclusion.
So the entire difficulty sits in one case: , where the top terms cancel and the degree count says nothing.
The identity that removes the hard case
Write . It is linear in . The useful fact is what it does to one particular input:
The combination annihilates . By linearity, we may subtract any multiple of from without changing the value at all:
Now the hard case takes care of itself. Suppose . The degree count already showed . Since , choosing cancels the leading term of , producing a with and the same value . If then , which is excluded. Otherwise , so the first argument applies and gives . That contradicts .
Every solution has to sit somewhere on this lattice. Off the dashed line the leading terms survive, so the degree must fall to zero and only is left. On the dashed line, subtracting a multiple of moves straight down off it without changing anything, so that case collapses into the first one. The two ringed points are all that remain.
That is the whole proof. It uses nothing beyond the degree of a product and one line of differentiation.
The statement
Theorem A. Let be an integral domain of characteristic zero, let be an integer, and let satisfy
Then .
This is formalized in Lean 4 and kernel-checked, and registered as PALOMAR-2026-08-19-000005.
Where the characteristic matters
The proof leans on being nonzero. Over a field of characteristic that step can fail, because can be a nonzero integer that is still zero in the field. Bounding both quantities below repairs it, and that is exactly the hypothesis of the positive-characteristic version: the same conclusion holds in characteristic provided and .
Some bound is genuinely necessary. Take , , and
In characteristic the derivative is , so
a nonzero constant, while . The theorem fails without a bound, and this example shows the bound is doing real work rather than being an artifact of the proof.
What it is used for
The identity is the rigidity engine in the depth-two block of the strip reduction at Newton-degree pair . Through the bridge from that block to the differential equation above, Theorem A forces the edge polynomial of a hypothetical Keller counterexample to be a binomial. A general polynomial edge has many coefficients to play with; a binomial has almost none. That collapse is what makes the surrounding argument finite.
Scope, and what is not claimed
The characteristic-zero statement is elementary, and for it is the classical fact that two polynomials with constant nonzero Wronskian cannot both be nonlinear. We do not claim the characteristic-zero case as new. What the campaign contributes here is an independent proof, the machine-checked formalization linked above, and the positive-characteristic extension with its bound. If you know a prior reference for the general statement, please send it and we will credit it here.
The block-variety theorem that consumes this result is a separate statement and is not formalized. The Lean development covers Theorem A only.
A question to take away
The positive-characteristic bound is sufficient, and the example shows some bound is needed. Is sharp? For the example sits exactly at , so nothing between is ruled out by it. A counterexample with , or a proof that none exists, would pin the statement down.