Documentation

LeanPool.CCDN.Projection.CurveDerivativeReconstruction

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) :

Differentiate a family of degree-d plane equations to reconstruct any linear source function using the same derivative denominator.