Preserve the bad-prime factor through the normalized no-auxiliary comparison, as required by the coefficient-sensitive CCDN Theorem 3.1.1.

AuxiliaryRankComparison order f d z bad is the conclusion of the comparison for a finite prime set bad. It follows from a determinant lower bound with the charge of bad for every subfamily of the points (auxiliaryRankComparison_of_determinant_lower); the hypersurface instance uses the exact geometric bad-prime set.

noncomputable def CCDN.hypersurfaceBadPrimeNormalizedError (n : ℕ) : ℝ

The dimension-dependent error term in the normalized no-auxiliary comparison that retains the bad-prime charge, for forms in n + 3 variables: the determinant error plus the archimedean error normalized by $(n + 2) / ((n + 1)!)^{1/(n + 1)}$.

Equations

• CCDN.hypersurfaceBadPrimeNormalizedError n = CCDN.hypersurfaceDeterminantError n + (↑n + 2) * CCDN.hypersurfaceArchimedeanError (n + 1) / ↑(n + 1).factorial ^ (1 / (↑n + 1))

def CCDN.AuxiliaryRankComparison {n t : ℕ} (order : MonomialOrder (Fin (n + 3))) (f : MvPolynomial (Fin (n + 3)) ℤ) (d : ℕ) (z : Fin t → IntPoint (n + 3)) (bad : Finset ℕ) : Prop

The normalized no-auxiliary comparison with the charge of a finite prime set bad: for every radius B ≥ 1 bounding the points z and every degree M ≥ d in which each form vanishing on z is a multiple of f, the rank s of the evaluation matrix satisfies the normalized comparison retaining log b = ∑ p ∈ bad, log p / p.

Equations

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

theorem CCDN.auxiliaryRankComparison_of_determinant_lower {n d t : ℕ} (order : MonomialOrder (Fin (n + 3))) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 0 < d) (z : Fin t → IntPoint (n + 3)) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) (bad : Finset ℕ) (hdet : ∀ ⦃s N M : ℕ⦄ (a : Fin s → Fin t) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ), 0 < s → (∀ (j : Fin N), (F j).IsHomogeneous M) → LinearIndependent ℚ ((Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z (a i))) (F j)).map Int.cast).row → hypersurfaceRankLowerBound n s d (∑ p ∈ bad, Real.log ↑p / ↑p) ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z (a i))) (F j)))) : AuxiliaryRankComparison order f d z bad

The comparison follows from the rank-form determinant lower bound with the charge of bad, for every subfamily of the points and every family of common-degree forms.

theorem CCDN.hypersurface_auxiliaryRankComparison {n d t : ℕ} (order : MonomialOrder (Fin (n + 3))) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hd : 0 < d) (z : Fin t → IntPoint (n + 3)) (hprim : ∀ (i : Fin t), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) (bad : Finset ℕ) (hbad : ∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) : AuxiliaryRankComparison order f d z bad

The comparison retaining log b(f) for the exact geometric bad-prime set, rather than replacing it by the coefficient-height upper bound.