Exact-to-floating refinement¶

Refinement is a bounded validation contract, not a proof that floating execution implements an unlimited exact theory. The implemented profiles cover CPU NumPy/PyTorch float64 elementwise add, subtract, multiply, and direct divide. Pure sign4, canonical projective normalization, and typed projective decoding exist as runtime operations, but are not advertised by the refinement profiles until specialized validators can express and check their distinct result contracts.

Inputs are embedded as exact binary dyadics. One-step arithmetic compares the observed result with the exact rational result under an explicit error bound. Explicit binary32 imports round to IEEE binary32 before exact conversion. Validation dispatches the operation through the profile's declared NumPy or CPU Torch float64 backend; an unavailable or undeclared backend is a typed refusal rather than relabeled Python arithmetic. Outcomes are REFINED, EXACT_BOTTOM, AMBIGUOUS, REFUSED, or NUMERICAL_FAULT; refusal and ambiguity cannot become bottom. Each executed operation records input machine-zero classifications and an output classification. In particular, a non-zero exact result that rounds to floating zero is UNDERFLOWED_TO_ZERO, never silently relabeled exact zero.

The profile records rounding, subnormal/overflow/underflow policies, operator fragment, error/status obligations, ambiguity/refusal caps, and gradient contract. NumPy declares no gradient. Strict masked Torch and the projective surrogate profile state different gradient obligations. Unsupported reductions, backends, devices, dtypes, or operators are typed refusals.