Euclidean gap reduction and finite OGM-G guarantees in the current interface.

theorem V7.euclideanGap : EuclideanGapStatement

theorem V7.finiteDataOGMG : FiniteDataOGMGStatement