A certified above-two local trial yields the known-parameter upper query bound.

theorem V7.Stage5AboveTwoLowerS5F.knownParameterAboveTwoUpper : KnownParameterAboveTwoUpperStatement

theorem V7.knownParameterAboveTwoUpper : KnownParameterAboveTwoUpperStatement