The kernel Hessian satisfies the explicit quadratic-form upper bound.

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.pairing_kernelHessian_eq {r theta : ℝ} {d : ℕ} (x e : Point d) : O3.pairing e ((S5ARepair.kernelHessian r theta x) e) = 4 * theta * (2 * theta / r - 1) * r * O3.lpPower r x ^ (2 * theta / r - 2) * O3.pairing (O3.powerDualityMap r x) e ^ 2 + 4 * theta * (r - 1) * O3.lpPower r x ^ (2 * theta / r - 1) * ∑ i : Fin d, |x i| ^ (r - 2) * e i ^ 2

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.kernelHessian_radial_nonpos {r theta : ℝ} (_hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x e : Point d) : 4 * theta * (2 * theta / r - 1) * r * O3.lpPower r x ^ (2 * theta / r - 2) * O3.pairing (O3.powerDualityMap r x) e ^ 2 ≤ 0

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.weighted_diagonal_bound {r theta : ℝ} (hr : 2 < r) {d : ℕ} (x e : Point d) (hx : x ≠ 0) : O3.lpPower r x ^ (2 * theta / r - 1) * ∑ i : Fin d, |x i| ^ (r - 2) * e i ^ 2 ≤ O3.lpNorm r x ^ (2 * theta - 2) * O3.lpNorm r e ^ 2

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.kernelHessian_quadratic_bound {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x e : Point d) : O3.pairing e ((S5ARepair.kernelHessian r theta x) e) ≤ 4 * theta * (r - 1) * O3.lpNorm r x ^ (2 * theta - 2) * O3.lpNorm r e ^ 2

The exact dimension-free Hessian quadratic bound used in the manuscript.