A bounded geometrically good plane whose three parameter columns have an invertible minor in three selected ambient coordinates. This additional condition allows an effective containing hyperplane to be constructed.

theorem CCDN.exists_integer_good_plane_with_anchor {n : ℕ} (f : MvPolynomial (Option (Fin (3 + n))) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) : ∃ (v : PlaneParameters (Option (Fin (3 + n))) → ℤ), (∀ (p : PlaneParameters (Option (Fin (3 + n)))), 0 ≤ v p ∧ v p ≤ 2 * ↑f.totalDegree ^ 3 + 3) ∧ (Matrix.of fun (i j : Fin 3) => v (some (Fin.castAdd n i), j)).det ≠ 0 ∧ ((bivariateMap (Int.castRingHom (AlgebraicClosure ℚ))) (universalPlaneSection f v)).natDegree = f.totalDegree ∧ bivariateTotalDegree ((bivariateMap (Int.castRingHom (AlgebraicClosure ℚ))) (universalPlaneSection f v)) = f.totalDegree ∧ Irreducible ((bivariateMap (Int.castRingHom (AlgebraicClosure ℚ))) (universalPlaneSection f v))

The extra determinant condition costs only three in the integer grid size.