Exact finite-operation automation for Model

The exact-dyadic representation and checked finite-operation contracts are registered with the representation-independent numerics tactic. The runtime carrier remains Model fmt; the exact representation is a proof view used only by refinement.