A computer assisted existence proof for a non-Schwarzschild black hole in Einstein--Weyl gravity

Static, asymptotically flat, non-Schwarzschild black holes in four-dimensional Einstein--Weyl gravity have previously been constructed by numerical shooting, while the local field equations admit horizon and asymptotic expansions to all orders. We give a computer assisted existence proof for a non-Schwarzschild solution whose dimensionless horizon radius is one in units of the massive spin-two scale, with parameters close to the previously reported numerical branch. The exterior is divided into a convergent horizon series domain, a compact core enclosed by a parameter dependent Taylor model with directed rounding, and an infinite asymptotic domain treated as a centered stable manifold fixed point problem. The resulting five-dimensional matching map between the core and tail is continuous on a rigorously specified box. After exact rational preconditioning, the signs on opposite faces satisfy the hypotheses of the Poincaré--Miranda theorem and therefore certify a matching zero. The solution has a regular nondegenerate horizon, no additional exterior horizon, vanishing Ricci scalar, and nonvanishing Ricci tensor. The proof establishes existence, but not uniqueness of the matching zero.