In characteristic zero, a plane relation with a transcendental first coordinate has a nonzero derivative in the second coordinate. That derivative is a proper section of degree at most d-1 of the source curve.
theorem
CCDN.projection_derivative_proper
{K : Type u_1}
{τ : Type u_2}
[Field K]
[CharZero K]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
(a : Fin 2 → MvPolynomial τ K)
(ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1)
(f : MvPolynomial (Fin 2) K)
(hf : f ≠ 0)
(hker : ∀ (g : MvPolynomial (Fin 2) K), (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g)
(j k : Fin 2)
(hjk : j ≠ k)
(hj : Transcendental K ((Ideal.Quotient.mk I) (a j)))
:
(MvPolynomial.aeval a) ((MvPolynomial.pderiv k) f) ∉ I ∧ ((MvPolynomial.aeval a) ((MvPolynomial.pderiv k) f)).totalDegree ≤ f.totalDegree - 1
The derivative is a proper degree-(d-1) section when f generates the projection kernel. This is the proposed common reconstruction cut.