Refinement of format-parameterized binary arithmetic

The executable model operations agree with the independent descriptor-aware specifications for every validated FloatFormat.

These theorems connect the arithmetic dispatchers to the format's specifications before a result is transported to configured storage. Each dispatcher proof covers its optimized backends and generic fallback.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.add_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.add y = Spec.add x y

Public addition agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.sub_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.sub y = Spec.sub x y

Public subtraction agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.mul_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.mul y = Spec.mul x y

Public multiplication agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.div_eq_spec {fmt : FloatFormat} (x y : Model fmt) : x.div y = Spec.div x y

Public division agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.sqrt_eq_spec {fmt : FloatFormat} (x : Model fmt) : x.sqrt = Spec.sqrt x

Public square root agrees with its descriptor-aware specification for every FloatFormat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Proof.fma_eq_spec {fmt : FloatFormat} (x y z : Model fmt) : x.fma y z = Spec.fma x y z

Public FMA agrees with its descriptor-aware specification for every FloatFormat.