Documentation

LeanPool.CCDN.Projection.PlaneProjectionDerivative

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

The derivative is a proper degree-(d-1) section when f generates the projection kernel. This is the proposed common reconstruction cut.