Saving one boundary degree at a shared affine origin

The degree-only plane-curve estimate bounds the zero/pole support of the two coordinate functions by adding their two support degrees. If the curve contains the affine origin, the finite place selected above that point lies in both supports. Since every place has positive degree, the union estimate saves at least one.

This argument does not assert that a branch above an arbitrary singular rational point has residue degree one. Positivity of the selected place degree is sufficient for the one-unit saving.

theorem BGS.CorvajaZannier.planeCurve_propositionTwoExceptionalPlaces_weightedDegree_add_one_le {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Finite K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (origin : AffinePlaneCurvePoint f) (horiginFirst : (↑origin).1 = 0) (horiginSecond : (↑origin).2 = 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have hx := ⋯; ∑ w ∈ propositionTwoExceptionalPlaces K (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n), finiteExtensionPlaceDegree K (PlaneCurveFunctionField f) w + 1 ≤ 2 * (MvPolynomial.degreeOf 0 f + MvPolynomial.degreeOf 1 f)

If an irreducible plane curve contains the affine origin, then the zero/pole boundary of positive powers of its two coordinate functions saves one degree compared with the disjoint-support estimate.

theorem BGS.CorvajaZannier.planeCurve_canonicalDifferent_add_propositionTwoExceptional_add_one_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) (origin : AffinePlaneCurvePoint f) (horiginFirst : (↑origin).1 = 0) (horiginSecond : (↑origin).2 = 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have hx := ⋯; finiteExtensionDivisorDegree K (PlaneCurveFunctionField f) (finiteExtensionCanonicalDifferentDivisor K (PlaneCurveFunctionField f) ⋯) + ∑ w ∈ propositionTwoExceptionalPlaces K (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n), ↑(finiteExtensionPlaceDegree K (PlaneCurveFunctionField f) w) + 1 ≤ ↑(2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)

Adding the canonical divisor preserves the one-unit saving from a common affine origin.