A degree-preserving linear plane projection admits reconstruction using the partial derivative of its image equation. This bounds the common denominator's degree by d-1 without normalization or a genus formula.
The constant and first-order equations of a polynomial family of plane relations, expressed as equations in the target algebra.
theorem
CCDN.exists_derivative_reconstruction
{K : Type u_1}
{τ : Type u_2}
[Field K]
[CharZero K]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
[I.IsPrime]
(a : Fin 2 → MvPolynomial τ K)
(ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1)
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
(hu : Transcendental K ((Ideal.Quotient.mk I) (a 0)))
(f : MvPolynomial (Fin 2) K)
(hf : f ≠ 0)
(hfd : f.totalDegree = d)
(hker : ∀ (g : MvPolynomial (Fin 2) K), (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g)
(l : MvPolynomial τ K)
(hl : l.totalDegree ≤ 1)
:
∃ (P : MvPolynomial (Fin 2) K),
P.totalDegree ≤ d ∧ (MvPolynomial.aeval a) ((MvPolynomial.pderiv 1) f) * l - (MvPolynomial.aeval a) P ∈ I
Differentiate a family of degree-d plane equations to reconstruct any linear source function using the same derivative denominator.