Correctly Rounded or Refused: Toward a Certified Numerical Contract for the Paired Student-t Test in IEEE Binary64

We propose a three-valued result contract for the paired (one-sample) Student-t test in IEEE binary64, normative over the test's binary64 summary statistics and scoped to integer degrees of freedom df <= 30 (a versioned engineering bound): every returned quantity carries a status — exact_rounding_proved (the value is proven to be the correct rounding of the exact result), certified_interval_only (a certified outward-rounded enclosure), or refused (an explicit, reason-coded refusal). Three empirical studies ground the contract. (1) Adversarial benchmarks of two mainstream implementations — SciPy's Boost.Math-backed Student-t functions, and R's independently written pt/qt on the identical sampled inputs — against a defended 200-bit oracle: the SciPy CDF is correctly rounded on 55–81% of sampled inputs (misses mostly 1–2 ulp, ordinary for a fast library), but the benchmark also exposes genuine defects — a quantization plateau near t = 0 with errors up to 10^7 ulp (a known upstream regression we independently reproduce and quantify), quantile errors reaching the 10^3–10^5 ulp range, and wrong-signed infinite quantiles in the deep tail — that a value-only interface cannot signal; the R implementation exhibits neither defect class yet posts lower CDF correct-rounding rates and a quiet deep-tail accuracy cliff of its own — even two implementations of one algorithm family break in different places, and neither can say where. (2) A hardness analysis separating what is blocked at which scope: a-priori full-domain rounding guarantees face a bivariate Table Maker's Dilemma at general degrees of freedom, and per-df worst-case search volumes at this contract's fixed integer degrees of freedom; per-call certification faces neither. (3) Prototypes of per-call certification built on Arb ball arithmetic: every sampled input certified on all four tail surfaces — including log p and t = 0 — with no worst-case tables, every exported certification witness re-verified independently on GNU MPFR through integer-df closed forms, and confidence-interval endpoints certified through a rigorously verified sub-ulp quantile bracket, while the ordinary double composition collapses under cancellation and forced certification failure degrades to the enclosure status, never to a wrong certificate. Worst-case tables are demoted to an optional device for a-priori latency bounds. The archive bundles the paper (CC-BY-4.0), the complete pilot implementation with raw results (MIT), a tiered reproduction harness (reproduce.sh: verify / smoke / full), and a machine-checked validation suite: a computer-algebra proof of the closed forms used by the MPFR re-verification, property tests of the directed-rounding interval layer, bit-exact input-stream identity checks between the two benchmarked implementations, and an independent re-scoring of every stored worst-case record. Both defect classes and all certification results were additionally reproduced on a second platform (macOS / Apple Silicon), where correct-rounding rates shift by a few percentage points while the certification legs are unchanged.