Exact and machine zero evidence¶

ZeroEvidence records three independent observations: exact evidence, the machine event, and the threshold decision. PROVEN_ZERO requires an exact expression or certificate identity. Floating equality to zero records MachineZeroEvent.ZERO; it never proves algebraic bottom.

The supported float profiles distinguish nonzero, zero, subnormal, underflow-to-zero (when the exact source is available), and non-finite events. Signed IEEE zero is recorded and canonicalized to public positive zero. Threshold calibration can change only the operational decision; it cannot upgrade exact evidence.

Export targets that cannot carry exact evidence must refuse the semantic ABI or record explicit absence. They may not invent a certificate.

For tensor operations, raw integer status arrays are not trusted provenance. Any tensor containing PROVEN_ZERO must be constructed from ExactZeroTensorEvidence with a source and certificate-manifest identity. Device or dtype transfer preserves that typed evidence. Passing the ExactZeroEvidence.PROVEN_ZERO enum directly to tensor decoding is refused. Evidence arrays are copied on admission and carry a retained integrity digest; mutation of stored evidence fails closed before arithmetic.