Goldbach numbers in intervals of length $4.45 \log^2 x$ under the Riemann Hypothesis

Assuming the Riemann Hypothesis, we prove that for every real $x \ge 3$ the interval $(x, x + 4.45 \log^2 x)$ contains an even integer that is a sum of two odd primes. The proof combines a weighted mean square bound for the Chebyshev prime counting error in short intervals with a piecewise linear weight in a bilinear identity for short interval prime counts. The deduction is checked in Lean 4 conditionally on the explicit formula ExplicitA, the zero sum bound HadamardK, the zero count BPTN, the HSW zero counts, the bound $|\gamma| \ge 14$, and the Goldbach verification to $4 \cdot 10^{18}$, all stated as hypotheses.