Executable numerical-operation contracts

Numerical-operation contracts provide arity-neutral relations, named unary/binary/ternary forms, standard total and checked semantics, proof-indexed application helpers, and composition laws. All contracts are propositions, so optimized runtime kernels retain their concrete monomorphic function signatures.