Boolean rules for numerical automation

Symbolic proofs select the exact Boolean operation contracts. Closed reduction unfolds only the small native kernels.