The exact-rank Bombieri--Vaaler comparison when no integral auxiliary polynomial exists. This is the finite-matrix step of CCDN §3.3.

The arithmetic point is that a nonzero integer multiplier has a leading coefficient of absolute value at least one. This is the coefficient obstruction used in CCDN §3.3. The determinant bound needed to make the auxiliary polynomial small enough remains separate.

theorem CCDN.exists_small_homogeneous_vanishing_polynomial {n d M t : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hdM : d ≤ M) (points : Fin t → Fin (n + 1) → ℤ) (hzero : ∀ (i : Fin t), (MvPolynomial.eval (points i)) f = 0) : ∃ (s : ℕ) (a : Fin s → Fin t), Function.Injective a ∧ s < (n + M).choose M ∧ s + (n + (M - d)).choose (M - d) ≤ (n + M).choose M ∧ LinearIndependent ℚ ((evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).map Int.cast).row ∧ Submodule.span ℚ (Set.range ((evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).map Int.cast).row) = Submodule.span ℚ (Set.range ((evaluationMatrix (homogeneousMonomials n M) points).map Int.cast).row) ∧ ∃ (g : MvPolynomial (Fin (n + 1)) ℤ), g ≠ 0 ∧ g.IsHomogeneous M ∧ (∀ (i : Fin t), (MvPolynomial.eval (points i)) g = 0) ∧ CoefficientHeightLE g ((√↑(evaluationMatrix (homogeneousMonomials n M) (points ∘ a) * (evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).transpose).det / ↑(Int.Matrix.minorGcd (evaluationMatrix (homogeneousMonomials n M) (points ∘ a)))) ^ (↑((n + M).choose M) - ↑s)⁻¹)

A homogeneous equation yields a small homogeneous polynomial vanishing at every given integral point.

theorem CCDN.homogeneous_no_auxiliary_comparison {n d M t : ℕ} (order : MonomialOrder (Fin (n + 1))) (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hdM : d ≤ M) (points : Fin t → Fin (n + 1) → ℤ) (hzero : ∀ (i : Fin t), (MvPolynomial.eval (points i)) f = 0) (hrel : ∀ (g : MvPolynomial (Fin (n + 1)) ℤ), g.IsHomogeneous M → (∀ (i : Fin t), (MvPolynomial.eval (points i)) g = 0) → f ∣ g) : ∃ (s : ℕ) (a : Fin s → Fin t), Function.Injective a ∧ s < (n + M).choose M ∧ s + (n + (M - d)).choose (M - d) = (n + M).choose M ∧ LinearIndependent ℚ ((evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).map Int.cast).row ∧ |↑(order.leadingCoeff f)| ≤ (√↑(evaluationMatrix (homogeneousMonomials n M) (points ∘ a) * (evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).transpose).det / ↑(Int.Matrix.minorGcd (evaluationMatrix (homogeneousMonomials n M) (points ∘ a)))) ^ (↑((n + M).choose M) - ↑s)⁻¹

Without an auxiliary polynomial, selected rows have exact Hilbert rank and their Bombieri--Vaaler bound is at least the leading coefficient.

theorem CCDN.log_gcd_le_of_coefficient_bound {L G D k : ℝ} (hL : 0 < L) (hD : 0 < D) (hk : 0 < k) (hbound : L ≤ (√G / D) ^ k⁻¹) : 0 < G ∧ Real.log D ≤ Real.log G / 2 - k * Real.log L

Logarithmic form of the coefficient obstruction. Positivity of the Gram determinant follows from the positive coefficient bound itself.

theorem CCDN.evaluation_log_gram_le {n N s M : ℕ} (hN : 0 < N) (mon : Fin N → Fin n →₀ ℕ) (points : Fin s → Fin n → ℤ) {B : ℝ} (hB : 1 ≤ B) (hp : ∀ (i : Fin s), InBox (points i) B) (hdeg : ∀ (j : Fin N), Finsupp.degree (mon j) ≤ M) (hG : 0 < ↑(evaluationMatrix mon points * (evaluationMatrix mon points).transpose).det) : Real.log ↑(evaluationMatrix mon points * (evaluationMatrix mon points).transpose).det / 2 ≤ Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑N + ↑s * ↑M * Real.log B

Archimedean logarithmic bound for an integral evaluation matrix.

theorem CCDN.homogeneous_no_auxiliary_box_comparison {n d M t : ℕ} (order : MonomialOrder (Fin (n + 1))) (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hdM : d ≤ M) (points : Fin t → Fin (n + 1) → ℤ) (hzero : ∀ (i : Fin t), (MvPolynomial.eval (points i)) f = 0) {B : ℝ} (hB : 1 ≤ B) (hp : ∀ (i : Fin t), InBox (points i) B) (hrel : ∀ (g : MvPolynomial (Fin (n + 1)) ℤ), g.IsHomogeneous M → (∀ (i : Fin t), (MvPolynomial.eval (points i)) g = 0) → f ∣ g) : ∃ (s : ℕ) (a : Fin s → Fin t), Function.Injective a ∧ s < (n + M).choose M ∧ s + (n + (M - d)).choose (M - d) = (n + M).choose M ∧ LinearIndependent ℚ ((evaluationMatrix (homogeneousMonomials n M) (points ∘ a)).map Int.cast).row ∧ Real.log ↑(Int.Matrix.minorGcd (evaluationMatrix (homogeneousMonomials n M) (points ∘ a))) ≤ Real.log ↑s.factorial / 2 + ↑s / 2 * Real.log ↑((n + M).choose M) + ↑s * ↑M * Real.log B - (↑((n + M).choose M) - ↑s) * Real.log |↑(order.leadingCoeff f)|

The archimedean half of the determinant-method inequality, for bounded integer points and exact Hilbert rank.