Bounded fixed-point format inspection

Inspection for a bounded fixed-point code reports its radix, scale, signed coefficient range, and the three distinct overflow policies. It links refinement theorems for modular, checked, and saturating arithmetic.

No external wire standard is claimed for this mathematical family. The public entry point is FloatLib.Floats.Formats.FixedPoint.Bounded; this module contains only the optional meta-level inspection support.

def FloatLib.Floats.Formats.FixedPoint.Bounded.FloatInfo.Command.profile (base fractionalDigits width : ℕ) : ExecFloat.FormatProfile

Build the fixed-width description shared by raw codes and the configured ExecFloat wrapper. Carrier-specific reports replace the execution entries and may add wrapper theorems, but the represented range and overflow policies are defined here once.