The logarithmic Gauss direction of a plane curve

The logarithmic partial X_i * ∂_i f has exactly the same monomial support as a subpolynomial of f. Consequently a scalar relation between the two logarithmic partials forces every support exponent to lie on one affine line in the constant field.

If the support has a nonzero rank-two determinant and the characteristic is larger than the public Euler budget, that determinant stays nonzero in the constant field. Hence the logarithmic Gauss ratio cannot be constant on the curve. This isolates the high-characteristic input needed by the logarithmic-Gauss route to the powered-image index bound.

noncomputable def BGS.CorvajaZannier.planeCurveLogarithmicPDeriv {K : Type u_1} [Field K] (i : Fin 2) (f : MvPolynomial (Fin 2) K) : MvPolynomial (Fin 2) K

The logarithmic partial derivative X_i * ∂_i f.

Equations

• BGS.CorvajaZannier.planeCurveLogarithmicPDeriv i f = MvPolynomial.X i * (MvPolynomial.pderiv i) f

theorem BGS.CorvajaZannier.coeff_planeCurveLogarithmicPDeriv {K : Type u_1} [Field K] (i : Fin 2) (f : MvPolynomial (Fin 2) K) (m : Fin 2 →₀ ℕ) : (planeCurveLogarithmicPDeriv i f).coeff m = ↑(m i) * f.coeff m

noncomputable def BGS.CorvajaZannier.planeCurveLogarithmicDirection {K : Type u_1} [Field K] (a b : K) (f : MvPolynomial (Fin 2) K) : MvPolynomial (Fin 2) K

A constant linear combination of the two logarithmic partials.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.CorvajaZannier.coeff_planeCurveLogarithmicDirection {K : Type u_1} [Field K] (a b : K) (f : MvPolynomial (Fin 2) K) (m : Fin 2 →₀ ℕ) : (planeCurveLogarithmicDirection a b f).coeff m = (a * ↑(m 0) + b * ↑(m 1)) * f.coeff m

theorem BGS.CorvajaZannier.support_planeCurveLogarithmicDirection_subset {K : Type u_1} [Field K] (a b : K) (f : MvPolynomial (Fin 2) K) : (planeCurveLogarithmicDirection a b f).support ⊆ f.support

theorem BGS.CorvajaZannier.degreeOf_planeCurveLogarithmicDirection_le {K : Type u_1} [Field K] (a b : K) (f : MvPolynomial (Fin 2) K) (i : Fin 2) : MvPolynomial.degreeOf i (planeCurveLogarithmicDirection a b f) ≤ MvPolynomial.degreeOf i f

theorem BGS.CorvajaZannier.planeCurveLogarithmicDirection_eq_C_mul_of_dvd {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : f ≠ 0) (a b : K) (hQ : planeCurveLogarithmicDirection a b f ≠ 0) (hdvd : f ∣ planeCurveLogarithmicDirection a b f) : ∃ (d : K), planeCurveLogarithmicDirection a b f = MvPolynomial.C d * f

A nonzero logarithmic direction divisible by f is only a constant multiple of f; the coordinate degree bounds force the quotient to be constant.

theorem BGS.CorvajaZannier.planeCurveSupportDifferenceDet_cast_ne_zero_of_lt_char {K : Type u_1} [Field K] {p : ℕ} [CharP K p] {r s t : Fin 2 →₀ ℕ} (hdet : planeCurveSupportDifferenceDet r s t ≠ 0) (hlt : (planeCurveSupportDifferenceDet r s t).natAbs < p) : ↑(planeCurveSupportDifferenceDet r s t) ≠ 0

theorem BGS.CorvajaZannier.no_logarithmicPDeriv_scalar_relation_of_supportRankTwo {K : Type u_1} [Field K] {p : ℕ} [CharP K p] {f : MvPolynomial (Fin 2) K} (hrank : PlaneCurveSupportHasRankTwo f) (hlarge : 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p) : ¬∃ (c : K) (d : K), planeCurveLogarithmicPDeriv 0 f = MvPolynomial.C c * planeCurveLogarithmicPDeriv 1 f + MvPolynomial.C d * f

Rank-two support excludes a scalar logarithmic-Gauss relation in characteristic larger than the support determinant budget.

theorem BGS.CorvajaZannier.eval_planeCurveLogarithmicDirection_ne_zero_of_supportRankTwo {K : Type u_1} [Field K] {p : ℕ} [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hrank : PlaneCurveSupportHasRankTwo f) (hlarge : 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p) (c : K) : MvPolynomial.eval₂ (algebraMap K (PlaneCurveFunctionField f)) (planeCurveFunction f) (planeCurveLogarithmicDirection 1 (-c) f) ≠ 0

On an irreducible curve with rank-two support, no constant can be the logarithmic Gauss ratio in the high-characteristic range.