Proof-aware inspection of binary complex values

#float_info reports the component format, sign operations, arithmetic, squared magnitude, and scaled magnitude of ExecComplex fmt. The linked theorems describe intermediate rounding and list the required finiteness hypotheses.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.FloatInfo.BinarySummary : Type

Descriptor summary reused by the complex-format inspection report.

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.FloatInfo.profile (summary : BinarySummary) : ExecFloat.FormatProfile

Build the execution and proof profile for two-component binary complex values.