Default static-byte capability construction

This is the final wiring layer for byte-sized binary families. It packages each family-selected kernel with the refinement theorem from Backend.Proof, then installs the result as an ordinary ExecFloat capability.

Construction is shared so the six operations do not each need a family-specific adapter. Every Family instance uses this construction and supplies its own certified kernel, which may use a table or compute the operation directly.

@[instance_reducible, instance 100]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.addCapability (F : Type u) [Family F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Add F

@[instance_reducible, instance 100]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.subCapability (F : Type u) [Family F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Sub F

@[instance_reducible, instance 100]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.mulCapability (F : Type u) [Family F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Mul F

@[instance_reducible, instance 100]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.divCapability (F : Type u) [Family F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Div F

@[instance_reducible, instance 100]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.sqrtCapability (F : Type u) [Family F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Sqrt F

@[instance_reducible, instance 100]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.fmaCapability (F : Type u) [Family F] [planning : ExecFloat.Backend.PolicyFor F] : ExecFloat.Fma F