ADR-0012: Exact-zero and machine-zero evidence¶

Status: accepted Date: 2026-08-29

Decision¶

Exact-zero evidence, observed machine events, and threshold decisions are different types. Only PROVEN_ZERO from an exact expression or validated certificate may establish exact denominator-zero semantics. Floating denominator == 0 records a machine-zero event; it does not manufacture algebraic bottom. Underflow, subnormal values, signed zero, non-finite values, and rejection bands are reported separately.

Pure real sign4 has the exact truth table bottom -> bottom, negative -> -1, zero -> 0, positive -> +1. Projective orientation and complex unit phase have different signatures and modules.

Consequences¶

Strict decoding can return finite, bottom, ambiguous, rejected, fault, or representation-fault outcomes without overloading a single mask. Export that cannot preserve exact evidence must downgrade explicitly or refuse.