Choosing the prime endpoint at the dimension root of the row count produces the exact rank power and leading constant in CCDN Proposition 3.2.6. The aggregation step takes the local prime-power divisors as a hypothesis, so it applies to minor gcds, determinant-family gcds and affine-chart reductions alike.

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

An explicit error depending only on hypersurface dimension.

Equations

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

noncomputable def CCDN.hypersurfaceRankLowerBound (n s d : ℕ) (c : ℝ) : ℝ

The rank form of the lower bound in CCDN Proposition 3.2.6 for s points on a hypersurface of degree d with bad-prime charge c: ((n+1)!)^(1/(n+1)) / (n+2) * s^(1+1/(n+1)) * (log s - (n+1) (4 log d + c) - E_n).

Equations

• CCDN.hypersurfaceRankLowerBound n s d c = CCDN.factorialRoot n / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) * (Real.log ↑s - (↑n + 1) * (4 * Real.log ↑d + c) - CCDN.hypersurfaceDeterminantError n)

theorem CCDN.hypersurface_log_lower_at_rank_of_local_divisors_congruence {n s d : ℕ} (hs : 0 < s) (hd : 0 < d) (bad P : Finset ℕ) (hPbad : P ⊆ bad) (hP : ∀ p ∈ P, Nat.Prime p) (v : ℕ → ℕ) {D : ℤ} (hD : 0 < D) (hlocal : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊↑s ^ (1 / (↑n + 1))⌋₊) \ bad, stepanovThreshold ↑d < ↑p → ∃ (e : ℕ), hypersurfaceDeterminantMain n s / (↑p + hypersurfaceCountConstant n * ↑d ^ 2 * √↑p) - (↑n + 2) * ↑s ≤ ↑e ∧ ↑p ^ e ∣ D) (hcong : ∀ p ∈ P, ↑p ^ v p ∣ D) : hypersurfaceRankLowerBound n s d (∑ p ∈ bad, Real.log ↑p / ↑p) + ∑ p ∈ P, ↑(v p) * Real.log ↑p ≤ Real.log ↑D

Prime aggregation at the rank endpoint x = s ^ (1 / (n + 1)). Local divisors of D with the hypersurface exponent at every good prime above 27 d ^ 4, together with prescribed divisors at the primes of P ⊆ bad, give the rank form of CCDN Proposition 3.2.6.

theorem CCDN.hypersurface_log_lower_at_rank_of_local_divisors {n s d : ℕ} (hs : 0 < s) (hd : 0 < d) (bad : Finset ℕ) {D : ℤ} (hD : 0 < D) (hlocal : ∀ p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊↑s ^ (1 / (↑n + 1))⌋₊) \ bad, stepanovThreshold ↑d < ↑p → ∃ (e : ℕ), hypersurfaceDeterminantMain n s / (↑p + hypersurfaceCountConstant n * ↑d ^ 2 * √↑p) - (↑n + 2) * ↑s ≤ ↑e ∧ ↑p ^ e ∣ D) : hypersurfaceRankLowerBound n s d (∑ p ∈ bad, Real.log ↑p / ↑p) ≤ Real.log ↑D

hypersurface_log_lower_at_rank_of_local_divisors_congruence without prescribed divisors.

theorem CCDN.hypersurface_determinant_log_lower_at_rank {n s N d M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → IntPoint (n + 3)) (hprim : ∀ (i : Fin s), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) (hrows : LinearIndependent ℚ ((Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j)).map Int.cast).row) (bad : Finset ℕ) (hred : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], p ∈ Finset.filter Nat.Prime (Finset.Ioc 0 ⌊↑s ^ (1 / (↑n + 1))⌋₊) \ bad → stepanovThreshold ↑d < ↑p → HasGoodReduction f p) : 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 i)) (F j)))

The higher-dimensional rank-cutoff form of Proposition 3.2.6 for maximal minors and common-degree homogeneous evaluation columns.