Certificate for all six core arithmetic operations

The operation typeclasses already require every executable kernel to carry its refinement proof. FullArithmeticCertificate collects those six refinement statements, indexed by the shared operation enum.

Users can request this bundle when they want one machine-checked answer to “which core operations are certified for this format?” Formats supporting only a subset of operations continue to expose their individual ExecFloat.Proof.*_eq_spec theorems.

The certificate covers the universal execution boundary: each public operation equals the specification stored by its format capability. Standards conformance and denotational properties of that specification require separate format-family theorems.

def FloatLib.Floats.ExecFloat.Proof.OperationRefines (F : Type u) [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Add F] [Sub F] [Mul F] [Div F] [Sqrt F] [Fma F] : Backend.Operation → Prop

Pointwise specification-refinement proposition for one universal operation.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Proof.FullArithmeticCertificate (F : Type u) [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Add F] [Sub F] [Mul F] [Div F] [Sqrt F] [Fma F] : Prop

Kernel-checked refinement evidence for every universal arithmetic operation on one format.

Indexing by Backend.Operation avoids a second six-field record parallel to the executable capability hierarchy. This proposition certifies execution against the installed specifications; it does not replace format-specific theorems about what those specifications mean.

theorem FloatLib.Floats.ExecFloat.Proof.fullArithmeticCertificate (F : Type u) [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Add F] [Sub F] [Mul F] [Div F] [Sqrt F] [Fma F] : FullArithmeticCertificate F

Collect the refinement proofs supplied by the six operation capabilities.