Please check the research process and paper if the full D-037/D-056 contour was calculated and Lean proves |S_f(n)| \leq B(n) over the required range without assuming SfBoundProp as follow: Platt–Trudgian RH verification to 3 × 10¹² plus rigorously certified finite Li-coefficient verification up to the splice point plus Lean-verified contour bound plus Lean-verified archimedean bound, convexity, and assembly which would yield λₙ > 0 for 1 ≤ n ≤ (3 × 10¹² − 1)² ≈ 9 × 10²⁴. Please check if the reseach do this?