Inspection for exact logarithmic codes

The exact logarithmic core represents zero or a signed integral power of a chosen radix. Multiplication is the only arithmetic operation supplied and is exact exponent addition. General addition and conversion into this value set require rounding. Nonzero division could subtract exponents exactly, but division and its zero-divisor policy are not implemented.

This optional meta module reports the real denotation and multiplication refinement through #float_info, together with the limits of the implemented operation set.

def FloatLib.Floats.Formats.Logarithmic.FloatInfo.Command.profile (base : ℕ) : ExecFloat.FormatProfile

Build the logarithmic description shared by the exact code and its configured ExecFloat wrapper. Both carriers use the same value set and exact multiplication law; only execution and wrapper-level theorem entries differ.