Bounded integral linear forms dual to independent integer rows. A nonzero minor and its cofactors give the separation required in CCDN Lemma 5.4, with the bound s! T^s for s+1 independent equations.

theorem CCDN.exists_bounded_integer_dual_rows {s r : ℕ} (A : Matrix (Fin (s + 1)) (Fin r) ℤ) (hli : LinearIndependent ℚ fun (i : Fin (s + 1)) (j : Fin r) => ↑(A i j)) (T : ℕ) (hA : ∀ (i : Fin (s + 1)) (j : Fin r), |A i j| ≤ ↑T) : ∃ (D : ℤ), D ≠ 0 ∧ |D| ≤ ↑(s + 1).factorial * ↑T ^ (s + 1) ∧ ∃ (b : Fin (s + 1) → Fin r → ℤ), (∀ (i ℓ : Fin (s + 1)), ∑ j : Fin r, A ℓ j * b i j = if ℓ = i then D else 0) ∧ ∀ (i : Fin (s + 1)) (j : Fin r), |b i j| ≤ ↑s.factorial * ↑T ^ s

A full independent family admits simultaneous bounded integral dual forms.

theorem CCDN.exists_bounded_row_separator {s r : ℕ} (A : Matrix (Fin (s + 1)) (Fin r) ℤ) (hli : LinearIndependent ℚ fun (i : Fin (s + 1)) (j : Fin r) => ↑(A i j)) (T : ℕ) (hA : ∀ (i : Fin (s + 1)) (j : Fin r), |A i j| ≤ ↑T) (i : Fin (s + 1)) : ∃ (b : Fin r → ℤ), ∑ j : Fin r, A i j * b j ≠ 0 ∧ (∀ (ℓ : Fin (s + 1)), ℓ ≠ i → ∑ j : Fin r, A ℓ j * b j = 0) ∧ ∀ (j : Fin r), |b j| ≤ ↑s.factorial * ↑T ^ s

A valid factorial cofactor bound for the separation conclusion of CCDN Lemma 5.4. The different numerical constant printed in that lemma is refuted in CCDNPaper/Counterexample/RowSeparatorConstant.lean.