Equilibrated-flux residual certification for verified existence and outputs

We present a post-processing certification workflow for nonlinear elliptic boundary value problems that upgrades a standard finite element computation to a rigorous existence and output certificate. For a given approximate discrete state, we verify existence and local uniqueness of a weak solution in a computable neighbourhood via a Newton–Kantorovich argument based on three certified ingredients: a guaranteed dual-norm residual bound, a computable lower bound for the stability constant of the linearised operator, and a Lipschitz bound for the derivative on the verification ball. The residual bound is obtained by an equilibrated-flux reconstruction exploiting an explicit relation between nonconforming and mixed formulations, yielding $H(\mathrm{d}\mathrm{i}\mathrm{v})$-conforming fluxes without local mixed solves. The stability ingredient follows from a computable coercivity lower bound for the linearisation. An admissible verification radius is selected by a simple bracketing–bisection search, justified for an affine Lipschitz model. Once the verification ball is certified, we derive guaranteed enclosures for quantities of interest using computable variation bounds; an adjoint-based correction, in the spirit of goal-oriented error estimation, tightens these intervals while retaining full rigour. Numerical experiments for semilinear diffusion–reaction models show that the certificates are informative and that the adjoint enhancement substantially reduces enclosure widths.