The gcd divisor is controlled by the poles of the one-minus quotient.

theorem BGS.CorvajaZannier.gcdMultiplicity_add_outsidePole_le_secondPositivePart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (S : Finset (FiniteExtensionPlace K L)) (Du Dv Drho : FiniteExtensionPlace K L → ℤ) (P : FiniteExtensionPlace K L) (hRho : Drho P = Du P - Dv P) (hOutside : P ∉ S → 0 ≤ Du P ∧ 0 ≤ Dv P) (hInside : P ∈ S → min (Du P) (Dv P) ≤ 0) : ((min (Du P) (Dv P)).toNat + if P ∉ S ∧ Drho P < 0 then (Drho P).natAbs else 0) ≤ (Dv P).toNat

The local integer identity behind the Corvaja--Zannier comparison between the gcd divisor and the pole height of (1-u)/(1-v).

theorem BGS.CorvajaZannier.finiteExtensionGcdWeightedDegree_add_outsideHeight_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y rho : L) (S : Finset (FiniteExtensionPlace K L)) (hRho : ∀ (P : FiniteExtensionPlace K L), (finiteExtensionPrincipalDivisor K L rho) P = (finiteExtensionPrincipalDivisor K L x) P - (finiteExtensionPrincipalDivisor K L y) P) (hOutside : ∀ P ∉ S, 0 ≤ (finiteExtensionPrincipalDivisor K L x) P ∧ 0 ≤ (finiteExtensionPrincipalDivisor K L y) P) (hInside : ∀ P ∈ S, min ((finiteExtensionPrincipalDivisor K L x) P) ((finiteExtensionPrincipalDivisor K L y) P) ≤ 0) : finiteExtensionGcdWeightedDegree K L x y + finiteExtensionOutsideHeight K L rho S ≤ finiteExtensionPositiveDegree K L y

If the local order of rho is the difference of the two one-minus orders, those one-minus orders are nonnegative off S, and their minimum is nonpositive on S, then gcd degree plus outside pole height is bounded by the positive degree of the second one-minus function.