MATHEMATICAL VERIFICATION RECORD | October 17, 2026

1. The theta normalization is obtained by direct substitution in the complete
   density, with the e^(5t/2) factors canceled in the product before differentiation.
2. The R_k recurrence follows from differentiating the drift-free summand.
   The C_k formula is its x derivative, including the derivative of its weight.
3. Both infinite tails use an upper ratio (9/8)^26 exp(-17x). The exponent 26
   includes the additional n^2 from center differentiation. All polynomial
   coefficient absolute values enter the tail majorants.
4. Complete B_k and C_k intervals are multiplied before normalization; no
   finite-tail or tail-tail interaction is omitted. B_0 excludes zero.
5. Whole-cell interval evaluation proves S'>3e9 and positivity of the leading
   odd and full even blocks on a gap-free cover of [3.64,3.66].
6. Exact-rational endpoint signs bracket one root. Strict monotonicity proves
   its uniqueness in that interval. Neither midpoint sampling nor a numerical
   root finder is used as a sign certificate.
7. Even/odd parity splits M_5 into E and H. The Schur congruence splits H into
   G and S. E>0 and G>0 exclude every degree <=4 obstruction, including even
   quartics and mixed-parity polynomials. Thus degree five is minimal exactly
   on the negative side of the certified transition within the interval.
8. At the root S=0, the form is positive semidefinite, not negative. Above it,
   the result excludes degree <=5 obstructions, not higher-degree obstructions.
9. Rational rounding is controlled by the exact completed-square identity.
   The adaptive existence/termination argument is distinct from the supplied
   fixed-precision implementation.
10. The finite-difference congruence uses mixed derivatives of p(u-v), with
    phase diag(1,i,...,i^5), to transfer a negative moment direction to a
    six-point translation Gram for sufficiently small positive spacing.

Numerical evidence was replayed with Decimal and exact Fraction interval
arithmetic. The rational replay shares the moment assembly but uses separate
arithmetic primitives and an alternative determinant derivative. The retained
ordered-pair center program uses a different central derivative expansion.
These checks do not constitute independent external peer review.
