The below-two dual phase terminal gradient bound from the residual identity.

theorem V7.belowTerminalGradient : BelowTerminalGradientStatement